source: CIVL/include/impls/civl-omp2.cvl@ 1aaefd4

// civlc-omp.cvl: implementations of functions and types in civlc-omp.cvh
#include<civl-omp.cvh>
#include<civlc.cvh>
#include<pointer.cvh>
#include<seq.cvh>
#include<concurrency.cvh>
#include<domain.cvh>

/* Completes the definition of struct OMP_gshared given in civlc-omp.cvh.
 */
struct OMP_gshared {
  int nthreads;
  _Bool init[]; // which threads have joined
  $omp_shared shares[];
  void * original; // pointer to original variable
};

/* Completes the definition of struct OMP_shared given in civlc-omp.cvh.
 */
struct OMP_shared {
  $omp_gshared gshared;
  /* The thread id */
  int tid;
  /* Pointer to the local copy of the shared variable.
   * This provides the thread's "private view" of the variable. */
  void * local;
  /* Pointer to the local status variable */
  void * status;
};

/* Completes the definition of struct OMP_work_record
 * given in civlc-omp.cvh. */
struct OMP_work_record {
  int kind; // loop, barrier, sections, or single
  int location; // location in model of construct
  _Bool arrived; // has this thread arrived yet?
  $domain loop_domain; // full loop domain; null if not loop
  $domain subdomain; // tasks this thread must do
  // reduction operation?
};

struct OMP_gteam {
  /* scope in which data is allocated in heap */
  $scope scope;
  /* number of threads in team */
  int nthreads;
  /* which threads have joined this gteam */
  _Bool init[];
  /* work queues.  Length nthreads. For each thread,
   * a FIFO queue of work records */
  /* work queues. Width nthreads. For each worksharing region,
   * one entry of size nthreads is added. */
  $omp_work_record work[][];
  /* the shared object data. */
  $omp_gshared shared[];
  $gbarrier gbarrier;
};

struct OMP_team {
  $omp_gteam gteam;
  $scope scope;
  int tid;
  $omp_shared shared[];
  $barrier barrier;
};


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

$atomic $omp_gteam $omp_gteam_create($scope scope, int nthreads)
$depends {$nothing}
$reads {$nothing}
{
  //$omp_work_record empty[];
  $omp_gteam result = ($omp_gteam)$malloc(scope, sizeof(struct OMP_gteam));
  _Bool f = $false;

  //$seq_init(&empty, 0, NULL);
  result->scope = scope;
  result->nthreads = nthreads;
  $seq_init(&result->init, nthreads, &f);
  $seq_init(&result->work, 0, NULL);
  $seq_init(&result->shared, 0, NULL);
  result->gbarrier = $gbarrier_create(scope, nthreads);
  return result;
}


$fatomic void $omp_gteam_destroy($omp_gteam gteam)
$depends {$access(*gteam)}
$assigns {*gteam}
{
  int length = $seq_length(&gteam->work);
  
  $assert(length == 0, "There are still %d queued worksharing events.", length);
  $free(gteam->gbarrier);
  $free(gteam);
}

/* creates new local team object for a specific thread. */
$fatomic $omp_team $omp_team_create($scope scope, $omp_gteam gteam, int tid)
$depends {$nothing}
{
  $omp_team result = ($omp_team)$malloc(scope, sizeof(struct OMP_team));

  $assert(!gteam->init[tid], "Thread %d has already joined gteam",
          tid);
  gteam->init[tid] = $true;
  result->gteam = gteam;
  result->scope = scope;
  result->tid = tid;
  $seq_init(&result->shared, 0, NULL);
  result->barrier = $barrier_create(scope, gteam->gbarrier, tid);
  $read_set_push();
  $write_set_push();
  return result;
}

/* destroys the local team object */
$fatomic void $omp_team_destroy($omp_team team)
$depends {$access(*team)}
$assigns {*team}
{
  $read_set_pop();
  $write_set_pop();
  /*int numShared = $seq_length(&team->shared);

  for(int i = 0; i < numShared; i++){
    $free(team->shared[i]);
    }*/
  $free(team->barrier);
  $free(team);
}

/* creates new global shared object, associated to the given
 * global team. A pointer to the shared variable that this
 * object corresponds to is given.
 */
$fatomic $omp_gshared $omp_gshared_create($omp_gteam gteam,
                                 void *original)
$depends {$nothing}
$reads {$nothing}
{
  $omp_gshared result =
    ($omp_gshared)$malloc(gteam->scope, sizeof(struct OMP_gshared));
  _Bool f = $false;
  $omp_shared null = NULL;

  result->nthreads = gteam->nthreads;
  $seq_init(&result->init, gteam->nthreads, &f);
  result->original = original;
  $seq_init(&result->shares, gteam->nthreads, &null);
  //result->status = status;
  return result;
}

