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

program stopper:

void main()
{
	int dec1_pio;
	stopFlag = true;
	
	atomic
	{
		pendingIo=pendingIo - 1;
		dec1_pio = pendingIo;
	}
	
	if(dec1_pio==0)
	{
		stopEvent = true;
	}

	assume(stopEvent);
	
	stopped = true;
}

program adder1: 

void main()
{
	int inc1_status;
	int dec1_pio;
	int dec2_pio;
	int status;

	atomic
	{
		pendingIo = pendingIo + 1;
	}

	if(stopFlag)
	{
		atomic
		{
			pendingIo=pendingIo - 1;
			dec2_pio = pendingIo;
		}

		if(dec2_pio==0)
		{
			stopEvent = true;
		}

		inc1_status = 0;
	}
	else
	{
		inc1_status = 1;
	}

	status = inc1_status;

	if(status>0)
	{
		assert(!stopped);
		/* Perform IO */
		atomic
		{
			pendingIo=pendingIo - 1;
			dec1_pio = pendingIo;
		}

		if(dec1_pio==0)
		{
			stopEvent = true;
		}
	}
}

program adder2: 

void main()
{
	int inc1_status;
	int dec1_pio;
	int dec2_pio;
	int status;

	atomic
	{
		pendingIo = pendingIo + 1;
	}

	if(stopFlag)
	{
		atomic
		{
			pendingIo=pendingIo - 1;
			dec2_pio = pendingIo;
		}

		if(dec2_pio==0)
		{
			stopEvent = true;
		}

		inc1_status = 0;
	}
	else
	{
		inc1_status = 1;
	}

	status = inc1_status;

	if(status>0)
	{
		assert(!stopped);
		/* Perform IO */
		atomic
		{
			pendingIo=pendingIo - 1;
			dec1_pio = pendingIo;
		}

		if(dec1_pio==0)
		{
			stopEvent = true;
		}
	}
}