source: CIVL/examples/backend/mpiSumarray.cvl@ c2d9687

//======================= 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);
  }
}
//======================== civlc.cvh =======================
typedef struct $proc $proc;
typedef struct $scope $scope;
/*@ depends_on \nothing;
  @*/
$system[civlc] void $assert(_Bool expr, ...);
/*@ depends_on \nothing;
  @*/
$system[civlc] void $assume(_Bool expr);
/*@ pure;
  @ depends_on \nothing;
  @*/
$system[civlc] void $elaborate(int x);
/*@ depends_on \nothing;
  @*/
$system[civlc] void* $malloc($scope s, int size);
/*@ depends_on \nothing;
  @*/
$system[civlc] void $free(void* p);
/*@ depends_on \nothing;
  @*/
$system[civlc] void $assert(_Bool expr, ...);
/*@ depends_on \nothing;
  @*/
$system[civlc] void $assume(_Bool expr);
/*@ pure;
  @ depends_on \nothing;
  @*/
$system[civlc] void $elaborate(int x);
/*@ depends_on \nothing;
  @*/
$system[civlc] void* $malloc($scope s, int size);
/*@ depends_on \nothing;
  @*/
$system[civlc] void $free(void* p);
//========================= stdio.h ========================
$system[stdio] int printf(char* restrict format, ...);
//========================= seq.cvh ========================
$system[seq] void $seq_init(void* array, int count, void* value);
//======================== civlc.cvh =======================
/*@ depends_on \nothing;
  @*/
$system[civlc] void $assert(_Bool expr, ...);
/*@ depends_on \nothing;
  @*/
$system[civlc] void $assume(_Bool expr);
/*@ pure;
  @ depends_on \nothing;
  @*/
$system[civlc] void $elaborate(int x);
/*@ depends_on \nothing;
  @*/
$system[civlc] void* $malloc($scope s, int size);
/*@ depends_on \nothing;
  @*/
$system[civlc] void $free(void* p);
//======================= bundle.cvh =======================
typedef struct _bundle $bundle;
/*@ pure;
  @*/
$system[bundle] $bundle $bundle_pack(void* ptr, int size);
$system[bundle] void $bundle_unpack($bundle bundle, void* ptr);
//===================== concurrency.cvh ====================
typedef struct $gbarrier* $gbarrier;
typedef struct $barrier* $barrier;
/*@ requires size >= 0;
  @ 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 $collect_record $collect_record;
typedef struct $gcollect_checker* $gcollect_checker;
typedef struct $collect_checker* $collect_checker;
/*@ depends_on \nothing;
  @ reads \nothing;
  @ assigns \nothing;
  @*/
$atomic_f $gcollect_checker $gcollect_checker_create($scope scope);
/*@ depends_on \write(checker);
  @ assigns checker;
  @ reads \nothing;
  @*/
$atomic_f int $gcollect_checker_destroy($gcollect_checker checker);
/*@ depends_on \nothing;
  @ executes_when $true;
  @*/
$atomic_f $collect_checker $collect_checker_create($scope scope, $gcollect_checker gchecker);
/*@ depends_on \nothing;
  @ executes_when $true;
  @*/
$atomic_f void $collect_checker_destroy($collect_checker checker);
//========================== mpi.h =========================
typedef enum $anon_enum_0{
  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;
typedef struct MPI_Status{
    int MPI_SOURCE;
    int MPI_TAG;
    int MPI_ERROR;
    int size;
} MPI_Status;
//======================== 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;
  @ executes_when $true;
  @*/
$system[comm] 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);
/*@ depends_on \write(comm);
  @*/