/* destroys the global shared object, copying the content
 * to the original variable.
 */
$fatomic void $omp_gshared_destroy($omp_gshared gshared)
$depends {$access(*gshared)}
$assigns {*gshared}
{
  $free(gshared);
}

$fatomic $omp_shared $omp_shared_create($omp_team team,
                               $omp_gshared gshared, void *local, void *status)
$depends {$nothing}
$reads {$nothing}
{
  $omp_shared result =
    ($omp_shared)$malloc(team->scope, sizeof(struct OMP_shared));
  //void *statusRefs[];
  //int numStatusRefs;
  int sharedLength;

  $assert(!gshared->init[team->tid], "Thread %d has already created its local copy for %p.\n", 
    team->tid, gshared);
  result->gshared = gshared;
  result->tid = team->tid;
  result->local = local;
  // copies the shared data to the local copy
  $copy(local, gshared->original);
  result->status = status;
  // set all leaf nodes of status to FULL
  $set_leaf_nodes(status, FULL);
  //$leaf_node_ptrs(&statusRefs, status);
  //numStatusRefs = $seq_length(&statusRefs);
  //for(int i = 0; i < numStatusRefs; i++)
    //*((int*)(statusRefs[i])) = FULL;
  sharedLength = $seq_length(&team->shared);
  $seq_insert(&team->shared, sharedLength, &result, 1);
  //$seq_append(&team->shared, &result, 1);
  gshared->shares[team->tid] = result;
  return result;
}

$fatomic void $omp_shared_destroy($omp_shared shared)
$depends {$access(*shared)}
$assigns {*shared}
{
  $free(shared);
}

// returns the id of the thread that has some unflushed modification to
// the shared object
// shared->gshared->shares[*]->status(ref): only the specific reference matters
int $omp_modified_tid($omp_shared shared, void *ref)
  $reads {shared->tid, shared->gshared->shares[*]->status}
{
  int tid = shared->tid;
  $omp_gshared gshared = shared->gshared;
  int nthreads = gshared->nthreads;
  _Bool isIdentityRef = $is_identity_ref(ref);
  
  for(int i=0; i < nthreads;i++){
    if(i == tid)
      continue;
    else{
      $omp_shared other = gshared->shares[i];
      $omp_var_status other_status;
      _Bool hasModified = $false;

      if(!$is_valid_pointer(other))
        continue;
      if(isIdentityRef){
        hasModified = $has_leaf_node_equal_to(other->status, MODIFIED);
      }else{
        int *other_status_ref = (int*)$translate_ptr(ref, other->status);

        hasModified = ((*other_status_ref) == MODIFIED);
      }
      if(hasModified)
        return i;
    }
  }
  return -1;
}

$fatomic void $omp_read($omp_shared shared, void *result, void *ref)
$depends {$access(*result), $access(*ref), $write(*(shared->status), *(shared->gshared->original))}
$assigns {*result, *ref}//over-approximation, possibly assigns *ref.
$reads {*(shared->status), *(shared->gshared->original)}
{
  int otherTid = $omp_modified_tid(shared, ref);

  $assert(otherTid < 0,
    "Thread %d can't perform $omp_read because thread %d has written to the same variable and hasn't flushed yet.\n",
    shared->tid, otherTid);
  if($is_identity_ref(ref)){
    if($leaf_nodes_equal_to(shared->status, EMPTY)){
      $copy(ref, shared->gshared->original); // copy shared to local
      $set_leaf_nodes(shared->status, FULL);
    }
  }else{
    int *status_ref = (int*)$translate_ptr(ref, shared->status);
    int status = *status_ref;

    if(status == EMPTY){
      void *global = $translate_ptr(ref, shared->gshared->original);
 
      $copy(ref, global); // copy shared to local
      *status_ref = FULL; // set status to FULL
    }
  }
  // read local
  $copy(result, ref);
}

$fatomic void $omp_write($omp_shared shared, void *ref, void *value)
$depends 
{
  int otherTid = $omp_modified_tid(shared, ref);

  $assert(otherTid < 0, "Thread %d can't perform $omp_write because thread %d has written to the same variable and hasn't flushed yet.\n",
    shared->tid, otherTid);
  $copy(ref, value);
  if($is_identity_ref(ref)){
     $set_leaf_nodes(shared->status, MODIFIED);
  }else{
    int *status_ref = (int*)$translate_ptr(ref, shared->status);
    *status_ref = MODIFIED;
  }
}

