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 r0 = READ_ONCE(*y); 19 WRITE_ONCE(*z, 1); 20 spin_unlock(mylock); 21} 22 23P2(int *x, int *z) 24{ 25 int r1; 26 27 WRITE_ONCE(*z, 2); 28 smp_mb(); 29 r1 = READ_ONCE(*x); 30} 31 32exists (1:r0=1 /\ z=2 /\ 2:r1=0) 33