1C MP+polocks 2 3{} 4 5P0(int *x, int *y, spinlock_t *mylock) 6{ 7 WRITE_ONCE(*x, 1); 8 spin_lock(mylock); 9 WRITE_ONCE(*y, 1); 10 spin_unlock(mylock); 11} 12 13P1(int *x, int *y, spinlock_t *mylock) 14{ 15 int r0; 16 int r1; 17 18 spin_lock(mylock); 19 r0 = READ_ONCE(*y); 20 spin_unlock(mylock); 21 r1 = READ_ONCE(*x); 22} 23 24exists (1:r0=1 /\ 1:r1=0) 25