Java PathFinder を使った Thread の検証

Menu Menu

複数のJava の Thread が共有している文字列 String を調べて、Thread の実行の様子を調べよう。

interlave Server.stringWork() を実行する。

何回か実行して見て、動作が異なるかどうかを調べよう。

PathFinder による実行

Java PathFinder<a > 

    http://javapathfinder.sourceforge.net/
をinstallして実行しよう。

Java 8 を使用する

残念ながら PathFinder は現在は Java 9 では動かない。以下の関数をzsh( ~/.zshrc )に組み込む。

    function java_home {
        export JAVA_HOME=`/usr/libexec/java_home $@`
        echo "JAVA_HOME:" $JAVA_HOME
        echo "java -version:"
        java -version
    }
これを有効にするには、

    . ~/.zshrc
とする。

zsh から、

    
    java_home -v  1.8
で、そのzshから java 8 が使えるようになります。

文字列の結合の結果がさまざまになるはずである。これは、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 がないとだめ。

gradle project なら、top level から

  jpf +classpath=build/classes/java/main threadTest.TestThread

実行結果の説明

実行例の一つをUMLのシーケン図に示せ。

Thread が三つの場合のinterleave の例題の synchronized を取って、生成される文字列をすべて示せ。

synchornization がない場合

ThreadTest の例題で、

work() メソッドが直列可能でない実行している場合の文字列を一つ示し、それが、どのような実行によって、生成されたかを UML のシーケンス図で記述せよ。

assert

ThreadTest の例題で、Server.work() メソッドが直列可能である条件を Java のassert を用いて記述し、Thread が三つの場合に、

    (1) synchronized を付けた場合に、assert が valid であること
    (2) synchronized がない場合に、assert の否定が satisfiable であること
を PathFinder によって確認した結果を示せ。

AtomicInteger を使って、ThreadTestの例題(atomicWork)が正しく動くことを jpf で確認せよ。</div>

Shinji KONO / Tue Jan 16 11:24:43 2018
Shinji KONO / Tue Jan 16 11:24:45 2018