Java Pathfinder - Example

Example

The following system under test contains a simple race condition between two threads accessing the same variable d in statements (1) and (2), which can lead to a division by zero exception if (1) is executed before (2)

public class Racer implements Runnable { int d = 42; public void run { doSomething(1001); d = 0; // (1) } public static void main (String args){ Racer racer = new Racer; Thread t = new Thread(racer); t.start; doSomething(1000); int c = 420 / racer.d; // (2) System.out.println(c); } static void doSomething (int n) { try { Thread.sleep(n); } catch (InterruptedException ix) {} } }

Without any additional configuration, JPF would find and report the division by zero. If JPF is configured to verify absence of race conditions (regardless of their potential downstream effects), it will produce the following output, explaining the error and showing a counter example leading to the error

JavaPathfinder v6.0 - (C) RIACS/NASA Ames Research Center ====================================================== system under test application: Racer.java ... ====================================================== error #1 gov.nasa.jpf.listener.PreciseRaceDetector race for field Racer@13d.d main at Racer.main(Racer.java:16) "int c = 420 / racer.d; " : getfield Thread-0 at Racer.run(Racer.java:7) "d = 0; " : putfield ====================================================== trace #1 ---- transition #0 thread: 0 ... ---- transition #3 thread: 1 gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet Racer.java:22 : try { Thread.sleep(n); } catch (InterruptedException ix) {} Racer.java:23 : } Racer.java:7 : d = 0; ... ---- transition #5 thread: 0 gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet Racer.java:16 : int c = 420 / racer.d;