Fast Detection of Concurrency Errors by State Space Traversal with Randomization and Early Backtracking
Abstract
State space traversal is a very popular approach to detect concurrency errors and test concurrent programs. However, it is not practically feasible for complex programs with many thread interleavings and a large state space.
Many techniques explore only a part of the state space in order to find errors quickly --- building upon the observation that errors can often be found in a particular small part of the state space. Great improvements of performance have been achieved also through randomization.
In the context of this research direction, we present the DFS-RB algorithm that augments the standard algorithm for depth-first traversal with early backtracking. Specifically, it is possible to backtrack early from a state before all outgoing transitions have been explored.
The DFS-RB algorithm is non-deterministic --- it uses random numbers, together with values of several parameters, to determine when and how early backtracking takes place in the search. To evaluate DFS-RB, we performed a large experimental study with our prototype implementation in Java Pathfinder on several Java programs.
The results show that DFS-RB achieves better performance in terms of speed and error detection than many state-of-the-art techniques for many benchmarks in our set. Nevertheless, it is difficult to find a single configuration of DFS-RB that works well for many different benchmarks.
We designed a ranking algorithm whose purpose is to identify configurations that yield overall consistently good performance with a small variation.