0001 C LB+poacquireonce+pooncerelease
0002
0003 (*
0004 * Result: Never
0005 *
0006 * Does a release-acquire pair suffice for the load-buffering litmus
0007 * test, where each process reads from one of two variables then writes
0008 * to the other?
0009 *)
0010
0011 {}
0012
0013 P0(int *x, int *y)
0014 {
0015 int r0;
0016
0017 r0 = READ_ONCE(*x);
0018 smp_store_release(y, 1);
0019 }
0020
0021 P1(int *x, int *y)
0022 {
0023 int r0;
0024
0025 r0 = smp_load_acquire(y);
0026 WRITE_ONCE(*x, 1);
0027 }
0028
0029 exists (0:r0=1 /\ 1:r0=1)
