source: CIVL/include/impls/concurrency.cvl@ 1aaefd4

/* This file completes the definitions of types and some functions
 * for concurrency, which are declared in concurrency.cvh.
 */
 
#ifndef __CIVLC_CONCURRENCY__
#define __CIVLC_CONCURRENCY__
#include<civlc.cvh>
#include<concurrency.cvh>
#include<seq.cvh>
#pragma CIVL ACSL
/* *********************** Types *********************** */

/* A data type representing a global barrier which must be operated by local
 * barriers.  Completes the declaration of this type in civlc-common.h.
 */
struct _gbarrier {
  int nprocs;
  $proc proc_map[]; // initialized as all $proc_null.
  _Bool in_barrier[]; // initialized as all false.
  int num_in_barrier; // initialized as 0.
};

/* A data type representing a global barrier which used for 
 * operating global barriers. The local barrier type has 
 * a handle of a global barrier.
 * Completes the declaration of this type in civlc-common.h.
 */
struct _barrier {
  int place;
  $gbarrier gbarrier; // initialized as 0.
};

/* *********************** Functions *********************** */

/*@ depends_on \access(barrier);
  @ executes_when \true;
  @ */ 
$atomic_f void $barrier_enter($barrier barrier, int nprocs, void foo(void)){
  $gbarrier gbarrier=barrier->gbarrier;
  int myplace=barrier->place;

  $assert(!gbarrier->in_barrier[myplace],
          "the barrier of has already been entered with the place %d",
          myplace);
  gbarrier->in_barrier[barrier->place]=$true;
  if(gbarrier->nprocs < nprocs){
        nprocs = gbarrier->nprocs;
  }
  if(++gbarrier->num_in_barrier == nprocs){
    foo();
    for(int i=0; i<gbarrier->nprocs; i++)
      gbarrier->in_barrier[i]=$false;
    gbarrier->num_in_barrier=0;
  }
}

/*@ depends_on \access(barrier);
  @ executes_when \true;
  @ */ 
$atomic_f void $barrier_enter_simple($barrier barrier) {
  $gbarrier gbarrier=barrier->gbarrier;
  int myplace=barrier->place, nprocs = gbarrier->nprocs;

  $assert(!gbarrier->in_barrier[myplace],
          "the barrier of has already been entered with the place %d",
          myplace);
  gbarrier->in_barrier[myplace] = $true;
  if (++gbarrier->num_in_barrier == nprocs) {
    for(int i=0; i<nprocs; i++)
      gbarrier->in_barrier[i] = $false;
    gbarrier->num_in_barrier = 0;
  }
}

/*@ depends_on \access(barrier);
  @ */
$atomic_f void $barrier_exit($barrier barrier) {
  $when(!barrier->gbarrier->in_barrier[barrier->place]);
}

void $barrier_call($barrier barrier) {
  $barrier_enter_simple(barrier);
  $barrier_exit(barrier);
}

void $barrier_call_yield($barrier barrier) {
  $barrier_enter_simple(barrier);
  $yield();
  $barrier_exit(barrier);
}


void $barrier_call_subset($barrier barrier, int nprocs){
  void empty_func(){}
  $barrier_enter(barrier, nprocs, empty_func);
  $barrier_exit(barrier);
}

void $barrier_call_execute($barrier barrier, void foo(void)){
  $barrier_enter(barrier, barrier->gbarrier->nprocs, foo);
  $barrier_exit(barrier);
}

$atomic_f $gbarrier $gbarrier_create($scope scope, int size){
  $gbarrier gbarrier = ($gbarrier)$malloc(scope, sizeof(struct _gbarrier));

  gbarrier->nprocs=size;
  gbarrier->proc_map=($proc[size])$lambda(int i) $proc_null;
  gbarrier->in_barrier=(_Bool[size])$lambda(int i) $false;
  gbarrier->num_in_barrier=0;
  return gbarrier;
}

$atomic_f void $gbarrier_destroy($gbarrier gbarrier){
  $free(gbarrier);
}

int $get_nprocs($gbarrier gbarrier){
  return gbarrier->nprocs;
}

$atomic_f $barrier $barrier_create($scope scope, $gbarrier gbarrier, int place){
  $assert(gbarrier->proc_map[place]==$proc_null,
          "the place %d in the global barrier has already been taken.", place);

  $barrier barrier=($barrier)$malloc(scope, sizeof(struct _barrier));

  barrier->place=place;
  barrier->gbarrier=gbarrier;
  gbarrier->proc_map[place]=$self;
  return barrier;
}

$atomic_f void $barrier_destroy($barrier barrier) {
  $free(barrier);
}

#endif