X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/78c913384603a2111abf8f170b2a2d0090aabf45..e0300cbd373040c590de77e64cc6c6e5fc3c28bb:/src/mc/mc_comm_determinism.c

diff --git a/src/mc/mc_comm_determinism.c b/src/mc/mc_comm_determinism.c
index 37a6f9054f..8b59b3ada3 100644
--- a/src/mc/mc_comm_determinism.c
+++ b/src/mc/mc_comm_determinism.c
@@ -4,7 +4,13 @@
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
+#include "mc_state.h"
+#include "mc_comm_pattern.h"
+#include "mc_request.h"
+#include "mc_safety.h"
 #include "mc_private.h"
+#include "mc_record.h"
+#include "mc_smx.h"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_comm_determinism, mc,
                                 "Logging specific to MC communication determinism detection");
@@ -13,8 +19,6 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_comm_determinism, mc,
 
 xbt_dynar_t initial_communications_pattern;
 xbt_dynar_t incomplete_communications_pattern;
-xbt_dynar_t communications_pattern;
-int nb_comm_pattern;
 
 /********** Static functions ***********/
 
@@ -26,223 +30,285 @@ static void comm_pattern_free(mc_comm_pattern_t p)
   p = NULL;
 }
 
-static void comm_pattern_free_voidp(void *p)
+static void list_comm_pattern_free(mc_list_comm_pattern_t l)
 {
-  comm_pattern_free((mc_comm_pattern_t) * (void **) p);
-}
-
-static mc_comm_pattern_t get_comm_pattern_from_idx(xbt_dynar_t pattern,
-                                                   unsigned int *idx,
-                                                   e_smx_comm_type_t type,
-                                                   unsigned long proc)
-{
-  mc_comm_pattern_t current_comm;
-  while (*idx < xbt_dynar_length(pattern)) {
-    current_comm =
-        (mc_comm_pattern_t) xbt_dynar_get_as(pattern, *idx, mc_comm_pattern_t);
-    if (current_comm->type == type && type == SIMIX_COMM_SEND) {
-      if (current_comm->src_proc == proc)
-        return current_comm;
-    } else if (current_comm->type == type && type == SIMIX_COMM_RECEIVE) {
-      if (current_comm->dst_proc == proc)
-        return current_comm;
-    }
-    (*idx)++;
-  }
-  return NULL;
+  xbt_dynar_free(&(l->list));
+  xbt_free(l);
+  l = NULL;
 }
 
-static int compare_comm_pattern(mc_comm_pattern_t comm1,
-                                mc_comm_pattern_t comm2)
-{
+static e_mc_comm_pattern_difference_t compare_comm_pattern(mc_comm_pattern_t comm1, mc_comm_pattern_t comm2) {
+  if(comm1->type != comm2->type)
+    return TYPE_DIFF;
   if (strcmp(comm1->rdv, comm2->rdv) != 0)
-    return 1;
+    return RDV_DIFF;
   if (comm1->src_proc != comm2->src_proc)
-    return 1;
+    return SRC_PROC_DIFF;
   if (comm1->dst_proc != comm2->dst_proc)
-    return 1;
+    return DST_PROC_DIFF;
+  if (comm1->tag != comm2->tag)
+    return TAG_DIFF;
   if (comm1->data_size != comm2->data_size)
-    return 1;
-  if (memcmp(comm1->data, comm2->data, comm1->data_size) != 0)
-    return 1;
+    return DATA_SIZE_DIFF;
+  if(comm1->data == NULL && comm2->data == NULL)
+    return 0;
+  if(comm1->data != NULL && comm2->data !=NULL) {
+    if (!memcmp(comm1->data, comm2->data, comm1->data_size))
+      return 0;
+    return DATA_DIFF;
+  }else{
+    return DATA_DIFF;
+  }
   return 0;
 }
 
-static void deterministic_pattern(xbt_dynar_t initial_pattern,
-                                  xbt_dynar_t pattern)
-{
+static char* print_determinism_result(e_mc_comm_pattern_difference_t diff, int process, mc_comm_pattern_t comm, unsigned int cursor) {
+  char *type, *res;
 
-  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;
-  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)
-            return;
-        }
-        recv_index++;
-      }
-      cursor++;
-    }
-    cursor = 0;
-    send_index = 0;
-    recv_index = 0;
-    current_process++;
+  if(comm->type == SIMIX_COMM_SEND)
+    type = bprintf("The send communications pattern of the process %d is different!", process - 1);
+  else
+    type = bprintf("The recv communications pattern of the process %d is different!", process - 1);
+
+  switch(diff) {
+  case TYPE_DIFF:
+    res = bprintf("%s Different type for communication #%d", type, cursor);
+    break;
+  case RDV_DIFF:
+    res = bprintf("%s Different rdv for communication #%d", type, cursor);
+    break;
+  case TAG_DIFF:
+    res = bprintf("%s Different tag for communication #%d", type, cursor);
+    break;
+  case SRC_PROC_DIFF:
+      res = bprintf("%s Different source for communication #%d", type, cursor);
+    break;
+  case DST_PROC_DIFF:
+      res = bprintf("%s Different destination for communication #%d", type, cursor);
+    break;
+  case DATA_SIZE_DIFF:
+    res = bprintf("%s\n Different data size for communication #%d", type, cursor);
+    break;
+  case DATA_DIFF:
+    res = bprintf("%s\n Different data for communication #%d", type, cursor);
+    break;
+  default:
+    res = NULL;
+    break;
   }
