-title: Java PathFinder を使った Thread の検証

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

<a href="ssh://yomitan.ie.u-ryukyu.ac.jp//net/home/hg/teacher/kono/os/ex/ThreadTest">interlave </a>

Server.stringWork() を実行する。

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


--PathFinder による実行

Java PathFinder は Docker を使う方が良い。

<a href="https://ie.u-ryukyu.ac.jp/hg/cr/Docker/JavaPathFinder">
Docker/JavaPathFinder/
</a>


Java PathFinder
<a href="http://javapathfinder.sourceforge.net/">
    http://javapathfinder.sourceforge.net/
</a>
を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 が使えるようになります。

--comment-begin:
(naha:/net/open を共有して、
    /Volume/naha.ie.u-ryukyu.ac.jp/JAVA/jpf/bin/jpf
で実行しても良い。)
--comment-end:

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


<a href="ssh://ie.u-ryukyu.ac.jp//net/home/hg/teacher/kono/os/ex/ThreadTest">ThreadTest </a>

の例題で、

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

--assert

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

    (1) synchronized を付けた場合に、assert が valid であること
    (2) synchronized がない場合に、assert の否定が satisfiable であること

を PathFinder によって確認した結果を示せ。

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

---example

    +leo+kono ~/src/public/jpf-core/bin/jpf +classpath=. threadTest.TestThread

    JavaPathfinder core system v8.0 (rev 32) - (C) 2005-2014 United States Government. All rights reserved.


    ====================================================== system under test
    threadTest.TestThread.main()

    ====================================================== search started: 1/8/19 1:38 PM

    ====================================================== results
    no errors detected

    ====================================================== statistics
    elapsed time:       00:00:00
    states:             new=773,visited=1301,backtracked=2074,end=4
    search:             maxDepth=20,constraints=0
    choice generators:  thread=773 (signal=0,lock=156,sharedRef=335,threadApi=25,reschedule=257), data=0
    heap:               new=395,released=107,maxLive=384,gcCycles=1517
    instructions:       12688
    max memory:         245MB
    loaded code:        classes=65,methods=1514

    ====================================================== search finished: 1/8/19 1:38 PM
    +leo+kono cat ~/src/public/jpf-core/bin/jpf                                   

    #!/bin/bash
    #
    # unix shell script to run jpf
    #

    # JPF_HOME=`dirname "$0"`/..
    JPF_HOME=$HOME/src/public/jpf-core

    if test -z "$JVM_FLAGS"; then
      JVM_FLAGS="-Xmx2048m -ea"
    fi

    /usr/libexec/java_home -v 1.8.0_152 --exec java -jar "$JPF_HOME/build/RunJPF.jar" "$@"

    #java $JVM_FLAGS -jar "$JPF_HOME/build/RunJPF.jar" "$@"