source: CIVL/examples/concurrency/mp_root2.cvh@ dccd621

#define MPI_ANY_SOURCE $COMM_ANY_SOURCE
#define MPI_ANY_TAG $COMM_ANY_TAG
$input int NPROCS = 3;
$proc __procs[NPROCS];
_Bool __start = 0;
$gcomm __MPI_Comm_World = $gcomm_create($root, NPROCS);

typedef $comm MPI_Comm;

typedef int MPI_Datatype;

#define MPI_INT 1
#define MPI_DOUBLE 2
#define MPI_FLOAT 3
#define MPI_CHAR 4

struct __MPI_Status {
  int MPI_SOURCE;
  int MPI_TAG;
  int MPI_ERROR;
  int size;
};

typedef struct __MPI_Status MPI_Status;

//MPI_Status __MPI_Status_ignore;

MPI_Status *MPI_STATUS_IGNORE = (MPI_Status*) NULL;

int MPI_Get_count(const MPI_Status *status, MPI_Datatype datatype,
                  int *count) {
  int size;
  
  switch (datatype) {
  case MPI_INT:
    size = sizeof(int); 
    break;
  case MPI_FLOAT:
    size = sizeof(float);
    break;
  case MPI_DOUBLE:
    size = sizeof(double);    
    break; 
  case MPI_CHAR:
    size = sizeof(char);
    break;
  default:
    printf("Unsupported datatype %d\n", datatype);
    $assert($false);
  }
  $assert(status->size % size == 0);
  *count = status->size / size;
  return 0; 
}

void MPI_Process (int __rank);

void init() {
  for (int i=0; i<NPROCS; i++)
    __procs[i] = $spawn MPI_Process(i);
  __start=1;
}

void finalize() {
  for (int i=0; i<NPROCS; i++)
    $wait(__procs[i]);
  $gcomm_destroy(__MPI_Comm_World);
}

void main() {
  init();
  finalize();
}