- ReplayTracer and BMC
BUT - Faculty of Information Technology
FIT spiral-of-death

ReplayTracer and BMC

Model Checker JPF

Home Basic Information Download
Model checker - Java PathFinder

Java PathFinder (JPF) JPF-Wiki is an explicit-state model checker for Java byte-code, implemented over a specialized 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 directed run through the state space controlled by trying to follow a (partially) recorded suspicious run of a given program.

JPF implements several techniques for state space reduction, including partial order reduction which is based on the observation that a large number of theoretically possible thread interleaving 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 the given program.

Record Trace by IBM ConTest

We have implemented trace recording in the IBM ConTest infrastructure. ConTest provides a heuristic noise injection mechanism (to increase probaility of manifestation of concurrency-related bugs) and a listener architecture implementation via Java byte-code instrumentation. We use the listener architecture for recording some points in the run of the monitored application.

The selected events which are recorded contain following information: the appropriate thread identifier, the Java source code line, and the number of instruction generated from this line.

ReplaySearch & BMC in JPF
ReplaySearch

ReplaySearch is new search strategy, the basic is getting from other search strategies like depthFirstSearch (DFS), breadthFirstSearch (BFS) etc. The principle of this algorithm is describe in article: "Self-Healing Assurance Based on Bounded Model Checking", which has presented on EUROCAST 2009.

Bounded Model Checking

Model checking automatically checks whether a system satisfies a specification via a systematic exploration of its state space. A crucial problem with applying it to real software is the state explosion problem. To cope with this problem in our setting, we use bounded model checking in which we limit the depth of the search. This is motivated by an assumption that to show that a suspected concurrency bug is real, it often suffices to explore a bounded neighborhood of the suspected state. This approach is not complete, but a full state space exploration is anyway usually impossible.

In our particular setting of checking whether a suspected data race is real, we use the PreciseDataRace listener available in JPF. JPF allows using or creation next listeners for checking required specification of application.

Ing.Vendula Hrubá, ihruba at fit.vutbr.cz