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