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 int x; 14 int y; 15} 16 17P0(int *x, int *y) 18{ 19 WRITE_ONCE(*x, 1); 20 smp_mb(); 21 WRITE_ONCE(*y, 1); 22} 23 24P1(int *x, int *y) 25{ 26 int r0; 27 28 WRITE_ONCE(*y, 2); 29 smp_mb(); 30 r0 = READ_ONCE(*x); 31} 32 33exists (y=2 /\ 1:r0=0) 34