1C LB+poacquireonce+pooncerelease 2 3(* 4 * Result: Never 5 * 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 8 * to the other? 9 *) 10 11{ 12 int x; 13 int y; 14} 15 16P0(int *x, int *y) 17{ 18 int r0; 19 20 r0 = READ_ONCE(*x); 21 smp_store_release(y, 1); 22} 23 24P1(int *x, int *y) 25{ 26 int r0; 27 28 r0 = smp_load_acquire(y); 29 WRITE_ONCE(*x, 1); 30} 31 32exists (0:r0=1 /\ 1:r0=1) 33