Nov 24, 2015: Wytse Oortwijn: Distributed Binary Decision Diagrams for Symbolic Reachability

November 24, 2015Distributed Binary Decision Diagrams for Symbolic Reachability
Room: HB 2AWytse Oortwijn

Binary decision diagrams are used in symbolic verifcation to effciently represent state spaces. A crucial algorithm is symbolic reachability, which systematically yields all reachable system states. We propose novel algorithms for BDD-based symbolic reachability targeting high-performance networks of multi-core machines. Additionally, we provide a distributed hash table, cluster-based work stealing operations, and several caching structures that employ Remote Direct Memory Access (RDMA). All distributed data structures are lockless and carefully designed to minimize the number of roundtrips. We demonstrate speedups up to 45x with 64 machines, relative to sequential runs. Besides maintaining good time-effciency, the proposed algorithms also allow substantially more memory to be effciently employed, compared to non-distributed implementations.‚Äč