On Correctness of Data Structures under Reads-Write Concurrency

We study the correctness of shared data structures under read-write concurrency. A popular approach to ensuring correctness of a read-only operations in the presence of concurrent updates, is read-set validation, which checks that all read variables have not changed since they were first read. In practice, this approach is often too conservative, which adversely affects performance. In this paper, we introduce a new framework for reasoning about correctness of single-writer/multi-reader concurrent data structures, which replaces validation of the entire read-set with more general criteria. Namely, instead of verifying that all read shared variables still hold the values read from them, we verify abstract conditions over the shared variables, which we call base conditions. We show that obtaining a consistent snapshot of some base condition at every point in time implies correctness of read-only operations executing in parallel with updates. Somewhat surprisingly, the resulting correctness guarantees are weaker than linearizability, and instead captured through two new conditions: validity and regularity. Roughly, the former requires that a read-only operation never reaches a state unreachable in a sequential execution; and the latter is a generalization of the Lamport’s notion of regularity for arbitrary data structures. We illustrate how our framework can be applied for reasoning about correctness of a variety of data structure implementations, such as linked lists as well as those implemented according to a popular read-copy-update (RCU) methodology. We further extend our framework to capture other commonly used correctness criteria, such as linearizability and sequential consistency.