source: CIVL/examples/backend/mpiSumarray.cvl@ 978afe7

//======================= int_div.cvl ======================
$system[civlc] void $assert(_Bool expr, ...);
$system[int_div] int $remainder(int x, int y);
$system[int_div] int $quotient(int x, int y);
int $int_div(int numerator, int denominator) {
  $assert(denominator != 0, "Possible division by zero");
  if (numerator == 0)
    return 0;
  if (numerator >= 0) {
    if (denominator >= 0) {
      int $sef$0 = $quotient(numerator, denominator);
      return $sef$0;
    }
    else {
      int $sef$1 = $quotient(numerator, -denominator);
      return -$sef$1;
    }
  }
  else {
    if (denominator >= 0) {
      int $sef$2 = $quotient(-numerator, denominator);
      return -$sef$2;
    }
    else {
      int $sef$3 = $quotient(-numerator, -denominator);
      return $sef$3;
    }
  }
}
//=================== unsigned_arith.cvl ===================
int $signed_to_unsigned(int x, int bound) {
  if (x >= 0) {
    if (x < bound)
      return x;
    else {
      int $sef$9 = $remainder(x, bound);
      return $sef$9;
    }
  }
  else {
    if ((-x) <= bound)
      return bound + x;
    else {
      int $sef$10 = $remainder(-x, bound);
      return bound - $sef$10;
    }
  }
}
//======================= sum_array.c ======================
$input int _civl_argc;
$system[civlc] void $assume(_Bool expression);
$assume(0 < _civl_argc);
$input char  _civl_argv[_civl_argc][];
//======================== civlc.cvh =======================
typedef struct $scope $scope;
/*@ depends_on \nothing;
  @ executes_when $true;
  @*/
$system[civlc] void* $malloc($scope s, int size);
typedef unsigned long size_t;
typedef struct $proc $proc;
typedef struct $state $state;
/*@ depends_on \nothing;
  @ executes_when $true;
  @*/
$system[civlc] void $assert(_Bool expr, ...);
/*@ depends_on \nothing;
  @ executes_when $true;
  @*/
$system[civlc] void $assume(_Bool expr);

/*@ depends_on \access(p);
  @ executes_when $true;
  @*/
$system[civlc] void $free(void* p);
//========================== mpi.h =========================
typedef enum MPI_Datatype{
  MPI_CHAR=0,
  MPI_CHARACTER=1,
  MPI_SIGNED_CHAR,
  MPI_UNSIGNED_CHAR,
  MPI_BYTE=2,
  MPI_WCHAR,
  MPI_SHORT=3,
  MPI_UNSIGNED_SHORT,
  MPI_INT=4,
  MPI_INT16_T,
  MPI_INT32_T,
  MPI_INT64_T,
  MPI_INT8_T,
  MPI_INTEGER,
  MPI_INTEGER1,
  MPI_INTEGER16,
  MPI_INTEGER2,
  MPI_INTEGER4,
  MPI_INTEGER8,
  MPI_UNSIGNED,
  MPI_LONG=5,
  MPI_UNSIGNED_LONG,
  MPI_FLOAT=9,
  MPI_DOUBLE=10,
  MPI_LONG_DOUBLE=11,
  MPI_LONG_LONG_INT=6,
  MPI_UNSIGNED_LONG_LONG=7,
  MPI_LONG_LONG=8,
  MPI_PACKED,
  MPI_LB,
  MPI_UB,
  MPI_UINT16_T,
  MPI_UINT32_T,
  MPI_UINT64_T,
  MPI_UINT8_T,
  MPI_FLOAT_INT,
  MPI_DOUBLE_INT,
  MPI_LONG_INT,
  MPI_SHORT_INT,
  MPI_2INT=12,
  MPI_LONG_DOUBLE_INT,
  MPI_AINT,
  MPI_OFFSET,
  MPI_2DOUBLE_PRECISION,
  MPI_2INTEGER,
  MPI_2REAL,
  MPI_C_BOOL,
  MPI_C_COMPLEX,
  MPI_C_DOUBLE_COMPLEX,
  MPI_C_FLOAT_COMPLEX,
  MPI_C_LONG_DOUBLE_COMPLEX,
  MPI_COMPLEX,
  MPI_COMPLEX16,
  MPI_COMPLEX32,
  MPI_COMPLEX4,
  MPI_COMPLEX8,
  MPI_REAL,
  MPI_REAL16,
  MPI_REAL2,
  MPI_REAL4,
  MPI_REAL8
} MPI_Datatype;
//======================= sum_array.c ======================
$input long NB = 20;
$input long N;
$assume((0 < N) && (N <= NB));
//========================= seq.cvh ========================
/*@ depends_on \access(array);
  @ executes_when $true;
  @*/
