Finding Concurrency Errors Using Stateless Model Checking
Powered by Optimal Dynamic Partial Order Reduction

Kostis Sagonas

We will present some of the techniques used in Concuerror, a stateless model checking tool able to find and reproduce a wide class of concurrency errors in Erlang programs. We will first describe how we take advantage of the characteristics of Erlang's actor model of concurrency to selectively instrument the program under test and how we subsequently employ a stateless search strategy to systematically explore the state space of process interleaving sequences triggered by unit tests. To ameliorate the problem of combinatorial explosion, we have designed an implemented two novel dynamic partial order reduction (DPOR) algorithms: one based on a new idea of avoiding exploration of redundant interleaving and one which is provably optimal. The tool combines these DPOR algorithms with preemption bounding, a heuristic algorithm for exploring interleaving sequences up to a context bound. We also briefly discuss issues related to soundness, completeness and effectiveness of techniques covered in the talk. Experimental results will also be presented.

The talk will be interactive and will include a demo of the tool.