Causality-based Verification of Multi-threaded Programs?

Abstract. We present a new model checking procedure for concurrent systems against safety properties such as data races or atomicity vi-olations. Our analysis sidesteps the state space explosion problem by inferring causal dependencies for concurrent traces instead of searching over a space of reachable states, and can be understood as an interplay between local trace inference and termination analysis based on causal loops. Local trace inference introduces new actions anywhere in the trace if they causally follow from the context. Our procedure terminates if we either find a complete error trace or the whole space of potential er-ror traces is covered by causal loops. The causality-based verification of multi-threaded programs can be dramatically faster than the standard state space traversal. In particular, we show that the complexity of ver-ifying multi-threaded programs with locks reduces from exponential to polynomial.