Static Verification of Data-Consistency Properties
Show full item record
- University of Wisconsin-Madison Department of Computer Sciences
- Writing correct shared-memory concurrent programs is hard. Not only must a
programmer reason about the correctness of the sequential execution of code, but
also about the possible side effects caused by interleaved execution of
concurrently executing threads. Incorrect use of synchronization primitives can
lead to data-consistency errors, which can have drastic consequences (cf.~the
Northeast Blackout of 2003).
This dissertation presents techniques to verify statically that the programmer's
use of synchronization primitives preserves data consistency. The notion of data
consistency used throughout the dissertation is atomic-set serializability
(AS-serializability), which was first proposed by Vaziri et al. (2006).
AS-serializability is a property of a program execution, and is a relaxation of
serializability. An execution is serializable if its outcome is equivalent to an
execution where all transactions are executed serially. AS-serializability
relaxes serializability to be only with respect to specific memory locations.
The approach taken is to use software model checking to verify that every
possible execution of a concurrent program is AS-serializable. First, an abstract program is generated from a concrete program. The abstract program is defined such that it over-approximates the set of behaviors of the concrete program. Second, a software model checker explores all possible executions of the abstract program.
The challenge is to define abstractions and techniques that account for the
multitude of sources of unboundedness in a concrete program. Concrete programs
have dynamic memory allocation, recursion, dynamic thread creation, and reentrant locks, to name a few.
The contributions of the dissertation are generic techniques to permit model
checking to be performed in the presence of several sources of unboundedness. My
research addressed the problem of determining whether all possible executions of
a certain class of models of concurrent Java programs are AS-serializable.
Somewhat surprisingly, given the many sources of unboundedness allowed in the
models considered, I was able to show that the problem is decidable, and gave a
practical algorithm for the problem. The technique has been implemented in a tool called Empire, which has been used to find known bugs in concurrent Java
- Permanent link
Export to RefWorks
Show full item record