Symbolic pruning of concurrent program executions

ABSTRACT

We propose a new algorithm for verifying concurrent programs, which uses concrete executions to partition the program into a set of lean partitions called concurrent trace programs (CTPs), and symbolically verifies each CTP using a satisfiability solver. A CTP, derived from a concrete execution trace, implicitly captures all permutations of the trace that also respect the control flow of the program. We show that a CTP, viewed as a coarser equivalence class than the popular (Mazurkiewicz) trace equivalence in partial order reduction (POR) literature, leads to more effective pruning of the search space during model checking. While classic POR can prune away redundant interleavings within each trace equivalence class, the pruning in POR is not property driven. We use symbolic methods to achieve property-driven pruning. The effort of exploration is distributed between a symbolic component (verification of a particular CTP) and an enumerative component (exploration of the space of CTPs). We show that the proposed method facilitates more powerful pruning of the search space during the enumerative exploration.

REFERENCES

• 1: S. Burckhardt, R. Alur, and M. Martin. CheckFence: checking consistency of concurrent data types on relaxed memory models. In Programming Language Design and Implementation, pages 12--21. ACM, 2007.
• 2: F. Chen and G. Rosu. Parametric and sliced causality. In Computer Aided Verification, pages 240--253. 2007.
• 3: E. M. Clarke, D. Kroening, and F. Lerda. A tool for checking ANSI-C programs. In Tools and Algorithms for Construction and Analysis of Systems, pages 168--176. Springer, 2004.
• 4: B. Cook, D. Kroening, and N. Sharygina. Symbolic model checking for asynchronous boolean programs. In SPIN Workshop on Model Checking Software, pages 75--90. Springer, 2005.
• 5: B. Dutertre and L. de Moura. A fast linear-arithmetic solver for dpll(t). In Computer Aided Verification, pages 81--94. Springer, 2006.
• 6: C. Flanagan and P. Godefroid. Dynamic partial-order reduction for model checking software. In Principles of programming languages, pages 110--121, 2005.
• 7: M. Ganai and A. Gupta. Efficient modeling of concurrent systems in BMC. In SPIN Workshop on Model Checking Software, pages 114--133. Springer, 2008.
• 8: P. Godefroid. Software model checking: The VeriSoft approach. Formal Methods in System Design, 26(2):77--101, 2005.
• 9: O. Grumberg, F. Lerda, O. Strichman, and M. Theobald. Proof-guided underapproximation-widening for multi-process systems. In Principles of programming languages, pages 122--131, 2005.
• 10: F. Ivančić, I. Shlyakhter, A. Gupta, M.K. Ganai, V. Kahlon, C. Wang, and Z. Yang. Model checking C program using F-Soft. In International Conference on Computer Design, pages 297--308, October 2005.
• 11: V. Kahlon, A. Gupta, and N. Sinha. Symbolic model checking of concurrent programs using partial orders and on-the-fly transactions. In Computer Aided Verification, pages 286--299. Springer, 2006.
• 12: V. Kahlon, C. Wang, and A. Gupta. Monotonic partial order reduction: An optimal symbolic partial order reduction technique. In Computer Aided Verification, pages 398--413, 2009.
• 13: S. Lahiri and S. Qadeer. Back to the future: revisiting precise program verification using SMT solvers. In Principles of Programming Languages, pages 171--182. ACM, 2008.
• 14: J. Lee, D. Padua, and S. Midkiff. Basic compiler algorithms for parallel programs. In Principles and Practice of Parallel Programming, pages 1--12, 1999.
• 15: A. W. Mazurkiewicz. Trace theory. In Advances in Petri Nets, pages 279--324. Springer, 1986.
• 16: M. Musuvathi and S. Qadeer. CHESS: Systematic stress testing of concurrent software. In Logic-Based Program Synthesis and Transformation, pages 15--16. Springer, 2006.
• 17: G. Necula, S. McPeak, S. Rahul, and W. Weimer. CIL: Intermediate language and tools for analysis and transformation of c programs. In International Conference on Compiler Construction, pages 213--228. Springer, 2002.
• 18: I. Rabinovitz and O. Grumberg. Bounded model checking of concurrent programs. In Computer Aided Verification, pages 82--97. Springer, 2005.
• 19: K. Sen, G. Rosu, and G. Agha. Detecting errors in multithreaded programs by generalized predictive analysis of executions. In Formal Methods for Open Object-Based Distributed Systems, pages 211--226. Springer, 2005.
• 20: J. P. M. Silva and K. A. Sakallah. Grasp - a new search algorithm for satisfiability. In International Conference on Computer-Aided Design, pages 220--227, November 1996.
• 21: C. Wang, Y. Yang, A. Gupta, and G. Gopalakrishnan. Dynamic model checking with property driven pruning to detect race conditions. In Automated Technology for Verification and Analysis. Springer, 2008.
• 22: C. Wang, Z. Yang, V. Kahlon, and A. Gupta. Peephole partial order reduction. In Tools and Algorithms for Construction and Analysis of Systems, pages 382--396. Springer, 2008.
• 23: Y. Yang, X. Chen, and G. Gopalakrishnan. Inspect: A Runtime Model Checker for Multithreaded C Programs. Technical Report UUCS-08-004, University of Utah, 2008.
• 24: Y. Yang, X. Chen, G. Gopalakrishnan, and C. Wang. Automatic discovery of transition symmetry in multithreaded programs using dynamic analysis. In SPIN workshop on Software Model Checking, 2009.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

General Terms:
Verification

Keywords:
concurrency, partial order reduction, pruning, sat