Thread Quantification for Concurrent Shape Analysis

In this paper we address the problem of shape analysis for concurrent
programs. We present new algorithms, based on abstract interpretation, for automatically
verifying properties of programs with an unbounded number of threads
manipulating an unbounded shared heap.
Our algorithms are based on a new abstract domain whose elements represent
thread-quantified invariants: i.e., invariants satisfied by all threads. We exploit
existing abstractions to represent the invariants. Thus, our technique lifts existing
abstractions by wrapping universal quantification around elements of the base
abstract domain. Such abstractions are effective because they are thread modular:
e.g., they can capture correlations between the local variables of the same thread
as well as correlations between the local variables of a thread and global variables,
but forget correlations between the states of distinct threads. (The exact nature of
the abstraction, of course, depends on the base abstraction lifted in this style.)
We present techniques for computing sound transformers for the new abstraction
by using transformers of the base abstract domain. We illustrate our technique in
this paper by instantiating it to the Boolean Heap abstraction, producing a Quantified
Boolean Heap abstraction. We have implemented an instantiation of our
technique with Canonical Abstraction as the base abstraction and used it to successfully
verify linearizability of data-structures in the presence of an unbounded
number of threads.