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 is a correctness condition for a concurrent object. Its observed invocation and response history must admit an explanation as a legal sequential history for that object's specification, while preserving the real-time order of operations that did not overlap. Overlapping calls may be ordered in whichever way yields a legal explanation. Informally, each completed operation appears to take effect at some point between its invocation and response; the apparent point is a witness to the history condition, not necessarily one fixed instruction in the implementation.[1]
The formal rule also handles pending calls. A history may be extended by responses to some pending invocations; the remaining incomplete calls are removed before testing equivalence to a legal sequential history. This matters because an operation can affect another call before its own caller receives a response. The rule does not require a pending call in every linearizable history.[1]
Structural Signature¶
Signature: object with sequential operation specification + concurrent invocation/response history → complete or discard pending calls under the formal extension rule → find a legal sequential witness → preserve every completed-before-started precedence relation.[1]
- Abstract object and sequential specification. The queue, register or other object supplies legal operation behavior. A total order alone cannot certify a FIFO queue if it returns an item inconsistent with its queue rules.[1]
- Invocation-response history. Calls and returns determine which operations overlap and which definitely precede later ones. A final value without the event history loses that information.[1]
- Legal sequential witness. There must be a sequential history permitted by the object's own specification and equivalent to the completed operation observations.[1]
- Real-time precedence. If one call returns before another begins, the witness keeps the first before the second. The freedom to reorder applies to calls that overlap.[1]
- Pending-call treatment. When pending calls occur, the formal extension can complete some and omit the rest. This is a conditional rule for incomplete histories, not a demand that every example contain incomplete work.[1]
What It Is Not¶
It is not sequential consistency alone: a sequentially legal ordering that reverses completed-before-started operations can fail the real-time condition. It is not proved by finding a successful compare-and-swap instruction in one run; the proof must account for every permitted concurrent history and the object's sequential semantics. Some implementations have useful code-level linearization points, but the definition does not insist on one universal CAS step.[1]
It is also not the same as database transaction serializability or a guarantee about a multi-object transaction. Herlihy and Wing prove locality for individual concurrent objects under their model. That theorem does not, by itself, grant an atomic transaction spanning several objects.[1]
Scope of Application¶
The original condition is formulated for typed concurrent objects whose operations are called by processes. It applies to shared-memory data structures such as queues and registers, and its contract can also be used to judge atomic read/write objects implemented over message-passing networks. It is a property of histories relative to a sequential specification, not a promise that an implementation uses locks, a particular network protocol, or a particular latency budget.[1][2]
The consulted distributed example is Attiya, Bar-Noy and Dolev's atomic single-writer multi-reader register emulation in asynchronous message-passing systems under specified failure and connectivity assumptions. Their paper calls the register atomic; identifying that history contract with Herlihy–Wing linearizability is a cross-paper interpretation of the two formal models, not terminology quoted from their article.[2][1]
Clarity¶
The test separates two questions that are easily conflated. First, can the observed returns be explained by any legal sequential execution of the chosen object type? Second, does that explanation respect calls already completed before later calls began? Both must pass. A queue can fail the first by returning items out of FIFO order; a register can fail the second if a later read is explained as occurring before a write that had already completed.[1]
“Instantaneous effect” is a semantic illusion at the history level. The machine may perform many instructions or messages during an operation. The condition asks whether the external result could have arisen from one legal ordering within the calls' time intervals; it does not state that one physical instant is observed by all machines.[1]
Manages Complexity¶
Linearizability lets clients reason about a concurrent object using its familiar sequential specification once the implementation has been proved correct. Herlihy and Wing's locality theorem says a system history is linearizable if and only if each object subhistory is linearizable, within their concurrent-object model. This supports object-level modular verification; it should not be stretched into a claim about cross-object transaction atomicity.[1]
The condition also compresses many possible low-level interleavings into a smaller set of legal abstract histories. A verifier can test order constraints and operation semantics without treating every internal instruction as part of the interface. Pending invocations and nondeterministic witness choices still need explicit handling.[1]
Abstract Reasoning¶
The core move is search for a witness order. List invocation and response events; mark which operations definitely precede others; account for pending calls; then ask whether some sequential order both extends that real-time partial order and satisfies the object's sequential rules. If none exists, the history is a counterexample. If one does, that particular history passes, though implementation correctness requires all allowed histories to pass.[1]
This move explains why overlap matters. Two overlapping calls need not have a predetermined order from wall-clock start times alone; either order can be a valid witness if the returned results and type specification permit it. Nonoverlapping calls lose that freedom. The criterion is thus stronger than a merely plausible sequential story but does not prohibit concurrency.[1]
Knowledge Transfer¶
To use linearizability on a new concurrent object, write the sequential operation specification, identify the public call/return events, and state what incomplete invocations can have done. Then test candidate sequential witnesses against both object legality and completed-before-started order. Record whether a proof covers all histories or an experiment checks only selected executions.[1]
The method transfers from in-memory queues to networked registers because the abstract history roles can be filled in both settings. The implementations, failure assumptions and evidence do not transfer automatically. The Attiya–Bar-Noy–Dolev register result applies to its single-writer multi-reader and network assumptions; it does not prove that every replicated key-value store or every multi-writer system is linearizable.[1][2]
Examples¶
Shared-memory FIFO queue. Herlihy and Wing model enqueue and dequeue operations as invocation/response events and give FIFO sequential axioms. An overlapping execution is acceptable only when a sequential queue order can explain the returned items while preserving nonoverlapping real-time precedence. Their figures include acceptable and unacceptable queue histories, and their implementation section studies a concurrent queue. The role of the example is the abstract history/specification match, not a universal CAS-step claim.[1]
Message-passing atomic register. Attiya, Bar-Noy and Dolev construct a wait-free atomic single-writer multi-reader register in unreliable asynchronous networks subject to their failure assumptions. Reads and writes are the object operations; atomicity supplies the legal single-register ordering expected of a linearizable register. Mapping the paper's atomicity to this entry's formal vocabulary is an explicit cross-paper inference using Herlihy–Wing's condition. It is a different carrier and implementation setting from the shared-memory queue.[2][1]
Structural Tensions¶
Scheduling freedom versus a real-time legal explanation. Allowing operations to overlap gives an implementation choices about their apparent order. Requiring a legal sequential witness that also respects nonoverlapping real-time precedence excludes some otherwise imaginable outcomes. An implementation cannot accept every arbitrary interleaving and still satisfy that condition. Diagnostic question: for this observed history, which witness orders remain after imposing the type's sequential rules and completed-before-started relations? A failed search identifies a correctness violation; a successful search for one history does not prove all possible histories. This is a formal admissibility pressure, not a universal claim about latency or availability.[1]
Structural–Framed Character¶
Linearizability is structural. Its core is a relation between an operation history, a sequential specification and a precedence-preserving witness. Once those are fixed, satisfaction is a formal property, not an evaluator's preference. Designers choose the abstract type and allowed implementation behavior, so human practice enters at specification and proof boundaries. The name comes from concurrent-computing research rather than an institution that can declare a history legal. Its vocabulary travels literally from shared-memory objects to atomic network registers when the history models match; using “linear” to mean simple or orderly in ordinary speech does not instantiate it. The pattern is recognized by formal histories rather than imported by analogy. Its character: a specialist formal correctness relation for concurrent objects.[1][2]
Structural Core vs. Domain Accent¶
The structural core is: choose a legal sequential witness and preserve real-time precedence between nonoverlapping operations. The domain accent is computer-science concurrency: typed objects, invocations, responses, pending calls and operation specifications. A queue and a register differ in behavior and implementation but fill those same formal roles.[1][2]
A portable-looking order-and-specification skeleton alone does not make this a Prime. Live Prime Consistency Model has a fuller signature about divergent read/write observers, propagation or staleness budgets, and coordination cost; a shared-memory queue history can satisfy linearizability without that entire genus. Strong Consistency discusses linearizability for replicated stores, but it is narrower in carrier and also accommodates looser informal usage. A future cross-domain Prime for legal-history witnesses would require its own evidence and admission decision. This entry stays with its literal concurrent-object condition.[1]
Instantiates / Related Primes¶
Approved specialist root with no strict DAG parent. Prime Consistency Model is the closest vocabulary neighbor, but its full shared-view and propagation signature is not required by every linearizable shared-memory object. Strong Consistency names the strict replicated-store case, not a parent of all linearizable histories. Prime Concurrency is also nearby, yet a linearizable object may have a history with no overlapping calls, so an all-instance prerequisite is not established. Prime Constraint and Formalization capture different complete identities. The empty edge list records these tested boundaries, not a missing topology decision.[1][2]
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 order operations legally while ignoring real-time precedence. Serializability orders transactions and has different cross-object commitments. Atomic register is an object/type contract and a useful instance of linearizability under a matching history model; it is not the entire criterion. A fixed linearization instruction is a proof device some implementations may offer, not part of the universal definition. Strong consistency in distributed systems often uses linearizability for its strict case but carries replicated-store scope and implementation concerns that this formal history predicate does not require.[1][2]
References¶
[1] 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). registry ↩a ↩b ↩c ↩d ↩e ↩f ↩g ↩h ↩i ↩j ↩k ↩l ↩m ↩n ↩o ↩p ↩q ↩r ↩s ↩t ↩u ↩v ↩w ↩x ↩y ↩z ↩27 ↩28
[2] 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. registry ↩a ↩b ↩c ↩d ↩e ↩f ↩g ↩h