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