Stubborn Transaction Reduction

Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10811)

Abstract

The exponential explosion of parallel interleavings remains a fundamental challenge to model checking of concurrent programs. Both partial-order reduction (POR) and transaction reduction (TR) decrease the number of interleavings in a concurrent system. Unlike POR, transactions also reduce the number of intermediate states. Modern POR techniques, on the other hand, offer more dynamic ways of identifying commutative behavior, a crucial task for obtaining good reductions.

We show that transaction reduction can use the same dynamic commutativity as found in stubborn set POR. We also compare reductions obtained by POR and TR, demonstrating with several examples that these techniques complement each other. With an implementation of the dynamic transactions in the model checker LTSmin, we compare its effectiveness with the original static TR and two POR approaches. Several inputs, including realistic case studies, demonstrate that the new dynamic TR can surpass POR in practice.

References

  1. 1.
    Abdulla, P., Aronis, S., Jonsson, B., Sagonas, K.: Optimal dynamic partial order reduction. In: POPL, pp. 373–384. ACM (2014)Google Scholar
  2. 2.
    Albert, E., Arenas, P., de la Banda, M.G., Gómez-Zamalloa, M., Stuckey, P.J.: Context-sensitive dynamic partial order reduction. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 526–543. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-63387-9_26 CrossRefGoogle Scholar
  3. 3.
    Alur, R., Brayton, R.K., Henzinger, T.A., Qadeer, S., Rajamani, S.K.: Partial-order reduction in symbolic state space exploration. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 340–351. Springer, Heidelberg (1997).  https://doi.org/10.1007/3-540-63166-6_34 CrossRefGoogle Scholar
  4. 4.
    Barnat, J., Brim, L., Ročkai, P.: Parallel partial order reduction with topological sort proviso. In: SEFM, pp. 222–231. IEEE (2010)Google Scholar
  5. 5.
    Bošnački, D., Holzmann, G.J.: Improving spin’s partial-order reduction for breadth-first search. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol. 3639, pp. 91–105. Springer, Heidelberg (2005).  https://doi.org/10.1007/11537328_10 CrossRefGoogle Scholar
  6. 6.
    Cohen, E., Lamport, L.: Reduction in TLA. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 317–331. Springer, Heidelberg (1998).  https://doi.org/10.1007/BFb0055631 CrossRefGoogle Scholar
  7. 7.
    Doeppner Jr., T.W.: Parallel program correctness through refinement. In: POPL, pp. 155–169. ACM (1977)Google Scholar
  8. 8.
    Dwyer, M., et al.: Exploiting object escape and locking information in partial-order reductions for concurrent object-oriented programs. FMSD 25(2–3), 199–240 (2004)MATHGoogle Scholar
  9. 9.
    Elmas, T., Qadeer, S., Tasiran, S.: A calculus of atomic actions. In: POPL, pp. 2–15. ACM (2009)Google Scholar
  10. 10.
    Evangelista, S., Pajault, C.: Solving the ignoring problem for partial order reduction. STTT 12, 155–170 (2010)CrossRefGoogle Scholar
  11. 11.
    Flanagan, C., Freund, S.N., Qadeer, S.: Thread-modular verification for shared-memory programs. In: Le Métayer, D. (ed.) ESOP 2002. LNCS, vol. 2305, pp. 262–277. Springer, Heidelberg (2002).  https://doi.org/10.1007/3-540-45927-8_19 CrossRefGoogle Scholar
  12. 12.
    Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: POPL, vol. 40, no. 1, pp. 110–121. ACM (2005)Google Scholar
  13. 13.
    Flanagan, C., Qadeer, S.: Transactions for software model checking. ENTCS 89(3), 518–539 (2003)MATHGoogle Scholar
  14. 14.
    Flanagan, C., Qadeer, S.: A type and effect system for atomicity. In: PLDI, pp. 338–349. ACM (2003)Google Scholar
  15. 15.
    Flanagan, C., Qadeer, S.: Types for atomicity. In: SIGPLAN Notices, vol. 38(3), pp. 1–12, January 2003Google Scholar
  16. 16.
    Freund, S.N., Qadeer, S.: Checking concise specifications for multithreaded software. J. Object Technol. 3, 81–101 (2004)CrossRefGoogle Scholar
  17. 17.
    Gerth, R., Kuiper, R., Peled, D., Penczek, W.: A partial order approach to branching time logic model checking. In: TCS, pp. 130–139. IEEE (1995)Google Scholar
  18. 18.
    Godefroid, P., Pirottin, D.: Refining dependencies improves partial-order verification methods (extended abstract). In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 438–449. Springer, Heidelberg (1993).  https://doi.org/10.1007/3-540-56922-7_36 CrossRefGoogle Scholar
  19. 19.
    Godefroid, P., Wolper, P.: Using partial orders for the efficient verification of deadlock freedom and safety properties. FMSD 2, 149–164 (1993)MATHGoogle Scholar
  20. 20.
    Godefroid, P. (ed.): Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol. 1032. Springer, Heidelberg (1996).  https://doi.org/10.1007/3-540-60761-7 MATHGoogle Scholar
  21. 21.
    Gribomont, E.P.: Atomicity refinement and trace reduction theorems. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 311–322. Springer, Heidelberg (1996).  https://doi.org/10.1007/3-540-61474-5_79 CrossRefGoogle Scholar
  22. 22.
    Grumberg, O., et al.: Proof-guided underapproximation-widening for multi-process systems. In: POPL, pp. 122–131. ACM (2005)Google Scholar
  23. 23.
    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).  https://doi.org/10.1007/978-3-540-73370-6_8 CrossRefGoogle Scholar
  24. 24.
    Günther, H., Laarman, A., Weissenbacher, G.: Vienna verification tool: IC3 for parallel software. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 954–957. Springer, Heidelberg (2016).  https://doi.org/10.1007/978-3-662-49674-9_69 CrossRefGoogle Scholar
  25. 25.
    Günther, H., Laarman, A., Sokolova, A., Weissenbacher, G.: Dynamic reductions for model checking concurrent software. In: Bouajjani, A., Monniaux, D. (eds.) VMCAI 2017. LNCS, vol. 10145, pp. 246–265. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-52234-0_14 CrossRefGoogle Scholar
  26. 26.
    Holzmann, G.J.: The model checker SPIN. IEEE TSE 23, 279–295 (1997)Google Scholar
  27. 27.
    Holzmann, G.J., Peled, D.: An improvement in formal verification. In: IFIP WG6.1 ICFDT VII, pp. 197–211. Chapman & Hall Ltd. (1995)Google Scholar
  28. 28.
    Janicki, R., Kleijn, J., Koutny, M., Mikulski, Ł.: Step traces. Acta Inform. 53(1), 35–65 (2016)MathSciNetCrossRefMATHGoogle Scholar
  29. 29.
    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).  https://doi.org/10.1007/11817963_28 CrossRefGoogle Scholar
  30. 30.
    Kahlon, V., Wang, C., Gupta, A.: Monotonic partial order reduction: an optimal symbolic partial order reduction technique. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 398–413. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-02658-4_31 CrossRefGoogle Scholar
  31. 31.
    Kant, G., Laarman, A., Meijer, J., van de Pol, J., Blom, S., van Dijk, T.: LTSmin: high-performance language-independent model checking. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 692–707. Springer, Heidelberg (2015).  https://doi.org/10.1007/978-3-662-46681-0_61 Google Scholar
  32. 32.
    Kastenberg, H., Rensink, A.: Dynamic partial order reduction using probe sets. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 233–247. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-85361-9_21 CrossRefGoogle Scholar
  33. 33.
    Katz, S., Peled, D.: An efficient verification method for parallel and distributed programs. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) REX 1988. LNCS, vol. 354, pp. 489–507. Springer, Heidelberg (1989).  https://doi.org/10.1007/BFb0013032 CrossRefGoogle Scholar
  34. 34.
    Katz, S., Peled, D.: Defining conditional independence using collapses. Theor. Comput. Sci. 101(2), 337–359 (1992)MathSciNetCrossRefMATHGoogle Scholar
  35. 35.
    Laarman, A.W., Pater, E., van de Pol, J.C., Hansen, H.: Guard-based partial-order reduction. In: STTT, pp. 1–22 (2014)Google Scholar
  36. 36.
    Laarman, A., Wijs, A.: Partial-order reduction for multi-core LTL model checking. In: Yahav, E. (ed.) HVC 2014. LNCS, vol. 8855, pp. 267–283. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-13338-6_20 Google Scholar
  37. 37.
    Lamport, L., Schneider, F.B.: Pretending atomicity. Technical report, Cornell University (1989)Google Scholar
  38. 38.
    Lipton, R.J.: Reduction: a method of proving properties of parallel programs. Commun. ACM 18(12), 717–721 (1975)MathSciNetCrossRefMATHGoogle Scholar
  39. 39.
    Malkis, A., Podelski, A., Rybalchenko, A.: Thread-modular verification is Cartesian abstract interpretation. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds.) ICTAC 2006. LNCS, vol. 4281, pp. 183–197. Springer, Heidelberg (2006).  https://doi.org/10.1007/11921240_13 CrossRefGoogle Scholar
  40. 40.
    Papadimitriou, C.: The Theory of Database Concurrency control. Principles of Computer Science Series. Computer Science Press, Rockville (1986)MATHGoogle Scholar
  41. 41.
    Rodríguez, C., et al.: Unfolding-based partial order reduction. In: CONCUR. LIPIcs, vol. 42, pp. 456–469. Leibniz-Zentrum fuer Informatik (2015)Google Scholar
  42. 42.
    Van Der Schoot, H., Ural, H.: An improvement of partial-order verification. Softw. Test. Verif. Reliab. 8(2), 83–102 (1998)CrossRefGoogle Scholar
  43. 43.
    Stoller, S.D., Cohen, E.: Optimistic synchronization-based state-space reduction. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 489–504. Springer, Heidelberg (2003).  https://doi.org/10.1007/3-540-36577-X_36 CrossRefGoogle Scholar
  44. 44.
    Tarjan, R.: Depth-first search and linear graph algorithms. SIAM J. Comput. 1(2), 146–160 (1972)MathSciNetCrossRefMATHGoogle Scholar
  45. 45.
    Valmari, A.: Error detection by reduced reachability graph generation. In: APN, pp. 95–112 (1988)Google Scholar
  46. 46.
    Valmari, A.: Eliminating redundant interleavings during concurrent program verification. In: Odijk, E., Rem, M., Syre, J.-C. (eds.) PARLE 1989. LNCS, vol. 366, pp. 89–103. Springer, Heidelberg (1989).  https://doi.org/10.1007/3-540-51285-3_35 CrossRefGoogle Scholar
  47. 47.
    Valmari, A.: Stubborn sets for reduced state space generation. In: Rozenberg, G. (ed.) ICATPN 1989. LNCS, vol. 483, pp. 491–515. Springer, Heidelberg (1991).  https://doi.org/10.1007/3-540-53863-1_36 CrossRefGoogle Scholar
  48. 48.
    Valmari, A.: The state explosion problem. In: Reisig, W., Rozenberg, G. (eds.) ACPN 1996. LNCS, vol. 1491, pp. 429–528. Springer, Heidelberg (1998).  https://doi.org/10.1007/3-540-65306-6_21 CrossRefGoogle Scholar
  49. 49.
    Valmari, A., Hansen, H.: Can stubborn sets be optimal? In: Lilius, J., Penczek, W. (eds.) PETRI NETS 2010. LNCS, vol. 6128, pp. 43–62. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-13675-7_5 CrossRefGoogle Scholar
  50. 50.
    Valmari, A.: A stubborn attack on state explosion. In: Clarke, E.M., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 156–165. Springer, Heidelberg (1991).  https://doi.org/10.1007/BFb0023729 CrossRefGoogle Scholar
  51. 51.
    Valmari, A.: Stubborn set methods for process algebras. In: DIMACS POMIV, POMIV 1996, pp. 213–231. AMS Press, Inc., New York (1997)Google Scholar
  52. 52.
    Valmari, A., Hansen, H.: Stubborn set intuition explained. In: Petri Nets and Software Engineering 2016, CEUR-WS, pp. 213–232. CEUR (2016)Google Scholar
  53. 53.
    Valmari, A., Vogler, W.: Fair testing and stubborn sets. In: Bošnački, D., Wijs, A. (eds.) SPIN 2016. LNCS, vol. 9641, pp. 225–243. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-32582-8_16 CrossRefGoogle Scholar
  54. 54.
    van der Berg, F., Laarman, A.: SpinS: extending LTSmin with Promela through SpinJa. ENTCS 296, 95–105 (2013)Google Scholar
  55. 55.
    Varpaaniemi, K.: Finding small stubborn sets automatically. In: ISCIS, vol. I, pp. 133–142. Middle East Technical University, Ankara, Turkey (1996)Google Scholar
  56. 56.
    Varpaaniemi, K.: On the stubborn set method in reduced state space generation. Ph.D. thesis, Helsinki University of Technology (1998)Google Scholar
  57. 57.
    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).  https://doi.org/10.1007/978-3-540-78800-3_29 CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  1. 1.Leiden UniversityLeidenThe Netherlands

Personalised recommendations