Multi-Core BDD Operations for Symbolic Reachability

Tom van Dijk, Alfons Laarman, Jan Cornelis van de Pol

  • 9 Citations

Abstract

This paper presents scalable parallel BDD operations for modern multi-core hardware. We aim at increasing the performance of reachability analysis in the context of model checking. Existing approaches focus on performing multiple independent BDD operations rather than parallelizing the BDD operations themselves. In the past, attempts at parallelizing BDD operations have been unsuccessful due to communication costs in shared memory. We solved this problem by extending an existing lockless hashtable to support BDDs and garbage collection and by implementing a lockless memoization table. Using these lockless hashtables and the work-stealing framework Wool, we implemented a multi-core BDD package called Sylvan. We provide the experimental results of using this multi-core BDD package in the framework of the model checker LTSmin. We measured the runtime of the reachability algorithm on several models from the BEEM model database on a 48-core machine, demonstrating speedups of over 30 for some models, which is a breakthrough compared to earlier work. In addition, we improved the standard symbolic reachability algorithm to use a modified BDD operation that calculates the relational product and the variable substitution in one step. We show that this new algorithm improves the performance of symbolic reachability and decreases the memory requirements by up to 40%.
Original languageUndefined
Title of host publication11th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2012
EditorsK. Heljanko, W.J. Knottenbelt
Place of PublicationAmsterdam
PublisherELSEVIER
Pages127-143
Number of pages18
DOIs
StatePublished - 17 Sep 2012
Event11th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2012 - London, United Kingdom

Publication series

NameElectronic Notes in Theoretical Computer Science
PublisherElsevier
Volume296
ISSN (Print)2075-2180
ISSN (Electronic)2075-2180

Workshop

Workshop11th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2012
Abbreviated titlePDMC
CountryUnited Kingdom
CityLondon
Period17/09/1217/09/12
Internet address

Fingerprint

Model checking
Wool
Substitution reactions
Hardware
Communication
Costs

Keywords

  • METIS-289673
  • EWI-22166
  • Decision diagram
  • BDD
  • IR-82124
  • Sylvan
  • Symbolic reachability
  • garbage collection
  • LTSMIN
  • Wool
  • memoization table
  • lockless hashtable
  • lossy hashtable
  • parallel model checking
  • FMT-BDD: BINARY DECISION DIAGRAMS
  • Multi-Core

Cite this

van Dijk, T., Laarman, A., & van de Pol, J. C. (2012). Multi-Core BDD Operations for Symbolic Reachability. In K. Heljanko, & W. J. Knottenbelt (Eds.), 11th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2012 (pp. 127-143). (Electronic Notes in Theoretical Computer Science; Vol. 296). Amsterdam: ELSEVIER. DOI: 10.1016/j.entcs.2013.07.009

van Dijk, Tom; Laarman, Alfons; van de Pol, Jan Cornelis / Multi-Core BDD Operations for Symbolic Reachability.

11th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2012. ed. / K. Heljanko; W.J. Knottenbelt. Amsterdam : ELSEVIER, 2012. p. 127-143 (Electronic Notes in Theoretical Computer Science; Vol. 296).

Research output: Scientific - peer-reviewConference contribution

@inbook{4810091a0b054c6eb496040eb79e51a8,
title = "Multi-Core BDD Operations for Symbolic Reachability",
abstract = "This paper presents scalable parallel BDD operations for modern multi-core hardware. We aim at increasing the performance of reachability analysis in the context of model checking. Existing approaches focus on performing multiple independent BDD operations rather than parallelizing the BDD operations themselves. In the past, attempts at parallelizing BDD operations have been unsuccessful due to communication costs in shared memory. We solved this problem by extending an existing lockless hashtable to support BDDs and garbage collection and by implementing a lockless memoization table. Using these lockless hashtables and the work-stealing framework Wool, we implemented a multi-core BDD package called Sylvan. We provide the experimental results of using this multi-core BDD package in the framework of the model checker LTSmin. We measured the runtime of the reachability algorithm on several models from the BEEM model database on a 48-core machine, demonstrating speedups of over 30 for some models, which is a breakthrough compared to earlier work. In addition, we improved the standard symbolic reachability algorithm to use a modified BDD operation that calculates the relational product and the variable substitution in one step. We show that this new algorithm improves the performance of symbolic reachability and decreases the memory requirements by up to 40%.",
keywords = "METIS-289673, EWI-22166, Decision diagram, BDD, IR-82124, Sylvan, Symbolic reachability, garbage collection, LTSMIN, Wool, memoization table, lockless hashtable, lossy hashtable, parallel model checking, FMT-BDD: BINARY DECISION DIAGRAMS, Multi-Core",
author = "{van Dijk}, Tom and Alfons Laarman and {van de Pol}, {Jan Cornelis}",
year = "2012",
month = "9",
doi = "10.1016/j.entcs.2013.07.009",
series = "Electronic Notes in Theoretical Computer Science",
publisher = "ELSEVIER",
pages = "127--143",
editor = "K. Heljanko and W.J. Knottenbelt",
booktitle = "11th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2012",

}

