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

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

<a href="https://gitlab.ie.u-ryukyu.ac.jp/os/ThreadTest.git">ThreadTest on gitlab </a>

Server.stringWork() を実行する。

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


--PathFinder による実行

以下の singularity sif を

 singularity shell --shell=/bin/zsh  /mnt/ie-virsh/singularity/pathfinder/pathfinder.sif 

と実行する

def file は

<a href="https://gitlab.ie.u-ryukyu.ac.jp/ie-syskan/singularity/-/tree/main/pathfinder?ref_type=heads">
singluarity def for Java Path Finder
</a>


Java PathFinder
<a href="https://github.com/javapathfinder/jpf-core">
    https://github.com/javapathfinder/jpf-core
</a>

--Java 11 を使用する

Ubuntu ならば

    apt install openjdk-11-jre-headless
    update-java-alternatives --set java-1.11.0-openjdk-amd64

--実行してみる

   % java -cp build/classes/java/main threadTest.TestThread

--JavaPathFinder で bug を見つける

  % /opt/jpf-core/bin/jpf +classpath=build/classes/java/main threadTest.TestThread

実行で、どこで、bug  を見つけているかを示せ

--bug の修正

このbugが起きないようにthreadTest.TestThreadを修正せよ

--DeadLock

走らせてみる

   java -cp build/classes/java/main deadLockTest.TestDeadLock

Dead lock がたまに起きることを確認する

JavaPathFinder で dead lock を見つけた場所を指摘する

   /opt/jpf-core/bin/jpf +classpath=build/classes/java/main deadLockTest.TestDeadLock

--bug の修正

このbugが起きないように deadLockTest.TestDeadLock を修正せよ