On Correctness of Data Structures under Reads-Write Concurrency. / Lev-Ari, Kfir; Chockler, Gregory; Keidar, Idit.

Distributed Computing: 28th International Symposium DISC 2014, Austin, TX, USA, October 12-15, 2014, Proceedings. ed. / Fabian Kuhn. Vol. 8784 1. ed. Springer-Verlag Berlin Heidelberg, 2014. p. 273-287 (Lecture Notes in Computer Science).

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

Published

Documents

Links

Abstract

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
Pages273-287
Number of pages15
Volume8784
Edition1
ISBN (Electronic)978-3-662-45174-8
ISBN (Print)978-3-662-45173-1
DOIs
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

Conference

Conference28th International Symposium on Distributed Computing (DISC'14)
CountryUnited States
CityAustin, Texas
Period12/10/1415/10/14

Projects

This open access research output is licenced under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.

ID: 25549116