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 paper at CAV 2011 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