$system[seq] int $seq_length(void* array);
/*@ depends_on \access(array, value);
  @ executes_when $true;
  @*/
$system[seq] void $seq_init(void* array, int count, void* value);
/*@ depends_on \access(array, values);
  @ executes_when $true;
  @*/
$system[seq] void $seq_insert(void* array, int index, void* values, int count);
/*@ depends_on \access(array, values);
  @*/
$atomic_f void $seq_append(void* array, void* values, int count);
//======================= bundle.cvh =======================
typedef struct _bundle $bundle;
/*@ depends_on \access(ptr);
  @ executes_when $true;
  @*/
$system[bundle] $bundle $bundle_pack(const void* ptr, int size);
/*@ depends_on \access(ptr);
  @ executes_when $true;
  @*/
$system[bundle] void $bundle_unpack($bundle bundle, void* ptr);
//===================== concurrency.cvh ====================
typedef struct _gbarrier* $gbarrier;
typedef struct _barrier* $barrier;
/*@ depends_on \nothing;
  @ assigns \nothing;
  @ reads \nothing;
  @*/
$atomic_f $gbarrier $gbarrier_create($scope scope, int size);
/*@ depends_on \access(gbarrier);
  @ reads \nothing;
  @ assigns gbarrier;
  @*/
$atomic_f void $gbarrier_destroy($gbarrier gbarrier);
/*@ depends_on \nothing;
  @ assigns gbarrier;
  @ reads gbarrier;
  @*/
$atomic_f $barrier $barrier_create($scope scope, $gbarrier gbarrier, int place);
/*@ depends_on \access(barrier);
  @ assigns barrier;
  @ reads \nothing;
  @*/
$atomic_f void $barrier_destroy($barrier barrier);
//======================== comm.cvh ========================
typedef struct _message{
  int source;
  int dest;
  int tag;
  $bundle data;
  int size;
} $message;
typedef struct _queue $queue;
typedef struct _gcomm* $gcomm;
typedef struct _comm* $comm;
/*@ depends_on \access(data);
  @ executes_when $true;
  @*/
$atomic_f $message $message_pack(int source, int dest, int tag, void* data, int size);
/*@ depends_on \nothing;
  @ executes_when $true;
  @*/
$atomic_f int $message_source($message message);
/*@ depends_on \nothing;
  @ executes_when $true;
  @*/
$atomic_f int $message_tag($message message);
/*@ depends_on \nothing;
  @ executes_when $true;
  @*/
$atomic_f int $message_dest($message message);
/*@ depends_on \nothing;
  @ executes_when $true;
  @*/
$atomic_f int $message_size($message message);
/*@ depends_on \access(buf);
  @ executes_when $true;
  @*/
$atomic_f void $message_unpack($message message, void* buf, int size);
/*@ depends_on \nothing;
  @ assigns \nothing;
  @ reads \nothing;
  @*/
$atomic_f $gcomm $gcomm_create($scope scope, int size);
/*@ depends_on \access(junkMsgs), \access(gcomm);
  @ assigns junkMsgs, gcomm;
  @*/
$atomic_f int $gcomm_destroy($gcomm gcomm, void* junkMsgs);
/*@ depends_on \nothing;
  @ reads gcomm;
  @ assigns gcomm;
  @*/
$atomic_f $comm $comm_create($scope scope, $gcomm gcomm, int place);
/*@ depends_on \access(comm);
  @ assigns comm;
  @ reads \nothing;
  @*/
$atomic_f void $comm_destroy($comm comm);
/*@ depends_on \nothing;
  @*/
$atomic_f int $comm_size($comm comm);
/*@ depends_on \nothing;
  @ executes_when $true;
  @*/
