Linearizability¶
Herlihy, M. P., & Wing, J. M. (1990). Linearizability: A Correctness Condition for Concurrent Objects. ACM Transactions on Programming Languages and Systems, 12(3), 463-492.
Cited by¶
6 citations across 6 artifacts.
Each citation links to the sentence it supports in the citing article.
Primes¶
- Concurrency
- Interleaving-safe invariants and atomicity boundaries
SupportedVerified against the work's full text
Herlihy and Wing define operations as appearing atomic between invocation and response and show that invariants on concurrent objects must hold at every step, not just between operations.
“In conclusion, the rep invariant I must be continually satisfied and the abstraction function continually defined, not only between abstract operations, but also between rep operations implementing abstract operations.”
- Interleaving-safe invariants and atomicity boundaries
- Consistency Model
- It does not say what the state is; it says which interleavings of reads and writes count as legal observations, and therefore what observers may assume about one another's view.
This sourceDefines linearizability as the strongest single-object consistency condition requiring a real-time-consistent total order.
Supported in partVerified against the work's full text
Supports the idea that a linearizability condition specifies which interleavings may occur rather than the state itself; the general 'consistency model' framing is the encyclopedia's.
“it states that certain interleavings cannot occur, but makes no guarantees about what must occur”
- It does not say what the state is; it says which interleavings of reads and writes count as legal observations, and therefore what observers may assume about one another's view.
- Fault Tolerance
- Listed in the references but not attached to a specific claim.
- Transaction
Mechanisms¶
- Atomic Check-and-Use Operation
- Its strength is absolute for what it covers: it is the only guard that fully eliminates the check-to-use race on the protected referent, making the action linearizable — it appears to take effect at a single instant.
This sourceDefines linearizability as making each concurrent operation appear to take effect at a single instant between invocation and response.
- Its strength is absolute for what it covers: it is the only guard that fully eliminates the check-to-use race on the protected referent, making the action linearizable — it appears to take effect at a single instant.
- Sequential-Consistency Trace Protocol
- Sequential consistency is not compositional — verifying components does not verify the whole — and it is strictly weaker than linearizability, so passing this check does not mean the store is linearizable; a sequentially-consistent read may legally be stale.
This sourceShows that sequential consistency is non-local and weaker than linearizability, so component checks need not compose and histories may violate real-time ordering.
- Sequential consistency is not compositional — verifying components does not verify the whole — and it is strictly weaker than linearizability, so passing this check does not mean the store is linearizable; a sequentially-consistent read may legally be stale.
Verification¶
Does it exist? Confirmed. This work's DOI resolves to a registered record, which fixes its identity. That is all it fixes.
Does it back the claim? Read against the text for 2 of 6 citations: 1 supported, 1 supported in part. Each verdict is shown under its citation below, with what in the work backs the sentence.
Was it audited? Yes. A second, independent pass read the citation against the article text and recorded a verdict.
Support is checked per citation rather than per work — the same source can be cited soundly in one article and wrongly in another. Per-citation recording began recently, so a citation with no recorded check is a gap in the record rather than evidence it went unchecked.
See how references were verified.
Registry ID ref:9f6f519c74eb · see in the full table