1C cmpxchg-fail-unordered-1 2 3(* 4 * Result: Sometimes 5 * 6 * Demonstrate that a failing cmpxchg() operation does not act as a 7 * full barrier. (In contrast, a successful cmpxchg() does act as a 8 * 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