Multi-core On-The-Fly Saturation

Tom van Dijk*, Jeroen Meijer, Jaco van de Pol

*Corresponding author for this work

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

2 Citations (Scopus)
17 Downloads (Pure)

Abstract

Saturation is an efficient exploration order for computing the set of reachable states symbolically. Attempts to parallelize saturation have so far resulted in limited speedup. We demonstrate for the first time that on-the-fly symbolic saturation can be successfully parallelized at a large scale. To this end, we implemented saturation in Sylvan’s multi-core decision diagrams used by the LTSmin model checker. We report extensive experiments, measuring the speedup of parallel symbolic saturation on a 48-core machine, and compare it with the speedup of parallel symbolic BFS and chaining. We find that the parallel scalability varies from quite modest to excellent. We also compared the speedup of on-the-fly saturation and saturation for pre-learned transition relations. Finally, we compared our implementation of saturation with the existing sequential implementation based on Meddly. The empirical evaluation uses Petri nets from the model checking contest, but thanks to the architecture of LTSmin, parallel on-the-fly saturation is now available to multiple specification languages. Data or code related to this paper is available at: [34].

Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems
Subtitle of host publication25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings
EditorsLijun Zhang, Tomáš Vojnar
Place of PublicationCham
PublisherSpringer
Pages58-75
Number of pages18
ISBN (Electronic)978-3-030-17465-1
ISBN (Print)978-3-030-17464-4
DOIs
Publication statusPublished - 1 Jan 2019
Event25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 - Charles University, Prague, Czech Republic
Duration: 6 Apr 201911 Apr 2019
Conference number: 25

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume11428
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349
NameTheoretical Computer Science and General Issues
PublisherSpringer

Conference

Conference25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019
Abbreviated titleTACAS 2019
CountryCzech Republic
CityPrague
Period6/04/1911/04/19
Otherheld as part of the 22nd European Joint Conferences on Theory and Practice of Software, ETAPS 2019

Fingerprint Dive into the research topics of 'Multi-core On-The-Fly Saturation'. Together they form a unique fingerprint.

Cite this