Static Verification of Data-Consistency Properties
Nicholas Kidd
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 programs.
(Click here to access the dissertation:
PDF.)
University of Wisconsin