zbMATH — the first resource for mathematics

Improved multi-core nested depth-first search. (English) Zbl 1374.68281
Chakraborty, Supratik (ed.) et al., Automated technology for verification and analysis. 10th international symposium, ATVA 2012, Thiruvananthapuram, India, October 3–6, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-33385-9/pbk). Lecture Notes in Computer Science 7561, 269-283 (2012).
Summary: This paper presents Cndfs, a tight integration of two earlier multi-core nested depth-first search (Ndfs) algorithms for LTL model checking. Cndfs combines the different strengths and avoids some weaknesses of its predecessors. We compare Cndfs to an earlier ad-hoc combination of those two algorithms and show several benefits: It has shorter and simpler code and a simpler correctness proof. It exhibits more robust performance with similar scalability, while at the same time reducing memory requirements.
The algorithm has been implemented in the multi-core backend of the LTSmin model checker, which is now benchmarked for the first time on a 48 core machine (previously 16). The experiments demonstrate better scalability than other parallel LTL model checking algorithms, but we also investigate apparent bottlenecks. Finally, we noticed that the multi-core Ndfs algorithms produce shorter counterexamples, surprisingly often shorter than their BFS-based counterparts.
For the entire collection see [Zbl 1251.68006].

68Q60 Specification and verification (program logics, model checking, etc.)
LTSmin; DiVinE
Full Text: DOI