Sylvan: Multi-core Decision Diagrams

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

14 Citations (Scopus)
177 Downloads (Pure)

Abstract

Decision diagrams such as binary decision diagrams and multi-valued decision diagrams play an important role in various fields, including symbolic model checking. An ongoing challenge is to develop datastructures and algorithms for modern multi-core architectures. The BDD package Sylvan provides one contribution by implementing parallelized BDD operations and thus allowing sequential algorithms to exploit the power of multi-core machines. We present several extensions to Sylvan. We implement parallel operations on list decision diagrams, a variant of multi-valued decision diagrams that is useful for symbolic model checking. We also substitute several core components of Sylvan by new designs, such as the work-stealing framework, the unique table and the operation cache. Furthermore, we combine parallel operations with parallelization on a higher level, by partitioning the transition relation. We show that this results in an improved speedup using the model checking toolset ltsmin. We also demonstrate that the parallelization of symbolic model checking for explicit-state modeling languages with an on-the-fly next-state function, as supported by ltsmin, scales well.
Original languageUndefined
Title of host publicationProceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2015
Place of PublicationLondon
PublisherSpringer
Pages677-691
Number of pages15
ISBN (Print)978-3-662-46680-3
DOIs
Publication statusPublished - Apr 2015

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag
Volume9035
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Keywords

  • EWI-26445
  • METIS-315021
  • IR-98404

Cite this

van Dijk, T., & van de Pol, J. C. (2015). Sylvan: Multi-core Decision Diagrams. In Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2015 (pp. 677-691). (Lecture Notes in Computer Science; Vol. 9035). London: Springer. https://doi.org/10.1007/978-3-662-46681-0_60
van Dijk, Tom ; van de Pol, Jan Cornelis. / Sylvan: Multi-core Decision Diagrams. Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2015. London : Springer, 2015. pp. 677-691 (Lecture Notes in Computer Science).
@inproceedings{11cc5969dd5f49439fa2a955756ba0f9,
title = "Sylvan: Multi-core Decision Diagrams",
abstract = "Decision diagrams such as binary decision diagrams and multi-valued decision diagrams play an important role in various fields, including symbolic model checking. An ongoing challenge is to develop datastructures and algorithms for modern multi-core architectures. The BDD package Sylvan provides one contribution by implementing parallelized BDD operations and thus allowing sequential algorithms to exploit the power of multi-core machines. We present several extensions to Sylvan. We implement parallel operations on list decision diagrams, a variant of multi-valued decision diagrams that is useful for symbolic model checking. We also substitute several core components of Sylvan by new designs, such as the work-stealing framework, the unique table and the operation cache. Furthermore, we combine parallel operations with parallelization on a higher level, by partitioning the transition relation. We show that this results in an improved speedup using the model checking toolset ltsmin. We also demonstrate that the parallelization of symbolic model checking for explicit-state modeling languages with an on-the-fly next-state function, as supported by ltsmin, scales well.",
keywords = "EWI-26445, METIS-315021, IR-98404",
author = "{van Dijk}, Tom and {van de Pol}, {Jan Cornelis}",
note = "10.1007/978-3-662-46681-0_60",
year = "2015",
month = "4",
doi = "10.1007/978-3-662-46681-0_60",
language = "Undefined",
isbn = "978-3-662-46680-3",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "677--691",
booktitle = "Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2015",

}

van Dijk, T & van de Pol, JC 2015, Sylvan: Multi-core Decision Diagrams. in Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2015. Lecture Notes in Computer Science, vol. 9035, Springer, London, pp. 677-691. https://doi.org/10.1007/978-3-662-46681-0_60

Sylvan: Multi-core Decision Diagrams. / van Dijk, Tom; van de Pol, Jan Cornelis.

Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2015. London : Springer, 2015. p. 677-691 (Lecture Notes in Computer Science; Vol. 9035).

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

TY - GEN

T1 - Sylvan: Multi-core Decision Diagrams

AU - van Dijk, Tom

AU - van de Pol, Jan Cornelis

N1 - 10.1007/978-3-662-46681-0_60

PY - 2015/4

Y1 - 2015/4

N2 - Decision diagrams such as binary decision diagrams and multi-valued decision diagrams play an important role in various fields, including symbolic model checking. An ongoing challenge is to develop datastructures and algorithms for modern multi-core architectures. The BDD package Sylvan provides one contribution by implementing parallelized BDD operations and thus allowing sequential algorithms to exploit the power of multi-core machines. We present several extensions to Sylvan. We implement parallel operations on list decision diagrams, a variant of multi-valued decision diagrams that is useful for symbolic model checking. We also substitute several core components of Sylvan by new designs, such as the work-stealing framework, the unique table and the operation cache. Furthermore, we combine parallel operations with parallelization on a higher level, by partitioning the transition relation. We show that this results in an improved speedup using the model checking toolset ltsmin. We also demonstrate that the parallelization of symbolic model checking for explicit-state modeling languages with an on-the-fly next-state function, as supported by ltsmin, scales well.

AB - Decision diagrams such as binary decision diagrams and multi-valued decision diagrams play an important role in various fields, including symbolic model checking. An ongoing challenge is to develop datastructures and algorithms for modern multi-core architectures. The BDD package Sylvan provides one contribution by implementing parallelized BDD operations and thus allowing sequential algorithms to exploit the power of multi-core machines. We present several extensions to Sylvan. We implement parallel operations on list decision diagrams, a variant of multi-valued decision diagrams that is useful for symbolic model checking. We also substitute several core components of Sylvan by new designs, such as the work-stealing framework, the unique table and the operation cache. Furthermore, we combine parallel operations with parallelization on a higher level, by partitioning the transition relation. We show that this results in an improved speedup using the model checking toolset ltsmin. We also demonstrate that the parallelization of symbolic model checking for explicit-state modeling languages with an on-the-fly next-state function, as supported by ltsmin, scales well.

KW - EWI-26445

KW - METIS-315021

KW - IR-98404

U2 - 10.1007/978-3-662-46681-0_60

DO - 10.1007/978-3-662-46681-0_60

M3 - Conference contribution

SN - 978-3-662-46680-3

T3 - Lecture Notes in Computer Science

SP - 677

EP - 691

BT - Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2015

PB - Springer

CY - London

ER -

van Dijk T, van de Pol JC. Sylvan: Multi-core Decision Diagrams. In Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2015. London: Springer. 2015. p. 677-691. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-662-46681-0_60