$system[comm] $message $comm_dequeue($comm comm, int source, int tag);
//====================== civl-mpi.cvh ======================
typedef enum _mpi_state_{
  _MPI_UNINIT,
  _MPI_INIT,
  _MPI_FINALIZED
} $mpi_state;
typedef struct MPI_Comm MPI_Comm;
typedef struct MPI_Status MPI_Status;
typedef struct $mpi_gcomm $mpi_gcomm;
int sizeofDatatype(MPI_Datatype);
$mpi_gcomm $mpi_gcomm_create($scope, int);
void $mpi_gcomm_destroy($mpi_gcomm);
MPI_Comm $mpi_comm_create($scope, $mpi_gcomm, int);
void $mpi_comm_destroy(MPI_Comm, $mpi_state);
int $mpi_send(void*, int, MPI_Datatype, int, int, MPI_Comm);
int $mpi_recv(void*, int, MPI_Datatype, int, int, MPI_Comm, MPI_Status*);
$system[mpi] void $mpi_assert_consistent_basetype(void* buf, MPI_Datatype datatype);
//========================= mpi.cvl ========================
struct MPI_Comm{
    $comm p2p;
    $comm col;
    $collect_checker collect_checker;
    $barrier barrier;
    int gcommIndex;
};
//======================== civlc.cvh =======================
/*@ depends_on \nothing;
  @*/
$system[civlc] void $assert(_Bool expr, ...);
/*@ depends_on \nothing;
  @*/
$system[civlc] void $assume(_Bool expr);
/*@ pure;
  @ depends_on \nothing;
  @*/
$system[civlc] void $elaborate(int x);
/*@ depends_on \nothing;
  @*/
$system[civlc] void* $malloc($scope s, int size);
/*@ depends_on \nothing;
  @*/
$system[civlc] void $free(void* p);
//======================= bundle.cvh =======================
/*@ pure;
  @*/
$system[bundle] $bundle $bundle_pack(void* ptr, int size);
$system[bundle] void $bundle_unpack($bundle bundle, void* ptr);
//===================== concurrency.cvh ====================
/*@ requires size >= 0;
  @ 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);
/*@ depends_on \nothing;
  @ reads \nothing;
  @ assigns \nothing;
  @*/
$atomic_f $gcollect_checker $gcollect_checker_create($scope scope);
/*@ depends_on \write(checker);
  @ assigns checker;
  @ reads \nothing;
  @*/
$atomic_f int $gcollect_checker_destroy($gcollect_checker checker);
/*@ depends_on \nothing;
  @ executes_when $true;
  @*/
$atomic_f $collect_checker $collect_checker_create($scope scope, $gcollect_checker gchecker);
/*@ depends_on \nothing;
  @ executes_when $true;
  @*/
$atomic_f void $collect_checker_destroy($collect_checker checker);
//========================= seq.cvh ========================
$system[seq] void $seq_init(void* array, int count, void* value);
//===================== concurrency.cvl ====================
struct $gbarrier{
    int nprocs;
    $proc  proc_map[];
    _Bool  in_barrier[];
    int num_in_barrier;
};
struct $barrier{
    int place;
    $gbarrier gbarrier;
};
struct $collect_record{
    $bundle entries;
    _Bool  marks[];
    int numMarked;
};
struct $gcollect_checker{
    int length;
    $collect_record  records[];
};
struct $collect_checker{
    $gcollect_checker checker;
};
/*@ requires size >= 0;
  @ 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 $gcollect_checker $gcollect_checker_create($scope scope)
{
  $gcollect_checker gchecker = ($gcollect_checker)($malloc(scope, sizeof(struct $gcollect_checker)));
  (gchecker)->length = 0;
  $seq_init(&((gchecker)->records), 0, (void*)0);
  return gchecker;
}
/*@ depends_on \write(checker);
  @ assigns checker;
  @ reads \nothing;
  @*/
$atomic_f int $gcollect_checker_destroy($gcollect_checker checker)
{
  int numRemaining = (checker)->length;
  $free(checker);
  return numRemaining;
}
/*@ depends_on \nothing;
  @ executes_when $true;
  @*/
$atomic_f $collect_checker $collect_checker_create($scope scope, $gcollect_checker gchecker)
{
  $collect_checker checker = ($collect_checker)($malloc(scope, sizeof(struct $collect_checker)));
  (checker)->checker = gchecker;
  return checker;
}
/*@ depends_on \nothing;
  @ executes_when $true;
  @*/
$atomic_f void $collect_checker_destroy($collect_checker checker)
{
  $free(checker);
}
//======================== civlc.cvh =======================
/*@ depends_on \nothing;
  @*/
$system[civlc] void $assert(_Bool expr, ...);
/*@ depends_on \nothing;
  @*/
$system[civlc] void $assume(_Bool expr);
/*@ pure;
  @ depends_on \nothing;
  @*/
