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.