+
+  return res;
 }
 
-static void print_communications_pattern(xbt_dynar_t comms_pattern)
+// FIXME, remote comm
+static void update_comm_pattern(mc_comm_pattern_t comm_pattern, smx_synchro_t comm)
 {
-  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");
+  mc_process_t process = &mc_model_checker->process;
+  void *addr_pointed;
+  smx_process_t src_proc = MC_smx_resolve_process(comm->comm.src_proc);
+  smx_process_t dst_proc = MC_smx_resolve_process(comm->comm.dst_proc);
+  comm_pattern->src_proc = src_proc->pid;
+  comm_pattern->dst_proc = dst_proc->pid;
+  // TODO, resolve host name
+  comm_pattern->src_host = MC_smx_process_get_host_name(src_proc);
+  comm_pattern->dst_host = MC_smx_process_get_host_name(dst_proc);
+  if (comm_pattern->data_size == -1 && comm->comm.src_buff != NULL) {
+    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 > (void*) process->heap_address
+        && addr_pointed < MC_process_get_heap(process)->breakval)
+      memcpy(comm_pattern->data, addr_pointed, comm_pattern->data_size);
     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");
+      memcpy(comm_pattern->data, comm->comm.src_buff, comm_pattern->data_size);
   }
 }
 
+static void deterministic_comm_pattern(int process, mc_comm_pattern_t comm, int backtracking) {
+
+  mc_list_comm_pattern_t list_comm_pattern = (mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, process, mc_list_comm_pattern_t);
+
+  if(!backtracking){
+    mc_comm_pattern_t initial_comm = xbt_dynar_get_as(list_comm_pattern->list, list_comm_pattern->index_comm, mc_comm_pattern_t);
+    e_mc_comm_pattern_difference_t diff;
+    
+    if((diff = compare_comm_pattern(initial_comm, comm)) != NONE_DIFF){
+      if (comm->type == SIMIX_COMM_SEND){
+        initial_global_state->send_deterministic = 0;
+        if(initial_global_state->send_diff != NULL)
+          xbt_free(initial_global_state->send_diff);
+        initial_global_state->send_diff = print_determinism_result(diff, process, comm, list_comm_pattern->index_comm + 1);
+      }else{
+        initial_global_state->recv_deterministic = 0;
+        if(initial_global_state->recv_diff != NULL)
+          xbt_free(initial_global_state->recv_diff);
+        initial_global_state->recv_diff = print_determinism_result(diff, process, comm, list_comm_pattern->index_comm + 1);
+      }
+      if(_sg_mc_send_determinism && !initial_global_state->send_deterministic){
+        XBT_INFO("*********************************************************");
+        XBT_INFO("***** Non-send-deterministic communications pattern *****");
+        XBT_INFO("*********************************************************");
+        XBT_INFO("%s", initial_global_state->send_diff);
+        xbt_free(initial_global_state->send_diff);
+        initial_global_state->send_diff = NULL;
+        MC_print_statistics(mc_stats);
+        xbt_abort(); 
+      }else if(_sg_mc_comms_determinism && (!initial_global_state->send_deterministic && !initial_global_state->recv_deterministic)) {
+        XBT_INFO("****************************************************");
+        XBT_INFO("***** Non-deterministic communications pattern *****");
+        XBT_INFO("****************************************************");
+        XBT_INFO("%s", initial_global_state->send_diff);
+        XBT_INFO("%s", initial_global_state->recv_diff);
+        xbt_free(initial_global_state->send_diff);
+        initial_global_state->send_diff = NULL;
+        xbt_free(initial_global_state->recv_diff);
+        initial_global_state->recv_diff = NULL;
+        MC_print_statistics(mc_stats);
+        xbt_abort();
+      } 
+    }
+  }
+    
+  comm_pattern_free(comm);
+
+}
 
 /********** Non Static functions ***********/
 
