[cpp-threads] Causality on more than two processors, write atomicity

[Bill Pugh]

> Part of my question in that example was whether putting "volatile"  
> on x
> and y would be sufficient.

   volatile int x, y;

   start: x == y == 0;
   invariant:  x-1 <= y <= x+1

   P0: if( x == 0 ) x = 1;
   P1: if( x == 1 ) y = 2;
   P2: assert( invariant );

OK, so 0 <= x <= 1 and 0 <= y <= 2

So the only way assert( invariant ) can fail is to have
test y <= x+1 with y = 2 and x = 0

Let's break down the code a little further:

P0:
r1 = X
if (r1 == 0) x = 1

P1:
r2 = X
if (r1 == 1) y = 2

P2:
r3 = x
r4 = y
assert r3 -1 <= r4
r5 = x
assert r4 <= r5+1

OK, if r4 == 2, then we have
x = 1 hb r2 = X hb y = 2 hb r4 = y hb r5 = x

so the only legal value for r5 is 1

and the assertion will not fail.

Note that the invariant can't be checked atomically, so we got lucky.

If the invariant had been

     x-1 <= y && x+1 >= y

it would not have held.