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.