A Constructive Approach for Proving Data Structures’ Linearizability

Kfir Lev-Ari, Gregory Chockler, Idit Keidar

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

54 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 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

Keywords

  • shared memory systems
  • concurrency
  • data structure
  • formal verification

Cite this