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 contribution

  • 32 Citations

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.
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 Verlag
Pages269-283
Number of pages15
ISBN (Print)978-3-642-33386-6
DOIs
StatePublished - 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

Evangelista, S., Laarman, A., Petrucci, L., & van de Pol, J. C. (2012). Improved Multi-Core Nested Depth-First Search. In S. Ramesh (Ed.), Proceedings of the 10th International Symposium on Automated Technology for Verification and Analysis, ATVA 2012 (pp. 269-283). (Lecture Notes in Computer Science; Vol. 7561). London: Springer Verlag. DOI: 10.1007/978-3-642-33386-6_22
Evangelista, Sami ; Laarman, Alfons ; Petrucci, Laure ; van de Pol, Jan Cornelis. / Improved Multi-Core Nested Depth-First Search. Proceedings of the 10th International Symposium on Automated Technology for Verification and Analysis, ATVA 2012. editor / S. Ramesh. London : Springer Verlag, 2012. pp. 269-283 (Lecture Notes in Computer Science).
@inproceedings{ae49d82f6ea845a8b7ab5da85559f685,
title = "Improved Multi-Core Nested Depth-First Search",
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.",
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",
author = "Sami Evangelista and Alfons Laarman and Laure Petrucci and {van de Pol}, {Jan Cornelis}",
year = "2012",
month = "10",
day = "3",
doi = "10.1007/978-3-642-33386-6_22",
language = "Undefined",
isbn = "978-3-642-33386-6",
series = "Lecture Notes in Computer Science",
publisher = "Springer Verlag",
pages = "269--283",
editor = "S. Ramesh",
booktitle = "Proceedings of the 10th International Symposium on Automated Technology for Verification and Analysis, ATVA 2012",
address = "Germany",

}

Evangelista, S, Laarman, A, Petrucci, L & van de Pol, JC 2012, Improved Multi-Core Nested Depth-First Search. in S Ramesh (ed.), Proceedings of the 10th International Symposium on Automated Technology for Verification and Analysis, ATVA 2012. Lecture Notes in Computer Science, vol. 7561, Springer Verlag, London, pp. 269-283, 10th International Symposium on Automated Technology for Verification and Analysis, ATVA 2012, Thiruvananthapuram, India, 3/10/12. DOI: 10.1007/978-3-642-33386-6_22

Improved Multi-Core Nested Depth-First Search. / Evangelista, Sami; Laarman, Alfons; Petrucci, Laure; van de Pol, Jan Cornelis.

Proceedings of the 10th International Symposium on Automated Technology for Verification and Analysis, ATVA 2012. ed. / S. Ramesh. London : Springer Verlag, 2012. p. 269-283 (Lecture Notes in Computer Science; Vol. 7561).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

T1 - Improved Multi-Core Nested Depth-First Search

AU - Evangelista,Sami

AU - Laarman,Alfons

AU - Petrucci,Laure

AU - van de Pol,Jan Cornelis

PY - 2012/10/3

Y1 - 2012/10/3

N2 - 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.

AB - 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.

KW - METIS-287890

KW - CNDFS

KW - IR-80818

KW - LTL model checking

KW - LTSMIN

KW - Verification

KW - EWI-21967

KW - Multi-Core

KW - liveness properties

KW - paralll

KW - nested depth-first search

KW - FMT-MC: MODEL CHECKING

KW - NDFS

U2 - 10.1007/978-3-642-33386-6_22

DO - 10.1007/978-3-642-33386-6_22

M3 - Conference contribution

SN - 978-3-642-33386-6

T3 - Lecture Notes in Computer Science

SP - 269

EP - 283

BT - Proceedings of the 10th International Symposium on Automated Technology for Verification and Analysis, ATVA 2012

PB - Springer Verlag

CY - London

ER -

Evangelista S, Laarman A, Petrucci L, van de Pol JC. Improved Multi-Core Nested Depth-First Search. In Ramesh S, editor, Proceedings of the 10th International Symposium on Automated Technology for Verification and Analysis, ATVA 2012. London: Springer Verlag. 2012. p. 269-283. (Lecture Notes in Computer Science). Available from, DOI: 10.1007/978-3-642-33386-6_22