Multi-Core Nested Depth-First Search

Share/Save/Bookmark

Laarman, Alfons and Langerak, Rom and Pol, Jaco van de and Weber, Michael and Wijs, Anton (2011) Multi-Core Nested Depth-First Search. In: 9th International Symposium on Automated Technology for Verification and Analysis, ATVA 2011, 11-14 October 2011, Tapei, Taiwan.

[img] PDF
Restricted to UT campus only
: Request a copy
926kB
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.
Item Type:Conference or Workshop Item
Copyright:© 2011 Springer
Faculty:
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/77725
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page