//======================= int_div.cvl ======================
$system[civlc] void $assert(_Bool expr, ...);
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)
      return numerator / denominator;
    else
      return -(numerator / (-denominator));
  }
  else {
    if (denominator >= 0)
      return -((-numerator) / denominator);
    else
      return (-numerator) / (-denominator);
  }
}
//======================= 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 struct $proc $proc;
/*@ depends_on \nothing;
  @ executes_when $true;
  @*/
$system[civlc] void $assert(_Bool expr, ...);
/*@ depends_on \nothing;
  @ executes_when $true;
  @*/
$system[civlc] void $assume(_Bool expr);
/*@ pure;
  @ depends_on \nothing;
  @ executes_when $true;
  @*/
$system[civlc] void $elaborate(int x);
/*@ depends_on \write(p);
  @ executes_when $true;
  @*/
$system[civlc] void $free(void* p);
//======================= sum_array.c ======================
$input long NB = 20;
$input long N;
$assume((0 < N) && (N <= NB));
//========================= seq.cvh ========================
/*@ depends_on \write(array);
  @ executes_when $true;
  @*/
$system[seq] int $seq_length(void* array);
/*@ depends_on \write(array, value);
  @ executes_when $true;
  @*/
$system[seq] void $seq_init(void* array, int count, void* value);
/*@ depends_on \write(array, values);
  @ executes_when $true;
  @*/
$system[seq] void $seq_insert(void* array, int index, void* values, int count);
/*@ depends_on \write(array, values);
  @*/
$atomic_f void $seq_append(void* array, void* values, int count);
//======================= bundle.cvh =======================
typedef struct _bundle $bundle;
/*@ depends_on \write(ptr);
  @ executes_when $true;
  @*/
$system[bundle] $bundle $bundle_pack(void* ptr, int size);
/*@ depends_on \write(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 \write(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 \write(barrier);
  @ assigns barrier;
  @ reads \nothing;
  @*/
$atomic_f void $barrier_destroy($barrier barrier);
typedef struct _collator_entry $collator_entry;
typedef struct _gcollator* $gcollator;
typedef struct _collator* $collator;
/*@ depends_on \nothing;
  @ reads \nothing;
  @ assigns \nothing;
  @*/
$atomic_f $gcollator $gcollator_create($scope scope);
/*@ depends_on \write(gcollator);
  @ assigns gcollator;
  @ reads \nothing;
  @*/
$atomic_f int $gcollator_destroy($gcollator gcollator);
/*@ depends_on \nothing;
  @ executes_when $true;
  @*/
$atomic_f $collator $collator_create($scope scope, $gcollator gcollator);
/*@ depends_on \write(collator);
  @ executes_when $true;
  @*/
$atomic_f void $collator_destroy($collator collator);
//======================== 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;
/*@ pure;
  @ depends_on \nothing;
  @ executes_when $true;
  @*/
$atomic_f $message $message_pack(int source, int dest, int tag, void* data, int size);
/*@ pure;
  @ depends_on \nothing;
  @ executes_when $true;
  @*/
$atomic_f int $message_source($message message);
/*@ pure;
  @ depends_on \nothing;
  @ executes_when $true;
  @*/
$atomic_f int $message_tag($message message);
/*@ pure;
  @ depends_on \nothing;
  @ executes_when $true;
  @*/
$atomic_f int $message_dest($message message);
/*@ pure;
  @ depends_on \nothing;
  @ executes_when $true;
  @*/
$atomic_f int $message_size($message message);
/*@ depends_on \write(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 \write(junkMsgs), \write(gcomm);
  @ assigns junkMsgs, gcomm;
  @*/
$atomic_f int $gcomm_destroy($gcomm gcomm, void* junkMsgs);
$atomic_f $comm $comm_create($scope scope, $gcomm gcomm, int place);
/*@ depends_on \write(comm);
  @ assigns comm;
  @ reads \nothing;
  @*/
$atomic_f void $comm_destroy($comm comm);
/*@ pure;
  @ depends_on \nothing;
  @*/
$atomic_f int $comm_size($comm comm);
/*@ pure;
  @ depends_on \nothing;
  @ executes_when $true;
  @*/
