int pendingIo = 1;
bool stopFlag = false;
bool stopEvent = false;
bool stopped = false;

program stopper:

void main()
{
	stopFlag = true;
	dec();
	
	assume(stopEvent);
	
	stopped = true;
}

void dec()
{
	int pio;

	atomic
	{
		pendingIo=pendingIo - 1;
		pio = pendingIo;
	}

	if(pio==0)
	{
		stopEvent = true;
	}
	else
	{
		nop;
	}
	
}

program adder: 

void main()
{
	int status;

	status = inc();
	if(status>0)
	{
		assert(!stopped);
		/* Perform IO */
	}
	else
	{
		nop;
	}

	dec();
}

int inc()
{
	if(stopFlag)
	{
		return 0;
	}
	else
	{
		nop;
	}
	
	atomic
	{
		pendingIo = pendingIo + 1;
	}

	return 1;
}

void dec()
{
	int pio;

	atomic
	{
		pendingIo=pendingIo - 1;
		pio = pendingIo;
	}

	if(pio==0)
	{
		stopEvent = true;
	}
	else
	{
		nop;
	}
	
}