-void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, int call)
+void comm_pattern_free_voidp(void *p) {
+  comm_pattern_free((mc_comm_pattern_t) * (void **) p);
+}
+
+void list_comm_pattern_free_voidp(void *p) {
+  list_comm_pattern_free((mc_list_comm_pattern_t) * (void **) p);
+}
+
+void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking)
 {
-  mc_comm_pattern_t pattern = NULL;
-  pattern = xbt_new0(s_mc_comm_pattern_t, 1);
-  pattern->num = ++nb_comm_pattern;
+  mc_process_t process = &mc_model_checker->process;
+
+  mc_comm_pattern_t pattern = xbt_new0(s_mc_comm_pattern_t, 1);
   pattern->data_size = -1;
+  pattern->data = NULL;
+
+  // Fill initial_pattern->index_comm:
+  const smx_process_t issuer = MC_smx_simcall_get_issuer(request);
+  mc_list_comm_pattern_t initial_pattern =
+    (mc_list_comm_pattern_t) xbt_dynar_get_as(initial_communications_pattern, issuer->pid, mc_list_comm_pattern_t);
+  xbt_dynar_t incomplete_pattern =
+    (xbt_dynar_t) xbt_dynar_get_as(incomplete_communications_pattern, issuer->pid, xbt_dynar_t);
+  pattern->index =
+    initial_pattern->index_comm + xbt_dynar_length(incomplete_pattern);
+  
   void *addr_pointed;
-  if (call == 1) {              // ISEND
-    pattern->comm = simcall_comm_isend__get__result(request);
+  
+  if (call_type == MC_CALL_TYPE_SEND) {
+    /* Create comm pattern */
     pattern->type = SIMIX_COMM_SEND;
-    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;
-    pattern->data = xbt_malloc0(pattern->data_size);
-    addr_pointed = *(void **) pattern->comm->comm.src_buff;
-    if (addr_pointed > std_heap
-        && addr_pointed < ((xbt_mheap_t) std_heap)->breakval)
-      memcpy(pattern->data, addr_pointed, pattern->data_size);
-    else
-      memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size);
-  } else {                      // IRECV
-    pattern->comm = simcall_comm_irecv__get__result(request);
+    pattern->comm = simcall_comm_isend__get__result(request);
+    // FIXME, remote access to rdv->name
+    pattern->rdv = (pattern->comm->comm.rdv != NULL) ? strdup(pattern->comm->comm.rdv->name) : strdup(pattern->comm->comm.rdv_cpy->name);
+    pattern->src_proc = MC_smx_resolve_process(pattern->comm->comm.src_proc)->pid;
+    pattern->src_host = MC_smx_process_get_host_name(issuer);
+    pattern->tag = ((MPI_Request)simcall_comm_isend__get__data(request))->tag;
+    if(pattern->comm->comm.src_buff != NULL){
+      pattern->data_size = pattern->comm->comm.src_buff_size;
+      pattern->data = xbt_malloc0(pattern->data_size);
+      addr_pointed = *(void **) pattern->comm->comm.src_buff;
+      if (addr_pointed > (void*) process->heap_address
+          && addr_pointed < MC_process_get_heap(process)->breakval)
+        memcpy(pattern->data, addr_pointed, pattern->data_size);
+      else
+        memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size);
+    }
+    if(((MPI_Request)simcall_comm_isend__get__data(request))->detached){
+      if (!initial_global_state->initial_communications_pattern_done) {
+        /* Store comm pattern */
+        xbt_dynar_push(((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, pattern->src_proc, mc_list_comm_pattern_t))->list, &pattern);
+      } else {
+        /* Evaluate comm determinism */
+        deterministic_comm_pattern(pattern->src_proc, pattern, backtracking);
+        ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, pattern->src_proc, mc_list_comm_pattern_t))->index_comm++;
+      }
+      return;
+    }
+  } else if (call_type == MC_CALL_TYPE_RECV) {                      
     pattern->type = SIMIX_COMM_RECEIVE;
-    pattern->dst_proc = pattern->comm->comm.dst_proc->pid;
-    pattern->dst_host =
-        simcall_host_get_name(pattern->comm->comm.dst_proc->smx_host);
+    pattern->comm = simcall_comm_irecv__get__result(request);
+    // TODO, remote access
+    pattern->tag = ((MPI_Request)simcall_comm_irecv__get__data(request))->tag;
+    pattern->rdv = (pattern->comm->comm.rdv != NULL) ? strdup(pattern->comm->comm.rdv->name) : strdup(pattern->comm->comm.rdv_cpy->name);
+    pattern->dst_proc = MC_smx_resolve_process(pattern->comm->comm.dst_proc)->pid;
+    // FIXME, remote process access
+    pattern->dst_host = MC_smx_process_get_host_name(issuer);
+  } else {
+    xbt_die("Unexpected call_type %i", (int) call_type);
   }
 
