Jeff Huang
ABSTRACT
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 has also revealed several new data races and null pointer dereference errors in frequently studied real-world programs.
- A. Mazurkiewicz. Trace theory. Advances in Petri Nets, 1987.Google Scholar
Cross Ref
- ASM bytecode analysis framework. http://asm.ow2.org/.Google Scholar
- P. Abdulla, S. Aronis, B. Jonsson, and K. Sagonas. Optimal dynamic partial order reduction. In POPL, 2014. Google ScholarDigital Library
- S. Burckhardt, P. Kothari, M. Musuvathi, and S. Nagarakatte. A randomized scheduler with probabilistic guarantees of finding bugs. In ASPLOS, 2010. Google ScholarDigital Library
- E. M. Clarke, O. Grumberg, M. Minea, and D. Peled. State space reduction using partial order techniques. STTT, 1998.Google Scholar
- K. E. Coons, M. Musuvathi, and K. S. McKinley. Bounded partialorder reduction. In OOPSLA, 2013. Google ScholarDigital Library
- L. De Moura and N. Bjørner. Z3: an efficient SMT solver. In TACAS, 2008. Google ScholarDigital Library
- B. Dutertre and L. D. Moura. The Yices SMT solver. Technical report, 2006.Google Scholar
- A. Farzan, P. Madhusudan, N. Razavi, and F. Sorrentino. Predicting null-pointer dereferences in concurrent programs. In FSE, 2012. Google ScholarDigital Library
- C. Flanagan and P. Godefroid. Dynamic partial-order reduction for model checking software. In POPL, 2005. Google ScholarDigital Library
- P. Godefroid. Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. PhD thesis, University of Liôlge., 1996. ISBN 3540607617.Google ScholarCross Ref
- P. Godefroid. Model checking for programming languages using verisoft. In POPL, 1997. Google ScholarDigital Library
- P. Godefroid. Software model checking: The verisoft approach. Form. Methods Syst. Des., 2005. Google ScholarDigital Library
- J. Huang, P. Liu, and C. Zhang. LEAP: Lightweight deterministic multi-processor replay of concurrent Java programs. In FSE, 2010. Google ScholarDigital Library
- J. Huang, C. Zhang, and J. Dolby. Clap: Recording local executions to reproduce concurrency failures. In PLDI, 2013. Google ScholarDigital Library
- J. Huang, P. O. Meredith, and G. Rosu. Maximal sound predictive race detection with control flow abstraction. In PLDI, 2014. Google ScholarDigital Library
- V. Jagannath, Q. Luo, and D. Marinov. Change-aware preemption prioritization. In ISSTA, 2011. Google ScholarDigital Library
- V. Kahlon, C. Wang, and A. Gupta. Monotonic partial order reduction: An optimal symbolic partial order reduction technique. In CAV, 2009. Google ScholarDigital Library
- M. Kusano and C. Wang. Assertion guided abstraction: a cooperative optimization for dynamic partial order reduction. In ASE, 2014. Google ScholarDigital Library
- L. Lamport. Time, clocks, and the ordering of events in a distributed system. CACM, 1978. Google ScholarDigital Library
- S. Lu, W. Jiang, and Y. Zhou. A study of interleaving coverage criteria. In ESEC-FSE, 2007. Google ScholarDigital Library
- M. Musuvathi and S. Qadeer. Partial-order reduction for contextbounded state exploration. In Tech. Rep. MSR-TR-2007-12, 2007.Google Scholar
- M. Musuvathi and S. Qadeer. Iterative context bounding for systematic testing of multithreaded programs. In PLDI, 2007. Google ScholarDigital Library
- M. Musuvathi and S. Qadeer. Fair stateless model checking. In PLDI, 2008. Google ScholarDigital Library
- M. Musuvathi, S. Qadeer, T. Ball, G. Basler, P. A. Nainar, and I. Neamtiu. Finding and reproducing heisenbugs in concurrent programs. In OSDI, 2008. Google ScholarDigital Library
- S. Nagarakatte, S. Burckhardt, M. M. Martin, and M. Musuvathi. Multicore acceleration of priority-based schedulers for concurrency bug detection. In PLDI, 2012. Google ScholarDigital Library
- H. Patil, C. Pereira, M. Stallcup, G. Lueck, and J. Cownie. Pinplay: a framework for deterministic replay and reproducible analysis of parallel programs. In CGO, 2010. Google ScholarDigital Library
- M. Said, C. Wang, Z. Yang, and K. Sakallah. Generating data race witnesses by an SMT-based analysis. In NFM, 2011. Google ScholarDigital Library
- K. Sen. Race directed random testing of concurrent programs. In PLDI, 2008. Google ScholarDigital Library
- T. F. Serbanuta, F. Chen, and G. Rosu. Maximal causal models for sequentially consistent systems. In RV, 2012.Google Scholar
- J. van den Hooff. Fast bug finding in lock-free data structures with cb-dpor. In Master thesis, Massachusetts Institute of Technology, 2014.Google Scholar
- C. Wang, R. Limaye, M. K. Ganai, and A. Gupta. Trace-based symbolic analysis for atomicity violations. In TACAS, 2010. Google ScholarDigital Library
- C. Wang, M. Said, and A. Gupta. Coverage guided systematic concurrency testing. In ICSE, 2011. Google ScholarDigital Library
- J. Yu, S. Narayanasamy, C. Pereira, and G. Pokam. Maple: A coverage-driven testing tool for multithreaded programs. In OOPSLA, 2012. Google ScholarDigital Library
Index Terms
- Stateless model checking concurrent programs with maximal causality reduction
Recommendations
Stateless model checking concurrent programs with maximal causality reduction
PLDI '15We 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 causality reduction for TSO and PSO
OOPSLA '16Verifying concurrent programs is challenging due to the exponentially large thread interleaving space. The problem is exacerbated by relaxed memory models such as Total Store Order (TSO) and Partial Store Order (PSO) which further explode the ...
Fair stateless model checking
PLDI '08Stateless model checking is a useful state-space exploration technique for systematically testing complex real-world software. Existing stateless model checkers are limited to the verification of safety properties on terminating programs. However, ...
Comments