39 lines · plain
1C WRC+pooncerelease+fencermbonceonce+Once2 3(*4 * Result: Never5 *6 * This litmus test is an extension of the message-passing pattern, where7 * the first write is moved to a separate process. Because it features8 * a release and a read memory barrier, it should be forbidden. More9 * specifically, this litmus test is forbidden because smp_store_release()10 * is A-cumulative in LKMM.11 *)12 13{}14 15P0(int *x)16{17 WRITE_ONCE(*x, 1);18}19 20P1(int *x, int *y)21{22 int r0;23 24 r0 = READ_ONCE(*x);25 smp_store_release(y, 1);26}27 28P2(int *x, int *y)29{30 int r0;31 int r1;32 33 r0 = READ_ONCE(*y);34 smp_rmb();35 r1 = READ_ONCE(*x);36}37 38exists (1:r0=1 /\ 2:r0=1 /\ 2:r1=0)39