source: CIVL/examples/messagePassing/ring.cvl@ c19cfd5

/* Create nprocs processes.  Have them exchange data in a cycle.
 * Command line execution:
 *     civl verify -inputNPROCS_BOUND=10 -inputN_BOUND=5 ring.cvl
 */
#include<civlc.h>
#define TAG 0

$input int NPROCS_BOUND; // upper bound of the number of mpi processes
$input int NPROCS; // number of mpi processes
$assume 0 < NPROCS && NPROCS <= NPROCS_BOUND;
$input int N_BOUND; // upper bound on number times to loop
$input int N; // number of times to loop
$assume 0 < N && N <= N_BOUND;
_Bool initialized = $false;
$comm MPI_COMM_WORLD; // the default MPI communicator

void MPI_Process (int rank) {
  int left = (rank+NPROCS-1)%NPROCS;
  int right = (rank+NPROCS+1)%NPROCS;
  int i=0;
  int x=rank, y; // send a message from x, recv into y, for checking
  $message in, out;
  
  $when (initialized);
  while (i<N) {
    if (rank%2==0) { // send first, then recv
      out = $message_pack(rank, right, TAG, &x, sizeof(int));
      $comm_enqueue(&MPI_COMM_WORLD, out);
      in = $comm_dequeue(&MPI_COMM_WORLD, left, rank, TAG);
      $message_unpack(in, &y, sizeof(int));
      $assert(y==left);
    } else { // recv first, then send
      in = $comm_dequeue(&MPI_COMM_WORLD, left, rank, TAG);
      $message_unpack(in, &y, sizeof(int));
      $assert(y==left);
      out = $message_pack(rank, right, TAG, &x, sizeof(int));
      $comm_enqueue(&MPI_COMM_WORLD, out);
    }
    i++;
  }
}

void main() {
  $proc procs[NPROCS];
  
  for (int i=0; i<NPROCS; i++)
    procs[i] = $spawn MPI_Process(i);
  MPI_COMM_WORLD = $comm_create(NPROCS, procs);
  initialized = $true;
  for (int i=0; i<NPROCS; i++)
    $wait procs[i];
}