Linearizability: real-time ordered single-object safety

A concurrent history is linearizable when each completed operation can be placed at one point between its invocation and response so the resulting sequential history obeys the object specification and real-time precedence. If operation A responds before B is invoked, A must precede B. Overlapping operations may be ordered either way if the sequential specification permits it.

Linearizability is a safety property and is local/compositional by object. It does not promise progress, fairness, or availability, and per-key linearizability does not create a multi-key transaction. Pending operations require careful completion or removal when checking a history; a timeout may have taken effect.

Prerequisites and model

• The history records invocation, response, process, object/key, operation, value, and ambiguous outcomes.
• A precise sequential specification defines legal object transitions and return values.
• The checker preserves real-time precedence for non-overlapping completed operations.
• Multi-object claims are tested with a transactional model rather than inferred from per-object checks.

Correctness claims and invariants

• LIN-C1. Each completed operation linearizes between invocation and response in a legal sequential history.
• LIN-C2. A response-before-invocation relation constrains order; overlapping operations may be placed in either legal order.
• LIN-C3. A read starting after a completed write on the same object cannot return an older value.
• LIN-C4. Pending operations may be completed or removed in an extension of the history, so timeout outcomes remain ambiguous.
• LIN-C5. Linearizability is local per object; per-key checks do not imply cross-key atomicity.
• LIN-C6. Linearizability is safety, not liveness; under partition a side may need to reject or block operations.

What the scenarios prove

• Real-time precedence (real-time-order): A completed write before a later read invocation constrains the read result.

• Overlapping writes (overlapping-writes): Two overlapping operations may linearize in either legal order.

• Stale read violation (stale-read-violation): A read invoked after completed write(2) cannot return the older 1.

• Pending operation completion (pending-operation): A timeout may have taken effect and must stay ambiguous in the history.

• Per-key is not a transaction (per-key-not-transaction): Each key can be linearizable while a two-key transfer exposes a partial state.

• Partition forces unavailability (partition-unavailability): An isolated replica cannot safely acknowledge a conflicting mutation while preserving linearizability.

Failure, concurrency, and retry traps

• Latest wall-clock timestamp is not the definition of linearizability.
• Sequential consistency does not impose the same real-time precedence.
• Dropping timed-out operations as definitely failed can hide a violation.
• Checking every key independently cannot verify transfers or uniqueness across keys.
• A checker returning unknown due to search/resource limits is not a pass.

Boundaries and non-guarantees

• Linearizability does not require every replica to contain the latest value at every instant.
• Linearizability is distinct from serializability; strict serializability combines transaction order with real time.
• No quorum formula is inherent in the definition.
• A linearizable system may be unavailable during faults.

Related material

Primary sources

1. Herlihy and Wing, Linearizability: A Correctness Condition for Concurrent Objects
2. Herlihy and Wing paper PDF
3. Herlihy and Wing preliminary paper
4. Jepsen linearizable consistency model
5. Jepsen consistency models