source: CIVL/examples/por/trade4.cvl

#include<civlc.cvh>

/* A deadlock should be possible in this program as follows:
 * p1: x=1, then blocks at $when(x==2), losing atomic lock.
 * p2: $when(x==1); x=2, x=4; terminates.
 * at this point p1 is blocked, as is main.
 */

int x=0;

void p1() {
  $atomic {
    x=1;
    $when(x==2);
    x=3;
  }
}

void p2() {
  $when(x==1);
  x=2;
  x=4;
}

void main() {
  $proc proc1 = $spawn p1();
  $proc proc2 = $spawn p2();

  $wait(proc1);
  $wait(proc2);
  $assert((x==4)); // false
}