linearizability and the linearization point
/ lin-ee-uh-rize-uh-BIL-i-tee /
When several threads operate on a shared data structure at once, their operations overlap in real time and there is no obvious single order to them. So what does it even MEAN for a concurrent stack or queue to be correct? Linearizability is the standard answer: a concurrent object is correct if, despite all the overlapping, it behaves exactly as if each operation took effect instantaneously at some single moment between when it was called and when it returned. It is the gold-standard correctness condition for lock-free data structures.
Make it precise with the linearization point. Each operation, even though it spans an interval of real time, is treated as if it happened atomically at one instant within that interval — its linearization point. If you can choose, for every operation, a linearization point inside its call-to-return interval such that running the operations one at a time in linearization-point order gives a result a correct sequential version of the object would produce, then the execution is linearizable. In practice the linearization point is usually a specific instruction: for a Treiber stack push it is the successful CAS that swings head; for an SPSC enqueue it is the release store that publishes the new tail. Before that instruction the operation has not happened; after it, it has, atomically, with no in-between state visible to anyone.
Why it matters so much: linearizability lets you reason about a concurrent object as if it were a simple sequential one, which is the only way humans keep these things in their heads. It also composes — a system built from individually linearizable objects has a coherent global behavior. Two honest distinctions: linearizability is stronger than mere serializability (it additionally respects real-time order, so an operation that finished before another began must be ordered first), and it is a different concern from the progress guarantees — an algorithm can be linearizable but blocking, or lock-free but, if you got it wrong, not linearizable. Correctness and progress are two separate axes you must satisfy independently.
/* The linearization point is the single instant the operation 'takes effect'. */ Node *pop(void) { do { old = head; if (!old) return NULL; next = old->next; } while (!CAS(&head, old, next)); /* <-- linearization point: the winning CAS */ return old; } /* Before the winning CAS the pop has not happened; after it, it has, atomically. */
Pinpointing the single instruction at which each operation atomically takes effect is how you prove a lock-free structure is linearizable.
Linearizability (correctness) and the progress class (lock-free, wait-free) are independent: a structure can be linearizable yet blocking, or lock-free yet buggy and not linearizable. You must establish both separately.