Abstract

The report 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. The main challenge is the design of efficient concurrent data structures.
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%.

Additional Resources

1. The paper