A.3.3.TR:5.1 - Two correct local increments can lose a global increment
Participants A and B each read an integer counter and later write the saved value plus one. Individual reads and writes are atomic. Each participant reads before it writes. Initially x = 0.
Use the state x, positions pA and pB in the two local procedures, and saved values rA and rB after their reads. Positions 0, 1 and 2 mean before read, after read and finished. Initially pA = pB = 0 and rA = rB = 0; each participant overwrites its saved value before using it.
The four action rules are:
| Action | Enabled when | Changed values | Other values |
|---|---|---|---|
| ReadA | pA = 0 | rA’ = x; pA’ = 1 | x, pB and rB retain their values |
| WriteA | pA = 1 | x’ = rA + 1; pA’ = 2 | rA, pB and rB retain their values |
| ReadB | pB = 0 | rB’ = x; pB’ = 1 | x, pA and rA retain their values |
| WriteB | pB = 1 | x’ = rB + 1; pB’ = 2 | rB, pA and rA retain their values |
The next step is any one enabled action. From pA = pB = 0, six complete histories respect the local orders. ReadA, WriteA, ReadB, WriteB and its A/B reversal finish at x = 2. In the other four, both reads precede either write; both saved values are zero, so the final value is one.
The result identifies how interference defeats the intended total. Serializing the two read-and-write pairs or supplying an indivisible increment changes the transition rule and removes these lost-increment histories. If serialization introduces waiting, a claim of eventual completion still needs its scheduling conditions.
The ordering rules already suffice to exhibit failure. If a scheduler chooses uniformly among enabled actions at each step, the two serialized histories each have probability 1/4 and the other four each have probability 1/8; the lost-increment probability is 1/2. Uniform choice among the six complete histories instead gives 2/3. Choose and justify a scheduler model when a likelihood estimate is needed.