Advertisement

Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique

  • Vineet Kahlon
  • Chao Wang
  • Aarti Gupta
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5643)

Abstract

We present a new technique called Monotonic Partial Order Reduction (MPOR) that effectively combines dynamic partial order reduction with symbolic state space exploration for model checking concurrent software. Our technique hinges on a new characterization of partial orders defined by computations of a concurrent program in terms of quasi-monotonic sequences of thread-ids. This characterization, which is of independent interest, can be used both for explicit or symbolic model checking. For symbolic model checking, MPOR works by adding constraints to allow automatic pruning of redundant interleavings in a SAT/SMT solver based search by restricting the interleavings explored to the set of quasi-monotonic sequences. Quasi-monotonicity guarantees both soundness (all necessary interleavings are explored) and optimality (no redundant interleaving is explored) and is, to the best of our knowledge, the only known optimal symbolic POR technique.

Keywords

Model Check Concurrent Program Symbolic Model Check Bound Model Check Schedule Constraint 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    Alur, R., Brayton, R.K., Henzinger, T.A., Qadeer, S., Rajamani, S.K.: Partial-order reduction in symbolic state-space exploration. Formal Methods in System Design 18(2), 97–116 (2001)CrossRefzbMATHGoogle Scholar
  2. 2.
    Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, p. 193. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  3. 3.
    Cook, B., Kroening, D., Sharygina, N.: Symbolic model checking for asynchronous boolean programs. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol. 3639, pp. 75–90. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  4. 4.
    Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for dpll(t). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81–94. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  5. 5.
    Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: Principles of programming languages (POPL 2005), pp. 110–121 (2005)Google Scholar
  6. 6.
    Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Explosion Problem. Springer, Heidelberg (1996)CrossRefzbMATHGoogle Scholar
  7. 7.
    Godefroid, P., Pirottin, D.: Refining dependencies improves partial-order verification methods. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 438–449. Springer, Heidelberg (1993)CrossRefGoogle Scholar
  8. 8.
    Grumberg, O., Lerda, F., Strichman, O., Theobald, M.: Proof-guided underapproximation-widening for multi-process systems. In: POPL (2005)Google Scholar
  9. 9.
    Gueta, G., Flanagan, C., Yahav, E., Sagiv, M.: Cartesian partial-order reduction. In: Bošnački, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 95–112. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  10. 10.
    Kahlon, V., Gupta, A., Sinha, N.: Symbolic model checking of concurrent programs using partial orders and on-the-fly transactions. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 286–299. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  11. 11.
    Katz, S., Peled, D.: Defining conditional independence using collapses. Theor. Comput. Sci. 101(2), 337–359 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    Lerda, F., Sinha, N., Theobald, M.: Symbolic model checking of software. Electr. Notes Theor. Comput. Sci. 89(3) (2003)Google Scholar
  13. 13.
    Mazurkiewicz, A.W.: Trace theory. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) APN 1986. LNCS, vol. 255, pp. 279–324. Springer, Heidelberg (1987)Google Scholar
  14. 14.
    Peled, D.: All from one, one for all: on model checking using representatives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697. Springer, Heidelberg (1993)CrossRefGoogle Scholar
  15. 15.
    Silva, J.P.M., Sakallah, K.A.: Grasp—a new search algorithm for satisfiability. In: International Conference on Computer-Aided Design, San Jose, CA (1996)Google Scholar
  16. 16.
    Valmari, A.: Stubborn sets for reduced state space generation. In: Rozenberg, G. (ed.) APN 1990. LNCS, vol. 483, pp. 491–515. Springer, Heidelberg (1991)CrossRefGoogle Scholar
  17. 17.
    Wang, C., Yang, Z., Kahlon, V., Gupta, A.: Peephole partial order reduction. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 382–396. Springer, Heidelberg (2008)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Vineet Kahlon
    • 1
  • Chao Wang
    • 1
  • Aarti Gupta
    • 1
  1. 1.NEC Laboratories AmericaPrincetonUSA

Personalised recommendations