Java PathFinder を使った Thread の検証

Menu

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

ThreadTest on gitlab Server.stringWork() を実行する。

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

---

PathFinder による実行

以下の singularity sif を

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

と実行する

def file は

singluarity def for Java Path Finder

Java PathFinder

    https://github.com/javapathfinder/jpf-core

---

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 を修正せよ