1C MP+unlocklockonceonce+fencermbonceonce 2 3(* 4 * Result: Never 5 * 6 * If two locked critical sections execute on the same CPU, stores in the 7 * first must propagate to each CPU before stores in the second do, even if 8 * the critical sections are protected by different locks. 9 *) 10 11{} 12 13P0(spinlock_t *s, spinlock_t *t, int *x, int *y) 14{ 15 spin_lock(s); 16 WRITE_ONCE(*x, 1); 17 spin_unlock(s); 18 spin_lock(t); 19 WRITE_ONCE(*y, 1); 20 spin_unlock(t); 21} 22 23P1(int *x, int *y) 24{ 25 int r1; 26 int r2; 27 28 r1 = READ_ONCE(*y); 29 smp_rmb(); 30 r2 = READ_ONCE(*x); 31} 32 33exists (1:r1=1 /\ 1:r2=0) 34