$atomic_f int $comm_place($comm comm);
/*@ depends_on \write(comm);
  @ executes_when $true;
  @*/
$system[comm] void $comm_enqueue($comm comm, $message message);
/*@ pure;
  @ depends_on \write(comm);
  @ executes_when $true;
  @*/
$system[comm] _Bool $comm_probe($comm comm, int source, int tag);
/*@ depends_on \write(comm);
  @ executes_when $comm_probe(comm, source, tag);
  @*/
$system[comm] $message $comm_dequeue($comm comm, int source, int tag);
//====================== civl-mpi.cvh ======================
typedef struct $mpi_gcomm $mpi_gcomm;
$mpi_gcomm $mpi_gcomm_create($scope, int);
void $mpi_gcomm_destroy($mpi_gcomm);
//========================= seq.cvl ========================
/*@ depends_on \write(array, values);
  @*/
$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;
};
struct _collator_entry{
  $bundle entries;
  _Bool  marks[];
  int numMarked;
};
struct _gcollator{
  int length;
  $collator_entry  entries[];
};
struct _collator{
  $gcollator gcollator;
};
/*@ depends_on \nothing;
  @ assigns \nothing;
  @ reads \nothing;
  @*/
$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;
}
/*@ depends_on \write(gbarrier);
  @ reads \nothing;
  @ assigns gbarrier;
  @*/
$atomic_f void $gbarrier_destroy($gbarrier gbarrier) {
  $free(gbarrier);
}
/*@ depends_on \nothing;
  @ assigns gbarrier;
  @ reads 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;
}
/*@ depends_on \write(barrier);
  @ assigns barrier;
  @ reads \nothing;
  @*/
$atomic_f void $barrier_destroy($barrier barrier) {
  $free(barrier);
}
/*@ depends_on \nothing;
  @ reads \nothing;
  @ assigns \nothing;
  @*/
$atomic_f $gcollator $gcollator_create($scope scope) {
  $gcollator gcollator = ($gcollator)($malloc(scope, sizeof(struct _gcollator)));
  (gcollator)->length = 0;
  $seq_init(&((gcollator)->entries), 0, (void*)0);
  return gcollator;
}
/*@ depends_on \write(gcollator);
  @ assigns gcollator;
  @ reads \nothing;
  @*/
$atomic_f int $gcollator_destroy($gcollator gcollator) {
  int numRemaining = (gcollator)->length;
  $free(gcollator);
  return numRemaining;
}
/*@ depends_on \nothing;
  @ executes_when $true;
  @*/
$atomic_f $collator $collator_create($scope scope, $gcollator gcollator) {
  $collator collator = ($collator)($malloc(scope, sizeof(struct _collator)));
  (collator)->gcollator = gcollator;
  return collator;
}
/*@ depends_on \write(collator);
  @ executes_when $true;
  @*/
$atomic_f void $collator_destroy($collator collator) {
  $free(collator);
}
//====================== 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);
  result.gbarrier = $gbarrier_create(scope, size);
  return result;
}
void $mpi_gcomm_destroy($mpi_gcomm gc) {
  int numJunkRecord;
  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($false, "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($false, "MPI message leak: There is a message sent by rank %d for collective routine %s that is never received.", src, routine);
    }
  }
  numJunkRecord = $gcollator_destroy(gc.gcollator);
  $gbarrier_destroy(gc.gbarrier);
  $assert(numJunkRecord == 0, "MPI collective routines are called inappropriately because there are %d collective records still remaining the collective routine checker.", numJunkRecord);
}
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($false, "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;
};
/*@ depends_on \write(data);
  @*/
$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;
  result.data = $bundle_pack(data, size);
  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;
}
/*@ depends_on \write(buf);
  @*/
$atomic_f void $message_unpack($message message, void* buf, int size) {
  $bundle_unpack(message.data, buf);
  $assert(message.size <= size, "Message of size %d exceeds the specified size %d.", message.size, size);
}
/*@ depends_on \nothing;
  @ assigns \nothing;
  @ reads \nothing;
  @*/
$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) $false);
  (gcomm)->buf = (($queue[size][size]) $lambda (int i, j) empty);
  return gcomm;
}
/*@ depends_on \write(junkMsgs), \write(gcomm);
  @ assigns junkMsgs, gcomm;
  @ reads \nothing;
  @*/
