46 lines · plain
1C IRIW+fencembonceonces+OnceOnce2 3(*4 * Result: Never5 *6 * Test of independent reads from independent writes with smp_mb()7 * between each pairs of reads. In other words, is smp_mb() sufficient to8 * cause two different reading processes to agree on the order of a pair9 * of writes, where each write is to a different variable by a different10 * process? This litmus test exercises LKMM's "propagation" rule.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 int r1;24 25 r0 = READ_ONCE(*x);26 smp_mb();27 r1 = READ_ONCE(*y);28}29 30P2(int *y)31{32 WRITE_ONCE(*y, 1);33}34 35P3(int *x, int *y)36{37 int r0;38 int r1;39 40 r0 = READ_ONCE(*y);41 smp_mb();42 r1 = READ_ONCE(*x);43}44 45exists (1:r0=1 /\ 1:r1=0 /\ 3:r0=1 /\ 3:r1=0)46