1C IRIW+fencembonceonces+OnceOnce 2 3(* 4 * Result: Never 5 * 6 * Test of independent reads from independent writes with smp_mb() 7 * between each pairs of reads. In other words, is smp_mb() sufficient to 8 * cause two different reading processes to agree on the order of a pair 9 * of writes, where each write is to a different variable by a different 10 * 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