A Thread-Safe Library for Binary Decision Diagrams

We describe the motivations, technical problems and solutions behind the implementation of BeeDeeDee, a new thread-safe Java library for Binary Decision Diagrams (BDDs) manipulation. BeeDeeDee allows clients to share a single factory of BDDs, in real parallelism, and reduce the memory footprint of their overall execution, at a very low synchronization cost. We prove through experiments on multi-core computers that BeeDeeDee is an effective thread-safe library for BDD manipulation. As test cases, we consider multiple instances of the n-queens problem, the construction of circuits and the parallel execution of information flow static analyses of Java programs, for distinct properties of variables. For sequential-only executions, BeeDeeDee is faster than other non-thread-safe Java libraries and as fast as non-thread-safe C libraries.