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 spinlock_t mylock; 12 int x; 13 int y; 14 int z; 15} 16 17P0(int *x, int *y, spinlock_t *mylock) 18{ 19 spin_lock(mylock); 20 WRITE_ONCE(*x, 1); 21 WRITE_ONCE(*y, 1); 22 spin_unlock(mylock); 23} 24 25P1(int *y, int *z, spinlock_t *mylock) 26{ 27 int r0; 28 29 spin_lock(mylock); 30 r0 = READ_ONCE(*y); 31 WRITE_ONCE(*z, 1); 32 spin_unlock(mylock); 33} 34 35P2(int *x, int *z) 36{ 37 int r1; 38 int r2; 39 40 r2 = READ_ONCE(*z); 41 smp_mb(); 42 r1 = READ_ONCE(*x); 43} 44 45exists (1:r0=1 /\ 2:r2=1 /\ 2:r1=0) 46