1 C LB+poacquireonce+pooncerelease
6 * Does a release-acquire pair suffice for the load-buffering litmus
7 * test, where each process reads from one of two variables then writes
18 smp_store_release(y, 1);
25 r0 = smp_load_acquire(y);
29 exists (0:r0=1 /\ 1:r0=1)