40 lines · plain
1C ISA2+pooncerelease+poacquirerelease+poacquireonce2 3(*4 * Result: Never5 *6 * This litmus test demonstrates that a release-acquire chain suffices7 * to order P0()'s initial write against P2()'s final read. The reason8 * that the release-acquire chain suffices is because in all but one9 * case (P2() to P0()), each process reads from the preceding process's10 * write. In memory-model-speak, there is only one non-reads-from11 * (AKA non-rf) link, so release-acquire is all that is needed.12 *)13 14{}15 16P0(int *x, int *y)17{18 WRITE_ONCE(*x, 1);19 smp_store_release(y, 1);20}21 22P1(int *y, int *z)23{24 int r0;25 26 r0 = smp_load_acquire(y);27 smp_store_release(z, 1);28}29 30P2(int *x, int *z)31{32 int r0;33 int r1;34 35 r0 = smp_load_acquire(z);36 r1 = READ_ONCE(*x);37}38 39exists (1:r0=1 /\ 2:r0=1 /\ 2:r1=0)40