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 proceedingConference contribution

Published

Documents

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 languageEnglish
Title of host publicationDistributed Computing 29th International Symposium, DISC 2015 Tokyo, Japan, October 7–9, 2015 Proceedings
EditorsYoram Moses
PublisherSpringer-Verlag
Pages356–370
Number of pages15
Volume9363
ISBN (Electronic)978-3-662-48653-5
ISBN (Print)978-3-662-48652-8
DOIs
Publication statusPublished - 5 Nov 2015

Publication series

NameLecture Notes in Computer Science

Projects

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

ID: 25549057