Java PathFinder を使った Thread の検証
Menu複数のJava の Thread が共有している文字列 String を調べて、Thread の実行の様子を調べよう。
interleave の例題 interleave の例題 (tgz) これを展開して、
ant runで実行してみる。(Eclipse からでも良い)
何回か実行して見て、動作が異なるかどうかを調べよう。
PathFinder による実行
Java PathFinderhttp://javapathfinder.sourceforge.net/をinstallして実行しよう。
文字列の結合の結果がさまざまになるはずである。これは、Thread がinterleaving (混ぜこぜ)に実行されることを示している。PathFinder はすべての可能な結果を示している。
Thread を三つに増やした場合は、どんな文字列が生成されるか。実際に PathFinderを動作させて、生成された文字列と比較してみよ。
jpf のscript は、
JPF_HOME=/Users/kono/src/public/jpf-coreと言うように、絶対パスで JPF_HOME を指定する方が便利。
jpf +classpath=. threadTest.TestThreadというように実行します。threadTest/TestThread.java をcompileしたthreadTest/TestThread.class がないとだめ。
実行結果の説明
実行例の一つをUMLのシーケン図に示せ。Thread が三つの場合のinterleave の例題の synchronized を取って、生成される文字列をすべて示せ。
synchornization がない場合
ThreadTest ssh://ie.u-ryukyu.ac.jp//net/home/hg/teacher/kono/os/ex/ThreadTest の例題で、work() メソッドが直列可能でない実行している場合の文字列を一つ示し、それが、どのような実行によって、生成されたかを UML のシーケンス図で記述せよ。
assert
ThreadTest の例題で、この場合のwork() メソッドが直列可能である条件を Java のassert を用いて記述し、Thread が三つの場合に、
(1) synchronized を付けた場合に、assert が valid であること (2) synchronized がない場合に、assert の否定が satisfiable であることを PathFinder によって確認した結果を示せ。