35 lines · plain
1C cmpxchg-fail-unordered-12 3(*4 * Result: Sometimes5 *6 * Demonstrate that a failing cmpxchg() operation does not act as a7 * full barrier. (In contrast, a successful cmpxchg() does act as a8 * full barrier.)9 *)10 11{}12 13P0(int *x, int *y, int *z)14{15 int r0;16 int r1;17 18 WRITE_ONCE(*x, 1);19 r1 = cmpxchg(z, 1, 0);20 r0 = READ_ONCE(*y);21}22 23P1(int *x, int *y, int *z)24{25 int r0;26 int r1;27 28 WRITE_ONCE(*y, 1);29 r1 = cmpxchg(z, 1, 0);30 r0 = READ_ONCE(*x);31}32 33locations[0:r1;1:r1]34exists (0:r0=0 /\ 1:r0=0)35