-  if (pattern->comm->comm.rdv != NULL)
-    pattern->rdv = strdup(pattern->comm->comm.rdv->name);
-  else
-    pattern->rdv = strdup(pattern->comm->comm.rdv_cpy->name);
-
-  xbt_dynar_push(list, &pattern);
-
-  xbt_dynar_push_as(incomplete_communications_pattern, int,
-                    xbt_dynar_length(list) - 1);
+  xbt_dynar_push((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, issuer->pid, xbt_dynar_t), &pattern);
 
+  XBT_DEBUG("Insert incomplete comm pattern %p for process %lu", pattern, issuer->pid);
 }
 
-void complete_comm_pattern(xbt_dynar_t list, smx_action_t comm)
-{
-  mc_comm_pattern_t current_pattern;
+void complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm, unsigned int issuer, int backtracking) {
+  mc_comm_pattern_t current_comm_pattern;
   unsigned int cursor = 0;
-  int index;
+  mc_comm_pattern_t comm_pattern;
   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--;
+
+  /* Complete comm pattern */
+  xbt_dynar_foreach((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t), cursor, current_comm_pattern) {
+    if (current_comm_pattern-> comm == comm) {
+      update_comm_pattern(current_comm_pattern, comm);
+      completed = 1;
+      xbt_dynar_remove_at((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t), cursor, &comm_pattern);
+      XBT_DEBUG("Remove incomplete comm pattern for process %u at cursor %u", issuer, cursor);
+      break;
     }
   }
+  if(!completed)
+    xbt_die("Corresponding communication not found!");
+
+  if (!initial_global_state->initial_communications_pattern_done) {
+    /* Store comm pattern */
+    xbt_dynar_push(((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, issuer, mc_list_comm_pattern_t))->list, &comm_pattern);
+  } else {
+    /* Evaluate comm determinism */
+    deterministic_comm_pattern(issuer, comm_pattern, backtracking);
+    ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, issuer, mc_list_comm_pattern_t))->index_comm++;
+  }
 }
 
