A Constructive Approach for Proving Data Structures’ Linearizability - DIStributed Computing 2015 Access content directly
Conference Papers Year : 2015

A Constructive Approach for Proving Data Structures’ 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.
Fichier principal
Vignette du fichier
30.pdf (712.75 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01206583 , version 1 (29-09-2015)

Identifiers

Cite

Kfir Lev-Ari, Gregory Chockler, Idit Keidar. A Constructive Approach for Proving Data Structures’ Linearizability. DISC 2015, Toshimitsu Masuzawa; Koichi Wada, Oct 2015, Tokyo, Japan. ⟨10.1007/978-3-662-48653-5_24⟩. ⟨hal-01206583⟩

Collections

DISC2015
47 View
114 Download

Altmetric

Share

Gmail Facebook X LinkedIn More