1C R+fencembonceonces 2 3(* 4 * Result: Never 5 * 6 * This is the fully ordered (via smp_mb()) version of one of the classic 7 * counterintuitive litmus tests that illustrates the effects of store 8 * propagation delays. Note that weakening either of the barriers would 9 * cause the resulting test to be allowed. 10 *) 11 12{} 13 14P0(int *x, int *y) 15{ 16 WRITE_ONCE(*x, 1); 17 smp_mb(); 18 WRITE_ONCE(*y, 1); 19} 20 21P1(int *x, int *y) 22{ 23 int r0; 24 25 WRITE_ONCE(*y, 2); 26 smp_mb(); 27 r0 = READ_ONCE(*x); 28} 29 30exists (y=2 /\ 1:r0=0) 31