+
 /************************ Main algorithm ************************/
 
 void MC_pre_modelcheck_comm_determinism(void)
 {
-
-  int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
+  MC_SET_MC_HEAP;
 
   mc_state_t initial_state = NULL;
   smx_process_t process;
-
-  if (!mc_mem_set)
-    MC_SET_MC_HEAP;
+  int i;
 
   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;
+    visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
+ 
+  initial_communications_pattern = xbt_dynar_new(sizeof(mc_list_comm_pattern_t), list_comm_pattern_free_voidp);
+  for (i=0; i < MC_smx_get_maxpid(); i++){
+    mc_list_comm_pattern_t process_list_pattern = xbt_new0(s_mc_list_comm_pattern_t, 1);
+    process_list_pattern->list = xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp);
+    process_list_pattern->index_comm = 0;
+    xbt_dynar_insert_at(initial_communications_pattern, i, &process_list_pattern);
+  }
+  incomplete_communications_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp);
+  for (i=0; i < MC_smx_get_maxpid(); i++){
+    xbt_dynar_t process_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), NULL);
+    xbt_dynar_insert_at(incomplete_communications_pattern, i, &process_pattern);
+  }
 
   initial_state = MC_state_new();
-
   MC_SET_STD_HEAP;
-
+  
   XBT_DEBUG("********* Start communication determinism verification *********");
 
   /* Wait for requests (schedules processes) */
@@ -251,11 +317,11 @@ void MC_pre_modelcheck_comm_determinism(void)
   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) {
+  MC_EACH_SIMIX_PROCESS(process,
     if (MC_process_is_enabled(process)) {
       MC_state_interleave_process(initial_state, process);
     }
-  }
+  );
 
   xbt_fifo_unshift(mc_stack, initial_state);
 
@@ -268,18 +334,15 @@ void MC_modelcheck_comm_determinism(void)
 
   char *req_str = NULL;
   int value;
+  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;
 
   while (xbt_fifo_size(mc_stack) > 0) {
 
     /* Get current state */
-    state =
-        (mc_state_t)
-        xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
+    state = (mc_state_t) xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
 
     XBT_DEBUG("**************************************************");
     XBT_DEBUG("Exploration depth = %d (state = %d, interleaved processes = %d)",
@@ -291,67 +354,37 @@ 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)) {
-
-      /* Debug information */
-      if (XBT_LOG_ISENABLED(mc_comm_determinism, xbt_log_priority_debug)) {
-        req_str = MC_request_to_string(req, value);
-        XBT_DEBUG("Execute: %s", req_str);
-        xbt_free(req_str);
-      }
-
-      MC_SET_MC_HEAP;
-      if (dot_output != NULL)
+        && (visited_state == NULL)) {
+
+      req_str = MC_request_to_string(req, value);  
+      XBT_DEBUG("Execute: %s", req_str);                 
+      xbt_free(req_str);
+      
+      if (dot_output != NULL) {
+        MC_SET_MC_HEAP;
         req_str = MC_request_get_dot_output(req, value);
-      MC_SET_STD_HEAP;
+        MC_SET_STD_HEAP;
+      }
 
       MC_state_set_executed_request(state, req, value);
       mc_stats->executed_transitions++;
 
       /* TODO : handle test and testany simcalls */
+      e_mc_call_type_t call = MC_CALL_TYPE_NONE;
       if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
-        if (req->call == SIMCALL_COMM_ISEND)
-          comm_pattern = 1;
-        else if (req->call == SIMCALL_COMM_IRECV)
-          comm_pattern = 2;
-        else if (req->call == SIMCALL_COMM_WAIT)
-          comm_pattern = 3;
-        else if (req->call == SIMCALL_COMM_WAITANY)
-          comm_pattern = 4;
+        call = mc_get_call_type(req);
       }
 
       /* Answer the request */
