Assertion guided abstraction: a cooperative optimization for dynamic partial order reduction

Abstract

We propose a new method for reducing the interleaving space during stateless model checking of multithreaded C/C++ programs. The problem is challenging because of the exponential growth of possible interleavings between threads. We have developed a new method, called assertion guided abstraction, which leverages both static and dynamic program analyses in a cooperative framework to reduce the interleaving space. Unlike existing methods that consider all interleavings of all conflicting memory accesses in a program, our new method relies on a new notion of predicate dependence based on which we can soundly abstract the interleaving space to only those conflicting memory accesses that may cause assertion violations and/or deadlocks. Our experimental evaluation of assertion guided abstraction on open source benchmarks shows that it is capable of achieving a significant reduction, thereby allowing for the verification of programs that were previously too complex for existing algorithms to handle.