Abstract
The LTL Model Checking problem is reducible to finding accepting cycles in a graph. The Nested Depth-First Search (Ndfs) algorithm detects accepting cycles efficiently: on-the-fly, with linear-time complexity and negligible memory overhead. The only downside of the algorithm is that it relies on an inherently-sequential, depth-first search. It has not been parallelized beyond running the independent nested search in a separate thread (dual core).
In this paper, we introduce, for the first time, a multi-core Ndfs algorithm that can scale beyond two threads, while maintaining exactly the same worst-case time complexity. We prove this algorithm correct, and present experimental results obtained with an implementation in the LTSmin tool set on the entire Beem benchmark database. We measured considerable speedups compared to the current state of the art in parallel cycle detection algorithms.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press, Cambridge (2008)
Barnat, J., Brim, L., Ročkai, P.: Scalable Shared Memory LTL Model Checking. STTT 12(2), 139–153 (2010)
Barnat, J., Brim, L., Češka, M., Ročkai, P.: DiVinE: Parallel Distributed Model Checker (Tool paper). In: Parallel and Distributed Methods in Verification and High Performance Computational Systems Biology (HiBi/PDMC 2010), pp. 4–7. IEEE, Los Alamitos (2010)
Barnat, J., Brim, L., Ročkai, P.: A Time-Optimal On-The-Fly Parallel Algorithm for Model Checking of Weak LTL Properties. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 407–425. Springer, Heidelberg (2009)
Courcoubetis, C., Vardi, M.Y., Wolper, P., Yannakakis, M.: Memory-Efficient Algorithms for the Verification of Temporal Properties. Formal Methods in System Design 1(2/3), 275–288 (1992)
Dwyer, M.B., Elbaum, S.G., Person, S., Purandare, R.: Parallel Randomized State-Space Search. In: Proc. ICSE 2007, pp. 3–12. IEEE Computer Society Press, Los Alamitos (2007)
Evangelista, S., Petrucci, L., Youcef, S.: Parallel nested depth-first searches for LTL model checking. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 381–396. Springer, Heidelberg (2011)
Foster, I.: Designing and Building Parallel Programs. Addison-Wesley, Reading (1995)
Gaiser, A., Schwoon, S.: Comparison of Algorithms for Checking Emptiness on Büchi Automata. CoRR, abs/0910.3766 (2009)
Geldenhuys, J., Valmari, A.: Tarjan’s Algorithm Makes On-the-Fly LTL Verification More Efficient. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 205–219. Springer, Heidelberg (2004)
Holzmann, G.J., Bošnački, D.: The Design of a Multicore Extension of the SPIN Model Checker. IEEE Trans. On Software Engineering 33(10), 659–674 (2007)
Holzmann, G.J., Bošnački, D.: The Design of a Multicore Extension of the SPIN Model Checker. IEEE Transactions on Software Engineering 33(10), 659–674 (2007)
Holzmann, G.J., Joshi, R., Groce, A.: Swarm Verification. In: Proc. ASE 2008, pp. 1–6. IEEE Computer Society Press, Los Alamitos (2008)
Holzmann, G.J., Joshi, R., Groce, A.: Tackling Large Verification Problems with the Swarm Tool. In: Havelund, K., Majumdar, R. (eds.) SPIN 2008. LNCS, vol. 5156, pp. 134–143. Springer, Heidelberg (2008)
Holzmann, G.J., Peled, D., Yannakakis, M.: On Nested Depth First Search. In: The Spin Verification System, pp. 23–32. American Mathematical Society, Providence (1996)
Laarman, A.W., van de Pol, J.C., Weber, M.: Boosting Multi-Core Reachability Performance with Shared Hash Tables. In: Sharygina, N., Bloem, R. (eds.) Proceedings of the 10th International Conference on Formal Methods in Computer-Aided Design, Lugano, Swiss, USA. IEEE Computer Society, Los Alamitos (2010)
Laarman, A.W., van de Pol, J.C., Weber, M.: Multi-core LTSmin: Marrying modularity and scalability. In: Bobaru, M., Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 506–511. Springer, Heidelberg (2011)
Moore, G.E.: Cramming more Components onto Integrated Circuits. Electronics 38(10), 114–117 (1965)
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)
Reif, J.H.: Depth-first Search is Inherently Sequential. Information Processing Letters 20(5), 229–234 (1985)
Schwoon, S., Esparza, J.: A Note on On-the-Fly Verification Algorithms. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 174–190. Springer, Heidelberg (2005)
Sivaraj, H., Gopalakrishnan, G.: Random Walk Based Heuristic Algorithms for Distributed Memory Model Checking. Electronic Notes in Theoretical Computer Science 89(1), 51–67 (2003)
Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. 1st Symp. on Logic in Computer Science, Cambridge, pp. 332–344 (June 1986)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Laarman, A., Langerak, R., van de Pol, J., Weber, M., Wijs, A. (2011). Multi-core Nested Depth-First Search. In: Bultan, T., Hsiung, PA. (eds) Automated Technology for Verification and Analysis. ATVA 2011. Lecture Notes in Computer Science, vol 6996. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24372-1_23
Download citation
DOI: https://doi.org/10.1007/978-3-642-24372-1_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-24371-4
Online ISBN: 978-3-642-24372-1
eBook Packages: Computer ScienceComputer Science (R0)