/* Only applicable to scalar type? */
void $omp_apply_assoc($omp_shared shared,
                      $operation op,
                      void *local){
  $atomic {
    void *shared_ref = $translate_ptr(local, shared->gshared->original);
    
    $apply(shared_ref, op, local, shared_ref);
  }
}

void $omp_flush($omp_shared shared, void *ref) {
  // need to drill down into all leaf nodes of the object
  // being flushed...
  // also, it should be ok to flush a memory unit if you are not
  // the owner but you also have no reads or writes to that variable
  // TODO: assert there is at most one thread for which this memory unit has status MODIFIED;
  $omp_gshared gshared = shared->gshared;
  int tid = shared->tid;
  void *refs[];
  int numRefs;
  
  // get all leaf node pointers
  $leaf_node_ptrs(&refs, ref);
  numRefs = $seq_length(&refs);
  for(int i = 0; i < numRefs; i++){
    void *leaf = refs[i];
    int *leaf_status = (int *)$translate_ptr(leaf, shared->status);
    //void *leaf_local = (int *)$translate_ptr(leaf, shared->local);
    void *leaf_shared = (int *)$translate_ptr(leaf, gshared->original);
    
    switch(*leaf_status){
      case EMPTY:
        break;
      case MODIFIED:
        $copy(leaf_shared, leaf);
      case FULL:
        *leaf_status = EMPTY;
        $set_default(leaf);
        break;
    }
  }
}

void $omp_flush_all($omp_team team) {
   int num_shared = $seq_length(&team->shared);

   for (int i=0; i<num_shared; i++) {
     $omp_shared shared = team->shared[i];
     
     $omp_flush(shared, shared->local);
   }
}

void $omp_barrier($omp_team team){
  $barrier_call(team->barrier);
}

void $omp_barrier_and_flush($omp_team team) {
  $read_set_pop();
  $write_set_pop();
  // this is a collective operation: all members of team call
  $barrier_call(team->barrier);
  $omp_flush_all(team);
  $barrier_call(team->barrier);
  $read_set_push();
  $write_set_push();
}

/**
 * performs the checking of workrecords when the last thread arrives the workshared region,
 * including:
 * number of workrecords in the entry should be nthreads
 * all workrecords are arrived
 * all workrecords have the same location as specified
 * all workrecords are of the same kind
 */
void $omp_check_workrecords($omp_gteam gteam, int location, $omp_worksharing_kind kind, int index){
  int nthreads = gteam->nthreads;
  int numWorkrecords;
  
  numWorkrecords = $seq_length(&gteam->work[index]);
  $assert(numWorkrecords == nthreads, "The %d-th workshared entry has length %d while the expected length should be %d.", index, numWorkrecords, nthreads);
  for(int i = 0; i < nthreads; i++){
    $omp_work_record workrecord = gteam->work[index][i];

    $assert(workrecord.arrived, "The workshared event of location %d for thread %d hasn't been arrived yet.",
            location, i);
    $assert(workrecord.location == location, "Wrong workshared location of thread %d: expected %d, but saw %d.", 
            i, location, workrecord.location);
    $assert(workrecord.kind == kind, "Wrong workshared kind of thread %d: expected %d but saw %d", 
            i, kind, workrecord.kind);
  }
}

/* finds the workrecord of the given location for a certain thread in a team,
 * stores the workrecord in the buffer provided, 
 * returns the index of the workrecod entry in the work queue
 * or -1 if the workrecord is absent.
 *
 * gteam: the global team object
 * tid: the id of the thread
 * location: the location of the workrecord being searched for
 * result: the buffer for store the workrecord found
 */
int find_work_record($omp_gteam gteam, int tid, int location, $omp_work_record *result){
  int numEntires = $seq_length(&gteam->work);
  
  for(int i = 0; i < numEntires; i++){
    $omp_work_record workrecord = gteam->work[i][tid];
    
    if(workrecord.location == location){
      *result = workrecord;
      return i;
    }
  }
  return -1;
}

/* checks if all threads have arrived the workrecord at the given index */
_Bool all_arrived($omp_gteam gteam, int index){
  for(int tid = 0; tid < gteam->nthreads; tid++){
    if(!gteam->work[index][tid].arrived)
      return $false;
  }
  return $true;
}

