Java PathFinder (JPF) is an
explicit-state model checker for Java byte-code, implemented over a specialised
Java virtual machine. JPF provides several state space search strategies like
depth-first search (DFS) or breadth-first search (BFS) as well as a
listener-based mechanism allowing new user-specific strategies to be defined. We
exploit this feature in our work to implement a navigation through a state space
based on a (partially) recorded suspicious run of a given program.
JPF implements several techniques for state space reduction, including the partial order reduction (POR) which is based on the observation
that a large number of possible thread interleavings are irrelevant for the
properties being checked in concurrent programs. JPF automatically detects which
schedules are relevant when checking a certain property. Moreover, JPF provides
a mechanism to influence the mechanism of choosing the relevant schedules. This
is important for us because, on one hand, we cannot avoid partial order
reduction not to significantly increase the number of explored states, and, on
the other hand, the implicit partial order reduction of JPF may interfere with
our intention to reconstruct a certain specific run of a given program.
We have implemented the trace recording on top of the infrastructure provided by
the
IBM Contest
tool. Contest provides a heuristic noise injection mechanism, to increase
probability of manifestation of concurrency-related errors, and a listener
architecture, implemented via a Java byte-code instrumentation, for retrieving
various information about the program being monitored. We use the listener
architecture to record some information (monitored events) during the execution
of the monitored program.
Each monitored event contains information about the source-code location from
which it was generated (class and method name, line and instruction number) and
the thread which generated it.
ReplayHeuristicSearch is a new search strategy for navigation through a state
space of a program in the JPF model checker based on the information contained
in a recorded trace. The approach for navigation through a state space has been
proposed and published in the article Self-Healing Assurance Based on
Bounded Model Checking in EUROCAST 2009.
The ReplayHeuristicSearch simply tries to generate some execution whose
underlying trace corresponds with a recorded trace. It is also possible to let
the model checker generate more executions with the same trace.
Bounded model checking is performed in the vicinity of the replayed executions,
trying to confirm that there is really some error in the program and/or to debug
the recorded suspicious behaviour. The verification listeners looking for
occurrences of errors may be activated either at the very beginning of replaying
of a trace, or they may be activated at the beginning of each application of
bounded model checking. The users can adjust the bounded model checking settings
(the depth of the bounded model checking as well as the number of backward
steps). This approach is not complete, however the full model checking is much
more time costly.
For instance, we are using the PreciseRaceDetector listener available in JPF for
checking whether a data race is real. But JPF allows to add other user-specific
listeners for checking the required features of programs.
