Linearizability and progress: two different promises

Record invocation, response, arguments, return values, and operation identity. If one operation returns before another is invoked, the sequential explanation must preserve that precedence. Overlapping operations may be ordered either way if the result matches the object's sequential contract. For a FIFO queue, a dequeue must return the oldest previously enqueued item in the chosen order; it cannot invent a value. The history includes failed or empty outcomes because they constrain which state could legally have existed.

A linearization point is an abstract instant within an operation's invocation-response interval at which its effect is considered to occur. Some algorithms have an obvious successful CAS as that point. Others need a more involved proof, an operation-dependent point, or reasoning based on a later observation. Do not require every concurrent algorithm to share one fixed source line for every operation. Pending operations also need careful treatment when formally completing or discarding parts of a finite history.

A blocking method can depend on a particular owner or waiter taking a step. Obstruction freedom guarantees completion when an operation eventually runs without interference for long enough. Lock freedom guarantees system-wide progress under its execution assumptions: threads continue taking steps and some operations complete, even though a particular caller may repeatedly lose. Wait freedom provides per-operation completion within a finite bound on that caller's own steps, potentially dependent on parameters such as participant count. None of these labels is a wall-clock latency service level by itself.

The progress scope must include what the advertised operation actually does. A lock-free pointer algorithm wrapped around a blocking allocator is not automatically a lock-free public queue operation. Reclamation may accumulate memory when a participant stalls; user-defined item construction may acquire locks or throw. State whether the proof assumes preallocated storage, lock-free atomic primitives, nonblocking callbacks, finite participants, or a specific scheduler condition. Those assumptions are part of the claim a caller needs to assess.

For a request-serving queue, a short mutex critical section may outperform a complex nonblocking design under the measured workload. For a runtime where one paused owner must not halt all other participants, a system-progress guarantee may be essential. Decide from failure and latency requirements rather than assuming lock-free means faster. Measure contention, tail latency, memory growth, and operation outcomes, while keeping those measurements distinct from the proof that excludes a class of bad executions.

The queue lab illustrates the difference between throughput and an individual latency promise. Begin a fixed-rate experiment with Reset, explicitly set arrival to two and service to three, predict draining from four jobs, then Play or Step. Compare a separate near-capacity run by choosing Reset again, explicitly setting arrival to 2.5 and service to three, predicting, then Play or Step. The separate M/M/1 residence estimate is two seconds rather than one under its assumptions. A control edit retains elapsed time and recomputes the fixed-rate model; it does not continue the old backlog with a new slope. Neither readout guarantees that a particular concurrent caller finishes, and the model has no CAS retries, locks, or scheduler. Use the animation to ask which metric a claim describes before inspecting the algorithm's actual progress argument.