MATH.1:5.4 - Keep the intermediate states of interacting updates

Two updates to a counter each read its current value, retain that reading and later write the reading plus one. From zero, finishing one update before the other gives two. If both read zero before either writes, the final value is one.

To represent the difference, a state retains the counter, each update’s saved reading and whether its read and write have occurred. A read copies the counter into that update’s saved value; its later write replaces the counter by that saved value plus one. Form paths in which each read precedes its own write. The paths read-A, write-A, read-B, write-B and read-A, read-B, write-A, write-B return two and one respectively.

Treating each update as one indivisible arrow would lose the second path. If the work can require one complete update to finish before the other, the restricted paths preserve both increments. FPF C.29 establishes how these transitions describe the implemented work; Method Engineering ME.7 helps change its composition. Choosing an implementation also depends on how it handles waiting, interruption and failure.