Transcript Document

Java PathFinder (JPF)
cs498dm
Software Testing
January 19, 2012
What is Java PathFinder (JPF)?
• First open source project by NASA (100K)
• JPF is Java Virtual Machine (JVM)
• JPF is implemented in Java itself
2
Demo JPF as JVM
• Obtain a copy
– hg clone http://babelfish.arc.nasa.gov/hg/jpf/jpf-core
• Build
– ant
• Run
– HelloWorld.java
– java HelloWorld
– bin/jpf HelloWorld
3
What is Actually JPF?
• Tool for systematic testing of Java programs
• JVM that has support for fast backtracking
• “the Swiss army knife of Java verification”
4
Non-determinism
• Explicit non-determinism with Verify.getInt
• JPF can be used to find concurrency bugs
• Thread interleavings are another form of
non-determinism
5
GetIntExample
import gov.nasa.jpf.jvm.Verify;
public class GetIntExample {
public static void main(String[] args) {
int i = Verify.getInt(0, 1);
int j = Verify.getInt(2, 3);
System.out.println("i = " + i + " j = " + j);
}
}
Demo: (1) run on JVM (x3); (2) run on JPF; (3) visualize
6
Prints in the Middle
import gov.nasa.jpf.jvm.Verify;
public class GetIntExample {
public static void main(String[] args) {
int i = Verify.getInt(0, 1);
System.out.println("i = " + i);
int j = Verify.getInt(2, 3);
System.out.println(“j = " + j);
}
}
Can be confusing? Documentation not perfect!
7
Inlined print(s)
import gov.nasa.jpf.jvm.Verify;
public class GetIntExample {
public static void main(String[] args) {
System.out.println("i = " + Verify.getInt(0, 1));
int j = Verify.getInt(2, 3);
System.out.println(“j = " + j);
}
}
Example due to Mateusz Ujma
8
JPF How
• JPF explores all possible interleavings
– Regular JVM executes one interleaving, but
repeated executions may differ… or not
• Intuitively, JPF re-executes the program
for all possible interleavings
– Does not actually re-execute from start
– Does not actually explore all interleavings
• Various search strategies:
– DFS, BFS, random… (Demo BFS)
9
java.lang.Thread
• Basic class for threads in Java
• All (started) objects of this class can be
running concurrently
• Need to provide code for the thread
• Some relevant methods
– start, join
– yield, sleep (not so interesting in JPF)
10
Example 2: Counter
class Counter {
int c = 0;
void increment() { c++; }
void decrement() { c--; }
int value() { return c; }
}
• What could go wrong with multithreading?
11
Two Threads Sharing Counter
• What could go wrong with multithreading?
final Counter c = new Counter();
Thread t1 = new Thread() {
public void run() {
c.increment();
}
};
Thread t2 = new Thread() {
public void run() {
c.increment();
}
};
System.out.println(c.value());
12
Extending JPF - Listeners
•
Preferred way of extending JPF:
–‘Listener’ variant of the Observer pattern keep extensions out of the core classes
13
Listeners, the JPF Plugins
14
Example Listener: Count Instructions
public class CountInstListener extends ListenerAdapter {
private int count = 0;
public void executeInstruction(JVM vm) {
// counts only instance creation
if (vm.getCurrentThread().getPC() instanceof NEW)
count++;
}
public void searchFinished(Search search) {
System.out.println("COUNT: " + count);
}
}
15
Main JPF Operations
• Bytecode execution
• State storing/restoring for backtracking
– JPF does not literally re-execute program
from the beginning for each choice
• State comparison
– What is in the state?
16
State of a Java Program
• Stack(s)/thread(s)
– Each thread has a stack with a number of
stack frames that store local variables
– Also a program counter (PC) and thread info
• Heap (in JPF: dynamic area)
– Objects in dynamically allocated memory (can
be shared among threads)
• Classinfo (in JPF: static area)
– Static data once it’s loaded
17
Bytecode Execution
•
•
•
•
Each bytecode changes the state
Some for local data (e.g., IADD)
Some for control/PC (e.g., IFNULL)
Some for shared data (e.g., GETFIELD)
18
State Storing/Restoring
• Stores the entire JVM state (threads,
dynamic area, static area)
• Some pieces of state may not be visible in
source code
• Does NOT restore JPF’s internal info
– E.g., getInt counts what it returned
19
State Comparison
• Compares the entire JVM state (threads,
dynamic area, static area)
• Again, some pieces of state may not be
visible in source code
20
JPF Search
•
•
•
•
Start program from the beginning
Execute bytecodes to get to a new state
Compare if that state was already seen
If not, explore successors from the state
• Various search strategies:
– DFS, BFS, random…
21
Reminder: Project
• Testing a part of JPF
• Deliverables
– Proposal (due in three weeks)
– Progress report (around midterm)
– Final report (by the grade submission
deadline)
– Bug reports (hopefully you’ll find some bugs)
• Extra bonus points for reporting bugs to us
22
How to Test?
• How would you test JPF?
– Execution?
– Storing/restoring?
– State matching?
?
?
JPF
23
Contributions from Darko's Students
• http://mir.cs.illinois.edu/jpf/
• http://babelfish.arc.nasa.gov/trac/jpf/wiki/projects/jpf-actor
• Personal experience
– Have been working with JPF since 2007
– Dozen of bug reports
– Numerous patches (enhancements and bug fixes)
• http://mir.cs.illinois.edu/~gliga/patches.html
–
–
–
–
http://babelfish.arc.nasa.gov/trac/jpf/wiki/projects/jpf-delayed
X10X: Model checking X10 programs with JPF
Granted write access for jpf-core in 2010
Visited NASA Ames in December 2011
24
Conclusions
• JPF is “the Swiss army knife of Java
verification”
• Complex system
– Bytecode execution
– State storing/restoring for backtracking
– State comparison
• Your project will focus on testing one of the
main (sub)parts of JPF
25