source: CIVL/examples/concurrency/barrier4.cvl

/* Using the concurrency.cvh library's barrier inside atomic block.
 *      civl verify -inputB=4 barrier.cvl
 */
#include <concurrency.cvh>

$input int B = 4; // upper bound on number of threads
$input int N;     // number of threads
$assume(1<=N && N<=B);
int counter = 0; // shared variable used to test barrier
$scope root = $here;
$gbarrier gbarrier;

void run(int tid) {
  $barrier barrier = $barrier_create(root, gbarrier, tid); 
  
  $atomic {
    while ($true) {
      $assert(counter == 0);
      $barrier_call_yield(barrier);
      counter++;
      $barrier_call_yield(barrier);
      $assert(counter == N);
      $barrier_call_yield(barrier);
      counter--;
      $barrier_call_yield(barrier);
    }
  }
  $barrier_destroy(barrier);
}

void main() {
  gbarrier = $gbarrier_create(root, N);
  $parfor(int i: 0 .. N-1)
    run(i);
  $gbarrier_destroy(gbarrier);
}