source: CIVL/examples/concurrency/hybrid.cvl

/* CIVL model of simple hybrid MPI+threads program.
 * The program has a defect.
 */
#include<comm.cvh>
#include<stdio.h>
#include "mp_root2.cvh"
#define TAG 0

void MPI_Process (int __rank) {
#include "mp_proc2.cvh"
  int rank;
  _Bool tStart = $false;
  MPI_Comm MPI_COMM_WORLD = $comm_create($here, __MPI_Comm_World, __rank);

  MPI_Comm_rank(MPI_COMM_WORLD, &rank);
  $proc threads[2];
  void Thread(int tid) {
    int x = 2*rank + tid, y;
    
    $when(tStart);
    for (int j=0; j<2; j++) {
      if (rank == 1) {
        for (int i=0; i<2; i++)
          MPI_Send(&x, 1, MPI_INT, 0, TAG, MPI_COMM_WORLD);
        for (int i=0; i<2; i++)
          MPI_Recv(&y, 1, MPI_INT, 0, TAG, MPI_COMM_WORLD, MPI_STATUS_IGNORE);
      } else if (rank == 0) {
        for (int i=0; i<2; i++)
          MPI_Recv(&y, 1, MPI_INT, 1, TAG, MPI_COMM_WORLD, MPI_STATUS_IGNORE);
        for (int i=0; i<2; i++)
          MPI_Send(&x, 1, MPI_INT, 1, TAG, MPI_COMM_WORLD);
      }
    }
  }
  for (int i=0; i<2; i++) {
    threads[i] = $spawn Thread(i);
  }
  tStart = $true;
  for (int i=0; i<2; i++) $wait(threads[i]);
  $comm_destroy(MPI_COMM_WORLD);
}