JPF-Partial State Matching: Java PathFinder making State matching more efficient

The goal of the extension is (1) to automaticaly identify irrelevant parts of the program state and (2) not to consider those parts during state matching.

A value (part of the program state) is irrelevant iff for any continuation of the program the value is not read by the program at all or it is not read before it is overwritten.

Benefits:

  • Fewer program states
  • Smaller program states (faster state matching)

Methods:

  • Hybrid analysis - Based on Interprocedural Future-Field-Read static analysis and current call stacks it identifies fields which will not be read by the program before it terminates. The analysis is cheap, compatible with both standard JPF state serializers (Canonicalizing and Filtering) and any search algorithm. It typically results in small reduction of visited states, but it significantly reduces the size of the state vector, thus speeding-up JPF run.
  • Dynamic analysis - The analysis observes the reads and writes performed by the program. Together with the program state it stores which fields were relevant (included in that state). These information are used later in state matching when detecting whether reduced state matches or not. The analysis is precise and it typically results in considerable reduction in number of program states, but it takes longer to match the states, thus it can accualy slow down JPF (compared to JPF using normal state matching). Moreover it needs additional memory to store which parts of the state are relevant and requires DFS search. Current prototype implementation supports only Filtering serializer and loop-less state space.

Usage

Sources can be downloaded bellow. The package contains all required ingredients - sources, benchmarks, jpf-core, Wala (used in hybrid analyses) and ant build script. Ant script ant can used to compilaion, running benchmarks and simple examples.

Configuration:
Before you ran the state matching extension, you have to modify configuration. In the file extenals/wala/dat/wala.properties modify entry java_runtime_dir to contain full-path into directory with Java Runtime libraries of the Java you are using (to run JPF). The hybrid analyses needs to process used Java libraries to be able to detetmine its behaviour (future reads); if wrong version of libraries (from older/newer Java) is specified, the soundness of the hybrid analysis can be broken.

Running benchmarks:
To run bunchmarks, run ant check.benchmarks command. It will compile the project and execute standard (clean) JPF as well as JPF with Partial state matching using Hybrid resp. Dynamic analysis on each benchmark. The results (logs with output of the JPF) can be found in the directory output.

Running from command line:
The main class is tools.RunAnalysisWithJPF. The class will run all necessary analysis, configure JPF for specified state matching and run the JPF. It takes the same parameters as JPF (like *.jpf file, +listener=...). In addition, the parameter -useFFRHybrid enables state matching which uses hybrid Future-Field-Read analysis to found irrelevant parts of program states. The parameter -useFFRDynamic enabled dynamic tracking of (ir)relevant parts of program state ommits them from stata matching.

Contact persons: Pavel Jančík, Jan Kofroň

Downloads

 Date  Links
2015-05-12Benchmarks used for evaluationBenchmarks.zip
2015-05-12Sources Sources.zip
2015-05-12Results - logs from benchmarksResults.zip
Logo of Faculty of Mathematics and Physics
  • Phone: +420 951 554 267, +420 951 554 236
  • Email: info<at-sign>d3s.mff.cuni.cz
  •  
  • How to find us?
Modified on 2016-02-19