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

TL;DR

This paper introduces a declarative approach to proving linearizability of concurrent algorithms like the timestamped stack by using visibility and separability relations, avoiding traditional linearization points.

Contribution

It systematically derives axiomatizations of visibility and separability relations from the sequential specification, enabling simplified, declarative proofs of linearizability.

Findings

Axiomatization of visibility relations derived systematically from sequential specs.

Introduction of a separability relation to generalize real-time precedence.

Simplified proof reducing the algorithm to atomic timestamp generation.

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.