#define PASSES 10

bit flip = 0;
bit ctr[2];
byte passctr = 0;

proctype rdr()
{
	bit lcl_flip;
	bit both;

	do
	:: passctr < PASSES ->
		lcl_flip = flip;
		/* need smp_read_barrier_depends() */
		ctr[lcl_flip]++;
		/* need smp_mb__after_atomic_inc() */
		if
		:: lcl_flip == flip ->
			both = 0
		:: else ->
			ctr[!lcl_flip]++;
			/* need smp_mb__after_atomic_inc() */
			both = 1
		fi;
		passctr++;
		passctr++;
		/* need smp_mb__before_atomic_dec() */
		ctr[lcl_flip]--;
		if
		:: both ->
			ctr[!lcl_flip]--;
		:: else -> skip
		fi;
	:: passctr >= PASSES ->
		break
	od
}

proctype upd()
{
	byte lcl_passctr;

	do
	::	passctr < PASSES ->
		lcl_passctr = passctr;
		if
		::	lcl_passctr / 2 * 2 == lcl_passctr ->
			lcl_passctr = 255
		::	else -> skip
		fi;
		do
		::	ctr[!flip] == 0 -> break
		::	true -> skip
		od;
		/* Need smp_mb()? */
		flip = !flip;
		/* Need smp_mb()? */
		do
		::	ctr[!flip] == 0 -> break
		::	true -> skip
		od;
		assert(lcl_passctr != passctr);
	::	passctr >= PASSES ->
		break
	od
}

init {
	atomic {
		ctr[0] = 0;
		ctr[1] = 0;
		run rdr();
		run upd();
	}
}