BDD Algortihms and Cache Misses

Nils Klarlund, Theis Rauhe

Abstract


Within the last few years, CPU speed has greatly overtaken memory speed. For this reason, implementation of symbolic algorithms - with their extensive use of pointers and hashing - must be reexamined. In this paper, we introduce the concept of cache miss complexity
as an analytical tool for evaluating algorithms depending on pointer chasing. Such algorithms are typical of symbolic computation found in verification. We show how this measure suggests new data structures and algorithms
for multi-terminal BDDs. Our ideas have been implemented in
a BDD package, which is used in a decision procedure for the Monadic Second-order Logic on strings.
Experimental results show that on large examples involving e.g the verification of concurrent programs, our implementation runs 4 to 5 times faster than a widely used BDD implementation.
We believe that the method of cache miss complexity is of general interest to any implementor of symbolic algorithms used in verification.

Full Text:

PDF


DOI: http://dx.doi.org/10.7146/brics.v3i26.20007
This website uses cookies to allow us to see how the site is used. The cookies cannot identify you or any content at your own computer.
OK


ISSN: 0909-0878 

Hosted by the Royal Danish Library and Aarhus University Library