HTTPS SSH

JArmus: a verification library for barrier deadlocks

JArmus is a library for deadlock detection and avoidance. It includes support for: Thread.join, CyclicBarrier, CountDownLatch, and Phaser.

Usage

JArmus expects a compiled Java program (a JAR or a directory with classes). JArmus instruments a given program (by introducing some checks) and then outputs a checked program. The usual workflow is therefore:

  1. compile
  2. instrument
  3. run

Example

JArmus comes with multiple examples to pick from, located in src/pos-samples/java/. Our running example is the file src/pos-samples/java/IterativeAveraging1D.java.

Compile. The input is file src/pos-samples/java/IterativeAveraging1D.java, the output is in directory tmp. The program is linked to jarmusc.jar. Additionally, you can run the program and note how it deadlocks.

mkdir tmp # temporary directory holding the compiled and unchecked program
javac -d tmp -cp target/jarmusc.jar src/pos-samples/java/IterativeAveraging1D.java

Instrument. The expected console output is verbose; warnings are OK. JArmus lists where verification checks are introduced in the program.

$ java -jar target/jarmusc.jar tmp out.jar
[warning] couldn't find aspectjrt.jar on classpath, checked: ...

Join point 'method-call(int java.util.concurrent.Phaser.arriveAndAwaitAdvance())' in Type 'IterativeAveraging1D$1' (IterativeAveraging1D.java:31) advised by around advice from 'pt.ul.jarmus.inst.PhaserObserver' (PhaserObserver.class:41(from PhaserObserver.aj)) [with runtime test]

Join point 'method-call(int java.util.concurrent.Phaser.arriveAndAwaitAdvance())' in Type 'IterativeAveraging1D$1' (IterativeAveraging1D.java:33) advised by around advice from 'pt.ul.jarmus.inst.PhaserObserver' (PhaserObserver.class:41(from PhaserObserver.aj)) [with runtime test]

Join point 'method-call(int java.util.concurrent.Phaser.arriveAndDeregister())' in Type 'IterativeAveraging1D$1' (IterativeAveraging1D.java:35) advised by before advice from 'pt.ul.jarmus.inst.PhaserObserver' (PhaserObserver.class:50(from PhaserObserver.aj)) [with runtime test]

Join point 'method-call(int java.util.concurrent.Phaser.arriveAndDeregister())' in Type 'IterativeAveraging1D$1' (IterativeAveraging1D.java:36) advised by before advice from 'pt.ul.jarmus.inst.PhaserObserver' (PhaserObserver.class:50(from PhaserObserver.aj)) [with runtime test]

Join point 'method-call(int java.util.concurrent.Phaser.arriveAndAwaitAdvance())' in Type 'IterativeAveraging1D' (IterativeAveraging1D.java:46) advised by around advice from 'pt.ul.jarmus.inst.PhaserObserver' (PhaserObserver.class:41(from PhaserObserver.aj)) [with runtime test]


1 warning

Run. The 5 tasks avoid the deadlock, print a message, and then terminate. The order in which the lines appear can differ.

$ java -cp target/jarmusc.jar:out.jar IterativeAveraging1D
DeadlockIdentifiedException T1
DeadlockIdentifiedException T3
DeadlockIdentifiedException T0
DeadlockIdentifiedException T4
DeadlockIdentifiedException T2

How do I enable deadlock detection?

JArmus runs in deadlock avoidance by default. To enabled deadlock detection, we need to provide some configuration options.

$ java -Darmus.detection.enabled=true -Darmus.avoidance.enabled=false -cp target/jarmusc.jar:out.jar IterativeAveraging1D
Nov 14, 2014 5:14:04 PM pt.ul.armus.DeadlockDetection$1 run
WARNING: deadlock found [...]
Nov 14, 2014 5:14:04 PM pt.ul.armus.deadlockresolver.FatalDeadlockResolver onDeadlockDetected
SEVERE: Deadlock detected: [...]

How do I configure the graph model selection used for cycle detection?

By default JArmus automatically chooses a graph model that better suits the application it is checking. We can enforce Armus to fix the graph model with a command line option. The available options are: auto (default), wfg, and sg.

$ java -Darmus.graph=wfg  -cp target/jarmusc.jar:out.jar IterativeAveraging1D 
DeadlockIdentifiedException T2
DeadlockIdentifiedException T4
DeadlockIdentifiedException T1
DeadlockIdentifiedException T3
DeadlockIdentifiedException T0

Are there more examples?

Examples of deadlocks can be found in directory src/pos-samples/java/.

Examples of deadlock-free programs can be found in src/neg-samples/java/.

Are there tests?

Yes. Running ant test will run more than 100 tests, including checking all the deadlocked programs in src/pos-samples/java/.

Run ant test -Doffline=true if you do not have an internet connection.