Java Pathfinder
Encyclopedia
Java Pathfinder is a system to verify executable Java bytecode
programs. JPF was developed at the NASA
Ames Research Center and open sourced in 2005. The acronym JPF is not to be confused with the unrelated Java Plugin Framework project.
The core of JPF is a Java Virtual Machine
that is also implemented in Java. JPF executes normal Java bytecode
programs and can store, match and restore program states. Its primary application has been Model checking
of concurrent programs
, to find defects such as data races
and deadlocks
. With its respective extensions, JPF can also be used for a variety of other purposes, including
JPF has no fixed notion of state space branches and can handle both data and scheduling choices.
accessing the same variable
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
error #1
trace #1
------------------------------------------------------ transition #0 thread: 0
...
------------------------------------------------------ transition #3 thread: 1
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet[id="sleep",isCascaded:false,{main,>Thread-0}]
[3 insn w/o sources]
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[id="sharedField",isCascaded:false,{>main,Thread-0}]
Racer.java:16 : int c = 420 / racer.d;
JPF includes a runtime module system to package such constructs into separate JPF extension projects. A number of such projects are available from the main JPF server, including a symbolic execution mode, numeric analysis, race condition detection for relaxed memory models, user interface model checking and many more.
Java bytecode
Java bytecode is the form of instructions that the Java virtual machine executes. Each bytecode opcode is one byte in length, although some require parameters, resulting in some multi-byte instructions. Not all of the possible 256 opcodes are used. 51 are reserved for future use...
programs. JPF was developed at the NASA
NASA
The National Aeronautics and Space Administration is the agency of the United States government that is responsible for the nation's civilian space program and for aeronautics and aerospace research...
Ames Research Center and open sourced in 2005. The acronym JPF is not to be confused with the unrelated Java Plugin Framework project.
The core of JPF is a Java Virtual Machine
Java Virtual Machine
A Java virtual machine is a virtual machine capable of executing Java bytecode. It is the code execution component of the Java software platform. Sun Microsystems stated that there are over 4.5 billion JVM-enabled devices.-Overview:...
that is also implemented in Java. JPF executes normal Java bytecode
Java bytecode
Java bytecode is the form of instructions that the Java virtual machine executes. Each bytecode opcode is one byte in length, although some require parameters, resulting in some multi-byte instructions. Not all of the possible 256 opcodes are used. 51 are reserved for future use...
programs and can store, match and restore program states. Its primary application has been Model checking
Model checking
In computer science, model checking refers to the following problem:Given a model of a system, test automatically whether this model meets a given specification....
of concurrent programs
Concurrent computing
Concurrent computing is a form of computing in which programs are designed as collections of interacting computational processes that may be executed in parallel...
, to find defects such as data races
Race condition
A race condition or race hazard is a flaw in an electronic system or process whereby the output or result of the process is unexpectedly and critically dependent on the sequence or timing of other events...
and deadlocks
Deadlock
A deadlock is a situation where in two or more competing actions are each waiting for the other to finish, and thus neither ever does. It is often seen in a paradox like the "chicken or the egg"...
. With its respective extensions, JPF can also be used for a variety of other purposes, including
- model checking of distributed applications
- model checking of user interfaces
- test case generation by means of symbolic execution
- low level program inspection
- program instrumentation and runtime monitoring
JPF has no fixed notion of state space branches and can handle both data and scheduling choices.
Example
The following system under test contains a simple race condition between two threadsThread (computer science)
In computer science, a thread of execution is the smallest unit of processing that can be scheduled by an operating system. The implementation of threads and processes differs from one operating system to another, but in most cases, a thread is contained inside a process...
accessing the same variable
d in statements (1) and (2), which can lead to a division by zero exceptionException handling
Exception handling is a programming language construct or computer hardware mechanism designed to handle the occurrence of exceptions, special conditions that change the normal flow of program execution....
if (1) is executed before (2)
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
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[id="sleep",isCascaded:false,{main,>Thread-0}]
[3 insn w/o sources]
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[id="sharedField",isCascaded:false,{>main,Thread-0}]
Racer.java:16 : int c = 420 / racer.d;
Extensibility
JPF is an open system that can be extended in a variety of ways. The main extension constructs are- listeners - to implement complex properties (e.g. temporal properties)
- peer classes - to execute code at the host JVM level (instead of JPF), which is mostly used to implement native methods
- bytecode factories - to provide alternative execution semantics of bytecode instructions (e.g. to implement symbolic execution)
- choice generators - to implement state space branches such as scheduling choices or data value sets
- serializers - to implement program state abstractions
- publishers - to produce different output formats
- search policies - to use different program state space traversal algorithms
JPF includes a runtime module system to package such constructs into separate JPF extension projects. A number of such projects are available from the main JPF server, including a symbolic execution mode, numeric analysis, race condition detection for relaxed memory models, user interface model checking and many more.
Limitations
- JPF cannot analyze Java native methodsJava Native InterfaceThe Java Native Interface is a programming framework that enables Java code running in a Java Virtual Machine to call and to be called by native applications and libraries written in other languages such as C, C++ and assembly.-Purpose and features:JNI enables one to write native methods to...
. If the system under test calls such methods, these have to be provided within peer classes, or intercepted by listeners - as a model checker, JPF is susceptible to Combinatorial explosionCombinatorial explosionIn administration and computing, a combinatorial explosion is the rapidly accelerating increase in lines of communication as organizations are added in a process...
, although it performs on-the-fly Partial order reductionPartial order reductionIn computer science, partial order reduction is a technique for reducing the size of the state-space to be searched by a model checking algorithm... - the configuration system for JPF modules and runtime options can be complex
See also
- Bogor - software model checking framework of Kansas State University
- MoonWalker - similar to Java PathFinder, but for .NET programs instead of Java programs
External links
- Official site
- New NASA Software Detects 'Bugs' in Java Computer Code
- NASA Develops New Software to Detect "Bugs" in Java Computer Code
- Willem Visser, Corina S. Păsăreanu, Sarfraz Khurshid. Test Input Generation with Java PathFinder. In: George S. Avrunin, Gregg Rothermel (Eds.): Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis 2004. ACM Press, 2004. ISBN 1-58113-820-2.