| Title | Improved Multi-Core Nested Depth-First Search |
|---|---|
| Author | Evangelista, Sami; Laarman, Alfons; Petrucci, Laure; Pol, van de Jaco |
| Editor | Ramesh, S. |
| Date | 2012-10-03 |
| Type | conference object |
| Publisher | Springer Verlag |
| Abstract | 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 stable performance and 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. |
| Publication | http://purl.utwente.nl/publications/80818 |
| Persistent Identifier | URN:NBN:NL:UI:28-80818 |
| Metadata | XML |
| Repository | University of Twente |
Go to page top
Go back to contents
Go back to site navigation