bool x = false;
bool y = false;
int z = 0;

program p1:
void main(){
  x = true;
  if(!y)
  {
    /* Enter Critical Section */
    z = z + 1;
    nop;
    assert( z == 1);
    /* Leave Critical Section */
    atomic {x = false; z = z - 1;}
  }
}

program p2:
void main(){
  y = true;
  if(!x)
  {
    /* Enter Critical Section */
    z = z + 1;
    nop;
    assert(z == 1);
    /* Leave Critical Section */
    atomic {y = false; z = z - 1;}
  }	
}