Boom and Cutoffs

Boom implements symbolic reachability analysis for symmetric systems using an embedded form of counter abstraction and applies it to non-recursive shared-variable concurrent Boolean programs with a fixed number of threads (given as a parameter to Boom). We are using Boolean programs obtained from C programs by predicate abstraction, to analyze low-level Windows and Linux operating system code, such as device drivers. We believe Boom to be the fastest tool (2009) to exhaustively explore such programs. [BMWK09]

Collaborators: Gerard Basler, Daniel Kroening, Michele Mazzucchi.

We later extended Boom to handle an unbounded number of threads, created either dynamically during execution, or up-front in the manner of a parameterized program. Disallowing recursion in the Boolean programs retains decidability of the reachability problem, so that no approximation is necessary. Our method exploits that such parameterized programs have a cutoff: a number of threads with the property that adding more threads into the mix does not increase the set of reachable program locations. Knowing (an upper bound on) the cutoff solves the reachability problem for the entire family of concurrent programs, no matter how many threads are running.

Cutoffs can often be approximated by statically analyzing the Boolean program text. But cutoffs obtained this way will generally be of size proportional to the number of program states, which in practice can mean millions. Such a cutoff is of no use, since no model checker can analyze a concurrent program with a million threads. Such large cutoffs are, however, in stark contrast to the widely observed empiricism that, in practice, the number of threads one needs to start to ensure the set of reachable program location "stabilizes" is much smaller, sometimes a handful of threads will do. Our method is therefore dynamic in nature: we determine the set of reachable program locations for increasing thread counts. Program locations that are reachable given n+1 threads but not given n threads turn out to require the threads to cooperate in a particular fashion. If the set of reachable program locations given n threads does not allow such a cooperation, we can conclude that n is the cutoff. In a 2010 paper we present the details of this idea, and show how to make it complete for parameterized Boolean program verification [KKW10].

Collaborators: Alexander Kaiser, Daniel Kroening.