Sylvan: Multi-core Decision Diagrams

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

    18 Citations (Scopus)
    291 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