paper

Linearizability: A Correctness Condition for Concurrent Objects

  • Authors:
Read the paper

📜 Abstract

A concurrent object is a data object shared by concurrent processes. Linearizability is a correctness condition for concurrent objects that exploits the semantics of abstract data types. It permits a high degree of concurrency, yet it permits programmers to specify and reason about concurrent objects using known techniques from the sequential domain. Linearizability provides the illusion that each operation applied by concurrent processes takes effect instantaneously at some point between its invocation and its response, implying that the meaning of a concurrent object’s operations can be given by pre- and post-conditions. This paper defines linearizability, compares it to other correctness conditions, presents and demonstrates a method for proving the correctness of implementations, and shows how to reason about concurrent objects, given they are linearizable.

✨ Summary

Impact

  • The paper established linearizability as a formal correctness condition for concurrent objects: concurrent histories must correspond to legal sequential histories while preserving the real-time order of non-overlapping operations. Its emphasis on locality, compositional reasoning, and nonblocking behavior made it a foundation for subsequent work on concurrent data-structure correctness. (cs.brown.edu)
  • Later research extended or operationalized the concept for new execution models and verification techniques. Examples include causal linearizability for weak-memory systems, contextual trace-refinement results connecting object correctness to client behavior, and runtime verification and enforcement of linearizability. (arxiv.org)
  • The paper’s object-level concurrency model is also reflected in widely used software platforms. Java’s standard concurrency libraries provide concurrent collections, nonblocking FIFO queues, atomic variables, and synchronization primitives intended as reusable building blocks for concurrent applications. The documentation does not establish direct historical causation from this paper, but these facilities represent a concrete industry use of the same broad abstraction of safely composable concurrent objects. (docs.oracle.com)