source: CIVL/examples/verifyThisProblems/barrier2.cvl@ 22b4ef04

/* Barrier solution.
 * Got (1) but not (2).
 */
#include <civlc.cvh>
#include <stdlib.h>
#include <stdbool.h>
#include <stdio.h>

// the number of nodes... (tried with N=1,2,3)
$input int N = 3; // N=4 took 115 seconds

typedef struct _node {
  $proc p;
  struct _node *left, *right;
  struct _node *parent;
  _Bool sense;
  int version;
} *Node;

Node theNodes[N];
int count = 0;

// check all sensens in u and descendants are true...
void checkSensesTrue(Node u) {
  if (u != NULL) {
    $assert(u->sense);
    checkSensesTrue(u->left);
    checkSensesTrue(u->right);
  }
}

// the function a thread runs...
void thread(Node myNode) {

  // the barrier function
  void barrier() {
    $assert(!myNode->sense);

    // synchronization phase
    if (myNode->left != NULL)
      $when (myNode->left->sense);
    if (myNode->right != NULL)
      $when (myNode->right->sense);

    $atomic {
      myNode->sense = true;
      checkSensesTrue(myNode);
      myNode->version++;
      if (myNode->parent == NULL) {
        for (int i=0; i<N; i++)
          $assert(theNodes[i]->version == myNode->version);
      }
    }


    // wake-up phase
    if (myNode->parent == NULL) {
      myNode->sense = false;
    }

    $when (!myNode->sense);
    if (myNode->left != NULL)
      myNode->left->sense = false;
    if (myNode->right != NULL)
      myNode->right->sense = false;

    $assert(!myNode->sense);
  }

  //myNode->p = $self;
  // run around barrier 3 times...
  for (int i=0; i<3; i++) {
    barrier();
  }
}


Node makeTree(Node left, Node right) {
  Node result = (Node)malloc(sizeof(struct _node));

  result->left = left;
  result->right = right;
  result->sense = false;
  result->version = 0;
  if (left != NULL)
    left->parent = result;
  if (right != NULL)
    right->parent = result;
  result->parent = NULL;
  return result;
}


// create an arbitrary tree with numNodes nodes...
Node makeArbitraryTree(int numNodes) {
  printf("Entering makeArbitraryTree: numNodes = %d\n", numNodes);
  if (numNodes == 0)
    return NULL;

  // how many nodes in left sub-tree?
  // nondeterministically choose integer in range 0..numNodes-1.
  // total number of nodes = leftSize + rightSize + 1

  int leftSize = $choose_int(numNodes);

  printf("leftSize = %d\n", leftSize);
  $assert(leftSize >= 0);
  $assert(leftSize < numNodes);

  int rightSize = numNodes - (leftSize + 1);

  printf("rightSize = %d\n", rightSize);
  printf("numNodes = %d\n", numNodes);
  printf("\n");

  Node leftTree = makeArbitraryTree(leftSize);
  Node rightTree = makeArbitraryTree(numNodes - leftSize - 1);
  Node result = makeTree(leftTree, rightTree);

  theNodes[count] = result;
  count++;
  return result;
}

// compute number of nodes in tree...
int sizeOfTree(Node tree) {
  if (tree == NULL)
    return 0;

  int result = 1 + sizeOfTree(tree->left) + sizeOfTree(tree->right);

  return result;  
}

// free all nodes in the tree...
void freeTree(Node tree) {
  if (tree != NULL) {
    freeTree(tree->left);
    freeTree(tree->right);
    free(tree);
  }
}


int main() {
  Node theTree = makeArbitraryTree(N);

  $atomic {
    // sanity check...
    $assert(sizeOfTree(theTree) == N);
    $assert(count == N);
    for (int i=0; i<N; i++)
      $assert(theNodes[i] != NULL);
    for (int i=0; i<N; i++) {
      $proc p = $spawn thread(theNodes[i]);

      theNodes[i]->p = p;
    }
  }
  // now the procs are running, wait for them all to terminate...
  for (int i=0; i<N; i++)
    $wait(theNodes[i]->p);
  freeTree(theTree);
}