1C ISA2+pooncelock+pooncelock+pombonce 2 3(* 4 * Result: Never 5 * 6 * This test shows that write-write ordering provided by locks 7 * (in P0() and P1()) is visible to external process P2(). 8 *) 9 10{} 11 12P0(int *x, int *y, spinlock_t *mylock) 13{ 14 spin_lock(mylock); 15 WRITE_ONCE(*x, 1); 16 WRITE_ONCE(*y, 1); 17 spin_unlock(mylock); 18} 19 20P1(int *y, int *z, spinlock_t *mylock) 21{ 22 int r0; 23 24 spin_lock(mylock); 25 r0 = READ_ONCE(*y); 26 WRITE_ONCE(*z, 1); 27 spin_unlock(mylock); 28} 29 30P2(int *x, int *z) 31{ 32 int r1; 33 int r2; 34 35 r2 = READ_ONCE(*z); 36 smp_mb(); 37 r1 = READ_ONCE(*x); 38} 39 40exists (1:r0=1 /\ 2:r2=1 /\ 2:r1=0) 41