void arrive($omp_gteam gteam, int tid, int index,
$omp_work_record workrecord, $omp_worksharing_kind kind, int location){
  $assert(!workrecord.arrived, "The loop at location %d has been arrived before by thread %d!", 
          location, tid);
  $assert(workrecord.kind == kind, "Wrong workshare kind of thread %d: expected LOOP", 
          tid);
  (gteam->work[index][tid]).arrived = $true;
  if(all_arrived(gteam, index)){//this is the last thread 
    $assert(index == 0, "Inconsistent order or worksharing events.");
    $omp_check_workrecords(gteam, location, kind, index);
    $seq_remove(&gteam->work, index, NULL, 1);
  }
}

/* TODO: checks if loop_dom gets changed if the current thread is NOT the 
 * first thread entering the loop.
 */
$domain $omp_arrive_loop($omp_team team, int location, $domain loop_dom, 
    $domain_strategy strategy){
  $atomic{
    $omp_gteam gteam = team->gteam;
    int tid = team->tid;
    int nthreads = gteam->nthreads;
    int index;
    $omp_work_record workrecord;
    
    $assert(gteam->init[tid], "The current thread %d has not joined the gteam!", tid);
    if(nthreads == 1)
      return loop_dom;
    index = find_work_record(gteam, tid, location, &workrecord);
    if(index >= 0){//workrecord found
      $assert($equals(&gteam->work[index][0].loop_domain, &loop_dom), "The loop domain at location %d is changed when thread %d arrives it. \n Expected %s but saw %s.",
              location, 
              tid, 
              gteam->work[index][0].loop_domain, 
              loop_dom);
      arrive(gteam, tid, index, workrecord, LOOP, location);
      return workrecord.subdomain;
    }else{//workrecord not found, this should be the first thread
      $omp_work_record workrecords[nthreads];
      $domain_decomposition decomposition;
      int numEntries = $seq_length(&gteam->work);

      decomposition = $domain_partition(loop_dom, strategy, nthreads);
      workrecords[0].loop_domain = loop_dom;
      for(int i = 0; i< nthreads; i++){    
        workrecords[i].kind = LOOP; 
        workrecords[i].location = location;
        workrecords[i].arrived = (i == tid);
        workrecords[i].subdomain = decomposition.subdomains[i];
      }
      $seq_insert(&gteam->work, numEntries, &workrecords, 1);
      return workrecords[tid].subdomain;
    }
  }
}

/* TODO: need strategies? */
$domain(1) $omp_arrive_sections($omp_team team, int location, int numSections){
  $atomic{
    $omp_gteam gteam = team->gteam;
    int tid = team->tid;
    int nthreads = gteam->nthreads;
    int index;
    $omp_work_record workrecord;

    $assert(gteam->init[tid], "The current thread %d has not joined the gteam!", tid);
    if(nthreads == 1)
      return ($domain(1)) {0 .. numSections - 1 # 1};
    index = find_work_record(gteam, tid, location, &workrecord);
    if(index >= 0){//workrecord found
      arrive(gteam, tid, index, workrecord, SECTIONS, location);
      return workrecord.subdomain;
    }else{//workrecord not found, this should be the first thread
      $omp_work_record workrecords[nthreads];
      int numEntries = $seq_length(&gteam->work);

      for(int i = 0; i < nthreads; i++){
        int low = i, high = numSections - 1, step = nthreads;
        $range range = low .. high # step;
        $domain(1) dom = ($domain(1)) {range};

        workrecords[i].kind = SECTIONS; 
        workrecords[i].location = location;
        workrecords[i].arrived = (i == tid);
        workrecords[i].subdomain = dom;
      }
      $seq_insert(&gteam->work, numEntries, &workrecords, 1);
      return workrecords[tid].subdomain;
    }
  }
}

/* TODO: need strategies? */
 int $omp_arrive_single($omp_team team, int location){
  $atomic{
    $omp_gteam gteam = team->gteam;
    int tid = team->tid;
    int nthreads = gteam->nthreads;
    int index;
    $omp_work_record workrecord;

    $assert(gteam->init[tid], "The current thread %d has not joined the gteam!", tid);
    if(nthreads == 1)
      return tid;
    index = find_work_record(gteam, tid, location, &workrecord);
    if(index >= 0){//workrecord found
      arrive(gteam, tid, index, workrecord, SINGLE, location);
    }else{//workrecord not found, this should be the first thread
      $omp_work_record workrecords[nthreads];
      int numEntries = $seq_length(&gteam->work);

      for(int i = 0; i < nthreads; i++){
        workrecords[i].kind = SINGLE; 
        workrecords[i].location = location;
        workrecords[i].arrived = (i == tid);
      }
      $seq_insert(&gteam->work, numEntries, &workrecords, 1);
    }
    return 0;
  }
}