Multi-Core BDD Operations for Symbolic Reachability

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

    13 Citations (Scopus)
    68 Downloads (Pure)

    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
    Publication statusPublished - 17 Sep 2012
    Event11th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2012 - London, United Kingdom
    Duration: 17 Sep 201217 Sep 2012
    Conference number: 11
    http://anna.fi.muni.cz/PDMC/PDMC12/

    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

    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