C auto/C-RW-G+RW-R-relacq
{
}

P0(int *x0, int *x1, int *gpstart01, int *csend01)
{
	r1 = READ_ONCE(*x0);
	smp_mb();
	smp_store_release(gpstart01, 1);
	smp_mb();
	r60101 = smp_load_acquire(csend01);
	smp_mb();
	WRITE_ONCE(*x1, 1);
}


P1(int *x0, int *x1, int *gpstart01, int *csend01)
{
	r50101 = smp_load_acquire(gpstart01);
	r1 = READ_ONCE(*x1);
	WRITE_ONCE(*x0, 1);
	smp_store_release(csend01, 1);
}

exists ( (0:r1=1 /\ 1:r1=1)
 /\ (1:r50101=1 \/ 0:r60101=1) )