A Constructive Approach for Proving Data Structures’ Linearizability

Kfir Lev-Ari; Gregory Chockler; Idit Keidar

doi:10.1007/978-3-662-48653-5_24

A Constructive Approach for Proving Data Structures’ Linearizability

Kfir Lev-Ari, Gregory Chockler, Idit Keidar

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

50 Downloads (Pure)

Abstract

We present a comprehensive methodology for proving correctness of concurrent data structures. We exemplify our methodology by using it to give a roadmap for proving linearizability of the popular Lazy List implementation of the concurrent set abstraction. Correctness is based on our key theorem, which captures sufficient conditions for linearizability. In contrast to prior work, our conditions are derived directly from the properties of the data structure in sequential runs, without requiring the linearization points to be explicitly identified.

Original language	English
Title of host publication	Distributed Computing 29th International Symposium, DISC 2015 Tokyo, Japan, October 7–9, 2015 Proceedings
Editors	Yoram Moses
Publisher	Springer-Verlag
Pages	356–370
Number of pages	15
Volume	9363
ISBN (Electronic)	978-3-662-48653-5
ISBN (Print)	978-3-662-48652-8
DOIs	https://doi.org/10.1007/978-3-662-48653-5_24
Publication status	Published - 5 Nov 2015

Publication series

Name	Lecture Notes in Computer Science

Keywords

shared memory systems
concurrency
data structure
formal verification

Access to Document

10.1007/978-3-662-48653-5_24

Accepted ManuscriptAccepted author manuscript, 382 KB

Scalable Software for Multicores
Chockler, G.
Royal Society
1/01/14 → 1/01/14
Project: Research

Cite this

Lev-Ari, K., Chockler, G., & Keidar, I. (2015). A Constructive Approach for Proving Data Structures’ Linearizability. In Y. Moses (Ed.), Distributed Computing 29th International Symposium, DISC 2015 Tokyo, Japan, October 7–9, 2015 Proceedings (Vol. 9363, pp. 356–370). Article 97 (Lecture Notes in Computer Science). Springer-Verlag. https://doi.org/10.1007/978-3-662-48653-5_24

@inproceedings{8475aac9bbba46d68bc41bb65a937426,

title = "A Constructive Approach for Proving Data Structures{\textquoteright} Linearizability",

abstract = "We present a comprehensive methodology for proving correctness of concurrent data structures. We exemplify our methodology by using it to give a roadmap for proving linearizability of the popular Lazy List implementation of the concurrent set abstraction. Correctness is based on our key theorem, which captures sufficient conditions for linearizability. In contrast to prior work, our conditions are derived directly from the properties of the data structure in sequential runs, without requiring the linearization points to be explicitly identified.",

keywords = "shared memory systems, concurrency, data structure, formal verification",

author = "Kfir Lev-Ari and Gregory Chockler and Idit Keidar",

year = "2015",

month = nov,

day = "5",

doi = "10.1007/978-3-662-48653-5_24",

language = "English",

isbn = "978-3-662-48652-8",

volume = "9363",

series = "Lecture Notes in Computer Science",

publisher = "Springer-Verlag",

pages = "356–370",

editor = "Yoram Moses",

booktitle = "Distributed Computing 29th International Symposium, DISC 2015 Tokyo, Japan, October 7–9, 2015 Proceedings",

}

A Constructive Approach for Proving Data Structures’ Linearizability. / Lev-Ari, Kfir; Chockler, Gregory; Keidar, Idit.
Distributed Computing 29th International Symposium, DISC 2015 Tokyo, Japan, October 7–9, 2015 Proceedings. ed. / Yoram Moses. Vol. 9363 Springer-Verlag, 2015. p. 356–370 97 (Lecture Notes in Computer Science).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - A Constructive Approach for Proving Data Structures’ Linearizability

AU - Lev-Ari, Kfir

AU - Chockler, Gregory

AU - Keidar, Idit

PY - 2015/11/5

Y1 - 2015/11/5

N2 - We present a comprehensive methodology for proving correctness of concurrent data structures. We exemplify our methodology by using it to give a roadmap for proving linearizability of the popular Lazy List implementation of the concurrent set abstraction. Correctness is based on our key theorem, which captures sufficient conditions for linearizability. In contrast to prior work, our conditions are derived directly from the properties of the data structure in sequential runs, without requiring the linearization points to be explicitly identified.

AB - We present a comprehensive methodology for proving correctness of concurrent data structures. We exemplify our methodology by using it to give a roadmap for proving linearizability of the popular Lazy List implementation of the concurrent set abstraction. Correctness is based on our key theorem, which captures sufficient conditions for linearizability. In contrast to prior work, our conditions are derived directly from the properties of the data structure in sequential runs, without requiring the linearization points to be explicitly identified.

KW - shared memory systems

KW - concurrency

KW - data structure

KW - formal verification

U2 - 10.1007/978-3-662-48653-5_24

DO - 10.1007/978-3-662-48653-5_24

M3 - Conference contribution

SN - 978-3-662-48652-8

VL - 9363

T3 - Lecture Notes in Computer Science

SP - 356

EP - 370

BT - Distributed Computing 29th International Symposium, DISC 2015 Tokyo, Japan, October 7–9, 2015 Proceedings

A2 - Moses, Yoram

PB - Springer-Verlag

ER -

A Constructive Approach for Proving Data Structures’ Linearizability

Abstract

Publication series

Keywords

Access to Document

Projects

Scalable Software for Multicores

Cite this