Improved Multi-Core Nested Depth-First Search

Sami Evangelista, Alfons Laarman, Laure Petrucci, Jan Cornelis van de Pol

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

    42 Citations (Scopus)
    317 Downloads (Pure)

    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.
    Original languageUndefined
    Title of host publicationProceedings of the 10th International Symposium on Automated Technology for Verification and Analysis, ATVA 2012
    EditorsS. Ramesh
    Place of PublicationLondon
    PublisherSpringer
    Pages269-283
    Number of pages15
    ISBN (Print)978-3-642-33386-6
    DOIs
    Publication statusPublished - 3 Oct 2012
    Event10th International Symposium on Automated Technology for Verification and Analysis, ATVA 2012 - Thiruvananthapuram, India
    Duration: 3 Oct 20126 Oct 2012
    Conference number: 10

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag
    Volume7561

    Conference

    Conference10th International Symposium on Automated Technology for Verification and Analysis, ATVA 2012
    Abbreviated titleATVA
    CountryIndia
    CityThiruvananthapuram
    Period3/10/126/10/12

    Keywords

    • METIS-287890
    • CNDFS
    • IR-80818
    • LTL model checking
    • LTSMIN
    • Verification
    • EWI-21967
    • Multi-Core
    • liveness properties
    • paralll
    • nested depth-first search
    • FMT-MC: MODEL CHECKING
    • NDFS

    Cite this