source: CIVL/examples/translation/pthread/dekker_true.cvl@ d87ec9c

/* Testcase from Threader's distribution. For details see:
   http://www.model.in.tum.de/~popeea/research/threader
*/
#include <civlc.h>
#include "pthread.h"
#define assert(e) if (!(e)) $assert($false);

int flag1 = 0, flag2 = 0; // boolean flags
$input int turn; // integer variable to hold the ID of the thread whose turn is it
$assume 0<=turn && turn<=1;
int turn1 = turn;
int x; // boolean variable to test mutual exclusion
void *thr1(void *arg) {
  flag1 = 1;
  while (flag2 >= 1) {
    if (turn1 != 0) {
      flag1 = 0;
      while (turn1 != 0) {};
      flag1 = 1;
    }
  }
  // begin: critical section
  x = 0;
  assert(x<=0);
  // end: critical section
  turn1 = 1;
  flag1 = 0;
  return NULL; //Added this, should be here or pthread_exit should be called
}

void *thr2(void *arg) {
  flag2 = 1;
  while (flag1 >= 1) {
    if (turn1 != 1) {
      flag2 = 0;
      while (turn1 != 1) {};
      flag2 = 1;
    }
  }
  // begin: critical section
  x = 1;
  assert(x>=1);
  // end: critical section
  turn1 = 1;
  flag2 = 0;
  return NULL; //Added this, should be here or pthread_exit should be called
}

int main(void) {
  pthread_t t1, t2;
  pthread_create(&t1, 0, thr1, 0);
  pthread_create(&t2, 0, thr2, 0);
  pthread_join(t1, 0);
  pthread_join(t2, 0);
  return 0;
}