34 lines · plain
1C MP+unlocklockonceonce+fencermbonceonce2 3(*4 * Result: Never5 *6 * If two locked critical sections execute on the same CPU, stores in the7 * first must propagate to each CPU before stores in the second do, even if8 * 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