Distributed Binary Decision Diagrams for Symbolic Reachability

Wytse Oortwijn, Tom van Dijk, Jaco van de Pol

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

    4 Citations (Scopus)
    1 Downloads (Pure)

    Abstract

    Decision diagrams are used in symbolic verification to concisely represent state spaces. A crucial symbolic verification algorithm is reachability: systematically exploring all reachable system states. Although both parallel and distributed reachability algorithms exist, a combined solution is relatively unexplored. This paper contributes BDD-based reachability algorithms targeting compute clusters: high-performance networks of multi-core machines. The proposed algorithms may use the entire memory of every machine, allowing larger models to be processed while increasing performance by using all available computational power. To do this effectively, a distributed hash table, cluster-based work stealing algorithms, and several caching structures have been designed that all utilise the newest networking technology. The approach is evaluated extensively on a large collection of models, thereby demonstrating speedups up to 51,1x with 32 machines. The proposed algorithms not only benefit from the large amounts of available memory on compute clusters, but also from all available computational resources.
    Original languageEnglish
    Title of host publicationSPIN 2017 Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software
    PublisherAssociation for Computing Machinery (ACM)
    Pages21-30
    Number of pages10
    ISBN (Print)978-1-4503-5077-8
    DOIs
    Publication statusPublished - Jul 2017
    Event24th International SPIN Symposium 2017: Model Checking of Software - University of California, Santa Barbara, United States
    Duration: 13 Jul 201714 Jul 2017
    Conference number: 24
    http://conf.researchr.org/home/spin-2017

    Conference

    Conference24th International SPIN Symposium 2017
    Abbreviated titleSPIN 2017
    CountryUnited States
    CitySanta Barbara
    Period13/07/1714/07/17
    Internet address

      Fingerprint

    Keywords

    • Symbolic model checking
    • parallel computing
    • distributed computing
    • high-performance computing
    • reachability analysis

    Cite this

    Oortwijn, W., van Dijk, T., & van de Pol, J. (2017). Distributed Binary Decision Diagrams for Symbolic Reachability. In SPIN 2017 Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software (pp. 21-30). Association for Computing Machinery (ACM). https://doi.org/10.1145/3092282.3092284