A.3.3:5.9 - Possible execution orders do not supply a probability law

Two participants A and B each read shared integer x into a local saved value, then write that saved value plus one. Each read or write is atomic, and each participant’s read precedes its write. Initially x=0. To follow the permitted reads and writes, use x, each participant’s position in its two-step procedure and any value already read.

There are six interleavings that preserve those local orders. Only readA,writeA,readB,writeB and its A/B reversal finish at 2. The other four finish at 1: both reads occur before either write, so each participant later writes 1. This enumeration identifies allowed histories that defeat the intended two-increment result.

The six histories have no assigned execution probabilities. Inferring a probability of 2/3 for a lost increment from these counts requires a scheduler model that justifies equal likelihood for the six histories. To obtain the intended result for every allowed history, serialize the read-and-write pairs or supply an indivisible increment operation. If that repair introduces waiting, separately check the progress condition required by the use.