Concurrent software
verification
In recent years, we have developed methods to analyze concurrent Boolean programs. i.e.
programs whose variables have finite range, and that consist of
procedures intended to be run by many threads in parallel.
Communication among the threads is via global-scope shared variables.
For such programs, we are interested in various reachability problems,
such as detecting thread synchronization errors (mutual-exclusion
violations, deadlocks) or even simple assertion failures. Our work
showed how to beat concurrency explosion due to the thread
interleavings, first for a finite number of threads by exploiting counter abstraction [BMWK09,BMWK10], then for an infinite
number of threads by exploiting cutoff
properties of programs [KKW10]. See here for more background
on
these two techniques.
In these results, each thread manipulates finite-range variables. To
connect the results to system-level software analysis, say written in C
or Java, we have designed and implemented a predicate abstraction strategy for
concurrent C programs. The program model is very much the same as
described above for concurrent Boolean programs. In the presence of
concurrency, you want to do the abstraction in a way that allows the
Boolean program model checker to exploit the replication redundancy
inherent in programs of many threads executing a single procedure
(which can be thought of as a template). Thus, the abstraction should
be done at the level of the procedure that is to be executed by the
threads, not at the level of the ("multiplied-out") concurrent program
consisting of many copies of this procedure.
The challenge in doing the abstraction at the procedure (template)
level is that predicates can now refer to variables both inside the
procedure (local) and outside (global). If local, such a predicate
evaluates differently for different threads, since each thread has its
own copy of such a variable. So we somehow have to keep track of a copy
of this predicate for each thread, yet we do not want to syntactically
introduce n copies,
especially not if the number of threads that will run is unknown!
Moreover, if a thread modifies a global variable g in a predicate that also refers
to a local variable l, say a
predicate p like g = l, then any modification of g by a thread causes the value of p to change for each thread (whereas a modification
of l only changes p for the thread responsible for
the modification).
Our recent paper at CAV describes a "protocol" that solves this problem
by forcing the threads to cooperate and inform each other whenever they
update a variable that modifies predicates locally stored within other
threads [DKKW11]. This work
can
be viewed as an extension of the Slam
work done at Microsoft for sequential C code.
Collaborators (most recent only):
Alastair Donaldson, Alexander Kaiser,
Daniel Kroening