van Dijk, T, Laarman, A & van de Pol, JC 2012, Multi-Core BDD Operations for Symbolic Reachability. in K Heljanko & WJ Knottenbelt (eds), 11th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2012. Electronic Notes in Theoretical Computer Science, vol. 296, ELSEVIER, Amsterdam, pp. 127-143, 11th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2012, London, United Kingdom, 17-17 September. DOI: 10.1016/j.entcs.2013.07.009

Multi-Core BDD Operations for Symbolic Reachability. / van Dijk, Tom; Laarman, Alfons; van de Pol, Jan Cornelis.

11th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2012. ed. / K. Heljanko; W.J. Knottenbelt. Amsterdam : ELSEVIER, 2012. p. 127-143 (Electronic Notes in Theoretical Computer Science; Vol. 296).

Research output: Scientific - peer-reviewConference contribution

TY - CHAP

T1 - Multi-Core BDD Operations for Symbolic Reachability

AU - van Dijk,Tom

AU - Laarman,Alfons

AU - van de Pol,Jan Cornelis

PY - 2012/9/17

Y1 - 2012/9/17

N2 - This paper presents scalable parallel BDD operations for modern multi-core hardware. We aim at increasing the performance of reachability analysis in the context of model checking. Existing approaches focus on performing multiple independent BDD operations rather than parallelizing the BDD operations themselves. In the past, attempts at parallelizing BDD operations have been unsuccessful due to communication costs in shared memory. We solved this problem by extending an existing lockless hashtable to support BDDs and garbage collection and by implementing a lockless memoization table. Using these lockless hashtables and the work-stealing framework Wool, we implemented a multi-core BDD package called Sylvan. We provide the experimental results of using this multi-core BDD package in the framework of the model checker LTSmin. We measured the runtime of the reachability algorithm on several models from the BEEM model database on a 48-core machine, demonstrating speedups of over 30 for some models, which is a breakthrough compared to earlier work. In addition, we improved the standard symbolic reachability algorithm to use a modified BDD operation that calculates the relational product and the variable substitution in one step. We show that this new algorithm improves the performance of symbolic reachability and decreases the memory requirements by up to 40%.

AB - This paper presents scalable parallel BDD operations for modern multi-core hardware. We aim at increasing the performance of reachability analysis in the context of model checking. Existing approaches focus on performing multiple independent BDD operations rather than parallelizing the BDD operations themselves. In the past, attempts at parallelizing BDD operations have been unsuccessful due to communication costs in shared memory. We solved this problem by extending an existing lockless hashtable to support BDDs and garbage collection and by implementing a lockless memoization table. Using these lockless hashtables and the work-stealing framework Wool, we implemented a multi-core BDD package called Sylvan. We provide the experimental results of using this multi-core BDD package in the framework of the model checker LTSmin. We measured the runtime of the reachability algorithm on several models from the BEEM model database on a 48-core machine, demonstrating speedups of over 30 for some models, which is a breakthrough compared to earlier work. In addition, we improved the standard symbolic reachability algorithm to use a modified BDD operation that calculates the relational product and the variable substitution in one step. We show that this new algorithm improves the performance of symbolic reachability and decreases the memory requirements by up to 40%.

KW - METIS-289673

KW - EWI-22166

KW - Decision diagram

KW - BDD

KW - IR-82124

KW - Sylvan

KW - Symbolic reachability

KW - garbage collection

KW - LTSMIN

KW - Wool

KW - memoization table

KW - lockless hashtable

KW - lossy hashtable

KW - parallel model checking

KW - FMT-BDD: BINARY DECISION DIAGRAMS

KW - Multi-Core

U2 - 10.1016/j.entcs.2013.07.009

DO - 10.1016/j.entcs.2013.07.009

M3 - Conference contribution

T3 - Electronic Notes in Theoretical Computer Science

SP - 127

EP - 143

BT - 11th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2012

PB - ELSEVIER

ER -

van Dijk T, Laarman A, van de Pol JC. Multi-Core BDD Operations for Symbolic Reachability. In Heljanko K, Knottenbelt WJ, editors, 11th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2012. Amsterdam: ELSEVIER. 2012. p. 127-143. (Electronic Notes in Theoretical Computer Science). Available from, DOI: 10.1016/j.entcs.2013.07.009