/* CIVL model of simple hybrid MPI+threads program.
 * The program has a defect.
 */
#include<civlc.h>
#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_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, 1, TAG, MPI_COMM_WORLD);
        for (int i=0; i<2; i++)
          MPI_Recv(&y, 1, MPI_INT, 1, TAG, MPI_COMM_WORLD, MPI_STATUS_IGNORE);
      } else {
        for (int i=0; i<2; i++)
          MPI_Recv(&y, 1, MPI_INT, 0, TAG, MPI_COMM_WORLD, MPI_STATUS_IGNORE);
        for (int i=0; i<2; i++)
          MPI_Send(&x, 1, MPI_INT, 0, TAG, MPI_COMM_WORLD);
      }
    }
  }
  //$atomic {
  for (int i=0; i<2; i++) {
    threads[i] = $spawn Thread(i);
    $comm_add(MPI_COMM_WORLD, threads[i], rank);
  }
  tStart = $true;
  for (int i=0; i<2; i++) $wait threads[i];
  //}
}