Linearizability¶
Test whether a concurrent object's operation history has a legal sequential explanation that preserves the real-time order of nonoverlapping calls.
Core Idea¶
Linearizability asks whether concurrent calls to an object could have happened one at a time in a legal order, while keeping the real-time order of calls that did not overlap. A queue's order must follow its FIFO rules; a register's reads and writes must follow its register rules. Overlapping calls can be placed in either order when the returned results allow it. The test concerns the public call-and-return history, not a particular machine instruction.[^ref-4471bb11b4ff]
When a call has started but has not returned, the formal rule can complete some such calls and omit the rest before judging the history. That does not mean every example needs a pending call.[^ref-4471bb11b4ff]
Scope of Application¶
The original work applies to shared concurrent objects such as queues and registers. The same history criterion can be used for a networked atomic register when its model matches. Attiya, Bar-Noy and Dolev constructed an atomic single-writer multi-reader register in specified asynchronous, failure-prone networks. Calling that a linearizable-register realization is a cross-paper interpretation of their atomicity contract and Herlihy–Wing's definition, not a phrase taken from their paper.[ref-4471bb11b4ff][ref-cbf056b662f8]
Clarity¶
Two checks are needed. The proposed sequential order must be legal for the object type, and it must respect a call that finished before another began. A story that explains returned values but reverses completed-before-started operations fails. The imagined instant at which a call takes effect is a way to explain the history; it need not be a fixed compare-and-swap step in every implementation.[^ref-4471bb11b4ff]
Manages Complexity¶
Once an object's implementation is proved linearizable, clients can use its simpler sequential specification to reason about its behavior. Herlihy and Wing prove a locality result for their concurrent-object model: a system history is linearizable if each object's history is. This does not by itself prove an atomic transaction spanning several objects.[^ref-4471bb11b4ff]
Abstract Reasoning¶
Record invocations and responses. Mark each pair of operations where one finished before the other started. Handle pending calls according to the formal rule. Then search for an order that satisfies both those time relations and the object's ordinary sequential behavior. One impossible observed history is a counterexample; one possible history does not prove an implementation correct for every execution.[^ref-4471bb11b4ff]
Knowledge Transfer¶
The method transfers from an in-memory queue to a networked register by keeping the same questions: what is the object specification, what was observed, and can a legal order preserve real time? The implementation evidence does not transfer. The message-passing register result depends on its single-writer multi-reader and network-failure assumptions; it does not certify all replicated stores.[ref-4471bb11b4ff][ref-cbf056b662f8]
Example¶
In a shared-memory FIFO queue, overlapping enqueue and dequeue calls must have some sequential explanation that returns items in legal queue order while respecting calls that clearly happened earlier. Herlihy and Wing give both accepted and rejected queue histories. The criterion judges those observable histories rather than a generic CAS step.[^ref-4471bb11b4ff]
A different carrier is an atomic register accessed through asynchronous messages. In the Attiya–Bar-Noy–Dolev construction, clients read and write a single-writer multi-reader register under stated failure conditions. Its atomic history contract is a qualified distributed realization of the same legal-order idea; the equivalence to linearizability is an explicit cross-paper inference.[ref-cbf056b662f8][ref-4471bb11b4ff]
Neighborhood in Abstraction Space¶
Linearizability sits in a sparse region of the domain-specific corpus (98th percentile for distinctiveness): few abstractions share its structure, so a faithful description tends to retrieve it precisely.
Family — Unclustered & Miscellaneous (2551 abstractions)
Nearest neighbors
- Protocol Stack — 0.77
- Dynamic Amplification Factor — 0.76
- Non-Blocking Algorithm — 0.76
- Formal Verification — 0.76
- Queue (FIFO Abstract Data Type) — 0.76
Computed from structural-signature embeddings · 2026-10-08
Not to Be Confused With¶
Sequential consistency can use a legal total order that does not respect real-time precedence. Database serializability concerns transactions with different cross-object commitments. Strong Consistency uses linearizability for the strict replicated-store case, but this entry also covers shared-memory concurrent objects. The reviewed catalog supplied no strict all-instance parent; its V2 DAG records an approved specialist root with no edge.[ref-4471bb11b4ff][ref-cbf056b662f8]
References¶
[^ref-4471bb11b4ff]: Maurice P. Herlihy and Jeannette M. Wing, Linearizability, A Correctness Condition for Concurrent Objects, ACM Transactions on Programming Languages and Systems 12(3), 463–492 (1990); linked title transcribes the printed colon as a comma for citation binding; original full paper, abstract and §2.2 pp.467–470 (formal conditions L1–L2), §3.1 pp.470–471 (Theorem 1 locality), Figures 1–2 pp.464–466 and §4 pp.475–480 (queue histories and implementation). [^ref-cbf056b662f8]: Hagit Attiya, Amotz Bar-Noy and Danny Dolev, Sharing Memory Robustly in Message-Passing Systems, Journal of the ACM 42(1), 124–142 (1995); original full paper, abstract p.124 and §§1, 4–5 on atomic SWMR register emulation. The linearizability relationship in the body is a cross-paper inference, not the authors' label.