The correctness criterion
Linearizability is the gold standard for concurrent objects. It says that every operation, though it spans an interval from invocation to response, appears to take effect instantaneously at some single instant within that interval. The observed history must match some legal sequential history that respects real time order.
Linearization points
The heart of a proof is identifying each operation linearization point: the exact instruction where it logically takes effect.
- For a Treiber stack push, the linearization point is the successful CAS that swings head.
- For a successful dequeue, it is the CAS that advances head.
- For a read only lookup, it is often the atomic load that observes the relevant pointer.
Once you can name a single atomic step inside every operation interval, you argue that ordering operations by their linearization points yields a legal sequential history.
What a proof shows
A linearizability proof demonstrates two things: each operation has a valid linearization point within its interval, and the resulting order obeys the object sequential specification. This composes nicely, because a system built only from linearizable objects is itself linearizable, which is why the property is so prized.
Key idea
A linearizability proof assigns each operation a single linearization point inside its interval and shows that ordering by those points produces a legal sequential history matching the object specification.