C C-FR+w+w+w+reads.litmus

{
a=0;
}

P0(int *a)
{
	WRITE_ONCE(*a, 1);
}

P1(int *a)
{
	WRITE_ONCE(*a, 2);
}

P2(int *a)
{
	WRITE_ONCE(*a, 3);
}

P3(int *a)
{
	r1 = READ_ONCE(*a);
	r2 = READ_ONCE(*a);
	r3 = READ_ONCE(*a);
	r4 = READ_ONCE(*a);
}

exists
(3:r1=0 /\ 3:r2=1 /\ 3:r3=2 /\ 3:r4=3)