Relating a concurrent history to a legal sequence

Operations on a shared object can overlap. Linearizability requires an explanation consistent with the object’s sequential specification, as though each operation took effect at a point between its invocation and response.

That explanation preserves real-time precedence: if one operation finishes before another begins, their order cannot simply be reversed. Overlapping operations can admit different orders when those orders still satisfy the object’s semantics.

References: [1]

Results must match the object’s own semantics

For a FIFO queue, if enqueueing x finishes before enqueueing y begins, a later dequeue cannot return y first without an intervening removal of x. Overlapping enqueues can allow different orders, subject to all observed dequeue results.

Linearizability is therefore more than sorting log entries. It needs the object’s legal behavior. Queues, stacks, and sets have different specifications, so one collection of results can be valid for one kind of object and invalid for another.

References: [1]

Compositional reasoning differs from implementation progress

Herlihy and Wing prove a locality property that supports reasoning about objects independently. A business action comprising several calls can still interleave with others; separately linearizable reads and writes do not become one atomic update.

The condition does not require a lock-free implementation. The paper explicitly distinguishes the behavioral property from blocking or even deadlock introduced by an implementation. Correct outcomes, progress guarantees, and bounded latency require different arguments.

References: [1]