Declarative Linearizability Proofs for Descriptor-Based Concurrent Helping Algorithms

TL;DR

This paper introduces a declarative approach to proving linearizability of descriptor-based helping algorithms by axiomatizing visibility relations, improving abstraction and reusability over traditional linearization point methods.

Contribution

It presents a novel axiomatization technique for visibility relations that captures the helping behavior in concurrent algorithms, enabling more abstract and reusable proofs.

Findings

Axiomatization captures helping behavior in concurrent algorithms.

Shared proof components for multiple descriptor-based algorithms.

New linearizability proofs that are more abstract and reusable.

Abstract

Linearizability is a standard correctness criterion for concurrent algorithms, typically proved by establishing the algorithms' linearization points. However, relying on linearization points leads to proofs that are implementation-dependent, and thus hinder abstraction and reuse. In this paper we show that one can develop more declarative proofs by foregoing linearization points and instead relying on a technique of axiomatization of visibility relations. While visibility relations have been considered before, ours is the first study where the challenge is to formalize the helping nature of the algorithms. In particular, we show that by axiomatizing the properties of separation between events that contain bunches of help requests, we can extract what is common for high-level understanding of several descriptor-based helping algorithms of Harris et al. (RDCSS, MCAS, and optimizations), and produce novel proofs of their linearizability that share significant components.