DROPS

Document

DOI: 10.4230/LIPIcs.CONCUR.2023.30

Visibility and Separability for a Declarative Linearizability Proof of the Timestamped Stack

Authors: Jesús Domínguez and Aleksandar Nanevski

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)

Abstract

Linearizability is a standard correctness criterion for concurrent algorithms, typically proved by establishing the algorithms' linearization points (LP). However, LPs often hinder abstraction, and for some algorithms such as the timestamped stack, it is unclear how to even identify their LPs. In this paper, we show how to develop declarative proofs of linearizability by foregoing LPs and instead employing axiomatization of so-called visibility relations. While visibility relations have been considered before for the timestamped stack, our study is the first to show how to derive the axiomatization systematically and intuitively from the sequential specification of the stack. In addition to the visibility relation, a novel separability relation emerges to generalize real-time precedence of procedure invocation. The visibility and separability relations have natural definitions for the timestamped stack, and enable a novel proof that reduces the algorithm to a simplified form where the timestamps are generated atomically.

Cite as

Jesús Domínguez and Aleksandar Nanevski. Visibility and Separability for a Declarative Linearizability Proof of the Timestamped Stack. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 30:1-30:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{dominguez_et_al:LIPIcs.CONCUR.2023.30,
  author =	{Dom{\'\i}nguez, Jes\'{u}s and Nanevski, Aleksandar},
  title =	{{Visibility and Separability for a Declarative Linearizability Proof of the Timestamped Stack}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{30:1--30:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.30},
  URN =		{urn:nbn:de:0030-drops-190245},
  doi =		{10.4230/LIPIcs.CONCUR.2023.30},
  annote =	{Keywords: Linearizability, Visibility Relations, Timestamped Stack}
}

Search Results

Documents authored by Domínguez, Jesús

Visibility and Separability for a Declarative Linearizability Proof of the Timestamped Stack

Abstract

Cite as

Thanks for your feedback!

Could not send message