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

$comm comm;
_Bool initialized = $false;

void MPI_Process (int pid) {
  $proc threads[2];
  void Thread(int tid) {
    int x = pid;
    $message in, out = $message_pack(pid, 1-pid, TAG, &x, sizeof(int));
    
    for (int j=0; j<2; j++) {
      if (pid == 1) {
        for (int i=0; i<2; i++) $comm_enqueue(&comm, out);
        for (int i=0; i<2; i++) in = $comm_dequeue(&comm, 1-pid, pid, TAG);
      } else {
        for (int i=0; i<2; i++) in = $comm_dequeue(&comm, 1-pid, pid, TAG);
        for (int i=0; i<2; i++) $comm_enqueue(&comm, out);
      }
    }
  }
  
  $when (initialized) $atomic {
    for (int i=0; i<2; i++) threads[i] = $spawn Thread(i);
    for (int i=0; i<2; i++) $wait threads[i];
  }
}

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