2011-06-10
障害に関すること
検証 |
いろいろあって、障害というものについてちょっとだけ書いてみる。
万が一のときに壊滅的致命的破滅的災害にいたる技術を、人間は使っていいものか。
いい方悪いが飛行機事故で最悪1000人規模。スタジアムに落ちれば桁がかわってくるか。では原発事故では？被害の規模を死傷者数だけで比較していいものか*1？
それはともかく、
万が一の事故で起こる災害が桁違いで、しかも一度発生したらそれを止める手立てが(今の人類には)ないという意味で、使ってはいけない技術なのではないかという論理。
反論
反論として海底油田掘削がある。例えば昨年メキシコ湾で起きた油田事故は、最悪の場合大西洋が死の海になるところだった(のかもしれない)。
だからといって、油田掘削を否定する人は少ないはず。私も否定しない。やるようがあると思ってしまう。
純粋に技術論だけで原発推進を唱える人たちも、私の海底油田へと感覚と同じで、人類は原子炉を完全に制御できるとの観点からロジックを組み立てるので、どこまでいっても平行線だ。
特に、「未来のどこかの時点で完全制御可能だろう」と言われると、それを否定するには悪魔の証明をしなければならなくなってしまう。
疑問
本当のところ、対応しきれない技術をかかえること、それへの障害対応ってのはいったい何の事なのだろう、という深い深い疑問が生まれてしまった。
2011-03-14
イタリアのPostgreSQL Users Groupからのメッセージ
イタリアのPostgreSQL Users Groupからのメッセージ。
JPUGのあるメンバー向けメッセージですが、複数のMLにすでに流れているので、勝手に転載。
I want to express our deepest sympathy for the recents events in Japan. We hope that your families and loved ones are all safe. We are sure your people will recover from this natural disaster in the way the Japanese people have always done in the past. Please send our best wishes to all the members of the Postgres community in Japan. Regards, Gabriele Bartolini President Italian PostgreSQL Users Group
2011-03-07
JavaPathFinderの備忘録
検証 |
名前しか知らなかったjavaPathFinderを数時間いじってみた。
ダウンロード、セットアップ
JavaPathFinderから最新版をダウンロード。解凍すれば問題なく動作する。
できること
Javaのバイトコードを読み込んで、デッドロックや競合状態の有無などを検査する。
このPDFがわかりやすい。
最初期はJavaのソースコードをSPINのコードに変換するものだった。すぐにバイトコードを読み込み独自の検査ツールで検証をおこなうようになったが、マルチスレッドによる並行処理の問題点を検出するのが、おそらく最も適した使い方。
サンプル
複数スレッドで競合状態を起こしてみる。
public class test implements Runnable{ static int shared_data = 0; public static void main(String args[]){ int size = Integer.parseInt(args[0]); test mt = new test(); Thread[] th = new Thread[size]; for (int i = 0; i < size; i++) { th[i] = new Thread(mt); th[i].start(); } } void add_one() { int tmp = shared_data; shared_data += 1; assert(tmp + 1 == shared_data); } public void run() { add_one(); } }
これをコンパイルしてjpfで実行する。
$javac test.java $ time ../bin/jpf +classpath=. test 2 ... 略 ... ====================================================== error #1 gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty java.lang.AssertionError at test.add_one(test.java:20) at test.run(test.java:24) ====================================================== snapshot #1 thread index=2,name=Thread-1,status=RUNNING,this=java.lang.Thread@216,target=test@289,priority=5,lockCount=0,suspendCount=0 call stack: at test.add_one(test.java:20) at test.run(test.java:24) ====================================================== results error #1: gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty "java.lang.AssertionError at test.add_one(test..." ====================================================== statistics elapsed time: 0:00:01 states: new=18, visited=3, backtracked=8, end=4 search: maxDepth=13, constraints=0 choice generators: thread=17, data=0 heap: gc=22, new=309, free=66 instructions: 3367 max memory: 6MB loaded code: classes=76, methods=1063 ====================================================== search finished: 11/03/06 13:01 real 0m1.475s user 0m1.197s sys 0m0.052s
ということで、２つのスレッドが同時に関数add_one()を呼び出すと、変数shared_dataも書き換えてしまうので、shared_dataの値がassert()内で期待する値にならないことを検出した。
プログラムを修正し、関数add_one()にsynchronized宣言をつける。これで関数add_one()は同時に実行されることがなくなるので、assert文も成立するはずである。
... 略 ... synchronized void add_one() { int tmp = shared_data; shared_data += 1; assert(tmp + 1 == shared_data); } ... 略 ...
これをコンパイルしてjpfで実行する。
$javac test.java $ time ../bin/jpf +classpath=. test 2 JavaPathfinder v5.x - (C) RIACS/NASA Ames Research Center ====================================================== system under test application: test.java arguments: 2 ====================================================== search started: 11/03/06 13:06 ====================================================== results no errors detected ====================================================== statistics elapsed time: 0:00:01 states: new=73, visited=55, backtracked=127, end=15 search: maxDepth=15, constraints=0 choice generators: thread=73, data=0 heap: gc=122, new=336, free=479 instructions: 4878 max memory: 6MB loaded code: classes=73, methods=1033 ====================================================== search finished: 11/03/06 13:06 real 0m1.761s user 0m1.248s sys 0m0.071s
確かに競合状態がなくなった。
実行時間
JavaPathFinderは実行可能なすべてのパスを試すので、実行に非常に時間がかかる。
例えば、上の例ではスレッドが２つだったが、３つ、４つ、、、と増えるにしたがって実行可能なパスも組み合わせの数のように増えていく。
$ time ../bin/jpf +classpath=. test 3 real 0m2.037s user 0m1.366s sys 0m0.050s $ time ../bin/jpf +classpath=. test 4 real 0m4.534s user 0m2.456s sys 0m0.053s $ time ../bin/jpf +classpath=. test 5 real 0m6.658s user 0m5.331s sys 0m0.078s $ time ../bin/jpf +classpath=. test 6 real 0m21.848s user 0m16.953s sys 0m0.117s $ time ../bin/jpf +classpath=. test 7 real 1m21.716s user 1m8.190s sys 0m0.263s
大規模なシステムへの適用は難しいだろうが*1、適度な規模のシステムならば非常に役にたつと思う。
JavaPathFinderの検査方式である全パターン検査は、モデル検証の世界では最初期の手法で、今やもっとよい方式も出ているらしい。ちょっと最近のモデル検査ツールを調べてみたい。
その他
設定ファイルなど
JavaPathFinderの検証は"*.jpf"ファイルなどで制御できる。ファイルの書き方はここにある*2。
サーバプログラム
実は、サーバプログラムjgtmをチェックしたかったのだが、jpfに載せると、クライアントからの入力待ちになってエラーを検出し終了してしまう。念のためクライアントを接続しようとしても接続拒否になる。
$ time ../bin/jpf +classpath=./jgtm-0.3.3.jar jgtm -p 6666 -D . -x 100 ... 略 ... ====================================================== error #1 gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty java.lang.UnsatisfiedLinkError: java.net.PlainSocketImpl.initProto()V (no peer) at java.net.PlainSocketImpl.<clinit>(PlainSocketImpl.java:84) at java.net.ServerSocket.setImpl(ServerSocket.java:236) at java.net.ServerSocket.<init>(ServerSocket.java:178) at java.net.ServerSocket.<init>(ServerSocket.java:97) at jgtm.main(jgtm.java:141) ====================================================== snapshot #1 thread index=0,name=main,status=RUNNING,this=java.lang.Thread@0,target=null,priority=5,lockCount=0,suspendCount=0 owned locks:java.lang.Class@20946 call stack: at java.net.PlainSocketImpl.<clinit>(PlainSocketImpl.java:84) at java.net.ServerSocket.setImpl(ServerSocket.java:236) at java.net.ServerSocket.<init>(ServerSocket.java:178) at java.net.ServerSocket.<init>(ServerSocket.java:97) at jgtm.main(jgtm.java:141) ====================================================== results error #1: gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty "java.lang.UnsatisfiedLinkError: java.net.PlainSock..." ====================================================== statistics elapsed time: 0:00:18 states: new=0, visited=1, backtracked=0, end=0 search: maxDepth=0, constraints=0 choice generators: thread=1, data=0 heap: gc=40, new=20976, free=26 instructions: 223359 max memory: 17MB loaded code: classes=113, methods=1729 ====================================================== search finished: 11/03/06 14:50
原理からすると、通信するプログラムのチェックには使えないのが当たり前だ。
WEBをさまよってみたら、これを見つけた。
現実的なシステムのプログラムは、通常GUIや通信機能のための 標準ライブラリを使用しているが、この場合、そのままではJavaPathFinder を 使用して検証することができないため、... 略 .... 実際のシステム開発に適用するのが難しい。 現実的なシステムのプログラムの検証に必要な、複数プロセスの プログラムを1 プロセスのものに変換するノウハウ、また抽象化により ライブラリを使用しないプログラムに変換するノウハウを.... 略 ....
うまく使えるように変換しろということか。
*1：富士通のプレスリリースによれば、数々の工夫をこらして並列処理で数万ステップだそうである。
*2：まだ把握できていない
2011-03-01
PostgreSQL + QueryCache
2005年ころ、PostgreSQL+QueryCacheという実験をやっていたことをふと思い出す。
CBMCの使い方入門:3
検証 |
実際に使われている800行規模のCプログラムに対してCBMCを使ってみる。
ここでは拙作mcbというmemcachedのベンチマークプログラムを俎上にのせる。
このプログラムのバージョン1.0rc2はここで指摘されているように、初歩的なミスを含んでいる稚拙なものであった*1。
CBMC対応したmcb.c
現時点での最新バージョンは1.0rc5で、CBMCで検査しやすいように構造化を進め多くの事前条件を組み込んでいる。
また、CBMCとは直接関係ないassertも多数組込み、入力値の厳密な検査も行うようにした。
検査
ここでは、バグ報告があった部分に対応する1.0rc5の関数:send_cmd()について述べる。
以下は1.0rc5のsend_cmd()である。
最初に中身を把握するために必要最小限のコードだけ示す。次にCBMCに関連するところだけ抜粋し、CBMCを使うに当たっての注意点など記する。
では、最初は事前条件も事後条件もないバージョン。
static void send_cmd(const int fd, const int id, char *data, char *buff) { int key, msg_len, str_len; int _rand = rand(); double r; r = (double) (_rand / (RAND_MAX + 1.0)); key = 1 + (int) ((double) (sysval.max_key * r)); str_len = 1 + (int) ((double) ((sysval.data_len * 2) * r)); data[str_len] = '\0'; msg_len = build_mc_cmd(buff, buff_size, sysval.command, key, data, /*strlen(data) = */ str_len, id); /* marking */ data[str_len] = 'X'; do_cmd(fd, buff, msg_len, id); }
次に、CBMCで検査するために事前条件(+ダミーの変数)、事後条件を入れたバージョンを示す。
static void send_cmd(const int fd, const int id, char *data, char *buff) { int key, msg_len, str_len; int _rand = rand(); double r; /* * rについて検査する。 */ #ifdef __CBMC__ __CPROVER_assume(0 <= _rand && _rand <= RAND_MAX); /* assumption no.1 */ #endif r = (double) (_rand / (RAND_MAX + 1.0)); assert(0.0 <= r && r < 1.0); /* assertion no.1 */ /* * 次にkeyの設定値について検査する。 * あとでまとめて上部で定義すればよい。 */ #ifdef __CBMC__ /* * MAX_KEYはデフォルト値は65535と巨大なので、検査に莫大な時間がかかる。 * 検査に影響がない範囲で小さな値にする。 */ #undef MAX_KEY #define MAX_KEY 100 /* ダミーの値を設定 */ sysval.max_key = 10; // dummy : 構造体sysval_t sysvalを定義してもよいが、検索範囲を狭めるには必要な変数のみダミー値を設定するほうがよい。 /* sysval.max_keyの範囲を事前条件として記述する */ __CPROVER_assume(0 < sysval.max_key && sysval.max_key <= MAX_KEY); /* assumption no.2 */ #endif key = 1 + (int) ((double) (sysval.max_key * r)); assert(0 < key && key <= sysval.max_key); /* assertion no.2 */ /* * 次にstr_lenの検査 * こちらもあとで上にまとめればよい。 */ #ifdef __CBMC__ /* 上と同様、事前条件+(ダミーの)変数設定を記述する */ sysval.data_len = 10; // dummy __CPROVER_assume(0 < sysval.data_len && sysval.data_len <= MAX_DATA_LEN); /* assumption no.3 */ data_size = DATA_SIZE; #endif str_len = 1 + (int) ((double) ((sysval.data_len * 2) * r)); assert(0 < str_len && str_len < data_size); /* assertion no.3 */ /* 今回のメインパート。 * 旧バージョンではメモリアクセスに問題が発生した箇所。 */ #ifdef __CBMC__ char *data = (char *) malloc((DATA_SIZE)); #endif /* * --pointer-check,--bounds-checkで不正なアクセスの有無を検査 */ data[str_len] = '\0'; /* build_mc_cmd()内で検査する */ msg_len = build_mc_cmd(buff, buff_size, sysval.command, key, data, /*strlen(data) = */ str_len, id); #ifndef __CBMC__ assert(msg_len <= buff_size); #endif /* marking */ data[str_len] = 'X'; /* do_cmd()内で検査する */ do_cmd(fd, buff, msg_len, id); }
関数内のコメントで書いたように、内部を小分けにして事前条件+(ダミーの)変数設定をマメに入れるのがうまく検査するコツのようである。すべてうまくいったらまとめればよい。
実際にCBMCで検査する。
./cbmc mcb.c -D __CBMC__ --bounds-check --pointer-check --function send_cmd --unwind 10 ... 略 .... 114934 variables, 248853 clauses SAT checker: negated claim is UNSATISFIABLE, i.e., holds Runtime decision procedure: 3.227s VERIFICATION SUCCESSFUL
CBMCを信じれば「mcb.cの1.0rc5にはメモリ関連のバグはない(ｷﾘｯ」。
CBMCの結果が正しいか疑ってみる
念のため、条件を変えて問題を検出するかどうか調べてみる*2。
最初にassertion no.2の範囲を変えて、間違った範囲を指定する。
/* * わざとエラーを出す */ static void send_cmd(const int fd, const int id, char *data, char *buff) { 略 ... key = 1 + (int) ((double) (sysval.max_key * r)); assert(1 < key && key <= sysval.max_key); /* assertion no.2' */ ... 略 ... }
これでCBMCを実行すると、範囲がおかしい旨報告される。
./cbmc mcb.c -D __CBMC__ --bounds-check --pointer-check --function send_cmd --unwind 10 ... 略 ... Violated property: file mcb.c line 494 function send_cmd assertion 1 < key && key <= sysval.max_key FALSE VERIFICATION FAILED
また、今回のメインである配列data[]の不正アクセスの可能性について、本当に検査できているのか確認してみる。
ここでは、わざと配列data[]の大きさを1byteだけ小さくし、それによって不正アクセスをCBMCが検出するかどうかをみてみる。
static void send_cmd(const int fd, const int id, char *data, char *buff) { ... 略 ... #ifdef __CBMC__ char *data = (char *) malloc((DATA_SIZE) - 1); /* わざと1byte小さく確保 */ #endif data[str_len] = '\0'; ... 略 ... }
これでCBMCを実行すると、きちんと不正アクセスの可能性有りと報告してくれる。
./cbmc mcb.c -D __CBMC__ --bounds-check --pointer-check --function send_cmd --unwind 10 ... 略 ... Violated property: file mcb.c line 513 function send_cmd dereference failure: dynamic object upper bound !((unsigned int)(POINTER_OFFSET(data)) + (unsigned int)str_len >= __CPROVER_alloc_size[POINTER_OBJECT(data)]) || !(IS_DYNAMIC_OBJECT(data)) VERIFICATION FAILED
これなら、CBMCの結果を信じてもよさそうだ。
その他の関数の検査
実際のところ、mcb.cについてCBMCで検査できる関数はsend_cmd()、master_thread()、connector_thread()など数個に留まった。これはCBMCの問題ではもちろんなく、mcb.cが簡単な処理しか行っていないため、そもそも検査項目が限られているためである。
しかし、検査をするための準備過程でtypoの修正やassertの挿入、入力範囲の厳密チェックなど、間接的にソースの品質向上に役立ったことも多いので、単に利用率だけをみてツールの有効性云々をいうことは出来ないと感じた。
その他
mcbの検証
念のため、Intel Inspectorでもチェックを行い、こちらもパスした。valgrindで動的検査も行い、こちらもパスした。
Inspectorほど簡単ではないが、CBMCでもInspector並の検証ができることを確認できた。
なお、入力値の検査はできていない。これは入力テストを網羅的に行うツールが別途必要。
並行処理
今回はマルチスレッドとはいえ、各スレッドは独立して動作するので(共有資源がない)うまくいった。
CBMCは並行処理には対応していないので、並行処理を行うプログラムの検証には注意が必要。
応用
CBMCが(boundは規定したうえで)すべての実行可能なパスを検査することを利用して、ある箇所への到達可能性を検査したり、絶対に通過してはいけない場所にあえてassert(false)文を挿入して危険性を検出するなど、様々な使い方があるようだ。
また、"Automatic Test Generation for Coverage Analysis Using CBMC"という論文では、CBMCを使ってテストパターンを生成するなんてこともされている模様*3。