C C-locktest.litmus

{
}

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

	r1 = xchg_acquire(l, 1);
	if (r1 == 0) {
		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);
	if (r1 == 0) {
		r2 = READ_ONCE(*x);
		WRITE_ONCE(*x, 1);
		WRITE_ONCE(*x, 0);
		smp_store_release(l, 0);
	}
}

exists
((0:r1=0 /\ 0:r2=1) \/ (1:r1 = 0 /\ 1:r2=1))