1C cmpxchg-fail-unordered-2 2 3(* 4 * Result: Sometimes 5 * 6 * Demonstrate that a failing cmpxchg() operation does not act as either 7 * an acquire release operation. (In contrast, a successful cmpxchg() 8 * does act as both an acquire and a release operation.) 9 *) 10 11{} 12 13P0(int *x, int *y) 14{ 15 int r1; 16 17 WRITE_ONCE(*x, 1); 18 r1 = cmpxchg(y, 0, 1); 19} 20 21P1(int *x, int *y) 22{ 23 int r1; 24 int r2; 25 26 r1 = cmpxchg(y, 0, 1); 27 r2 = READ_ONCE(*x); 28} 29 30exists (0:r1=0 /\ 1:r1=1 /\ 1:r2=0) 31