Skip to main content
SpringerLink
Log in
Book cover

International Conference on Formal Engineering Methods

ICFEM 2019: Formal Methods and Software Engineering pp 370–386Cite as

Combining Parallel Emptiness Checks with Partial Order Reductions

  • Conference paper
  • First Online:

  • 872 Accesses

Part of the book series: Lecture Notes in Computer Science ((LNPSE,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.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    See Peled [22] for a survey of POR reductions with LTL.

  2. 2.

    All instructions (excepted recursive calls) are considered to be atomic.

  3. 3.

    For a description of our setup, including selected models, detailed results and code, see http://www.lrde.epita.fr/~renault/benchs/ICFEM-2019/results.html.

  4. 4.

    Notice that we only consider the blue DFS (without lines 33–37). When implementing an emptiness check the ignored lines could trigger complementary expansions. Thus the reported values here can be interpreted as the optimal bound (time, reduction, ...) for this algorithm.

  5. 5.

    Our implementation uses persistent sets since a special attention must be paid when combining ample sets with on-the-fly exploration [25].

  6. 6.

    See http://fmt.cs.utwente.nl/tools/ltsmin/#divine for more details.

References

  1. Barnat, J., Brim, L., Rockai, P.: Parallel partial order reduction with topological sort proviso. In: SEFM 2010, pp. 222–231. September 2010

    Google Scholar 

  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_2

    Chapter  Google Scholar 

  3. Bloemen, V., Laarman, A., van de Pol, J.: Multi-core on-the-fly SCC decomposition. vol. 51, March 2016

    Google Scholar 

  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_16

    Chapter  Google Scholar 

  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)

    Article  Google Scholar 

  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_16

    Chapter  Google Scholar 

  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_22

    Chapter  Google Scholar 

  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_8

    Chapter  Google Scholar 

  9. Evangelista, S., Pajault, C.: Solving the ignoring problem for partial order reduction. Int. J. Softw. Tools Technol. Transf. 12(2), 155–170 (2010)

    Article  Google Scholar 

  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_22

    Chapter  Google Scholar 

  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_7

    Chapter  Google Scholar 

  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 1996

    Google Scholar 

  13. Holzmann, G.J., Joshi, R., Groce, A.: Swarm verification techniques. IEEE Trans. Softw. Eng. 37(6), 845–857 (2011)

    Article  Google Scholar 

  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_3

    Chapter  Google Scholar 

  15. Laarman, A., Pater, E., Pol, J., Hansen, H.: Guard-based partial-order reduction. STTT, pp. 1–22 (2014)

    Google Scholar 

  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_20

    Chapter  Google Scholar 

  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_3

    Chapter  Google Scholar 

  18. Nalumasu, R., Gopalakrishnan, G.: An efficient partial order reduction algorithm with an alternative proviso implementation. FMSD 20(1), 231–247 (2002)

    MATH  Google Scholar 

  19. Pater, E.: Partial order reduction for pins, March 2011

    Google Scholar 

  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_17

    Chapter  Google Scholar 

  21. Pelánek, R.: Properties of state spaces and their applications. Int. J. Softw. Tools Technol. Transf. (STTT) 10, 443–454 (2008)

    Article  Google Scholar 

  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_69

    Chapter  Google Scholar 

  23. Peled, D., Valmari, A., Kokkarinen, I.: Relaxed visibility enhances partial order reduction. Formal Meth. Syst. Des. 19(3), 275–289 (2001)

    Article  Google Scholar 

  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)

    MATH  Google Scholar 

  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_27

    Chapter  Google Scholar 

  26. Tarjan, R.: Depth-first search and linear graph algorithms. SIAM J. Comput. 1(2), 146–160 (1972)

    Article  MathSciNet  Google Scholar 

  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_36

    Chapter  Google Scholar 

  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_13

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Sorbonne Université, CNRS, LIP6, 75005, Paris, France

    Denis Poitrenaud

  2. Université Paris Descartes, Paris, France

    Denis Poitrenaud

  3. LRDE, EPITA, Kremlin-Bicêtre, France

    Etienne Renault

Authors
  1. Denis Poitrenaud
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Etienne Renault
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Etienne Renault .

Editor information

Editors and Affiliations

  1. IRIT/INPT - ENSEEIHT, Toulouse, France

    Yamine Ait-Ameur

  2. Teesside University, Middlesbrough, UK

    Shengchao Qin

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Poitrenaud, D., Renault, E. (2019). Combining Parallel Emptiness Checks with Partial Order Reductions. In: Ait-Ameur, Y., Qin, S. (eds) Formal Methods and Software Engineering. ICFEM 2019. Lecture Notes in Computer Science(), vol 11852. Springer, Cham. https://doi.org/10.1007/978-3-030-32409-4_23

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-32409-4_23

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-32408-7

  • Online ISBN: 978-3-030-32409-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation