30 lines · plain
1C LB+poacquireonce+pooncerelease2 3(*4 * Result: Never5 *6 * Does a release-acquire pair suffice for the load-buffering litmus7 * test, where each process reads from one of two variables then writes8 * to the other?9 *)10 11{}12 13P0(int *x, int *y)14{15 int r0;16 17 r0 = READ_ONCE(*x);18 smp_store_release(y, 1);19}20 21P1(int *x, int *y)22{23 int r0;24 25 r0 = smp_load_acquire(y);26 WRITE_ONCE(*x, 1);27}28 29exists (0:r0=1 /\ 1:r0=1)30