JPR

Java PathFinder (JPF) is a backtrackable Java Virtual Machine (JVM), which is implemented in Java and runs on a standard JVM (e.g., Oracle HotSpot). Thus, a JPF developer can use off-the- shelf Java debuggers (e.g., jdb) when debugging code that makes up JPF. JPF explores all non-deterministic executions of a given target program and monitors for property violations. To facilitate debugging of the target program, JPF can capture and replay the execution trace that leads to a property violation. While the deterministic replay is invaluable, the replay with JPF does not allow the developer to attach an off-the-shelf Java debugger to the target program (e.g., step through the application code, set breakpoints, etc.). We present a technique, dubbed JPR, to improve the debugging experience of the JPF captured traces by migrating the JPF traces to a new format that can be executed using the standard JVM. JPR annotates each JPF trace, during the capture phase, with ex- tra data (e.g., instruction index, instruction count, etc.); the an- notated trace is then used to instrument Java bytecode to enforce the same execution trace on a standard JVM. JPR is compatible with various optimizations, e.g., state matching and partial-order reduction. We evaluated JPR on all multi-threaded Java pro- grams in the official JPF distribution. Our results show that JPR successfully replayed all JPF traces on the standard JVM with reasonable overhead during both recording and replaying.