X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/b40c2e9bf3cf6e8b2fad15594852ce186bf99574..a8aa2d7d477df7565dc963b9abcb571e8f6d87e2:/src/mc/mc_comm_determinism.c?ds=sidebyside

diff --git a/src/mc/mc_comm_determinism.c b/src/mc/mc_comm_determinism.c
index d5b086ce2f..15cc8d1b74 100644
--- a/src/mc/mc_comm_determinism.c
+++ b/src/mc/mc_comm_determinism.c
@@ -68,53 +68,56 @@ static int compare_comm_pattern(mc_comm_pattern_t comm1,
   return 0;
 }
 
-static void deterministic_pattern(xbt_dynar_t initial_pattern,
-                                  xbt_dynar_t pattern)
+static void deterministic_pattern(xbt_dynar_t pattern, int partial)
 {
 
-  if (!xbt_dynar_is_empty(incomplete_communications_pattern))
-    xbt_die
-        ("Damn ! Some communications are incomplete that means one or several simcalls are not handle ... ");
-
   unsigned int cursor = 0, send_index = 0, recv_index = 0;
   mc_comm_pattern_t comm1, comm2;
-  int comm_comparison = 0;
-  int current_process = 0;
+  unsigned int current_process = 1; /* Process 0 corresponds to maestro */
+  unsigned int nb_comms1, nb_comms2;
+  xbt_dynar_t process_comms_pattern1, process_comms_pattern2; 
+  
   while (current_process < simix_process_maxpid) {
-    while (cursor < xbt_dynar_length(initial_pattern)) {
-      comm1 =
-          (mc_comm_pattern_t) xbt_dynar_get_as(initial_pattern, cursor,
-                                               mc_comm_pattern_t);
-      if (comm1->type == SIMIX_COMM_SEND && comm1->src_proc == current_process) {
-        comm2 =
-            get_comm_pattern_from_idx(pattern, &send_index, comm1->type,
-                                      current_process);
-        comm_comparison = compare_comm_pattern(comm1, comm2);
-        if (comm_comparison == 1) {
-          initial_global_state->send_deterministic = 0;
-          initial_global_state->comm_deterministic = 0;
-          return;
-        }
-        send_index++;
-      } else if (comm1->type == SIMIX_COMM_RECEIVE
-                 && comm1->dst_proc == current_process) {
-        comm2 =
-            get_comm_pattern_from_idx(pattern, &recv_index, comm1->type,
-                                      current_process);
-        comm_comparison = compare_comm_pattern(comm1, comm2);
-        if (comm_comparison == 1) {
-          initial_global_state->comm_deterministic = 0;
-          if (!_sg_mc_send_determinism)
+    process_comms_pattern1 = (xbt_dynar_t)xbt_dynar_get_as(initial_communications_pattern, current_process, xbt_dynar_t);
+    process_comms_pattern2 = (xbt_dynar_t)xbt_dynar_get_as(pattern, current_process, xbt_dynar_t);
+    nb_comms1 = xbt_dynar_length(process_comms_pattern1);
+    nb_comms2 = xbt_dynar_length(process_comms_pattern2);
+    if(!xbt_dynar_is_empty((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t)))
+      xbt_die("Damn ! Some communications from the process %u are incomplete (%lu)! That means one or several simcalls are not handle.", current_process, xbt_dynar_length((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t)));
+    if (!partial && (nb_comms1 != nb_comms2)) {
+      XBT_INFO("The total number of communications is different between the compared patterns for the process %u.\n Communication determinism verification for this process cannot be performed.", current_process);
+      initial_global_state->send_deterministic = -1;
+      initial_global_state->comm_deterministic = -1;
+    } else {
+      while (cursor < nb_comms2) {
+        comm1 = (mc_comm_pattern_t)xbt_dynar_get_as(process_comms_pattern1, cursor, mc_comm_pattern_t);
+        if (comm1->type == SIMIX_COMM_SEND && comm1->src_proc == current_process) {
+          comm2 = get_comm_pattern_from_idx(process_comms_pattern2, &send_index, comm1->type, current_process);
+          if (compare_comm_pattern(comm1, comm2)) {
+            XBT_INFO("The communications pattern of the process %u is different!", current_process);
+            initial_global_state->send_deterministic = 0;
+            initial_global_state->comm_deterministic = 0;
             return;
+          }
+          send_index++;
+        } else if (comm1->type == SIMIX_COMM_RECEIVE && comm1->dst_proc == current_process) {
+          comm2 = get_comm_pattern_from_idx(process_comms_pattern2, &recv_index, comm1->type, current_process);
+          if (compare_comm_pattern(comm1, comm2)) {
+            initial_global_state->comm_deterministic = 0;
+            if (!_sg_mc_send_determinism){
+              XBT_INFO("The communications pattern of the process %u is different!", current_process);
+              return;
+            }
+          }
+          recv_index++;
         }
-        recv_index++;
+        cursor++;
       }
-      cursor++;
     }
+    current_process++;
     cursor = 0;
     send_index = 0;
     recv_index = 0;
-    current_process++;
   }
 }
 
@@ -122,18 +125,46 @@ static void print_communications_pattern(xbt_dynar_t comms_pattern)
 {
   unsigned int cursor = 0;
   mc_comm_pattern_t current_comm;
-  xbt_dynar_foreach(comms_pattern, cursor, current_comm) {
-    if (current_comm->type == SIMIX_COMM_SEND)
-      XBT_INFO("[(%lu) %s -> (%lu) %s] %s ", current_comm->src_proc,
-               current_comm->src_host, current_comm->dst_proc,
-               current_comm->dst_host, "iSend");
-    else
-      XBT_INFO("[(%lu) %s <- (%lu) %s] %s ", current_comm->dst_proc,
-               current_comm->dst_host, current_comm->src_proc,
-               current_comm->src_host, "iRecv");
+  unsigned int current_process = 1;
+  xbt_dynar_t current_pattern;
+  while (current_process < simix_process_maxpid) {
+    current_pattern = (xbt_dynar_t)xbt_dynar_get_as(comms_pattern, current_process, xbt_dynar_t);
+    XBT_INFO("Communications from the process %u:", current_process);
+    xbt_dynar_foreach(current_pattern, cursor, current_comm) {
+      if (current_comm->type == SIMIX_COMM_SEND) {
+        XBT_INFO("[(%lu) %s -> (%lu) %s] %s ", current_comm->src_proc,
+                 current_comm->src_host, current_comm->dst_proc,
+                 current_comm->dst_host, "iSend");
+      } else {
+        XBT_INFO("[(%lu) %s <- (%lu) %s] %s ", current_comm->dst_proc,
+                 current_comm->dst_host, current_comm->src_proc,
+                 current_comm->src_host, "iRecv");
+      }
+    }
+    current_process++;
+    cursor = 0;
   }
 }
 
+static void update_comm_pattern(mc_comm_pattern_t comm_pattern, smx_action_t comm)
+{
+  void *addr_pointed;
+  comm_pattern->src_proc = comm->comm.src_proc->pid;
+  comm_pattern->dst_proc = comm->comm.dst_proc->pid;
+  comm_pattern->src_host =
+    simcall_host_get_name(comm->comm.src_proc->smx_host);
+  comm_pattern->dst_host =
+    simcall_host_get_name(comm->comm.dst_proc->smx_host);
+  if (comm_pattern->data_size == -1) {
+    comm_pattern->data_size = *(comm->comm.dst_buff_size);
+    comm_pattern->data = xbt_malloc0(comm_pattern->data_size);
+    addr_pointed = *(void **) comm->comm.src_buff;
+    if (addr_pointed > std_heap && addr_pointed < ((xbt_mheap_t) std_heap)->breakval)
+      memcpy(comm_pattern->data, addr_pointed, comm_pattern->data_size);
+    else
+      memcpy(comm_pattern->data, comm->comm.src_buff, comm_pattern->data_size);
+  }
+}
 
 /********** Non Static functions ***********/
 
@@ -145,8 +176,8 @@ void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, int call)
   pattern->data_size = -1;
   void *addr_pointed;
   if (call == 1) {              // ISEND
-    pattern->comm = simcall_comm_isend__get__result(request);
     pattern->type = SIMIX_COMM_SEND;
+    pattern->comm = simcall_comm_isend__get__result(request);
     pattern->src_proc = pattern->comm->comm.src_proc->pid;
     pattern->src_host = simcall_host_get_name(request->issuer->smx_host);
     pattern->data_size = pattern->comm->comm.src_buff_size;
@@ -158,11 +189,10 @@ void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, int call)
     else
       memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size);
   } else {                      // IRECV
-    pattern->comm = simcall_comm_irecv__get__result(request);
     pattern->type = SIMIX_COMM_RECEIVE;
+    pattern->comm = simcall_comm_irecv__get__result(request);
     pattern->dst_proc = pattern->comm->comm.dst_proc->pid;
-    pattern->dst_host =
-        simcall_host_get_name(pattern->comm->comm.dst_proc->smx_host);
+    pattern->dst_host = simcall_host_get_name(request->issuer->smx_host);
   }
 
   if (pattern->comm->comm.rdv != NULL)
@@ -170,63 +200,124 @@ void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, int call)
   else
     pattern->rdv = strdup(pattern->comm->comm.rdv_cpy->name);
 
