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

Alfons Laarman, David Faragó

  • 4 Citations

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
StatePublished - 2013
Event5th International Symposium on NASA Formal Methods, NFM 2013 - Moffett Field, United States

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. DOI: 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. ed. / Guillaume Brat; Neha Rungta; Arnaud Venet. Springer, 2013. p. 32-47 (Lecture Notes in Computer Science; Vol. 7871).

Research output: Scientific - peer-reviewConference contribution

@inbook{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ó 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ó",
year = "2013",
doi = "10.1007/978-3-642-38088-4_3",
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-16 May. DOI: 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: Scientific - peer-reviewConference contribution

TY - CHAP

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

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). Available from, DOI: 10.1007/978-3-642-38088-4_3