-      SIMIX_simcall_pre(req, value);    /* After this call req is no longer usefull */
+      MC_simcall_handle(req, value);    /* After this call req is no longer useful */
 
       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_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(!initial_global_state->initial_communications_pattern_done)
+        handle_comm_pattern(call, req, value, initial_communications_pattern, 0);
+      else
+        handle_comm_pattern(call, req, value, NULL, 0);
       MC_SET_STD_HEAP;
 
-      comm_pattern = 0;
-
       /* Wait for requests (schedules processes) */
       MC_wait_for_requests();
 
@@ -360,24 +393,22 @@ void MC_modelcheck_comm_determinism(void)
 
       next_state = MC_state_new();
 
-      if ((visited_state = is_visited_state()) == -1) {
+      if ((visited_state = is_visited_state(next_state)) == NULL) {
 
-        /* Get an enabled process and insert it in the interleave set of the next state */
-        xbt_swag_foreach(process, simix_global->process_list) {
+        /* Get enabled processes and insert them in the interleave set of the next state */
+        MC_EACH_SIMIX_PROCESS(process,
           if (MC_process_is_enabled(process)) {
             MC_state_interleave_process(next_state, process);
           }
-        }
+        );
 
         if (dot_output != NULL)
-          fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,
-                  next_state->num, req_str);
+          fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,  next_state->num, req_str);
 
       } else {
 
         if (dot_output != NULL)
-          fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,
-                  visited_state, req_str);
+          fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
 
       }
 
@@ -392,63 +423,25 @@ 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, exploration stopped on this path.");
+      } 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) {
-            XBT_INFO("****************************************************");
-            XBT_INFO("***** Non-deterministic communications pattern *****");
-            XBT_INFO("****************************************************");
-            XBT_INFO("Initial communications pattern:");
-            print_communications_pattern(initial_communications_pattern);
-            XBT_INFO("Communications pattern counter-example:");
-            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) {
-            XBT_INFO
-                ("*********************************************************");
-            XBT_INFO
-                ("***** Non-send-deterministic communications pattern *****");
-            XBT_INFO
-                ("*********************************************************");
-            XBT_INFO("Initial communications pattern:");
-            print_communications_pattern(initial_communications_pattern);
-            XBT_INFO("Communications pattern counter-example:");
-            print_communications_pattern(communications_pattern);
-            MC_print_statistics(mc_stats);
-            MC_SET_STD_HEAP;
-            return;
-          }
-        } else {
-
-        }
-      } else {
+      if (!initial_global_state->initial_communications_pattern_done) 
         initial_global_state->initial_communications_pattern_done = 1;
-      }
 
       /* Trash the current state, no longer needed */
       xbt_fifo_shift(mc_stack);
-      MC_state_delete(state);
-      XBT_DEBUG("Delete state %d at depth %d", state->num,
-                xbt_fifo_size(mc_stack) + 1);
+      MC_state_delete(state, !state->in_visited_states ? 1 : 0);
+      XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
 
       MC_SET_STD_HEAP;
 
-      visited_state = -1;
+      visited_state = NULL;
 
       /* Check for deadlocks */
       if (MC_deadlock_check()) {
@@ -459,23 +452,20 @@ void MC_modelcheck_comm_determinism(void)
       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) {
+        if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
           /* We found a back-tracking point, let's loop */
-          XBT_DEBUG("Back-tracking to state %d at depth %d", state->num,
-                    xbt_fifo_size(mc_stack) + 1);
+          XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
           xbt_fifo_unshift(mc_stack, state);
           MC_SET_STD_HEAP;
 
-          MC_replay(mc_stack, -1);
+          MC_replay(mc_stack);
+
+          XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack));
 
-          XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num,
-                    xbt_fifo_size(mc_stack));
           break;
         } else {
-          XBT_DEBUG("Delete state %d at depth %d", state->num,
-                    xbt_fifo_size(mc_stack) + 1);
-          MC_state_delete(state);
+          XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
+          MC_state_delete(state, !state->in_visited_states ? 1 : 0);
         }
       }