-  xbt_dynar_push(list, &pattern);
+  xbt_dynar_push((xbt_dynar_t)xbt_dynar_get_as(list, request->issuer->pid, xbt_dynar_t), &pattern);
 
-  xbt_dynar_push_as(incomplete_communications_pattern, int,
-                    xbt_dynar_length(list) - 1);
+  xbt_dynar_push_as((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, request->issuer->pid, xbt_dynar_t), int, xbt_dynar_length((xbt_dynar_t)xbt_dynar_get_as(list, request->issuer->pid, xbt_dynar_t)) - 1);
 
 }
 
 void complete_comm_pattern(xbt_dynar_t list, smx_action_t comm)
 {
-  mc_comm_pattern_t current_pattern;
+  mc_comm_pattern_t current_comm_pattern;
   unsigned int cursor = 0;
   int index;
-  int completed = 0;
-  void *addr_pointed;
-  xbt_dynar_foreach(incomplete_communications_pattern, cursor, index) {
-    current_pattern =
-        (mc_comm_pattern_t) xbt_dynar_get_as(list, index, mc_comm_pattern_t);
-    if (current_pattern->comm == comm) {
-      current_pattern->src_proc = comm->comm.src_proc->pid;
-      current_pattern->dst_proc = comm->comm.dst_proc->pid;
-      current_pattern->src_host =
-          simcall_host_get_name(comm->comm.src_proc->smx_host);
-      current_pattern->dst_host =
-          simcall_host_get_name(comm->comm.dst_proc->smx_host);
-      if (current_pattern->data_size == -1) {
-        current_pattern->data_size = *(comm->comm.dst_buff_size);
-        current_pattern->data = xbt_malloc0(current_pattern->data_size);
-        addr_pointed = *(void **) comm->comm.src_buff;
-        if (addr_pointed > std_heap
-            && addr_pointed < ((xbt_mheap_t) std_heap)->breakval)
-          memcpy(current_pattern->data, addr_pointed,
-                 current_pattern->data_size);
-        else
-          memcpy(current_pattern->data, comm->comm.src_buff,
-                 current_pattern->data_size);
-      }
-      xbt_dynar_remove_at(incomplete_communications_pattern, cursor, NULL);
-      completed++;
-      if (completed == 2)
-        return;
-      cursor--;
+  unsigned int src = comm->comm.src_proc->pid;
+  unsigned int dst = comm->comm.dst_proc->pid;
+  int src_completed = 0, dst_completed = 0;
+
+  /* Looking for the corresponding communication in the comm pattern list of the src process */
+  xbt_dynar_foreach((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, src, xbt_dynar_t), cursor, index){
+    current_comm_pattern = (mc_comm_pattern_t) xbt_dynar_get_as((xbt_dynar_t)xbt_dynar_get_as(list, src, xbt_dynar_t), index, mc_comm_pattern_t);
+    if(current_comm_pattern->comm == comm){
+      update_comm_pattern(current_comm_pattern, comm);
+      xbt_dynar_remove_at((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, src, xbt_dynar_t), cursor, NULL);
+      src_completed = 1;
+      break;
+    }
+  }
+
+  if(!src_completed)
+    xbt_die("Corresponding communication for the source process not found!");
+
+  cursor = 0;
+
+  /* Looking for the corresponding communication in the comm pattern list of the dst process */
+  xbt_dynar_foreach((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, dst, xbt_dynar_t), cursor, index){
+    current_comm_pattern = (mc_comm_pattern_t) xbt_dynar_get_as((xbt_dynar_t)xbt_dynar_get_as(list, dst, xbt_dynar_t), index, mc_comm_pattern_t);
+    if(current_comm_pattern->comm == comm){
+      update_comm_pattern(current_comm_pattern, comm);
+      xbt_dynar_remove_at((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, dst, xbt_dynar_t), cursor, NULL);
+      dst_completed = 1;
+      break;
     }
   }
+
+  if(!dst_completed)
+    xbt_die("Corresponding communication for the dest process not found!");
+
+
 }
 
 /************************ Main algorithm ************************/
 
-static void MC_modelcheck_comm_determinism(void)
+void MC_pre_modelcheck_comm_determinism(void)
+{
+
+  int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
+
+  mc_state_t initial_state = NULL;
+  smx_process_t process;
+  int i;
+
+  if (!mc_mem_set)
+    MC_SET_MC_HEAP;
+
+  if (_sg_mc_visited > 0)
+    visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
+ 
+  initial_communications_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp);
+  for (i=0; i<simix_process_maxpid; i++){
+    xbt_dynar_t process_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp);
+    xbt_dynar_insert_at(initial_communications_pattern, i, &process_pattern);
+  }
+  communications_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp);
+  for (i=0; i<simix_process_maxpid; i++){
+    xbt_dynar_t process_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp);
+    xbt_dynar_insert_at(communications_pattern, i, &process_pattern);
+  }
+  incomplete_communications_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp);
+  for (i=0; i<simix_process_maxpid; i++){
+    xbt_dynar_t process_pattern = xbt_dynar_new(sizeof(int), NULL);
+    xbt_dynar_insert_at(incomplete_communications_pattern, i, &process_pattern);
+  }
+
+  nb_comm_pattern = 0;
+
+  initial_state = MC_state_new();
+
+  MC_SET_STD_HEAP;
+
+  XBT_DEBUG("********* Start communication determinism verification *********");
+
+  /* Wait for requests (schedules processes) */
+  MC_wait_for_requests();
+
+  MC_SET_MC_HEAP;
+
+  /* Get an enabled process and insert it in the interleave set of the initial state */
+  xbt_swag_foreach(process, simix_global->process_list) {
+    if (MC_process_is_enabled(process)) {
+      MC_state_interleave_process(initial_state, process);
+    }
+  }
+
+  xbt_fifo_unshift(mc_stack, initial_state);
+
+  MC_SET_STD_HEAP;
+
+}
+
+void MC_modelcheck_comm_determinism(void)
 {
 
   char *req_str = NULL;
-  int value;
+  int value, call = 0;
+  mc_visited_state_t visited_state = NULL;
   smx_simcall_t req = NULL;
   smx_process_t process = NULL;
   mc_state_t state = NULL, next_state = NULL;
-  int comm_pattern = 0, visited_state = -1;
   smx_action_t current_comm;
+  xbt_dynar_t current_pattern;
 
   while (xbt_fifo_size(mc_stack) > 0) {
 
@@ -245,7 +336,7 @@ static void MC_modelcheck_comm_determinism(void)
 
     if ((xbt_fifo_size(mc_stack) <= _sg_mc_max_depth)
         && (req = MC_state_get_request(state, &value))
-        && (visited_state == -1)) {
+        && (visited_state == NULL)) {
 
       /* Debug information */
       if (XBT_LOG_ISENABLED(mc_comm_determinism, xbt_log_priority_debug)) {
@@ -265,46 +356,36 @@ static void MC_modelcheck_comm_determinism(void)
       /* TODO : handle test and testany simcalls */
       if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
         if (req->call == SIMCALL_COMM_ISEND)
-          comm_pattern = 1;
+          call = 1;
         else if (req->call == SIMCALL_COMM_IRECV)
-          comm_pattern = 2;
+          call = 2;
         else if (req->call == SIMCALL_COMM_WAIT)
-          comm_pattern = 3;
+          call = 3;
         else if (req->call == SIMCALL_COMM_WAITANY)
-          comm_pattern = 4;
+          call = 4;
       }
 
       /* Answer the request */
       SIMIX_simcall_pre(req, value);    /* After this call req is no longer usefull */
 
       MC_SET_MC_HEAP;
-      if (comm_pattern == 1 || comm_pattern == 2) {
-        if (!initial_global_state->initial_communications_pattern_done)
-          get_comm_pattern(initial_communications_pattern, req, comm_pattern);
-        else
-          get_comm_pattern(communications_pattern, req, comm_pattern);
-      } else if (comm_pattern == 3) {
+      current_pattern = !initial_global_state->initial_communications_pattern_done ? initial_communications_pattern : communications_pattern; 
+      if (call == 1) { /* Send */
+        get_comm_pattern(current_pattern, req, call);
+      } else if (call == 2) { /* Recv */
+        get_comm_pattern(current_pattern, req, call);
+      } else if (call == 3) { /* Wait */
         current_comm = simcall_comm_wait__get__comm(req);
-        if (current_comm->comm.refcount == 1) { /* First wait only must be considered */
-          if (!initial_global_state->initial_communications_pattern_done)
-            complete_comm_pattern(initial_communications_pattern, current_comm);
-          else
-            complete_comm_pattern(communications_pattern, current_comm);
-        }
-      } else if (comm_pattern == 4) {
-        current_comm =
-            xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value,
-                             smx_action_t);
-        if (current_comm->comm.refcount == 1) { /* First wait only must be considered */
-          if (!initial_global_state->initial_communications_pattern_done)
-            complete_comm_pattern(initial_communications_pattern, current_comm);
-          else
-            complete_comm_pattern(communications_pattern, current_comm);
-        }
+        if (current_comm->comm.refcount == 1)  /* First wait only must be considered */
+          complete_comm_pattern(current_pattern, current_comm);
+      } else if (call == 4) { /* WaitAny */
+        current_comm = xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value, smx_action_t);
+        if (current_comm->comm.refcount == 1) /* First wait only must be considered */
+          complete_comm_pattern(current_pattern, current_comm);
       }
       MC_SET_STD_HEAP;
 
-      comm_pattern = 0;
+      call = 0;
 
       /* Wait for requests (schedules processes) */
       MC_wait_for_requests();
@@ -314,9 +395,9 @@ static void MC_modelcheck_comm_determinism(void)
 
       next_state = MC_state_new();
 
-      if ((visited_state = is_visited_state()) == -1) {
+      if ((visited_state = is_visited_state()) == NULL) {
 
-        /* Get an enabled process and insert it in the interleave set of the next state */
+        /* Get enabled processes and insert them in the interleave set of the next state */
         xbt_swag_foreach(process, simix_global->process_list) {
           if (MC_process_is_enabled(process)) {
             MC_state_interleave_process(next_state, process);
@@ -331,7 +412,7 @@ static void MC_modelcheck_comm_determinism(void)
 
         if (dot_output != NULL)
           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,
-                  visited_state, req_str);
+                  visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
 
       }
 
@@ -346,48 +427,48 @@ static void MC_modelcheck_comm_determinism(void)
 
       if (xbt_fifo_size(mc_stack) > _sg_mc_max_depth) {
         XBT_WARN("/!\\ Max depth reached ! /!\\ ");
-      } else if (visited_state != -1) {
-        XBT_DEBUG("State already visited, stop the exploration");
+      } else if (visited_state != NULL) {
+        XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.", visited_state->other_num == -1 ? visited_state->num : visited_state->other_num);
       } else {
-        XBT_DEBUG("There are no more processes to interleave. (depth %d)",
-                  xbt_fifo_size(mc_stack) + 1);
+        XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack));
       }
 
       MC_SET_MC_HEAP;
 
       if (initial_global_state->initial_communications_pattern_done) {
-        if (visited_state == -1) {
-          deterministic_pattern(initial_communications_pattern,
-                                communications_pattern);
-          if (initial_global_state->comm_deterministic == 0
-              && _sg_mc_comms_determinism) {
+        if (!visited_state) {
+          deterministic_pattern(communications_pattern, 0);
+        } else {
+          deterministic_pattern(communications_pattern, 1);
+        }
+
+        if (_sg_mc_comms_determinism && !initial_global_state->comm_deterministic) {
             XBT_INFO("****************************************************");
             XBT_INFO("***** Non-deterministic communications pattern *****");
             XBT_INFO("****************************************************");
-            XBT_INFO("Initial communications pattern:");
+            XBT_INFO("** Initial communications pattern (per process): **");
             print_communications_pattern(initial_communications_pattern);
-            XBT_INFO("Communications pattern counter-example:");
+            XBT_INFO("** Communications pattern counter-example (per process): **");
             print_communications_pattern(communications_pattern);
             MC_print_statistics(mc_stats);
+            MC_SET_STD_HEAP;
             return;
-          } else if (initial_global_state->send_deterministic == 0
-                     && _sg_mc_send_determinism) {
+          } else if (_sg_mc_send_determinism && !initial_global_state->send_deterministic) {
             XBT_INFO
                 ("*********************************************************");
             XBT_INFO
                 ("***** Non-send-deterministic communications pattern *****");
             XBT_INFO
                 ("*********************************************************");
-            XBT_INFO("Initial communications pattern:");
+            XBT_INFO("** Initial communications pattern: **");
             print_communications_pattern(initial_communications_pattern);
-            XBT_INFO("Communications pattern counter-example:");
+            XBT_INFO("** Communications pattern counter-example: **");
             print_communications_pattern(communications_pattern);
             MC_print_statistics(mc_stats);
+            MC_SET_STD_HEAP;
             return;
-          }
-        } else {
-
         }
+
       } else {
         initial_global_state->initial_communications_pattern_done = 1;
       }
@@ -400,7 +481,7 @@ static void MC_modelcheck_comm_determinism(void)
 
       MC_SET_STD_HEAP;
 
-      visited_state = -1;
+      visited_state = NULL;
 
       /* Check for deadlocks */
       if (MC_deadlock_check()) {
@@ -408,6 +489,8 @@ static void MC_modelcheck_comm_determinism(void)
         return;
       }
 
+      MC_SET_MC_HEAP;
+
       while ((state = xbt_fifo_shift(mc_stack)) != NULL) {
         if (MC_state_interleave_size(state)
             && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
@@ -438,56 +521,3 @@ static void MC_modelcheck_comm_determinism(void)
 
   return;
 }
-
-void MC_pre_modelcheck_comm_determinism(void)
-{
-
-  int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
-
-  mc_state_t initial_state = NULL;
-  smx_process_t process;
-
-  if (!mc_mem_set)
-    MC_SET_MC_HEAP;
-
-  if (_sg_mc_visited > 0)
-    visited_states =
-        xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
-
-  initial_communications_pattern =
-      xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp);
-  communications_pattern =
-      xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp);
-  incomplete_communications_pattern = xbt_dynar_new(sizeof(int), NULL);
-  nb_comm_pattern = 0;
-
-  initial_state = MC_state_new();
-
-  MC_SET_STD_HEAP;
-
-  XBT_DEBUG("********* Start communication determinism verification *********");
-
-  /* Wait for requests (schedules processes) */
-  MC_wait_for_requests();
-
-  if (_sg_mc_visited > 0) {
-    MC_ignore_heap(simix_global->process_to_run->data, 0);
-    MC_ignore_heap(simix_global->process_that_ran->data, 0);
-  }
-
-  MC_SET_MC_HEAP;
-
-  /* Get an enabled process and insert it in the interleave set of the initial state */
-  xbt_swag_foreach(process, simix_global->process_list) {
-    if (MC_process_is_enabled(process)) {
-      MC_state_interleave_process(initial_state, process);
-    }
-  }
-
-  xbt_fifo_unshift(mc_stack, initial_state);
-
-  MC_SET_STD_HEAP;
-
-  MC_modelcheck_comm_determinism();
-
-}