docs/intro/race_example.md

   1 # Example: Data Race #
   2
   3 That's nice, but of course we also could have provoked the error in our random value example by using explicit loops instead of the `Random.nextInt()` calls, i.e. by explicitly enumerating all possible `a` and `b` values in our program. This would be typically done in a program that is a dedicated test driver, in a process which is called *systematic testing*. However, the program we want to verify might not be a test driver, and we might not even have the sources so that we could modify it accordingly.
   4
   5 But the real show stopper for systematic testing lies within the instructions representing choices: at the application level, we might neither be aware of that there are choices, what the choice values are, nor be able to explicitly pick them.
   6
   7 To demonstrate this point, let us look at a little concurrency example using two threads of execution. Quite obviously, the program produces different results depending on if line (2) or (4) gets executed first. But assuming we can't control what happens in (1) and (2), this time we cannot explicitly enumerate the choices - they are made by the system scheduler, i.e. outside of our application.
   8
   9 ~~~~~~~~ {.java}
  10 public class Racer implements Runnable {
  11
  12      int d = 42;
  13
  14      public void run () {
  15           doSomething(1000);                   // (1)
  16           d = 0;                               // (2)
  17      }
  18
  19      public static void main (String[] args){
  20           Racer racer = new Racer();
  21           Thread t = new Thread(racer);
  22           t.start();
  23
  24           doSomething(1000);                   // (3)
  25           int c = 420 / racer.d;               // (4)
  26           System.out.println(c);
  27      }
  28
  29      static void doSomething (int n) {
  30           // not very interesting..
  31           try { Thread.sleep(n); } catch (InterruptedException ix) {}
  32      }
  33 }
  34 ~~~~~~~~
  35
  36 Chances are, we don't encounter this defect at all during normal testing:
  37
  38 ~~~~~~~~ {.bash}
  39 > java Racer
  40 10
  41 >
  42 ~~~~~~~~
  43
  44 Not so with JPF. Being a real virtual machine, there is nothing we can't control. And being a different kind of a Java virtual machine, JPF recognizes that 'racer' is an object that is shared between two threads, and hence executes all possible statement sequences / scheduling combinations in which this object can be accessed. This time, we give the complete output, which also shows the trace (the execution history) that lead to the defect found by JPF:
  45
  46 ~~~~~~~~ {.bash}
  47 > bin/jpf Racer
  48 JavaPathfinder v4.1 - (C) 1999-2007 RIACS/NASA Ames Research Center
  49 ====================================================== system under test
  50 application: /Users/pcmehlitz/tmp/Racer.java
  51
  52 ====================================================== search started: 5/24/07 12:32 AM
  53 10
  54 10
  55
  56 ====================================================== error #1
  57 gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty
  58 java.lang.ArithmeticException: division by zero
  59         at Racer.main(Racer.java:20)
  60
  61 ====================================================== trace #1
  62 ------------------------------------------------------ transition #0 thread: 0
  63 gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>main}
  64       [insn w/o sources](282)
  65   Racer.java:15                  : Racer racer = new Racer();
  66   Racer.java:1                   : public class Racer implements Runnable {
  67       [insn w/o sources](1)
  68   Racer.java:3                   : int d = 42;
  69   Racer.java:15                  : Racer racer = new Racer();
  70   Racer.java:16                  : Thread t = new Thread(racer);
  71       [insn w/o sources](51)
  72   Racer.java:16                  : Thread t = new Thread(racer);
  73   Racer.java:17                  : t.start();
  74 ------------------------------------------------------ transition #1 thread: 0
  75 gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>main,Thread-0}
  76   Racer.java:17                  : t.start();
  77   Racer.java:19                  : doSomething(1000);                   // (3)
  78   Racer.java:6                   : try { Thread.sleep(n); } catch (InterruptedException ix) {}
  79       [insn w/o sources](2)
  80   Racer.java:6                   : try { Thread.sleep(n); } catch (InterruptedException ix) {}
  81   Racer.java:7                   : }
  82   Racer.java:20                  : int c = 420 / racer.d;               // (4)
  83 ------------------------------------------------------ transition #2 thread: 1
  84 gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {main,>Thread-0}
  85   Racer.java:10                  : doSomething(1000);                   // (1)
  86   Racer.java:6                   : try { Thread.sleep(n); } catch (InterruptedException ix) {}
  87       [insn w/o sources](2)
  88   Racer.java:6                   : try { Thread.sleep(n); } catch (InterruptedException ix) {}
  89   Racer.java:7                   : }
  90   Racer.java:11                  : d = 0;                               // (2)
  91 ------------------------------------------------------ transition #3 thread: 1
  92 gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {main,>Thread-0}
  93   Racer.java:11                  : d = 0;                               // (2)
  94   Racer.java:12                  : }
  95 ------------------------------------------------------ transition #4 thread: 0
  96 gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>main}
  97   Racer.java:20                  : int c = 420 / racer.d;               // (4)
  98
  99 ====================================================== search finished: 5/24/07 12:32 AM
 100 >
 101 ~~~~~~~~
 102
 103 Looking at the output created by our test program, we see the result `"10"` printed twice, but that doesn't confuse us anymore. From our first example, we know this simply means that JPF first tried two scheduling sequences that normally terminated the program without provoking the defect, before finally picking the one that causes the error.
 104
 105 It still might be a bit confusing that the printed trace contains some source lines twice. Ignoring the details of its choice generation mechanism, this is caused by JPF executing bytecode instructions, not source lines, and a single source line can easily get translated into a number of bytecode instructions. This would go away if we configure JPF so that it reports the executed bytecode, but at the cost of much larger trace that is harder to read. What is more interesting is that JPF tells us about the thread choices it made in each transition (the lines starting with `gov.nasa.jpf.jvm.ThreadChoice..`).