Fast detection of concurrency errors by state space traversal with randomization and early backtracking

• DOI: 10.1007/s10009-018-0484-7
• Publication Date: 2018-01-30T06:55:14Z
• Authors: Pavel Parízek; Ondřej Lhoták
• Keywords: 0202 electrical engineering, electronic engineering, information engineering; 02 engineering and technology

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 in 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.