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 contributionAcademicpeer-review

    27 Citations (Scopus)
    164 Downloads (Pure)

    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.
    Original 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
    Pages321-335
    Number of pages15
    ISBN (Print)978-3-642-24372-1
    DOIs
    Publication statusPublished - 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. https://doi.org/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, 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",
    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",

    }

    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, London, pp. 321-335, 9th International Symposium on Automated Technology for Verification and Analysis, ATVA 2011, Tapei, Taiwan, Province of China, 11/10/11. https://doi.org/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, 2011. p. 321-335 (Lecture Notes in Computer Science; Vol. 6996).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    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

    A2 - Bultan, T.

    A2 - Hsiung, P.-A.

    PB - Springer

    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. 2011. p. 321-335. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-642-24372-1_23