Strict Linearizability and Abstract Atomicity

TL;DR

This paper introduces strict linearizability, a stronger correctness condition for concurrent objects that ensures client-side trace and state equivalence even when clients access shared memory directly, addressing limitations of traditional linearizability.

Contribution

The paper proposes strict linearizability, extending linearizability to allow shared memory access by clients, and establishes a correctness criterion combining linearizability and data abstraction.

Findings

Strict linearizability ensures client-side trace and state equivalence.

It relates to linearizability and data abstraction, providing a comprehensive correctness criterion.

The paper analyzes properties and implications of strict linearizability.

Abstract

Linearizability is a commonly accepted consistency condition for concurrent objects. Filipovi\'{c} et al. show that linearizability is equivalent to observational refinement. However, linearizability does not permit concurrent objects to share memory spaces with their client programs. We show that linearizability (or observational refinement) can be broken even though a client program of an object accesses the shared memory spaces without interference from the methods of the object. In this paper, we present strict linearizability which lifts this limitation and can ensure client-side traces and final-states equivalence even in a relaxed program model allowing clients to directly access the states of concurrent objects. We also investigate several important properties of strict linearizability. At a high level of abstraction, a concurrent object can be viewed as a concurrent implementation of an abstract data type (ADT). We also present a correctness criterion for relating an ADT and its concurrent implementation, which is the combination of linearizability and data abstraction and can ensure observational equivalence. We also investigate its relationship with strict linearizability.