名前しか知らなかった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の検査方式である全パターン検査は、モデル検証の世界では最初期の手法で、今やもっとよい方式も出ているらしい。ちょっと最近のモデル検査ツールを調べてみたい。
その他
サーバプログラム
実は、サーバプログラム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:まだ把握できていない
