Verifying safety properties of concurrent heap-manipulating programs

Abstract

We provide a parametric framework for verifying safety properties of concurrent heap-manipulating programs. The framework combines thread-scheduling information with information about the shape of the heap. This leads to verification algorithms that are more precise than existing techniques. The framework also provides a precise shape-analysis algorithm for concurrent programs. In contrast to most existing verification techniques, we do not put a bound on the number of allocated objects. The framework produces interesting results even when analyzing programs with an unbounded number of threads. The framework is applied to successfully verify the following properties of a concurrent program: Concurrent manipulation of linked-list based ADT preserves the ADT datatype invariant. The program does not perform inconsistent updates due to interference. The program does not reach a deadlock. The program does not produce runtime errors due to illegal thread interactions. We also found bugs in erroneous programs violating such properties. A prototype of our framework has been implemented and applied to small, but interesting, example programs. © 2010 ACM.