| C MP+unlocklockonceonce+fencermbonceonce |
| |
| (* |
| * Result: Never |
| * |
| * If two locked critical sections execute on the same CPU, stores in the |
| * first must propagate to each CPU before stores in the second do, even if |
| * the critical sections are protected by different locks. |
| *) |
| |
| {} |
| |
| P0(spinlock_t *s, spinlock_t *t, int *x, int *y) |
| { |
| spin_lock(s); |
| WRITE_ONCE(*x, 1); |
| spin_unlock(s); |
| spin_lock(t); |
| WRITE_ONCE(*y, 1); |
| spin_unlock(t); |
| } |
| |
| P1(int *x, int *y) |
| { |
| int r1; |
| int r2; |
| |
| r1 = READ_ONCE(*y); |
| smp_rmb(); |
| r2 = READ_ONCE(*x); |
| } |
| |
| exists (1:r1=1 /\ 1:r2=0) |