$system[civlc] void $elaborate(int x);
/*@ depends_on \nothing;
  @*/
$system[civlc] void* $malloc($scope s, int size);
/*@ depends_on \nothing;
  @*/
$system[civlc] void $free(void* p);
//======================= bundle.cvh =======================
/*@ pure;
  @*/
$system[bundle] $bundle $bundle_pack(void* ptr, int size);
$system[bundle] void $bundle_unpack($bundle bundle, void* ptr);
//===================== concurrency.cvh ====================
/*@ requires size >= 0;
  @ 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);
/*@ depends_on \nothing;
  @ reads \nothing;
  @ assigns \nothing;
  @*/
$atomic_f $gcollect_checker $gcollect_checker_create($scope scope);
/*@ depends_on \write(checker);
  @ assigns checker;
  @ reads \nothing;
  @*/
$atomic_f int $gcollect_checker_destroy($gcollect_checker checker);
/*@ depends_on \nothing;
  @ executes_when $true;
  @*/
$atomic_f $collect_checker $collect_checker_create($scope scope, $gcollect_checker gchecker);
/*@ depends_on \nothing;
  @ executes_when $true;
  @*/
$atomic_f void $collect_checker_destroy($collect_checker checker);
//======================== comm.cvh ========================
/*@ 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;
  @ executes_when $true;
  @*/
$system[comm] 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);
/*@ depends_on \write(comm);
  @*/
$system[comm] $message $comm_dequeue($comm comm, int source, int tag);
//====================== civl-mpi.cvh ======================
int sizeofDatatype(MPI_Datatype);
$mpi_gcomm $mpi_gcomm_create($scope, int);
void $mpi_gcomm_destroy($mpi_gcomm);
MPI_Comm $mpi_comm_create($scope, $mpi_gcomm, int);
void $mpi_comm_destroy(MPI_Comm, $mpi_state);
int $mpi_send(void*, int, MPI_Datatype, int, int, MPI_Comm);
int $mpi_recv(void*, int, MPI_Datatype, int, int, MPI_Comm, MPI_Status*);
$system[mpi] void $mpi_assert_consistent_basetype(void* buf, MPI_Datatype datatype);
//========================= seq.cvh ========================
$system[seq] void $seq_init(void* array, int count, void* value);
//====================== civl-mpi.cvl ======================
char* getCoroutineName(int tag);
struct $mpi_gcomm{
    $gcomm p2p;
    $gcomm col;
    $gcollect_checker collect_checker;
    $gbarrier gbarrier;
};
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_gcomm $mpi_gcomm_create($scope scope, int size)
{
  $mpi_gcomm result;
  result.p2p = $gcomm_create(scope, size);
  result.col = $gcomm_create(scope, size);
  result.collect_checker = $gcollect_checker_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 = getCoroutineName(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 = $gcollect_checker_destroy(gc.collect_checker);
  $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);
}
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.collect_checker = $collect_checker_create(scope, gc.collect_checker);
  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);
  $collect_checker_destroy(comm.collect_checker);
  $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$0 = sizeofDatatype(datatype);
    int size = count * $sef$0;
    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$1 = sizeofDatatype(datatype);
    int size = count * $sef$1;
    $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;
}
char* getCoroutineName(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);
  }
}
//======================== civlc.cvh =======================
/*@ depends_on \nothing;
  @*/
$system[civlc] void $assert(_Bool expr, ...);
/*@ depends_on \nothing;
  @*/
$system[civlc] void $assume(_Bool expr);
/*@ pure;
  @ depends_on \nothing;
  @*/
$system[civlc] void $elaborate(int x);
/*@ depends_on \nothing;
  @*/
$system[civlc] void* $malloc($scope s, int size);
/*@ depends_on \nothing;
  @*/
$system[civlc] void $free(void* p);
//======================= bundle.cvh =======================
/*@ pure;
  @*/
$system[bundle] $bundle $bundle_pack(void* ptr, int size);
$system[bundle] void $bundle_unpack($bundle bundle, void* ptr);
//======================== comm.cvh ========================
/*@ 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;
  @ executes_when $true;
  @*/
$system[comm] 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);
/*@ depends_on \write(comm);
  @*/
