0001 C IRIW+fencembonceonces+OnceOnce
0002
0003 (*
0004 * Result: Never
0005 *
0006 * Test of independent reads from independent writes with smp_mb()
0007 * between each pairs of reads. In other words, is smp_mb() sufficient to
0008 * cause two different reading processes to agree on the order of a pair
0009 * of writes, where each write is to a different variable by a different
0010 * process? This litmus test exercises LKMM's "propagation" rule.
0011 *)
0012
0013 {}
0014
0015 P0(int *x)
0016 {
0017 WRITE_ONCE(*x, 1);
0018 }
0019
0020 P1(int *x, int *y)
0021 {
0022 int r0;
0023 int r1;
0024
0025 r0 = READ_ONCE(*x);
0026 smp_mb();
0027 r1 = READ_ONCE(*y);
0028 }
0029
0030 P2(int *y)
0031 {
0032 WRITE_ONCE(*y, 1);
0033 }
0034
0035 P3(int *x, int *y)
0036 {
0037 int r0;
0038 int r1;
0039
0040 r0 = READ_ONCE(*y);
0041 smp_mb();
0042 r1 = READ_ONCE(*x);
0043 }
0044
0045 exists (1:r0=1 /\ 1:r1=0 /\ 3:r0=1 /\ 3:r1=0)