$atomic_f int $comm_place($comm comm);
/*@ depends_on \access(comm);
  @ executes_when $true;
  @*/
$system[comm] void $comm_enqueue($comm comm, $message message);
/*@ depends_on \access(comm);
  @ executes_when $true;
  @*/
$system[comm] $state_f _Bool $comm_probe($comm comm, int source, int tag);
/*@ depends_on \access(comm);
  @ executes_when $comm_probe(comm, source, tag);
  @*/
$system[comm] $message $comm_dequeue($comm comm, int source, int tag);
//======================= collate.cvh ======================
typedef struct _gcollator* $gcollator;
typedef struct _collator* $collator;
typedef struct _gcollate_state* $gcollate_state;
$atomic_f $gcollator $gcollator_create($scope scope, int nprocs);
$atomic_f $collator $collator_create($gcollator gcollator, $scope scope, int place);
//====================== civl-mpi.cvh ======================
typedef struct $mpi_gcomm $mpi_gcomm;
$mpi_gcomm $mpi_gcomm_create($scope, int);
void $mpi_gcomm_destroy($mpi_gcomm);
//========================= seq.cvl ========================
$atomic_f void $seq_append(void* array, void* values, int count) {
  int length = $seq_length(array);
  $seq_insert(array, length, values, count);
}
//===================== concurrency.cvl ====================
struct _gbarrier{
  int nprocs;
  $proc  proc_map[];
  _Bool  in_barrier[];
  int num_in_barrier;
};
struct _barrier{
  int place;
  $gbarrier gbarrier;
};
$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) 0);
  (gbarrier)->num_in_barrier = 0;
  return gbarrier;
}
$atomic_f void $gbarrier_destroy($gbarrier gbarrier) {
  $free(gbarrier);
}
$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);
}
//====================== civl-mpi.cvl ======================
char* $mpi_coroutine_name(int tag);
struct $mpi_gcomm{
  $gcomm p2p;
  $gcomm col;
  $gcollator gcollator;
  $gbarrier gbarrier;
};
$mpi_gcomm $mpi_gcomm_create($scope scope, int size) {
  $mpi_gcomm result;
  result.p2p = $gcomm_create(scope, size);
  result.col = $gcomm_create(scope, size);
  result.gcollator = $gcollator_create(scope, size);
  result.gbarrier = $gbarrier_create(scope, size);
  return result;
}
void $mpi_gcomm_destroy($mpi_gcomm gc) {
  int numJunkMsg;
  $message  junkMsgs[];
  $seq_init(&(junkMsgs), 0, (void*)0);
  numJunkMsg = $gcomm_destroy(gc.p2p, &(junkMsgs));
  {
    int i = 0;
    for (; i < numJunkMsg; i = i + 1) {
      int src;
      int dest;
      int tag;
      src = $message_source(junkMsgs[i]);
      dest = $message_dest(junkMsgs[i]);
      tag = $message_tag(junkMsgs[i]);
      $assert(0, "MPI message leak: There is a message from rank %d to rank %d with tag %d has been sent but is never received in point-to-point communication.", src, dest, tag);
    }
  }
  numJunkMsg = $gcomm_destroy(gc.col, &(junkMsgs));
  {
    int i = 0;
    for (; i < numJunkMsg; i = i + 1) {
      int src;
      int tag;
      char* routine;
      src = $message_source(junkMsgs[i]);
      tag = $message_tag(junkMsgs[i]);
      routine = $mpi_coroutine_name(tag);
      $assert(0, "MPI message leak: There is a message sent by rank %d for collective routine %s that is never received.", src, routine);
    }
  }
  $free(gc.gcollator);
  $gbarrier_destroy(gc.gbarrier);
}
char* $mpi_coroutine_name(int tag) {
  switch (tag) {
    case 9999:
      return "MPI_Bcast";
    case 9998:
      return "MPI_Reduce";
    case 9997:
      return "MPI_Allreduce";
    case 9996:
      return "MPI_Gather";
    case 9995:
      return "MPI_Scatter";
    case 9994:
      return "MPI_Gatherv";
    case 9993:
      return "MPI_Scatterv";
    case 9992:
      return "MPI_Allgather";
    case 9991:
      return "MPI_Reduce_scatter";
    case 9990:
      return "MPI_Alltoall";
    case 9989:
      return "MPI_Alltoallv";
    case 9988:
      return "MPI_Alltoallw";
    case 9987:
      return "MPI_Barrier";
    case 9986:
      return "MPI_Commdup";
    case 9985:
      return "MPI_Commfree";
    default:
      $assert(0, "Internal Error: Unexpected MPI routine tag:%d.\n", tag);
  }
}
//======================== comm.cvl ========================
struct _queue{
  int length;
  $message  messages[];
};
struct _gcomm{
  int nprocs;
  $proc  procs[];
  _Bool  isInit[];
  $queue  buf[][];
};
struct _comm{
  int place;
  $gcomm gcomm;
};
$atomic_f $message $message_pack(int source, int dest, int tag, void* data, int size) {
  $message result;
  result.source = source;
  result.dest = dest;
  result.tag = tag;
  if ((data != (void*)0) && (size > 0)) {
    result.data = $bundle_pack(data, size);
  }
  else
    if (data == (void*)0)
      $assert(size == 0, "Attempt to pack a non-zero size message with a NULL pointer");
  result.size = size;
  return result;
}
int $message_source($message message) {
  return message.source;
}
int $message_tag($message message) {
  return message.tag;
}
int $message_dest($message message) {
  return message.dest;
}
int $message_size($message message) {
  return message.size;
}
$atomic_f void $message_unpack($message message, void* buf, int size) {
  if ((buf != (void*)0) && (message.size > 0)) {
    $bundle_unpack(message.data, buf);
    $assert(message.size <= size, "Message of size %d exceeds the specified size %d.", message.size, size);
  }
  else
    if (buf == (void*)0)
      $assert(message.size == 0, "Attempt to unpack a non-zero size message with a NULL pointer.");
}
$atomic_f $gcomm $gcomm_create($scope scope, int size) {
  $gcomm gcomm = ($gcomm)($malloc(scope, sizeof(struct _gcomm)));
  $queue empty;
  empty.length = 0;
  $seq_init(&(empty.messages), 0, (void*)0);
  (gcomm)->nprocs = size;
  (gcomm)->procs = (($proc[size]) $lambda (int i) $proc_null);
  (gcomm)->isInit = ((_Bool[size]) $lambda (int i) 0);
  (gcomm)->buf = (($queue[size][size]) $lambda (int i, j) empty);
  return gcomm;
}
$atomic_f int $gcomm_destroy($gcomm gcomm, void* junkMsgs) {
  int nprocs = (gcomm)->nprocs;
  int numJunks = 0;
  if (junkMsgs != (void*)0) {
    {
      int i = 0;
      for (; i < nprocs; i = i + 1) {
        int j = 0;
        for (; j < nprocs; j = j + 1) {
          $queue queue = (gcomm)->buf[i][j];
          if (queue.length > 0)
            $seq_append(junkMsgs, queue.messages, queue.length);
        }
      }
    }
    numJunks = $seq_length(junkMsgs);
  }
  $free(gcomm);
  return numJunks;
}
$atomic_f $comm $comm_create($scope scope, $gcomm gcomm, int place) {
  $assert(!((gcomm)->isInit[place]), "the place %d is already occupied in the global communicator!", place);
  $comm comm = ($comm)($malloc(scope, sizeof(struct _comm)));
  (gcomm)->procs[place] = $self;
  (gcomm)->isInit[place] = 1;
  (comm)->gcomm = gcomm;
  (comm)->place = place;
  return comm;
}
$atomic_f void $comm_destroy($comm comm) {
  $free(comm);
}
$atomic_f int $comm_place($comm comm) {
  return (comm)->place;
}
$atomic_f int $comm_size($comm comm) {
  return ((comm)->gcomm)->nprocs;
}
//======================= collate.cvl ======================
struct _gcollator{
  int nprocs;
  $proc  procs[];
  int queue_length;
  $gcollate_state  queue[];
  _Bool  entered[];
};
struct _collator{
  int place;
  $gcollator gcollator;
};
struct _gcollate_state{
  int  status[];
  $state state;
  $bundle attribute;
};
$gcollator $gcollator_create($scope scope, int nprocs) {
  $gcollator gcollator = ($gcollator)($malloc(scope, sizeof(struct _gcollator)));
  (gcollator)->nprocs = nprocs;
  (gcollator)->procs = (($proc[nprocs]) $lambda (int i) $proc_null);
  (gcollator)->queue_length = 0;
  $seq_init(&((gcollator)->queue), 0, (void*)0);
  (gcollator)->entered = ((_Bool[nprocs]) $lambda (int i) 0);
  return gcollator;
}
$collator $collator_create($gcollator gcollator, $scope scope, int place) {
  $collator collator = ($collator)($malloc(scope, sizeof(struct _collator)));
  (collator)->place = place;
  (collator)->gcollator = gcollator;
  ((collator)->gcollator)->procs[place] = $self;
  return collator;
}
//===================== MPITransformer =====================
$input int _mpi_nprocs;
$input int _mpi_nprocs_lo = 1;
//======================= sum_array.c ======================
$input int _mpi_nprocs_hi = 8;
//===================== MPITransformer =====================
$assume((_mpi_nprocs_lo <= _mpi_nprocs) && (_mpi_nprocs <= _mpi_nprocs_hi));
$scope _mpi_root = $here;
$mpi_gcomm _mpi_gcomm;
$mpi_gcomm  _mpi_gcomms[];
void _mpi_process(int _mpi_rank) {
  /*@ depends_on \access(format);
    @ executes_when $true;
    @*/
  $system[stdio] int printf(char* restrict format, ...);
  typedef   struct MPI_Comm MPI_Comm;
  MPI_Comm $mpi_comm_create($scope, $mpi_gcomm, int);
  MPI_Comm MPI_COMM_WORLD = $mpi_comm_create($here, _mpi_gcomm, _mpi_rank);
  typedef   struct MPI_Status{
    int MPI_SOURCE;
    int MPI_TAG;
    int MPI_ERROR;
    int size;
  } MPI_Status;
  int MPI_Send(void*, int, MPI_Datatype, int, int, MPI_Comm);
  int MPI_Recv(void*, int, MPI_Datatype, int, int, MPI_Comm, MPI_Status*);
  int MPI_Get_count(MPI_Status*, MPI_Datatype, int*);
  int MPI_Comm_size(MPI_Comm, int*);
  int MPI_Comm_rank(MPI_Comm, int*);
  typedef   enum _mpi_state{
    _MPI_UNINIT,
    _MPI_INIT,
    _MPI_FINALIZED
  } $mpi_state;
  $mpi_state _mpi_state = _MPI_UNINIT;
  int $mpi_init(void) {
    $assert(_mpi_state == _MPI_UNINIT, "Process can only call MPI_Init() at most once.");
    _mpi_state = _MPI_INIT;
    return 0;
  }
  void $mpi_comm_destroy(MPI_Comm, $mpi_state);
  int MPI_Finalize(void);
  double oracle;
  void master(void);
  void slave(void);
  int _civl_main(int argc, char** argv) {
    int myrank;
    $mpi_init();
    MPI_Comm_rank(MPI_COMM_WORLD, &(myrank));
    if (!myrank)
      master();
    else
      slave();
    MPI_Finalize();
    return 0;
  }
  void master(void) {
    float  array[N];
    double mysum;
    double tmpsum;
    unsigned long long step;
    unsigned long long i;
    int size;
    MPI_Status status;
    for (i = $signed_to_unsigned(0, 4294967296); i < N; i = i + 1) {
      unsigned long long $sef$12 = $signed_to_unsigned(1, 4294967296);
      array[i] = i + $sef$12;
    }
    oracle = 0.0;
    for (i = $signed_to_unsigned(0, 4294967296); i < N; i = i + 1)
      oracle = oracle + (array[i]);
    MPI_Comm_size(MPI_COMM_WORLD, &(size));
    if (size != 1)
      step = $int_div(N, size - 1);
    else
      step = N;
    for (i = $signed_to_unsigned(0, 4294967296); i < (size - 1); i = i + 1) {
      unsigned long long $sef$13 = $signed_to_unsigned(1, 4294967296);
      MPI_Send(array + (i * step), step, MPI_FLOAT, i + $sef$13, 100, MPI_COMM_WORLD);
    }
    {
      i = (size - 1) * step;
      mysum = 0;
      for (; i < N; i = i + 1)
        mysum = mysum + (array[i]);
    }
    for (i = $signed_to_unsigned(1, 4294967296); 1; ) {
      unsigned long long $sef$14 = $signed_to_unsigned(size, 4294967296);
      if (!(i < $sef$14))
        break;
      MPI_Recv(&(tmpsum), 1, MPI_DOUBLE, -1, 101, MPI_COMM_WORLD, &(status));
      mysum = mysum + tmpsum;
      i = i + 1;
    }
    $assert(oracle == mysum, "The sum of %d array elements is %f but the expected one is %f.\n", N, mysum, oracle);
    printf("%lf\n", mysum);
  }
  void slave(void) {
    float  array[N];
    double sum;
    unsigned long long i;
    int count;
    MPI_Status status;
    MPI_Recv(array, N, MPI_FLOAT, 0, 100, MPI_COMM_WORLD, &(status));
    MPI_Get_count(&(status), MPI_FLOAT, &(count));
    {
      i = $signed_to_unsigned(0, 4294967296);
      sum = 0;
      for (; 1; i = i + 1) {
        unsigned long long $sef$15 = $signed_to_unsigned(count, 4294967296);
        if (!(i < $sef$15))
          break;
        sum = sum + (array[i]);
      }
    }
    MPI_Send(&(sum), 1, MPI_DOUBLE, 0, 101, MPI_COMM_WORLD);
  }
  /*@ depends_on \nothing;
    @ executes_when $true;
    @*/
  $atomic_f $state_f int sizeofDatatype(MPI_Datatype);
  int $mpi_send(void*, int, MPI_Datatype, int, int, MPI_Comm);
  int $mpi_recv(void*, int, MPI_Datatype, int, int, MPI_Comm, MPI_Status*);
  /*@ depends_on \access(buf);
    @ executes_when $true;
    @*/
  $system[mpi] void $mpi_check_buffer(void* buf, int count, MPI_Datatype datatype);
  struct MPI_Comm{
    $comm p2p;
    $comm col;
    $collator collator;
    $barrier barrier;
    int gcommIndex;
  };
  int MPI_Finalize(void) {
    $assert(_mpi_state == _MPI_INIT, "Process can only call MPI_Finalize() after the MPI enviroment is created and before cleaned.");
    _mpi_state = _MPI_FINALIZED;
    return 0;
  }
  int MPI_Comm_size(MPI_Comm comm, int* size) {
    $assert(_mpi_state == _MPI_INIT, "MPI_Comm_size() cannot be invoked without MPI_Init() being called before.\n");
    *size = $comm_size(comm.p2p);
    return 0;
  }
  int MPI_Comm_rank(MPI_Comm comm, int* rank) {
    $assert(_mpi_state == _MPI_INIT, "MPI_Comm_rank() cannot be invoked without MPI_Init() being called before.\n");
    *rank = $comm_place(comm.p2p);
    return 0;
  }
  int MPI_Send(void* buf, int count, MPI_Datatype datatype, int dest, int tag, MPI_Comm comm) {
    $assert(_mpi_state == _MPI_INIT, "MPI_Send() cannot be invoked without MPI_Init() being called before.\n");
    $mpi_check_buffer(buf, count, datatype);
    int $sef$16 = $mpi_send(buf, count, datatype, dest, tag, comm);
    return $sef$16;
  }
  int MPI_Recv(void* buf, int count, MPI_Datatype datatype, int source, int tag, MPI_Comm comm, MPI_Status* status) {
    $assert(_mpi_state == _MPI_INIT, "MPI_Recv() cannot be invoked without MPI_Init() being called before.\n");
    int $sef$17 = $mpi_recv(buf, count, datatype, source, tag, comm, status);
    return $sef$17;
  }
  int MPI_Get_count(MPI_Status* status, MPI_Datatype datatype, int* count) {
    $assert(_mpi_state == _MPI_INIT, "MPI_Get_count() cannot be invoked without MPI_Init() being called before.\n");
    int $sef$18 = sizeofDatatype(datatype);
    *count = $int_div((status)->size, $sef$18);
    return 0;
  }
  int sizeofDatatype(MPI_Datatype datatype) {
    size_t result;
    switch (datatype) {
      case MPI_INT:
        result = sizeof(int);
        break;
      case MPI_2INT:
        result = sizeof(int) * 2;
        break;
      case MPI_FLOAT:
        result = sizeof(float);
        break;
      case MPI_DOUBLE:
        result = sizeof(double);
        break;
      case MPI_CHAR:
        result = sizeof(char);
        break;
      case MPI_BYTE:
        result = sizeof(char);
        break;
      case MPI_SHORT:
        result = sizeof(short);
        break;
      case MPI_LONG:
        result = sizeof(long);
        break;
      case MPI_LONG_DOUBLE:
        result = sizeof(long double);
        break;
      case MPI_LONG_LONG_INT:
        result = sizeof(long long);
        break;
      case MPI_LONG_LONG:
        result = sizeof(long long);
        break;
      case MPI_UNSIGNED_LONG_LONG:
        result = sizeof(unsigned long long);
        break;
      default:
        $assert(0, "Unreachable");
    }
    return result;
  }
  MPI_Comm $mpi_comm_create($scope scope, $mpi_gcomm gc, int rank) {
    MPI_Comm result;
    result.p2p = $comm_create(scope, gc.p2p, rank);
    result.col = $comm_create(scope, gc.col, rank);
    result.collator = $collator_create(gc.gcollator, scope, rank);
    result.barrier = $barrier_create(scope, gc.gbarrier, rank);
    result.gcommIndex = 0;
    return result;
  }
  void $mpi_comm_destroy(MPI_Comm comm, $mpi_state mpi_state) {
    if (comm.gcommIndex == 0)
      $assert(mpi_state == _MPI_FINALIZED, "Process terminates without calling MPI_Finalize() first.");
    $comm_destroy(comm.p2p);
    $comm_destroy(comm.col);
    $free(comm.collator);
    $barrier_destroy(comm.barrier);
  }
  int $mpi_send(void* buf, int count, MPI_Datatype datatype, int dest, int tag, MPI_Comm comm) {
    if ((dest >= 0) && (count >= 0)) {
      int $sef$26 = sizeofDatatype(datatype);
      int size = count * $sef$26;
      int place = $comm_place(comm.p2p);
      $message out;
      $elaborate(dest);
      out = $message_pack(place, dest, tag, buf, size);
      $comm_enqueue(comm.p2p, out);
    }
    return 0;
  }
  int $mpi_recv(void* buf, int count, MPI_Datatype datatype, int source, int tag, MPI_Comm comm, MPI_Status* status) {
    if (((source >= 0) || (source == (-1))) && (count >= 0)) {
      $message in;
      int place = $comm_place(comm.p2p);
      int deterministicTag;
      $assert((tag == (-2)) || (tag >= 0), "Illegal MPI message receive tag %d.\n", tag);
      deterministicTag = tag < 0 ? -2 : tag;
      $elaborate(source);
      in = $comm_dequeue(comm.p2p, source, deterministicTag);
      int $sef$27 = sizeofDatatype(datatype);
      int size = count * $sef$27;
      $message_unpack(in, buf, size);
      if (status != (void*)0) {
        (status)->size = $message_size(in);
        (status)->MPI_SOURCE = $message_source(in);
        (status)->MPI_TAG = $message_tag(in);
        (status)->MPI_ERROR = 0;
      }
    }
    return 0;
  }
  {
    _civl_main(_civl_argc, ((char*[_civl_argc]) $lambda (int i) _civl_argv[i]));
  }
  $mpi_comm_destroy(MPI_COMM_WORLD, _mpi_state);
}
int main() {
  _mpi_gcomm = $mpi_gcomm_create(_mpi_root, _mpi_nprocs);
  $seq_init(&(_mpi_gcomms), 1, &(_mpi_gcomm));
  $parfor (int i: 0 .. _mpi_nprocs - 1)
    _mpi_process(i);
  $mpi_gcomm_destroy(_mpi_gcomm);
}