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)


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
Number of pages15
ISBN (Electronic)978-3-662-48653-5
ISBN (Print)978-3-662-48652-8
Publication statusPublished - 5 Nov 2015

Publication series

NameLecture Notes in Computer Science


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

Cite this