Stateless Model Checking Concurrent Programs with Maximal Causality Reduction Conference Paper uri icon

abstract

  • 2015 ACM. We present maximal causality reduction (MCR), a new technique for stateless model checking. MCR systematically explores the state-space of concurrent programs with a provably minimal number of executions. Each execution corresponds to a distinct maximal causal model extracted from a given execution trace, which captures the largest possible set of causally equivalent executions. Moreover, MCR is embarrassingly parallel by shifting the runtime exploration cost to offline analysis. We have designed and implemented MCR using a constraint-based approach and compared with iterative context bounding (ICB) and dynamic partial order reduction (DPOR) on both benchmarks and real-world programs. MCR reduces the number of executions explored by ICB and ICB+DPOR by orders of magnitude, and significantly improves the scalability, efficiency, and effectiveness of the state-of-the-art for both state-space exploration and bug finding. In our experiments, MCR also revealed several new data races and null pointer dereference errors in frequently studied real-world programs.

name of conference

  • PLDI '15: ACM SIGPLAN Conference on Programming Language Design and Implementation

published proceedings

  • ACM SIGPLAN NOTICES

altmetric score

  • 4.25

author list (cited authors)

  • Huang, J.

citation count

  • 14

complete list of authors

  • Huang, Jeff

publication date

  • August 2015