28 lines · plain
1C S+fencewmbonceonce+poacquireonce2 3(*4 * Result: Never5 *6 * Can a smp_wmb(), instead of a release, and an acquire order a prior7 * store against a subsequent store?8 *)9 10{}11 12P0(int *x, int *y)13{14 WRITE_ONCE(*x, 2);15 smp_wmb();16 WRITE_ONCE(*y, 1);17}18 19P1(int *x, int *y)20{21 int r0;22 23 r0 = smp_load_acquire(y);24 WRITE_ONCE(*x, 1);25}26 27exists (x=2 /\ 1:r0=1)28