Improved Multi-Core Nested Depth-First Search (2012)

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.
Persistent Identifier URN:NBN:NL:UI:28-80818
Metadata XML
Source University of Twente

Go to page top
Go back to contents
Go back to site navigation