Java Pathfinder

Java Pathfinder
Developer(s) NASA
Stable release 6.0 / November 30, 2010 (2010-11-30)
Written in Java
Operating system Cross-platform
Size 1.6 MB (archived)
Type Software verification tool, Virtual machine
License Apache License Version 2
Website http://babelfish.arc.nasa.gov/trac/jpf

Java Pathfinder (JPF) 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.

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[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

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

See also

External links

This article is issued from Wikipedia - version of the Saturday, February 06, 2016. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.