Abstract
In this article we present the parallelisation of an explicit-state CTL* model checking algorithm for a virtual shared-memory high-performance parallel machine architecture. The algorithm uses a combination of private and shared data structures for implicit and dynamic load balancing with minimal synchronisation overhead. The performance of the algorithm and the impact that different design decisions have on the performance are analysed using both mathematical cost models and experimental results. The analysis shows not only the practicality and effective speedup of the algorithm, but also the main pitfalls of parallelising model checking for shared-memory architectures.
Similar content being viewed by others
Notes
A tree, here, is modelled as a subset of \( \mathbb{N}^*\), where each sequence of \( \mathbb{N}\) uniquely identifies a node of the tree by its pathname.
References
Allmaier SC, Horton G (1997) Parallel shared-memory state-space exploration in stochastic modeling. In: Bilardi G, Ferreira A, Lüling R, Rolim J (eds) Proceedings of the 4th International Symposium on Solving Irregularly Structured Problems in Parallel (IRREGULAR'97), Volume 1253 of Lecture Notes in Computer Science. Springer-Verlag, Paderborn, Germany
Bane MK, Riley GD (2002) Extended overhead analysis for Open MP. Lect Notes Comput Sci 2400:162–166
Barnat J, Brim L, Stříbrnáj (2001) Distributed LTL model-checking in SPIN. In: Proceedings of the 8th International SPIN Workshop on Model Checking of Software, vol 2057 of Lecture Notes in Computer Science, Springer-Verlag, Toronto, Canada
Behrmann G, Hune TS, Vaandrager FW (2000) Distributed timed model checking—how the search order matters. In: Sistla AP, Emerson EA (eds) Proceedings of the 12th international conference on computer aided verification (CAV 2000), Volume 1855 of Lecture Notes in Computer Science. Springer-Verlag, Chicago, Illinois, pp 216–231
Ben-David S, Heyman T, Grumberg O, Schuster A (2000) Scalable distributed on-the-fly symbolic model checking. In: Proceedings of the 3rd International Conference on Formal Methods in Computer-Aided Design (FMCAD'00), vol 1954. Austin, Texas, pp 390–404
Bernholtz O (1995) Model checking for branching time temporal logics. PhD thesis, The Technion, Haifa, Israel
Bollig B, Leucker M, Weber M (2001) Parallel model checking for the alternation free μ-calculus. Lect Notes Comput Sci 2031:543–558
Bollig B, Leucker M, Weber M (2002) Local parallel model checking for the alternation-free mu-calculus. In: Proceedings of the 9th International SPIN Workshop on Model Checking of Software, Lecture Notes in Computer Science. Springer-Verlag, Grenoble, France
Brim L, Černá I, Krcal P, Pelánek R (2001) Distributed LTL model-checking based on negative cycle detection. Lect Notes Comput Sci 2245
Brim L, Crhová J, Yorav K (2002) Using assumptions to distribute CTL model checking. In: Proceedings of the 1st International Workshop on Parallel and Distributed Model Checking (PDMC 2002), vol 68 of Electronic Notes in Theoretical Computer Science. Brno, Czech Republic, pp 80–95
Brim L, Žídková J (2003) Using assumptions to distribute alternation free mu-calculus model checking. In: Brim L, Grumberg O (eds) Proceedings of the 2nd international workshop on parallel and distributed model checking (PDMC 2003), vol 89 of Electronic Notes in Theoretical Computer Science. Elsevier, Boulder, Colorado
Bull JM (1996) A hierarchical classification of overheads in parallel programs. In: Jelly I, Gorton I, Croll P (eds) Proceedings of the 1st IFIP TC10 international workshop on software engineering for parallel and distributed systems. Chapman Hall, pp 208–219
Černá I, Pelánek R (2003) Distributed explicit fair cycle detection. In: Ball T, Rajamani SK (eds) Proceedings of the 10th international SPIN workshop on model checking of software, vol 2648 of Lecture Notes in Computer Science. Springer-Verlag, Portland, Oregon
Dijkstra EW, Feijen WHJ, Gasteren AJM (1983) Derivation of a termination detection algorithm for distributed computations. Inf Process Lett 16:217–219
Garavel H, Mateescu R, Smarandache I (2001) Parallel state space construction for model-checking. In: Proceedings of the 8th International SPIN Workshop on Model Checking of Software, vol 2057 of Lecture Notes in Computer Science. Springer-Verlag, Toronto, Canada
Grumberg O, Heyman T, Schuster A (2001) Distributed symbolic model checking for μ-calculus. In: Berry G, Comon H, Finkel A (eds) Proceedings of the 13th international conference on computer aided verification (CAV 2001), vol 2102 of Lecture Notes in Computer Science. Springer-Verlag, Paris, France, pp 350–363
Heyman T, Geist D, Grumberg O, Schuster A (2000) Achieving scalability in parallel reachability analysis of very large circuits. In: Sistla AP, Emerson EA (eds) Proceedings of the 12th international Conference on computer aided verification (CAV 2000), vol 1855 of Lecture Notes in Computer Science. Springer-Verlag, Chicago, Illinois
Holzmann GJ (2003) The SPIN model checker: Primer and reference m anual. Addison-Wesley
Inggs CP (2004) Parallel Model Checking on Shared-Memory Multiprocessors. PhD thesis, Department of Computer Science, University of Manchester, Manchester
Krčál P (2003) Distributed explicit bounded LTL model checking. In: Brim L, Grumberg O (eds) Proceedings of the 2nd international workshop on parallel and distributed model checking (PDMC 2003), vol 89 of Electronic Notes in Theoretical Computer Science. Elsevier, Boulder, Colorado
Lafuente AL (2002) Simplified distributed LTL model checking by localizing cycles. Report00176, Institut für Informatik, Universität Freiburg
Lerda F, Sisto R (1999) Distributed-memory model checking with SPIN. In: Proceedings of the 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking (SPIN5 and SPIN6), vol. 1680 of Lecture Notes in Computer Science. Trento, Italy (SPIN5) and Toulouse, France (SPIN6). Springer-Verlag
Leucker M, Somla R, Weber M (2003) Parallel model checking for LTL, CTL*, and L μ 2. In: Brim L, Grumberg O (eds.) Proceedings of the 2nd international workshop on parallel and distributed model checking (PDMC 2003) of electronic notes in theoretical computer science vol. 89. Elsevier, Boulder, Colorado
Martin JMR, Huddart Y (2000) Parallel algorithms for deadlock and livelock analysis of concurrent systems. In: Communicating Process Architectures. IOS Press, pp 1–14
Stern U, Dill D (1997) Parallelizing the Murφ verifier. In: Grumberg O (ed) Proceedings of the 9th international conference on computer aided verification (CAV'97), Volume 1254 of lecture notes in Computer Science. Springer-Verlag, Haifa, Israel, pp 256–278
Vardi MY, Wolper P (1986) An automata theoretic approach to automatic program verification. In: Proceedings of the 1st symposium on logic in computer science, pp 322–331
Visser W, Barringer H (2000) Practical CTL model checking: Should SPIN be extended? Software Tools for Technology Transfer 2(4):350–365
Visser WC (1998) Efficient CTL* model checking using games and automata. PhD thesis, University of Manchester, Manchester
Author information
Authors and Affiliations
Corresponding author
Additional information
*This work was fully supported under a Universities UK ORS award, a University of Manchester School of Computer Science Scholarship, and a South African Harry Crossley Bursary.
Rights and permissions
About this article
Cite this article
Inggs, C.P., Barringer, H. CTL* model checking on a shared-memory architecture. Form Method Syst Des 29, 135–155 (2006). https://doi.org/10.1007/s10703-006-0008-z
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10703-006-0008-z