$system[comm] $message $comm_dequeue($comm comm, int source, int tag);
//========================= seq.cvh ========================
$system[seq] void $seq_init(void* array, int count, void* value);
//======================== comm.cvl ========================
struct $queue{
    int length;
    $message  messages[];
};
struct _gcomm_{
    int nprocs;
    $proc  procs[];
    _Bool  isInit[];
    $queue  buf[][];
};
struct _comm_{
    int place;
    $gcomm gcomm;
};
$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;
}
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)
{
  $free(gcomm);
  return 0;
}
/*@ 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);
}
int $comm_place($comm comm)
{
  return (comm)->place;
}
//======================== civlc.cvh =======================
/*@ depends_on \nothing;
  @*/
$system[civlc] void $assert(_Bool expr, ...);
/*@ depends_on \nothing;
  @*/
$system[civlc] void $assume(_Bool expr);
/*@ pure;
  @ depends_on \nothing;
  @*/
$system[civlc] void $elaborate(int x);
/*@ depends_on \nothing;
  @*/
$system[civlc] void* $malloc($scope s, int size);
/*@ depends_on \nothing;
  @*/
$system[civlc] void $free(void* p);
//========================= seq.cvh ========================
$system[seq] void $seq_init(void* array, int count, void* value);
//======================== civlc.cvh =======================
/*@ depends_on \nothing;
  @*/
$system[civlc] void $assert(_Bool expr, ...);
/*@ depends_on \nothing;
  @*/
$system[civlc] void $assume(_Bool expr);
/*@ pure;
  @ depends_on \nothing;
  @*/
$system[civlc] void $elaborate(int x);
/*@ depends_on \nothing;
  @*/
$system[civlc] void* $malloc($scope s, int size);
/*@ depends_on \nothing;
  @*/
$system[civlc] void $free(void* p);
//======================= bundle.cvh =======================
/*@ pure;
  @*/
$system[bundle] $bundle $bundle_pack(void* ptr, int size);
$system[bundle] void $bundle_unpack($bundle bundle, void* ptr);
//======================== civlc.cvh =======================
/*@ depends_on \nothing;
  @*/
$system[civlc] void $assert(_Bool expr, ...);
/*@ depends_on \nothing;
  @*/
$system[civlc] void $assume(_Bool expr);
/*@ pure;
  @ depends_on \nothing;
  @*/
$system[civlc] void $elaborate(int x);
/*@ depends_on \nothing;
  @*/
$system[civlc] void* $malloc($scope s, int size);
/*@ depends_on \nothing;
  @*/
$system[civlc] void $free(void* p);
//========================= stdio.h ========================
$system[stdio] int printf(char* restrict format, ...);
//======================= sum_array.c ======================
$input int _civl_argc;
$input char  _civl_argv[_civl_argc][];
$input long NB = 20;
$input long N;
//===================== 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));
$mpi_gcomm _mpi_gcomm = $mpi_gcomm_create($here, _mpi_nprocs);
$mpi_gcomm  _mpi_gcomms[];
$seq_init(&(_mpi_gcomms), 1, &(_mpi_gcomm));
void _mpi_process(int _mpi_rank)
{
  MPI_Comm MPI_COMM_WORLD = $mpi_comm_create($here, _mpi_gcomm, _mpi_rank);
  $system[sum_array] void $assume(_Bool expression);
  $assume(0 < _civl_argc);
  $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;
  }
  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_assert_consistent_basetype(buf, datatype);
    int $sef$2 = $mpi_send(buf, count, datatype, dest, tag, comm);
    return $sef$2;
  }
  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");
    $mpi_assert_consistent_basetype(buf, datatype);
    int $sef$3 = $mpi_recv(buf, count, datatype, source, tag, comm, status);
    return $sef$3;
  }
  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$4 = sizeofDatatype(datatype);
    *count = $int_div((status)->size, $sef$4);
    return 0;
  }
  $assume((0 < N) && (N <= NB));
  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);
  }
  {
    _civl_main(_civl_argc, (char*[_civl_argc]) $lambda (int i) _civl_argv[i]);
  }
  $mpi_comm_destroy(MPI_COMM_WORLD, _mpi_state);
}
int main()
{
  $parfor (int i: 0 .. _mpi_nprocs - 1)
    _mpi_process(i);
  $mpi_gcomm_destroy(_mpi_gcomm);
}