Improved Multi-Core Nested Depth-First Search

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

doi:10.1007/978-3-642-33386-6_22

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 proceeding › Conference contribution › Academic › peer-review

43 Citations (Scopus)

387 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 language	Undefined
Title of host publication	Proceedings of the 10th International Symposium on Automated Technology for Verification and Analysis, ATVA 2012
Editors	S. Ramesh
Place of Publication	London
Publisher	Springer
Pages	269-283
Number of pages	15
ISBN (Print)	978-3-642-33386-6
DOIs	https://doi.org/10.1007/978-3-642-33386-6_22
Publication status	Published - 3 Oct 2012
Event	10th International Symposium on Automated Technology for Verification and Analysis, ATVA 2012 - Thiruvananthapuram, India Duration: 3 Oct 2012 → 6 Oct 2012 Conference number: 10

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Verlag
Volume	7561

Conference

Conference	10th International Symposium on Automated Technology for Verification and Analysis, ATVA 2012
Abbreviated title	ATVA
Country/Territory	India
City	Thiruvananthapuram
Period	3/10/12 → 6/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

Access to Document

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

Cite this

@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 = oct,

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",

pages = "269--283",

editor = "S. Ramesh",

booktitle = "Proceedings of the 10th International Symposium on Automated Technology for Verification and Analysis, ATVA 2012",

address = "Netherlands",

note = "null ; Conference date: 03-10-2012 Through 06-10-2012",

}

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, London, pp. 269-283, 10th International Symposium on Automated Technology for Verification and Analysis, ATVA 2012, Thiruvananthapuram, India, 3/10/12. https://doi.org/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, 2012. p. 269-283 (Lecture Notes in Computer Science; Vol. 7561).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

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

N1 - Conference code: 10

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

A2 - Ramesh, S.

PB - Springer

CY - London

Y2 - 3 October 2012 through 6 October 2012

ER -