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

Alfons Laarman, David Faragó

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 languageUndefined
Title of host publicationProceedings of the Fifth NASA Formal Methods Symposium, NFM 2013
EditorsG.P. Brat, N. Rungta, A.J. Venet
Place of PublicationLondon
PublisherSpringer
Pages-
Number of pages15
StateAccepted/In press - 14 May 2013

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag

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. P. Brat, N. Rungta, & A. J. Venet (Eds.), Proceedings of the Fifth NASA Formal Methods Symposium, NFM 2013 (pp. -). (Lecture Notes in Computer Science). London: Springer.

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

Proceedings of the Fifth NASA Formal Methods Symposium, NFM 2013. ed. / G.P. Brat; N. Rungta; A.J. Venet. London : Springer, 2013. p. - (Lecture Notes in Computer Science).

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",
month = "5",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "--",
editor = "G.P. Brat and N. Rungta and A.J. Venet",
booktitle = "Proceedings of the Fifth NASA Formal Methods Symposium, NFM 2013",

}

Laarman, A & Faragó, D 2013, Improved On-The-Fly Livelock Detection: Combining Partial Order Reduction and Parallelism for DFSFIFO. in GP Brat, N Rungta & AJ Venet (eds), Proceedings of the Fifth NASA Formal Methods Symposium, NFM 2013. Lecture Notes in Computer Science, Springer, London, pp. -.

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

Proceedings of the Fifth NASA Formal Methods Symposium, NFM 2013. ed. / G.P. Brat; N. Rungta; A.J. Venet. London : Springer, 2013. p. - (Lecture Notes in Computer Science).

Research output: Scientific - peer-reviewConference contribution

TY - CHAP

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

AU - Laarman,Alfons

AU - Faragó,David

PY - 2013/5/14

Y1 - 2013/5/14

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

M3 - Conference contribution

T3 - Lecture Notes in Computer Science

SP - -

BT - Proceedings of the Fifth NASA Formal Methods Symposium, NFM 2013

PB - Springer

ER -

Laarman A, Faragó D. Improved On-The-Fly Livelock Detection: Combining Partial Order Reduction and Parallelism for DFSFIFO. In Brat GP, Rungta N, Venet AJ, editors, Proceedings of the Fifth NASA Formal Methods Symposium, NFM 2013. London: Springer. 2013. p. -. (Lecture Notes in Computer Science).