Sylvan: multi-core framework for decision diagrams

    Research output: Contribution to journalArticleAcademicpeer-review

    11 Citations (Scopus)
    24 Downloads (Pure)

    Abstract

    Decision diagrams, such as binary decision diagrams, multi-terminal binary decision diagrams and multi-valued decision diagrams, play an important role in various fields. They are especially useful to represent the characteristic function of sets of states and transitions in symbolic model checking. Most implementations of decision diagrams do not parallelize the decision diagram operations. As performance gains in the current era now mostly come from parallel processing, an ongoing challenge is to develop datastructures and algorithms for modern multi-core architectures. The decision diagram package Sylvan provides a contribution by implementing parallelized decision diagram operations and thus allowing sequential algorithms that use decision diagrams to exploit the power of multi-core machines. This paper discusses the design and implementation of Sylvan, especially an improvement to the lock-free unique table that uses bit arrays, the concurrent operation cache and the implementation of parallel garbage collection. We extend Sylvan with multi-terminal binary decision diagrams for integers, real numbers and rational numbers. This extension also allows for custom MTBDD leaves and operations and we provide an example implementation of GMP rational numbers.
    Furthermore, we show how the provided framework can be integrated in existing tools to provide out-of-the-box parallel BDD algorithms, as well as support for the parallelization of higher-level algorithms. As a case study, we parallelize on- the-fly symbolic reachability in the model checking toolset LTSmin. We experimentally demonstrate that the parallelization of symbolic model checking for explicit-state modeling languages, as supported by LTSmin, scales well. We also show that improvements in the design of the unique table result in faster execution of on-the-fly symbolic reachability.
    Original languageEnglish
    Pages (from-to)675-696
    Number of pages22
    JournalInternational journal on software tools for technology transfer
    Volume19
    Issue number6
    DOIs
    Publication statusPublished - Nov 2017

    Fingerprint

    Binary decision diagrams
    Model checking
    Parallel algorithms
    Processing

    Keywords

    • Multi-core
    • Parallel
    • Binary decision diagrams
    • Multi-terminal binary decision diagrams
    • Multi-valued decision diagrams
    • Symbolic model checking

    Cite this

    @article{5a62d54ba09f406f9e35bb9b09a1a799,
    title = "Sylvan: multi-core framework for decision diagrams",
    abstract = "Decision diagrams, such as binary decision diagrams, multi-terminal binary decision diagrams and multi-valued decision diagrams, play an important role in various fields. They are especially useful to represent the characteristic function of sets of states and transitions in symbolic model checking. Most implementations of decision diagrams do not parallelize the decision diagram operations. As performance gains in the current era now mostly come from parallel processing, an ongoing challenge is to develop datastructures and algorithms for modern multi-core architectures. The decision diagram package Sylvan provides a contribution by implementing parallelized decision diagram operations and thus allowing sequential algorithms that use decision diagrams to exploit the power of multi-core machines. This paper discusses the design and implementation of Sylvan, especially an improvement to the lock-free unique table that uses bit arrays, the concurrent operation cache and the implementation of parallel garbage collection. We extend Sylvan with multi-terminal binary decision diagrams for integers, real numbers and rational numbers. This extension also allows for custom MTBDD leaves and operations and we provide an example implementation of GMP rational numbers.Furthermore, we show how the provided framework can be integrated in existing tools to provide out-of-the-box parallel BDD algorithms, as well as support for the parallelization of higher-level algorithms. As a case study, we parallelize on- the-fly symbolic reachability in the model checking toolset LTSmin. We experimentally demonstrate that the parallelization of symbolic model checking for explicit-state modeling languages, as supported by LTSmin, scales well. We also show that improvements in the design of the unique table result in faster execution of on-the-fly symbolic reachability.",
    keywords = "Multi-core, Parallel, Binary decision diagrams, Multi-terminal binary decision diagrams , Multi-valued decision diagrams, Symbolic model checking",
    author = "{van Dijk}, Tom and {van de Pol}, Jaco",
    year = "2017",
    month = "11",
    doi = "10.1007/s10009-016-0433-2",
    language = "English",
    volume = "19",
    pages = "675--696",
    journal = "International journal on software tools for technology transfer",
    issn = "1433-2779",
    publisher = "Springer",
    number = "6",

    }

    Sylvan: multi-core framework for decision diagrams. / van Dijk, Tom; van de Pol, Jaco.

    In: International journal on software tools for technology transfer, Vol. 19, No. 6, 11.2017, p. 675-696.

    Research output: Contribution to journalArticleAcademicpeer-review

    TY - JOUR

    T1 - Sylvan: multi-core framework for decision diagrams

    AU - van Dijk, Tom

    AU - van de Pol, Jaco

    PY - 2017/11

    Y1 - 2017/11

    N2 - Decision diagrams, such as binary decision diagrams, multi-terminal binary decision diagrams and multi-valued decision diagrams, play an important role in various fields. They are especially useful to represent the characteristic function of sets of states and transitions in symbolic model checking. Most implementations of decision diagrams do not parallelize the decision diagram operations. As performance gains in the current era now mostly come from parallel processing, an ongoing challenge is to develop datastructures and algorithms for modern multi-core architectures. The decision diagram package Sylvan provides a contribution by implementing parallelized decision diagram operations and thus allowing sequential algorithms that use decision diagrams to exploit the power of multi-core machines. This paper discusses the design and implementation of Sylvan, especially an improvement to the lock-free unique table that uses bit arrays, the concurrent operation cache and the implementation of parallel garbage collection. We extend Sylvan with multi-terminal binary decision diagrams for integers, real numbers and rational numbers. This extension also allows for custom MTBDD leaves and operations and we provide an example implementation of GMP rational numbers.Furthermore, we show how the provided framework can be integrated in existing tools to provide out-of-the-box parallel BDD algorithms, as well as support for the parallelization of higher-level algorithms. As a case study, we parallelize on- the-fly symbolic reachability in the model checking toolset LTSmin. We experimentally demonstrate that the parallelization of symbolic model checking for explicit-state modeling languages, as supported by LTSmin, scales well. We also show that improvements in the design of the unique table result in faster execution of on-the-fly symbolic reachability.

    AB - Decision diagrams, such as binary decision diagrams, multi-terminal binary decision diagrams and multi-valued decision diagrams, play an important role in various fields. They are especially useful to represent the characteristic function of sets of states and transitions in symbolic model checking. Most implementations of decision diagrams do not parallelize the decision diagram operations. As performance gains in the current era now mostly come from parallel processing, an ongoing challenge is to develop datastructures and algorithms for modern multi-core architectures. The decision diagram package Sylvan provides a contribution by implementing parallelized decision diagram operations and thus allowing sequential algorithms that use decision diagrams to exploit the power of multi-core machines. This paper discusses the design and implementation of Sylvan, especially an improvement to the lock-free unique table that uses bit arrays, the concurrent operation cache and the implementation of parallel garbage collection. We extend Sylvan with multi-terminal binary decision diagrams for integers, real numbers and rational numbers. This extension also allows for custom MTBDD leaves and operations and we provide an example implementation of GMP rational numbers.Furthermore, we show how the provided framework can be integrated in existing tools to provide out-of-the-box parallel BDD algorithms, as well as support for the parallelization of higher-level algorithms. As a case study, we parallelize on- the-fly symbolic reachability in the model checking toolset LTSmin. We experimentally demonstrate that the parallelization of symbolic model checking for explicit-state modeling languages, as supported by LTSmin, scales well. We also show that improvements in the design of the unique table result in faster execution of on-the-fly symbolic reachability.

    KW - Multi-core

    KW - Parallel

    KW - Binary decision diagrams

    KW - Multi-terminal binary decision diagrams

    KW - Multi-valued decision diagrams

    KW - Symbolic model checking

    U2 - 10.1007/s10009-016-0433-2

    DO - 10.1007/s10009-016-0433-2

    M3 - Article

    VL - 19

    SP - 675

    EP - 696

    JO - International journal on software tools for technology transfer

    JF - International journal on software tools for technology transfer

    SN - 1433-2779

    IS - 6

    ER -