$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;
}
/*@ depends_on \nothing;
  @ reads gcomm;
  @ assigns gcomm;
  @*/
$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] = $true;
  (comm)->gcomm = gcomm;
  (comm)->place = place;
  return comm;
}
/*@ depends_on \write(comm);
  @ assigns comm;
  @ reads \nothing;
  @*/
$atomic_f void $comm_destroy($comm comm) {
  $free(comm);
}
/*@ pure;
  @ depends_on \nothing;
  @*/
$atomic_f int $comm_place($comm comm) {
  return (comm)->place;
}
/*@ pure;
  @ depends_on \nothing;
  @*/
$atomic_f int $comm_size($comm comm) {
  return ((comm)->gcomm)->nprocs;
}
//===================== 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 \write(format);  
  @ executes_when $true;
    @*/
  $system[stdio] int printf(char* restrict format, ...);
  typedef   enum MPI_Datatype{
      MPI_CHAR,
      MPI_CHARACTER,
      MPI_SIGNED_CHAR,
      MPI_UNSIGNED_CHAR,
      MPI_BYTE,
      MPI_WCHAR,
      MPI_SHORT,
      MPI_UNSIGNED_SHORT,
      MPI_INT,
      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,
      MPI_UNSIGNED_LONG,
      MPI_FLOAT,
      MPI_DOUBLE,
      MPI_LONG_DOUBLE,
      MPI_LONG_LONG_INT,
      MPI_UNSIGNED_LONG_LONG,
      MPI_LONG_LONG,
      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,
      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;
  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_Request* MPI_Request;
  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 = 0; i < N; i = i + 1)
      array[i] = i + 1;
    oracle = 0.0;
    for (i = 0; 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 = 0; i < (size - 1); i = i + 1)
      MPI_Send(array + (i * step), step, MPI_FLOAT, i + 1, 100, MPI_COMM_WORLD);
    {
      i = (size - 1) * step;
      mysum = 0;
      for (; i < N; i = i + 1)
        mysum = mysum + (array[i]);
    }
    for (i = 1; i < size; ) {
      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 = 0;
      sum = 0;
      for (; i < count; i = i + 1)
        sum = sum + (array[i]);
    }
    MPI_Send(&(sum), 1, MPI_DOUBLE, 0, 101, MPI_COMM_WORLD);
  }
  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 \write(buf);  
  @ executes_when $true;
    @*/
  $system[mpi] void $mpi_check_buffer(void* buf, int count, MPI_Datatype datatype);
  struct MPI_Request{
      MPI_Status status;
      _Bool isSend;
  };
  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$0 = $mpi_send(buf, count, datatype, dest, tag, comm);
    return $sef$0;
  }
  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$1 = $mpi_recv(buf, count, datatype, source, tag, comm, status);
    return $sef$1;
  }
  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$2 = sizeofDatatype(datatype);
    *count = $int_div((status)->size, $sef$2);
    return 0;
  }
  int sizeofDatatype(MPI_Datatype datatype) {
    switch (datatype) {
      case MPI_INT:
        return sizeof(int);
      case MPI_2INT:
        return sizeof(int) * 2;
      case MPI_FLOAT:
        return sizeof(float);
      case MPI_DOUBLE:
        return sizeof(double);
      case MPI_CHAR:
        return sizeof(char);
      case MPI_BYTE:
        return sizeof(char);
      case MPI_SHORT:
        return sizeof(short);
      case MPI_LONG:
        return sizeof(long);
      case MPI_LONG_DOUBLE:
        return sizeof(long double);
      case MPI_LONG_LONG_INT:
        return sizeof(long long);
      case MPI_LONG_LONG:
        return sizeof(long long);
      case MPI_UNSIGNED_LONG_LONG:
        return sizeof(unsigned long long);
      default:
        $assert(0, "Unreachable");
    }
  }
  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(scope, gc.gcollator);
    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);
    $collator_destroy(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) {
      int $sef$5 = sizeofDatatype(datatype);
      int size = count * $sef$5;
      int place = $comm_place(comm.p2p);
      $message 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))) {
      $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$6 = sizeofDatatype(datatype);
      int size = count * $sef$6;
      $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);
}