source: CIVL/examples/concurrency/dining.cvl@ 23207c6

/* Dining philosophers with fork switching. Even philosophers pick
 * up left fork first, odd pick up right first.  This breaks deadlock.
 *
 *       civl verify -inputB=4 dining.cvl
 */
#include <civlc.h>

$input int B; // upper bound on number of philosophers
$input int n; // number of philosophers
$assume 2<=n && n<=B;

// Each fork will be on the table (0) or in a hand (1).
int forks[n];

void dine(int id) {
  int left = id;
  int right = (id + 1) % n;

  $atomic{
  while (1) {
    if (id % 2 == 0) {
      $when (forks[left] == 0) {forks[left] = 1;}
      $when (forks[right] == 0) {forks[right] = 1;}
      forks[right] = 0;
      forks[left] = 0;
    } else {
      $when (forks[right] == 0) {forks[right] = 1;}
      $when (forks[left] == 0) {forks[left] = 1;}
      forks[right] = 0;
      forks[left] = 0;
    }
  }}
}

/* Put all forks on the table. */
void init() {
  for (int i = 0; i < n; i++) forks[i] = 0;
}

void main() {
  $proc philosophers[n];
  $atomic{
  init();
  for (int i = 0; i < n; i++)
    philosophers[i] = $spawn dine(i);}
  $atomic{
  for (int i = 0; i < n; i++)
    $wait philosophers[i];}
}