Multi-Core Nested Depth-First Search

Alfons Laarman, Romanus Langerak, Jan Cornelis van de Pol, M. Weber, Anton Wijs

Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 23 Citations

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.
LanguageUndefined
Title of host publicationProceedings of the 9th International Symposium on Automated Technology for Verification and Analysis, ATVA 2011
EditorsT. Bultan, P.-A. Hsiung
Place of PublicationLondon
PublisherSpringer Verlag
Pages321-335
Number of pages15
ISBN (Print)978-3-642-24372-1
DOIs
StatePublished - 8 Jul 2011
Event9th International Symposium on Automated Technology for Verification and Analysis, ATVA 2011 - Tapei, Taiwan, Province of China
Duration: 11 Oct 201114 Oct 2011
Conference number: 9

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag
Volume6996

Conference

Conference9th International Symposium on Automated Technology for Verification and Analysis, ATVA 2011
Abbreviated titleATVA
CountryTaiwan, Province of China
CityTapei
Period11/10/1114/10/11

Keywords

  • METIS-277719
  • IR-77725
  • Emptyness Problem
  • Nested DFS
  • Multi-Core
  • EWI-20337
  • Cycle Detection
  • Parallel
  • LTL
  • FMT-MC: MODEL CHECKING
  • Model Checking

Cite this

Laarman, A., Langerak, R., van de Pol, J. C., Weber, M., & Wijs, A. (2011). Multi-Core Nested Depth-First Search. In T. Bultan, & P-A. Hsiung (Eds.), Proceedings of the 9th International Symposium on Automated Technology for Verification and Analysis, ATVA 2011 (pp. 321-335). (Lecture Notes in Computer Science; Vol. 6996). London: Springer Verlag. DOI: 10.1007/978-3-642-24372-1_23
Laarman, Alfons ; Langerak, Romanus ; van de Pol, Jan Cornelis ; Weber, M. ; Wijs, Anton. / Multi-Core Nested Depth-First Search. Proceedings of the 9th International Symposium on Automated Technology for Verification and Analysis, ATVA 2011. editor / T. Bultan ; P.-A. Hsiung. London : Springer Verlag, 2011. pp. 321-335 (Lecture Notes in Computer Science).
@inproceedings{d1142d77986e43359098339b6899d64a,
title = "Multi-Core Nested Depth-First Search",
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.",
keywords = "METIS-277719, IR-77725, Emptyness Problem, Nested DFS, Multi-Core, EWI-20337, Cycle Detection, Parallel, LTL, FMT-MC: MODEL CHECKING, Model Checking",
author = "Alfons Laarman and Romanus Langerak and {van de Pol}, {Jan Cornelis} and M. Weber and Anton Wijs",
year = "2011",
month = "7",
day = "8",
doi = "10.1007/978-3-642-24372-1_23",
language = "Undefined",
isbn = "978-3-642-24372-1",
series = "Lecture Notes in Computer Science",
publisher = "Springer Verlag",
pages = "321--335",
editor = "T. Bultan and P.-A. Hsiung",
booktitle = "Proceedings of the 9th International Symposium on Automated Technology for Verification and Analysis, ATVA 2011",
address = "Germany",

}

Laarman, A, Langerak, R, van de Pol, JC, Weber, M & Wijs, A 2011, Multi-Core Nested Depth-First Search. in T Bultan & P-A Hsiung (eds), Proceedings of the 9th International Symposium on Automated Technology for Verification and Analysis, ATVA 2011. Lecture Notes in Computer Science, vol. 6996, Springer Verlag, London, pp. 321-335, 9th International Symposium on Automated Technology for Verification and Analysis, ATVA 2011, Tapei, Taiwan, Province of China, 11/10/11. DOI: 10.1007/978-3-642-24372-1_23

Multi-Core Nested Depth-First Search. / Laarman, Alfons; Langerak, Romanus; van de Pol, Jan Cornelis; Weber, M.; Wijs, Anton.

Proceedings of the 9th International Symposium on Automated Technology for Verification and Analysis, ATVA 2011. ed. / T. Bultan; P.-A. Hsiung. London : Springer Verlag, 2011. p. 321-335 (Lecture Notes in Computer Science; Vol. 6996).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

T1 - Multi-Core Nested Depth-First Search

AU - Laarman,Alfons

AU - Langerak,Romanus

AU - van de Pol,Jan Cornelis

AU - Weber,M.

AU - Wijs,Anton

PY - 2011/7/8

Y1 - 2011/7/8

N2 - 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.

AB - 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.

KW - METIS-277719

KW - IR-77725

KW - Emptyness Problem

KW - Nested DFS

KW - Multi-Core

KW - EWI-20337

KW - Cycle Detection

KW - Parallel

KW - LTL

KW - FMT-MC: MODEL CHECKING

KW - Model Checking

U2 - 10.1007/978-3-642-24372-1_23

DO - 10.1007/978-3-642-24372-1_23

M3 - Conference contribution

SN - 978-3-642-24372-1

T3 - Lecture Notes in Computer Science

SP - 321

EP - 335

BT - Proceedings of the 9th International Symposium on Automated Technology for Verification and Analysis, ATVA 2011

PB - Springer Verlag

CY - London

ER -

Laarman A, Langerak R, van de Pol JC, Weber M, Wijs A. Multi-Core Nested Depth-First Search. In Bultan T, Hsiung P-A, editors, Proceedings of the 9th International Symposium on Automated Technology for Verification and Analysis, ATVA 2011. London: Springer Verlag. 2011. p. 321-335. (Lecture Notes in Computer Science). Available from, DOI: 10.1007/978-3-642-24372-1_23