Advertisement

Combining Parallel Emptiness Checks with Partial Order Reductions

  • Denis Poitrenaud
  • Etienne RenaultEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11852)

Abstract

In explicit state model checking of concurrent systems, multi-core emptiness checks and partial order reductions (POR) are two major techniques to handle large state spaces. The first one tries to take advantage of multi-core architectures while the second one may decrease exponentially the size of the state space to explore.

For checking LTL properties, Bloemen and van de Pol [2] shown that the best performance is currently obtained using their multi-core SCC-based emptiness check. However, combining the latest SCC-based algorithm with POR is not trivial since a condition on cycles, the proviso, must be enforced on an algorithm which processes collaboratively cycles. In this paper, we suggest a pessimistic approach to tackle this problem for liveness properties. For safety ones, we propose an algorithm which takes benefit from the information computed by the SCC-based algorithm.

We also present new parallel provisos for both safety and liveness properties that relies on other multi-core emptiness checks. We observe that all presented algorithms maintain good reductions and scalability.

References

  1. 1.
    Barnat, J., Brim, L., Rockai, P.: Parallel partial order reduction with topological sort proviso. In: SEFM 2010, pp. 222–231. September 2010Google Scholar
  2. 2.
    Bloemen, V., van de Pol, J.: Multi-core SCC-based LTL model checking. In: Bloem, R., Arbel, E. (eds.) HVC 2016. LNCS, vol. 10028, pp. 18–33. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-49052-6_2CrossRefGoogle Scholar
  3. 3.
    Bloemen, V., Laarman, A., van de Pol, J.: Multi-core on-the-fly SCC decomposition. vol. 51, March 2016Google Scholar
  4. 4.
    Bošnački, D., Leue, S., Lafuente, A.L.: Partial-order reduction for general state exploring algorithms. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 271–287. Springer, Heidelberg (2006).  https://doi.org/10.1007/11691617_16CrossRefGoogle Scholar
  5. 5.
    Bošnaăźki, D., Leue, S., Lluch Lafuente, A.: Partial-order reduction for general state exploring algorithms. Int. J. Softw. Tools Technol. Transf. (STTT) 11(1), 39–51 (2009)CrossRefGoogle Scholar
  6. 6.
    Couvreur, J.-M.: On-the-fly verification of linear temporal logic. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 253–271. Springer, Heidelberg (1999).  https://doi.org/10.1007/3-540-48119-2_16CrossRefGoogle Scholar
  7. 7.
    Duret-Lutz, A., Kordon, F., Poitrenaud, D., Renault, E.: Heuristics for checking liveness properties with partial order reductions. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 340–356. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-46520-3_22CrossRefGoogle Scholar
  8. 8.
    Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, É., Xu, L.: Spot 2.0 — a framework for LTL and \(\omega \)-automata manipulation. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 122–129. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-46520-3_8CrossRefGoogle Scholar
  9. 9.
    Evangelista, S., Pajault, C.: Solving the ignoring problem for partial order reduction. Int. J. Softw. Tools Technol. Transf. 12(2), 155–170 (2010)CrossRefGoogle Scholar
  10. 10.
    Evangelista, S., Laarman, A., Petrucci, L., van de Pol, J.: Improved multi-core nested depth-first search. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, pp. 269–283. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-33386-6_22CrossRefGoogle Scholar
  11. 11.
    Hansen, H., Valmari, A.: Safety property-driven stubborn sets. In: Larsen, K.G., Potapov, I., Srba, J. (eds.) RP 2016. LNCS, vol. 9899, pp. 90–103. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-45994-3_7CrossRefGoogle Scholar
  12. 12.
    Holzmann, G.J., Peled, D.A., Yannakakis, M.: On nested depth first search. In: SPIN 1996, vol. 32, DIMACS: Series in Discrete Mathematics and Theoretical Computer Science. American Mathematical Society, May 1996Google Scholar
  13. 13.
    Holzmann, G.J., Joshi, R., Groce, A.: Swarm verification techniques. IEEE Trans. Softw. Eng. 37(6), 845–857 (2011)CrossRefGoogle Scholar
  14. 14.
    Laarman, A., Faragó, D.: Improved on-the-Fly livelock detection. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 32–47. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-38088-4_3CrossRefGoogle Scholar
  15. 15.
    Laarman, A., Pater, E., Pol, J., Hansen, H.: Guard-based partial-order reduction. STTT, pp. 1–22 (2014)Google Scholar
  16. 16.
    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_20CrossRefGoogle Scholar
  17. 17.
    Lerda, F., Sisto, R.: Distributed-memory model checking with SPIN. In: Dams, D., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol. 1680, pp. 22–39. Springer, Heidelberg (1999).  https://doi.org/10.1007/3-540-48234-2_3CrossRefGoogle Scholar
  18. 18.
    Nalumasu, R., Gopalakrishnan, G.: An efficient partial order reduction algorithm with an alternative proviso implementation. FMSD 20(1), 231–247 (2002)zbMATHGoogle Scholar
  19. 19.
    Pater, E.: Partial order reduction for pins, March 2011Google Scholar
  20. 20.
    Pelánek, R.: BEEM: benchmarks for explicit model checkers. In: Bošnački, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 263–267. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-73370-6_17CrossRefGoogle Scholar
  21. 21.
    Pelánek, R.: Properties of state spaces and their applications. Int. J. Softw. Tools Technol. Transf. (STTT) 10, 443–454 (2008)CrossRefGoogle Scholar
  22. 22.
    Peled, D.: Combining partial order reductions with on-the-fly model-checking. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 377–390. Springer, Heidelberg (1994).  https://doi.org/10.1007/3-540-58179-0_69CrossRefGoogle Scholar
  23. 23.
    Peled, D., Valmari, A., Kokkarinen, I.: Relaxed visibility enhances partial order reduction. Formal Meth. Syst. Des. 19(3), 275–289 (2001)CrossRefGoogle Scholar
  24. 24.
    Renault, E., Duret-Lutz, A., Kordon, F., Poitrenaud, D.: Variations on parallel explicit model checking for generalized Büchi automata. Int. J. Softw. Tools Technol. Transf. (STTT) 19, 1–21 (2016)zbMATHGoogle Scholar
  25. 25.
    Siegel, S.F.: What’s wrong with on-the-fly partial order reduction. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 478–495. Springer, Cham (2019).  https://doi.org/10.1007/978-3-030-25543-5_27CrossRefGoogle Scholar
  26. 26.
    Tarjan, R.: Depth-first search and linear graph algorithms. SIAM J. Comput. 1(2), 146–160 (1972) MathSciNetCrossRefGoogle Scholar
  27. 27.
    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_36CrossRefGoogle Scholar
  28. 28.
    Valmari, A.: More stubborn set methods for process algebras. In: Gibson-Robinson, T., Hopcroft, P., Lazić, R. (eds.) Concurrency, Security, and Puzzles. LNCS, vol. 10160, pp. 246–271. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-51046-0_13CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Sorbonne Université, CNRS, LIP6ParisFrance
  2. 2.Université Paris DescartesParisFrance
  3. 3.LRDE, EPITAKremlin-BicêtreFrance

Personalised recommendations