抽象化されたTransactionを実装する
トランザクションの振る舞いをより抽象化したコードを独自に用意してanomalyやdeadlockを再現することにする。
https://github.com/ie-Yoshisaur/transaction-emulator-java
↑書いた。
gradle buildすれば、
java -cp "build/classes/java/main:build/classes/java/test" DirtyReadAnomalyTest
/opt/jpf-core/bin/jpf +classpath=build/classes/java/main DirtyReadAnomalyTest
みたいに使える
Anomalyのテストも実装した、アノマリーに遭遇するとエラー出力するようなコードにしているが、アノマリーに遭遇する可能性があるのにも関わらず普通のテストではパスしてしまう。
それをモデル検査で検出する。
jpf.shというモデル検査をする際に使用するメモリを指定するshellを書く。
デフォルトだと1024MBしかなくてだめ。
code: jpf.sh
#!/bin/bash
#
# unix shell script to run jpf
#
if test -z "$JVM_FLAGS"; then
JVM_FLAGS="-Xmx10g -ea"
fi
java $JVM_FLAGS -jar "/opt/jpf-core/build/RunJPF.jar" "$@"
anomalyをモデル検査で検知できた。