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