On Correctness of Data Structures under Reads-Write Concurrency

Kfir Lev-Ari, Gregory Chockler, Idit Keidar

Research output: Chapter in Book/Report/Conference proceedingConference contribution

85 Downloads (Pure)


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.
Original languageEnglish
Title of host publicationDistributed Computing
Subtitle of host publication28th International Symposium DISC 2014, Austin, TX, USA, October 12-15, 2014, Proceedings
EditorsFabian Kuhn
PublisherSpringer-Verlag Berlin Heidelberg
Number of pages15
ISBN (Electronic)978-3-662-45174-8
ISBN (Print)978-3-662-45173-1
Publication statusPublished - 2014
Event28th International Symposium on Distributed Computing (DISC'14) - Austin, Texas, United States
Duration: 12 Oct 201415 Oct 2014

Publication series

NameLecture Notes in Computer Science


Conference28th International Symposium on Distributed Computing (DISC'14)
Country/TerritoryUnited States
CityAustin, Texas


  • Algorithm Analysis and Problem Complexity
  • Computer Communication Networks
  • Data Structures, Cryptology and Information Theory

Cite this