Improved On-The-Fly Livelock Detection: Combining Partial Order Reduction and Parallelism for DFSFIFO

Alfons Laarman, David Faragó

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

    7 Citations (Scopus)
    22 Downloads (Pure)

    Abstract

    Until recently, the preferred method of livelock detection was via LTL model checking, which imposes complex constraints on partial order reduction (POR), limiting its performance and parallelization. The introduction of the DFS_FIFO algorithm by Faragó et al. showed that livelocks can theoretically be detected faster, simpler, and with stronger POR. For the first time, we implement DFS_FIFO and compare it to the LTL approach by experiments on four established case studies. They show the improvements over the LTL approach: DFS_FIFO is up to 3.2 times faster, and it makes POR up to 5 times better than with SPIN's NDFS. Additionally, we propose a parallel version of DFS_FIFO, which demonstrates the efficient combination of parallelization and POR. We prove parallel DFS_FIFO correct and show why it provides stronger guarantees on parallel scalability and POR compared to LTL-based methods. Experimentally, we establish almost ideal linear parallel scalability and POR close to the POR for safety checks: easily an order of magnitude better than for LTL.
    Original languageEnglish
    Title of host publicationNASA Formal Methods
    Subtitle of host publication5th International Symposium, NFM 2013, Moffett Field, CA, USA, May 14-16, 2013. Proceedings
    EditorsGuillaume Brat, Neha Rungta, Arnaud Venet
    PublisherSpringer
    Pages32-47
    Number of pages15
    ISBN (Electronic)978-3-642-38088-4
    ISBN (Print)978-3-642-38087-7
    DOIs
    Publication statusPublished - 2013
    Event5th International Symposium on NASA Formal Methods, NFM 2013 - Moffett Field, United States
    Duration: 14 May 201316 May 2013
    Conference number: 5

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag
    Volume7871
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    Conference5th International Symposium on NASA Formal Methods, NFM 2013
    Abbreviated titleNFM
    CountryUnited States
    CityMoffett Field
    Period14/05/1316/05/13

    Fingerprint

    Scalability
    Model checking
    Experiments

    Keywords

    • EWI-23159
    • METIS-296352
    • tree compression
    • Partial order reduction
    • nested depth-first search
    • Parallel
    • LTL model checking
    • LTSMIN
    • Stubborn set
    • livelocks
    • liveness
    • DiVinE
    • Multi-Core
    • Promela
    • SPIN
    • IR-84628
    • DVE
    • DFS_FIFO
    • Model Checking
    • collapse compression

    Cite this

    Laarman, A., & Faragó, D. (2013). Improved On-The-Fly Livelock Detection: Combining Partial Order Reduction and Parallelism for DFSFIFO. In G. Brat, N. Rungta, & A. Venet (Eds.), NASA Formal Methods: 5th International Symposium, NFM 2013, Moffett Field, CA, USA, May 14-16, 2013. Proceedings (pp. 32-47). (Lecture Notes in Computer Science; Vol. 7871). Springer. https://doi.org/10.1007/978-3-642-38088-4_3
    Laarman, Alfons ; Faragó, David. / Improved On-The-Fly Livelock Detection : Combining Partial Order Reduction and Parallelism for DFSFIFO. NASA Formal Methods: 5th International Symposium, NFM 2013, Moffett Field, CA, USA, May 14-16, 2013. Proceedings. editor / Guillaume Brat ; Neha Rungta ; Arnaud Venet. Springer, 2013. pp. 32-47 (Lecture Notes in Computer Science).
    @inproceedings{eaef7e9dffac464eb0cfce74614b49dc,
    title = "Improved On-The-Fly Livelock Detection: Combining Partial Order Reduction and Parallelism for DFSFIFO",
    abstract = "Until recently, the preferred method of livelock detection was via LTL model checking, which imposes complex constraints on partial order reduction (POR), limiting its performance and parallelization. The introduction of the DFS_FIFO algorithm by Farag{\'o} et al. showed that livelocks can theoretically be detected faster, simpler, and with stronger POR. For the first time, we implement DFS_FIFO and compare it to the LTL approach by experiments on four established case studies. They show the improvements over the LTL approach: DFS_FIFO is up to 3.2 times faster, and it makes POR up to 5 times better than with SPIN's NDFS. Additionally, we propose a parallel version of DFS_FIFO, which demonstrates the efficient combination of parallelization and POR. We prove parallel DFS_FIFO correct and show why it provides stronger guarantees on parallel scalability and POR compared to LTL-based methods. Experimentally, we establish almost ideal linear parallel scalability and POR close to the POR for safety checks: easily an order of magnitude better than for LTL.",
    keywords = "EWI-23159, METIS-296352, tree compression, Partial order reduction, nested depth-first search, Parallel, LTL model checking, LTSMIN, Stubborn set, livelocks, liveness, DiVinE, Multi-Core, Promela, SPIN, IR-84628, DVE, DFS_FIFO, Model Checking, collapse compression",
    author = "Alfons Laarman and David Farag{\'o}",
    year = "2013",
    doi = "10.1007/978-3-642-38088-4_3",
    language = "English",
    isbn = "978-3-642-38087-7",
    series = "Lecture Notes in Computer Science",
    publisher = "Springer",
    pages = "32--47",
    editor = "Guillaume Brat and Neha Rungta and Arnaud Venet",
    booktitle = "NASA Formal Methods",

    }

    Laarman, A & Faragó, D 2013, Improved On-The-Fly Livelock Detection: Combining Partial Order Reduction and Parallelism for DFSFIFO. in G Brat, N Rungta & A Venet (eds), NASA Formal Methods: 5th International Symposium, NFM 2013, Moffett Field, CA, USA, May 14-16, 2013. Proceedings. Lecture Notes in Computer Science, vol. 7871, Springer, pp. 32-47, 5th International Symposium on NASA Formal Methods, NFM 2013, Moffett Field, United States, 14/05/13. https://doi.org/10.1007/978-3-642-38088-4_3

    Improved On-The-Fly Livelock Detection : Combining Partial Order Reduction and Parallelism for DFSFIFO. / Laarman, Alfons; Faragó, David.

    NASA Formal Methods: 5th International Symposium, NFM 2013, Moffett Field, CA, USA, May 14-16, 2013. Proceedings. ed. / Guillaume Brat; Neha Rungta; Arnaud Venet. Springer, 2013. p. 32-47 (Lecture Notes in Computer Science; Vol. 7871).

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

    TY - GEN

    T1 - Improved On-The-Fly Livelock Detection

    T2 - Combining Partial Order Reduction and Parallelism for DFSFIFO

    AU - Laarman, Alfons

    AU - Faragó, David

    PY - 2013

    Y1 - 2013

    N2 - Until recently, the preferred method of livelock detection was via LTL model checking, which imposes complex constraints on partial order reduction (POR), limiting its performance and parallelization. The introduction of the DFS_FIFO algorithm by Faragó et al. showed that livelocks can theoretically be detected faster, simpler, and with stronger POR. For the first time, we implement DFS_FIFO and compare it to the LTL approach by experiments on four established case studies. They show the improvements over the LTL approach: DFS_FIFO is up to 3.2 times faster, and it makes POR up to 5 times better than with SPIN's NDFS. Additionally, we propose a parallel version of DFS_FIFO, which demonstrates the efficient combination of parallelization and POR. We prove parallel DFS_FIFO correct and show why it provides stronger guarantees on parallel scalability and POR compared to LTL-based methods. Experimentally, we establish almost ideal linear parallel scalability and POR close to the POR for safety checks: easily an order of magnitude better than for LTL.

    AB - Until recently, the preferred method of livelock detection was via LTL model checking, which imposes complex constraints on partial order reduction (POR), limiting its performance and parallelization. The introduction of the DFS_FIFO algorithm by Faragó et al. showed that livelocks can theoretically be detected faster, simpler, and with stronger POR. For the first time, we implement DFS_FIFO and compare it to the LTL approach by experiments on four established case studies. They show the improvements over the LTL approach: DFS_FIFO is up to 3.2 times faster, and it makes POR up to 5 times better than with SPIN's NDFS. Additionally, we propose a parallel version of DFS_FIFO, which demonstrates the efficient combination of parallelization and POR. We prove parallel DFS_FIFO correct and show why it provides stronger guarantees on parallel scalability and POR compared to LTL-based methods. Experimentally, we establish almost ideal linear parallel scalability and POR close to the POR for safety checks: easily an order of magnitude better than for LTL.

    KW - EWI-23159

    KW - METIS-296352

    KW - tree compression

    KW - Partial order reduction

    KW - nested depth-first search

    KW - Parallel

    KW - LTL model checking

    KW - LTSMIN

    KW - Stubborn set

    KW - livelocks

    KW - liveness

    KW - DiVinE

    KW - Multi-Core

    KW - Promela

    KW - SPIN

    KW - IR-84628

    KW - DVE

    KW - DFS_FIFO

    KW - Model Checking

    KW - collapse compression

    U2 - 10.1007/978-3-642-38088-4_3

    DO - 10.1007/978-3-642-38088-4_3

    M3 - Conference contribution

    SN - 978-3-642-38087-7

    T3 - Lecture Notes in Computer Science

    SP - 32

    EP - 47

    BT - NASA Formal Methods

    A2 - Brat, Guillaume

    A2 - Rungta, Neha

    A2 - Venet, Arnaud

    PB - Springer

    ER -

    Laarman A, Faragó D. Improved On-The-Fly Livelock Detection: Combining Partial Order Reduction and Parallelism for DFSFIFO. In Brat G, Rungta N, Venet A, editors, NASA Formal Methods: 5th International Symposium, NFM 2013, Moffett Field, CA, USA, May 14-16, 2013. Proceedings. Springer. 2013. p. 32-47. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-642-38088-4_3