Static Verification of Data-Consistency Properties

Abstract

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.