C C-locktest.litmus

{
}

P0(int *x, int *l)
{
	int r1;
	int r2;

	r1 = xchg_acquire(l, 1);
	r2 = READ_ONCE(*x);
	WRITE_ONCE(*x, 1);
	WRITE_ONCE(*x, 0);
	smp_store_release(l, 0);
}

P1(int *x, int *l)
{
	int r1;
	int r2;

	r1 = xchg_acquire(l, 1);
	r2 = READ_ONCE(*x);
	WRITE_ONCE(*x, 1);
	WRITE_ONCE(*x, 0);
	smp_store_release(l, 0);
}

locations [0:r1;1:r1]
filter (0:r1=0 /\ 1:r1=0)
exists (0:r2=1 \/ 1:r2=1)