CMP.14:5 - Archetypal Grounding

CMP.14:5.1 - Two increments need an operation that survives interference

Initially x=0. Two components each perform r=x; x=r+1 once. Reads and writes are atomic, arithmetic uses unbounded integers, but the pair is not atomic. The required final result after both operations is 2.

One admitted execution is:

A reads 0
B reads 0
A writes 1
B writes 1

The final value 1 violates the required result. Replace each increment by:

repeat:
    v = read(x)
    if compare_and_swap(x, v, v+1) succeeds:
        return

Compare-and-swap tests the current value and, only if it equals v, changes it to v+1 in one atomic action. A failed attempt leaves x unchanged.

The invariant is x = number of successful compare-and-swap actions. It holds initially; each success increases both sides by one, while reads and failed attempts change neither. Each component returns after its first success. Thus, when both return, x=2. A successful action supplies the point at which its increment takes effect in the sequential account.

If A and B both read 0, A can succeed first; B’s stale attempt fails. B then reads 1 and succeeds with 2. For these two one-shot callers, each failed attempt is attributable to the other caller’s success, so there can be at most one failed attempt before that caller completes. With both callers continuing to receive steps, both finish. A system with an unlimited stream of competing callers needs a different per-caller progress argument.

Changed condition: the environment supplies only a separate comparison and write. The old failing order is possible again. Use a primitive that really combines them or protect the read-modify-write region. Naming the pair “compare-and-swap” does not create that operation.

CMP.14:5.2 - A retry must refer to the same logical operation

A sender requests that a receiver add 5 to a stored counter. Initially the counter is 0. Messages may be lost or duplicated; the receiver continues running and retains its state. The receiver performs the addition, but the reply is lost. Blindly repeating the addition can leave 10 even though the sender requested one increment.

Give the logical request an identifier k that is not reused while an old request or reply with that identifier can still arrive. The sender retries the same pair (k, add 5). At the receiver, process the following as one atomic state transition:

if k is already in completed:
    result = completed[k]
else:
    counter = counter + 5
    result = counter
    completed[k] = result
send reply(k, result)

Only the state-changing conditional must be atomic; sending the reply can occur afterward. The first request changes the counter to 5 and stores completed[k]=5. Every duplicate returns 5 without another addition. The invariant relates a remembered identifier to its one committed effect. It depends on the same identifier denoting the same request payload.

At-most-once effect needs no promise that a message is eventually delivered. To promise a returned answer as well, suppose the sender keeps retrying, delivered requests are eventually processed, and each direction is a fair-loss channel: a message sent infinitely often is delivered infinitely often. The receiver answers each delivered request. These conditions ensure a reply eventually arrives. The result is a delivery-and-processing argument, not a deadline.

Changed condition: after applying the effect, the receiver can restart with the counter retained but completed lost. A later retry can again produce 10. Preserve the effect and its identifying result together across the admitted failure, for example through a durable atomic state update, or use an operation whose repetition is acceptable. An effect performed by another service needs that service’s corresponding guarantee; persisting only the local identifier leaves the effect/record crash gap unresolved.

CMP.14:5.3 - An acquisition order removes a waiting cycle

Two computations need exclusive resources L and R. A obtains L and waits for R; B obtains R and waits for L. Both acquisitions were locally valid, but neither computation can proceed to release its first resource.

Choose one strict total order, L<R, and require both computations to acquire L before R. More generally, each computation acquires resources in strictly increasing order and releases them after its finite protected work. It waits only for these resource acquisitions.

A resource-wait cycle would require a strictly increasing sequence of resource positions to return to its starting position, which is impossible. The construction therefore excludes deadlock of this acquisition form. A waiting computation can still be postponed indefinitely by unfair grants. A starvation-freedom claim additionally needs a suitable grant policy and progress by holders; a bounded waiting time needs further bounds on their work and scheduling.

Changed condition: introduce a callback while holding R that tries to acquire L. This violates the shared order and can restore a cycle. Move the callback outside the protected region or redesign the acquisition protocol and its argument.

CMP.14:5.4 - Include an observed effect of a pending call

An initially empty FIFO queue has this history: A calls enqueue(7) at t=1; B calls dequeue() at t=2 and receives 7 at t=3; A has not returned by t=4. Comparing only completed operations would leave a dequeue from an empty queue.

For the comparison, append A’s response at t=5. The sequential order enqueue(7); dequeue() returns 7 is legal. For example, their effects can be placed at t=1.5 and t=2.5, within their call/response intervals. This is a witness for the finite history; it supplies no promise that A will eventually respond in the actual execution.

If there is no enqueue call at all, appending responses cannot invent one: a dequeue returning 7 from the empty queue remains invalid. If A instead returned at t=2 before B called at t=3, the sequential order must keep A before B. Pending-call completion thus preserves both the observed values and the order already imposed by completed calls.