Figure 1: State graph for test run
This is not intended to be a theoretical introduction into model checking, for which there is plenty of literature available. We try to demonstrate how JPF execution differs from using a normal JVM, and - in doing so - showing what a model checker can do to systematically explore all possible ways to execute your program (as opposed to testing, which only executes one path depending on your input data).
We start with a simple example that uses java.util.Random. Consider the following program that obtains two random values in (2) and (3), and then performs some computation (4) with them.
import java.util.Random;
public class Rand {
public static void main (String[] args) {
Random random = new Random(42); // (1)
int a = random.nextInt(2); // (2)
System.out.println("a=" + a);
//... lots of code here
int b = random.nextInt(3); // (3)
System.out.println(" b=" + b);
int c = a/(b+a -2); // (4)
System.out.println(" c=" + c);
}
}
Executing this program with a normal Java VM yields something like the following output. If we don't provide an explicit seed when creating the Random object in (1), the result is going to differ between runs, but every run will choose just a single 'a' and 'b' value (i.e. print just a single "a=.." and "b=.." line.
> java Rand
a=1
b=0
c=-1
>
Let's look at a graphical representation of all the ways our program could be executed, and how it actually was executed in our test run. The nodes of the graph represent "program states", and the edges "transitions" the execution could take from a certain state.
Figure 1: State graph for test run
Enter JPF - not much different results if we start JPF as a plain 'java' replacement. The only difference is that it (a) takes longer to complete, and (b) tells us something about a "search", which hints on that something more than in our test run is going on
> bin/jpf Rand
JavaPathfinder v4.1 - (C) 1999-2007 RIACS/NASA Ames Research Center
====================================================== system under test
application: /Users/pcmehlitz/tmp/Rand.java
====================================================== search started: 5/23/07 11:48 PM
a=1
b=0
c=-1
====================================================== results
no errors detected
====================================================== search finished: 5/23/07 11:48 PM
>
What is this "search" supposed to mean? Looking at source line (4) we realize that there is a potential problem: for certain 'a' and 'b' values, this expression can cause a "division by zero" ArithmeticException. Depending on the random seed used in (1), it's quite possible we would never encounter this case if we run (i.e. test) the program with a normal JVM.
Re-enter JPF - but this time we tell it to not only consider single values for 'a' and 'b', but look at all possible choices:
> bin/jpf +vm.enumerate_random=true Rand
JavaPathfinder v4.1 - (C) 1999-2007 RIACS/NASA Ames Research Center
====================================================== system under test
application: /Users/pcmehlitz/tmp/Rand.java
====================================================== search started: 5/23/07 11:49 PM
a=0
b=0
c=0
b=1
c=0
b=2
====================================================== error #1
gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty
java.lang.ArithmeticException: division by zero
at Rand.main(Rand.java:15)
....
>
What has happened? By specifying "+vm.enumerate_random=true" we told JPF to consider all possible values for expressions (2) and (3). JPF starts with "a=0", then picks "b=0", which yields a valid "c=0" value. But instead of terminating like a normal VM, JPF recognized that there are more choices left, so it "backtracks" to (3) and picks "b=1". Again, no problem here with computing "c=0". Back to (3), JPF now tries "b=2", which of course spells disaster for our little program when executing (4), as can be seen by the following error report.
Here is a graphical representation of this search process. It should be noted that JPF per default only runs up to the point where it finds an error or there are no more choices left to explore. But if we would somehow "fix" the "a=0,b=2" case, JPF would still find the "a=1,b=1" case in the next run, since it systematically tries all choices. No matter what error it finds, JPF also keeps the complete "trace" (execution path) how it got to this error (denoted by the red arrows), which means we don't have to debug the program to find out.
Figure 2: State graph search for model checking run
That's nice, but of course we also could have provoked this error by using explicit loops instead of (2) and (3), 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.
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.
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.
public class Racer implements Runnable {
int d = 42;
public void run () {
doSomething(1000); // (1)
d = 0; // (2)
}
public static void main (String[] args){
Racer racer = new Racer();
Thread t = new Thread(racer);
t.start();
doSomething(1000); // (3)
int c = 420 / racer.d; // (4)
System.out.println(c);
}
static void doSomething (int n) {
// not very interesting..
try { Thread.sleep(n); } catch (InterruptedException ix) {}
}
}
Chances are, we don't encounter this defect at all during normal testing:
> java Racer 10 >
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:
> bin/jpf Racer
JavaPathfinder v4.1 - (C) 1999-2007 RIACS/NASA Ames Research Center
====================================================== system under test
application: /Users/pcmehlitz/tmp/Racer.java
====================================================== search started: 5/24/07 12:32 AM
10
10
====================================================== error #1
gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty
java.lang.ArithmeticException: division by zero
at Racer.main(Racer.java:20)
====================================================== trace #1
------------------------------------------------------ transition #0 thread: 0
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>main}
[282 insn w/o sources]
Racer.java:15 : Racer racer = new Racer();
Racer.java:1 : public class Racer implements Runnable {
[1 insn w/o sources]
Racer.java:3 : int d = 42;
Racer.java:15 : Racer racer = new Racer();
Racer.java:16 : Thread t = new Thread(racer);
[51 insn w/o sources]
Racer.java:16 : Thread t = new Thread(racer);
Racer.java:17 : t.start();
------------------------------------------------------ transition #1 thread: 0
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>main,Thread-0}
Racer.java:17 : t.start();
Racer.java:19 : doSomething(1000); // (3)
Racer.java:6 : try { Thread.sleep(n); } catch (InterruptedException ix) {}
[2 insn w/o sources]
Racer.java:6 : try { Thread.sleep(n); } catch (InterruptedException ix) {}
Racer.java:7 : }
Racer.java:20 : int c = 420 / racer.d; // (4)
------------------------------------------------------ transition #2 thread: 1
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {main,>Thread-0}
Racer.java:10 : doSomething(1000); // (1)
Racer.java:6 : try { Thread.sleep(n); } catch (InterruptedException ix) {}
[2 insn w/o sources]
Racer.java:6 : try { Thread.sleep(n); } catch (InterruptedException ix) {}
Racer.java:7 : }
Racer.java:11 : d = 0; // (2)
------------------------------------------------------ transition #3 thread: 1
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {main,>Thread-0}
Racer.java:11 : d = 0; // (2)
Racer.java:12 : }
------------------------------------------------------ transition #4 thread: 0
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>main}
Racer.java:20 : int c = 420 / racer.d; // (4)
====================================================== search finished: 5/24/07 12:32 AM
>
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.
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..").
What really sets JPF apart from other model checkers is that it is not constrained to a fixed set of possible choice types. JPF is extensible in terms of what operations might represent choice points. This makes it possible to exploit the same verification capabilities for graphical programs (where user inputs are the simulated choices), web applications (URI's as choices), UML state charts (events as choices) and many more program types. In fact, the JPF user is not only in control of what kind of choices to consider, but can also configure JPF to use heuristics that define the choice values. Please read the page about configurable ChoiceGenerators for a more detailed discussion of the underlying mechanism.