Linearizability: A Typo

TL;DR

This paper identifies and corrects a typo in the original definition of linearizability, emphasizing the importance of handling pending invocations, especially for systems with non-volatile main memory.

Contribution

The paper highlights a previously unnoticed typo in the linearizability definition and proposes a correction to improve its completeness and applicability.

Findings

Identified a missing prime symbol in the original linearizability definition

Clarified the importance of handling pending invocations in concurrent systems

Provided a corrected version of the linearizability definition

Abstract

Linearizability is the de facto consistency condition for concurrent objects, widely used in theory and practice. Loosely speaking, linearizability classifies concurrent executions as correct if operations on shared objects appear to take effect instantaneously during the operation execution time. This paper calls attention to a somewhat-neglected aspect of linearizability: restrictions on how pending invocations are handled, an issue that has become increasingly important for software running on systems with non-volatile main memory. Interestingly, the original published definition of linearizability includes a typo (a symbol is missing a prime) that concerns exactly this issue. In this paper we point out the typo and provide an amendment to make the definition complete. We believe that pointing this typo out rigorously and proposing a fix is important and timely.