1C Z6.0+pooncelock+poonceLock+pombonce 2 3{} 4 5P0(int *x, int *y, spinlock_t *mylock) 6{ 7 spin_lock(mylock); 8 WRITE_ONCE(*x, 1); 9 WRITE_ONCE(*y, 1); 10 spin_unlock(mylock); 11} 12 13P1(int *y, int *z, spinlock_t *mylock) 14{ 15 int r0; 16 17 spin_lock(mylock); 18 smp_mb__after_spinlock(); 19 r0 = READ_ONCE(*y); 20 WRITE_ONCE(*z, 1); 21 spin_unlock(mylock); 22} 23 24P2(int *x, int *z) 25{ 26 int r1; 27 28 WRITE_ONCE(*z, 2); 29 smp_mb(); 30 r1 = READ_ONCE(*x); 31} 32 33exists (1:r0=1 /\ z=2 /\ 2:r1=0) 34