model-checker : communications determinism with visited state equality reduction

diff --git a/src/mc/mc_comm_determinism.c b/src/mc/mc_comm_determinism.c
index 9c01b85..b68e563 100644 (file)
--- a/src/mc/mc_comm_determinism.c
+++ b/src/mc/mc_comm_determinism.c
@@ -18,8 +18,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 initial_communications_pattern;
 xbt_dynar_t incomplete_communications_pattern;

-xbt_dynar_t communications_pattern;
-int nb_comm_pattern;

 
 /********** Static functions ***********/
 
 
 /********** Static functions ***********/
 


@@ -31,120 +29,136 @@ static void comm_pattern_free(mc_comm_pattern_t p)
   p = NULL;
 }
 
   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)
   if (strcmp(comm1->rdv, comm2->rdv) != 0)

-    return 1;
+    return RDV_DIFF;

   if (comm1->src_proc != comm2->src_proc)
   if (comm1->src_proc != comm2->src_proc)

-    return 1;
+    return SRC_PROC_DIFF;

   if (comm1->dst_proc != comm2->dst_proc)
   if (comm1->dst_proc != comm2->dst_proc)

-    return 1;
+    return DST_PROC_DIFF;

   if (comm1->data_size != comm2->data_size)
   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;
 }
 
   return 0;
 }
 

-static void deterministic_pattern(xbt_dynar_t pattern, int partial)
-{
-
-  unsigned int cursor = 0, send_index = 0, recv_index = 0;
-  mc_comm_pattern_t comm1, comm2;
-  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) {
-    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) {
-          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! (Different communication : %u)", current_process, cursor+1);
-            initial_global_state->send_deterministic = 0;
-            initial_global_state->comm_deterministic = 0;
-            return;
-          }
-          send_index++;
-        } else if (comm1->type == SIMIX_COMM_RECEIVE) {
-          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! (Different communication : %u)", current_process, cursor+1);
-              return;
-            }
-          }
-          recv_index++;
-        }
-        cursor++;
-      }
+static void print_determinism_result(e_mc_comm_pattern_difference_t diff, int process, mc_comm_pattern_t comm, unsigned int cursor) {
+  if (_sg_mc_comms_determinism && !initial_global_state->comm_deterministic) {
+    XBT_INFO("****************************************************");
+    XBT_INFO("***** Non-deterministic communications pattern *****");
+    XBT_INFO("****************************************************");
+    XBT_INFO("The communications pattern of the process %d is different!",  process);
+    switch(diff) {
+    case TYPE_DIFF:
+      XBT_INFO("Different communication type for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor);
+      break;
+    case RDV_DIFF:
+      XBT_INFO("Different communication rdv for communication %s at index %d",  comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor);
+      break;
+    case SRC_PROC_DIFF:
+        XBT_INFO("Different communication source process for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor);
+      break;
+    case DST_PROC_DIFF:
+        XBT_INFO("Different communication destination process for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor);
+      break;
+    case DATA_SIZE_DIFF:
+      XBT_INFO("Different communication data size for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor);
+      break;
+    case DATA_DIFF:
+      XBT_INFO("Different communication data for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor);
+      break;
+    default:
+      break;

     }
     }

-    current_process++;
-    cursor = 0;
-    send_index = 0;
-    recv_index = 0;
+    MC_print_statistics(mc_stats);
+    xbt_abort();
+  } else if (_sg_mc_send_determinism && !initial_global_state->send_deterministic) {
+    XBT_INFO("*********************************************************");
+    XBT_INFO("***** Non-send-deterministic communications pattern *****");
+    XBT_INFO("*********************************************************");
+    XBT_INFO("The communications pattern of the process %d is different!",  process);
+    switch(diff) {
+    case TYPE_DIFF:
+      XBT_INFO("Different communication type for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor);
+      break;
+    case RDV_DIFF:
+      XBT_INFO("Different communication rdv for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor);
+      break;
+    case SRC_PROC_DIFF:
+        XBT_INFO("Different communication source process for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor);
+      break;
+    case DST_PROC_DIFF:
+        XBT_INFO("Different communication destination process for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor);
+      break;
+    case DATA_SIZE_DIFF:
+      XBT_INFO("Different communication data size for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor);
+      break;
+    case DATA_DIFF:
+      XBT_INFO("Different communication data for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor);
+      break;
+    default:
+      break;
+    }
+    MC_print_statistics(mc_stats);
+    xbt_abort();

   }
 }
 
   }
 }
 

-static void print_communications_pattern(xbt_dynar_t comms_pattern)
+static void print_communications_pattern()

 {
 {

-  unsigned int cursor = 0;
+  unsigned int cursor = 0, cursor2 = 0;

   mc_comm_pattern_t current_comm;
   mc_comm_pattern_t current_comm;

+  mc_list_comm_pattern_t current_list;

   unsigned int current_process = 1;
   unsigned int current_process = 1;

-  xbt_dynar_t current_pattern;

   while (current_process < simix_process_maxpid) {
   while (current_process < simix_process_maxpid) {

-    current_pattern = (xbt_dynar_t)xbt_dynar_get_as(comms_pattern, current_process, xbt_dynar_t);
+    current_list = (mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, current_process, mc_list_comm_pattern_t);

     XBT_INFO("Communications from the process %u:", current_process);
     XBT_INFO("Communications from the process %u:", current_process);

-    xbt_dynar_foreach(current_pattern, cursor, current_comm) {
+    while(cursor2 < current_list->index_comm){
+      current_comm = (mc_comm_pattern_t)xbt_dynar_get_as(current_list->list, cursor2, mc_comm_pattern_t);

       if (current_comm->type == SIMIX_COMM_SEND) {
       if (current_comm->type == SIMIX_COMM_SEND) {

-        XBT_INFO("[(%lu) %s -> (%lu) %s] %s ", current_comm->src_proc,
+        XBT_INFO("(%u) [(%lu) %s -> (%lu) %s] %s ", cursor,current_comm->src_proc,

                  current_comm->src_host, current_comm->dst_proc,
                  current_comm->dst_host, "iSend");
       } else {
                  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,
+        XBT_INFO("(%u) [(%lu) %s <- (%lu) %s] %s ", cursor, current_comm->dst_proc,

                  current_comm->dst_host, current_comm->src_proc,
                  current_comm->src_host, "iRecv");
       }
                  current_comm->dst_host, current_comm->src_proc,
                  current_comm->src_host, "iRecv");
       }

+      cursor2++;
+    }
+    current_process++;
+    cursor = 0;
+    cursor2 = 0;
+  }
+}
+
+static void print_incomplete_communications_pattern(){
+  unsigned int cursor = 0;
+  unsigned int current_process = 1;
+  xbt_dynar_t current_pattern;
+  mc_comm_pattern_t comm;
+  while (current_process < simix_process_maxpid) {
+    current_pattern = (xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t);
+    XBT_INFO("Incomplete communications from the process %u:", current_process);
+    xbt_dynar_foreach(current_pattern, cursor, comm) {
+      XBT_DEBUG("(%u) Communication %p", cursor, comm);

     }
     current_process++;
     cursor = 0;
     }
     current_process++;
     cursor = 0;


@@ -156,11 +170,9 @@ static void update_comm_pattern(mc_comm_pattern_t comm_pattern, smx_synchro_t co
   void *addr_pointed;
   comm_pattern->src_proc = comm->comm.src_proc->pid;
   comm_pattern->dst_proc = comm->comm.dst_proc->pid;
   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->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->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;
     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;


@@ -171,87 +183,139 @@ static void update_comm_pattern(mc_comm_pattern_t comm_pattern, smx_synchro_t co
   }
 }
 
   }
 }
 

+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, comm->index, 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;
+      initial_global_state->comm_deterministic = 0;
+      print_determinism_result(diff, process, comm, list_comm_pattern->index_comm + 1);
+    }
+  }
+    
+  list_comm_pattern->index_comm++;
+  comm_pattern_free(comm);
+
+}
+

 /********** Non Static functions ***********/
 
 /********** Non Static functions ***********/
 

-void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, mc_call_type call_type)
+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)

 {
 {

+

   mc_comm_pattern_t pattern = NULL;
   pattern = xbt_new0(s_mc_comm_pattern_t, 1);
   mc_comm_pattern_t pattern = NULL;
   pattern = xbt_new0(s_mc_comm_pattern_t, 1);

-  pattern->num = ++nb_comm_pattern;

   pattern->data_size = -1;
   pattern->data_size = -1;

+  pattern->data = NULL;
+
+  pattern->index = ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, request->issuer->pid, mc_list_comm_pattern_t))->index_comm + xbt_dynar_length((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, request->issuer->pid, xbt_dynar_t));
+  

   void *addr_pointed;
   void *addr_pointed;

-  if (call_type == MC_CALL_TYPE_SEND) {              // ISEND
+  
+  if (call_type == MC_CALL_TYPE_SEND) {
+    /* Create comm pattern */

     pattern->type = SIMIX_COMM_SEND;
     pattern->comm = simcall_comm_isend__get__result(request);
     pattern->type = SIMIX_COMM_SEND;
     pattern->comm = simcall_comm_isend__get__result(request);

+    pattern->rdv = (pattern->comm->comm.rdv != NULL) ? strdup(pattern->comm->comm.rdv->name) : strdup(pattern->comm->comm.rdv_cpy->name);

     pattern->src_proc = pattern->comm->comm.src_proc->pid;
     pattern->src_host = simcall_host_get_name(request->issuer->smx_host);
     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 > (void*) std_heap && addr_pointed < std_heap->breakval)
-      memcpy(pattern->data, addr_pointed, pattern->data_size);
-    else
-      memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size);
-  } else if (call_type == MC_CALL_TYPE_RECV) {                      // IRECV
+    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*) std_heap && addr_pointed < std_heap->breakval)
+        memcpy(pattern->data, addr_pointed, pattern->data_size);
+      else
+        memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size);
+    }
+  } else if (call_type == MC_CALL_TYPE_RECV) {                      

     pattern->type = SIMIX_COMM_RECEIVE;
     pattern->comm = simcall_comm_irecv__get__result(request);
     pattern->type = SIMIX_COMM_RECEIVE;
     pattern->comm = simcall_comm_irecv__get__result(request);

+    pattern->rdv = (pattern->comm->comm.rdv != NULL) ? strdup(pattern->comm->comm.rdv->name) : strdup(pattern->comm->comm.rdv_cpy->name);

     pattern->dst_proc = pattern->comm->comm.dst_proc->pid;
     pattern->dst_host = simcall_host_get_name(request->issuer->smx_host);
   } else {
     xbt_die("Unexpected call_type %i", (int) call_type);
   }
 
     pattern->dst_proc = pattern->comm->comm.dst_proc->pid;
     pattern->dst_host = simcall_host_get_name(request->issuer->smx_host);
   } 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((xbt_dynar_t)xbt_dynar_get_as(list, request->issuer->pid, xbt_dynar_t), &pattern);
-
-  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);
+  xbt_dynar_push((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, request->issuer->pid, xbt_dynar_t), &pattern);

 
 

+  XBT_DEBUG("Insert incomplete comm pattern %p for process %lu", pattern, request->issuer->pid);

 }
 
 }
 

-void complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm)
-{
+void complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm, int backtracking) {
+

   mc_comm_pattern_t current_comm_pattern;
   unsigned int cursor = 0;
   mc_comm_pattern_t current_comm_pattern;
   unsigned int cursor = 0;

-  int index;

   unsigned int src = comm->comm.src_proc->pid;
   unsigned int dst = comm->comm.dst_proc->pid;
   unsigned int src = comm->comm.src_proc->pid;
   unsigned int dst = comm->comm.dst_proc->pid;

+  mc_comm_pattern_t src_comm_pattern;
+  mc_comm_pattern_t dst_comm_pattern;

   int src_completed = 0, dst_completed = 0;
 
   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){
+  /* Complete comm pattern */
+  xbt_dynar_foreach((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, src, xbt_dynar_t), cursor, current_comm_pattern) {
+    if (current_comm_pattern-> comm == comm) {

       update_comm_pattern(current_comm_pattern, 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;
       src_completed = 1;

+      xbt_dynar_remove_at((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, src, xbt_dynar_t), cursor, &src_comm_pattern);
+      XBT_DEBUG("Remove incomplete comm pattern for process %u at cursor %u", src, cursor);

       break;
     }
   }
       break;
     }
   }

-

   if(!src_completed)
     xbt_die("Corresponding communication for the source process not found!");
 
   cursor = 0;
 
   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){
+  xbt_dynar_foreach((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, dst, xbt_dynar_t), cursor, current_comm_pattern) {
+    if (current_comm_pattern-> comm == comm) {

       update_comm_pattern(current_comm_pattern, 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;
       dst_completed = 1;

+      xbt_dynar_remove_at((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, dst, xbt_dynar_t), cursor, &dst_comm_pattern);
+      XBT_DEBUG("Remove incomplete comm pattern for process %u at cursor %u", dst, cursor);

       break;
     }
   }
       break;
     }
   }

-

   if(!dst_completed)
   if(!dst_completed)

-    xbt_die("Corresponding communication for the dest process not found!");
-
-
+    xbt_die("Corresponding communication for the destination process not found!");
+  
+  if (!initial_global_state->initial_communications_pattern_done) {
+    /* Store comm pattern */
+    if(src_comm_pattern->index < xbt_dynar_length(((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, src, mc_list_comm_pattern_t))->list)){
+      xbt_dynar_set(((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, src, mc_list_comm_pattern_t))->list, src_comm_pattern->index, &src_comm_pattern);
+      ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, src, mc_list_comm_pattern_t))->list->used++;
+    } else {
+      xbt_dynar_insert_at(((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, src, mc_list_comm_pattern_t))->list, src_comm_pattern->index, &src_comm_pattern);
+    }
+    
+    if(dst_comm_pattern->index < xbt_dynar_length(((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, dst, mc_list_comm_pattern_t))->list)) {
+      xbt_dynar_set(((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, dst, mc_list_comm_pattern_t))->list, dst_comm_pattern->index, &dst_comm_pattern);
+      ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, dst, mc_list_comm_pattern_t))->list->used++;
+    } else {
+      xbt_dynar_insert_at(((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, dst, mc_list_comm_pattern_t))->list, dst_comm_pattern->index, &dst_comm_pattern);
+    }
+    ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, src, mc_list_comm_pattern_t))->index_comm++;
+    ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, dst, mc_list_comm_pattern_t))->index_comm++;
+  } else {
+    /* Evaluate comm determinism */
+    deterministic_comm_pattern(src, src_comm_pattern, backtracking);
+    deterministic_comm_pattern(dst, dst_comm_pattern, backtracking);
+  }

 }
 
 /************************ Main algorithm ************************/
 }
 
 /************************ Main algorithm ************************/


@@ -271,28 +335,22 @@ void MC_pre_modelcheck_comm_determinism(void)
   if (_sg_mc_visited > 0)
     visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
  
   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);
+  initial_communications_pattern = xbt_dynar_new(sizeof(mc_list_comm_pattern_t), list_comm_pattern_free_voidp);

   for (i=0; i<simix_process_maxpid; i++){
   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);
+    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<simix_process_maxpid; i++){
   }
   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_t process_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), NULL);

     xbt_dynar_insert_at(incomplete_communications_pattern, i, &process_pattern);
   }
 
     xbt_dynar_insert_at(incomplete_communications_pattern, i, &process_pattern);
   }
 

-  nb_comm_pattern = 0;
-

   initial_state = MC_state_new();
   initial_state = MC_state_new();

-

   MC_SET_STD_HEAP;
   MC_SET_STD_HEAP;

-
+  

   XBT_DEBUG("********* Start communication determinism verification *********");
 
   /* Wait for requests (schedules processes) */
   XBT_DEBUG("********* Start communication determinism verification *********");
 
   /* Wait for requests (schedules processes) */


@@ -322,14 +380,11 @@ void MC_modelcheck_comm_determinism(void)
   smx_simcall_t req = NULL;
   smx_process_t process = NULL;
   mc_state_t state = NULL, next_state = NULL;
   smx_simcall_t req = NULL;
   smx_process_t process = NULL;
   mc_state_t state = NULL, next_state = NULL;

-  xbt_dynar_t current_pattern;

 
   while (xbt_fifo_size(mc_stack) > 0) {
 
     /* Get current state */
 
   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)",
 
     XBT_DEBUG("**************************************************");
     XBT_DEBUG("Exploration depth = %d (state = %d, interleaved processes = %d)",


@@ -343,8 +398,10 @@ void MC_modelcheck_comm_determinism(void)
         && (req = MC_state_get_request(state, &value))
         && (visited_state == NULL)) {
 
         && (req = MC_state_get_request(state, &value))
         && (visited_state == NULL)) {
 

-      MC_LOG_REQUEST(mc_comm_determinism, req, value);
-
+      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);
       if (dot_output != NULL) {
         MC_SET_MC_HEAP;
         req_str = MC_request_get_dot_output(req, value);


@@ -355,7 +412,7 @@ void MC_modelcheck_comm_determinism(void)
       mc_stats->executed_transitions++;
 
       /* TODO : handle test and testany simcalls */
       mc_stats->executed_transitions++;
 
       /* TODO : handle test and testany simcalls */

-      mc_call_type call = MC_CALL_TYPE_NONE;
+      e_mc_call_type_t call = MC_CALL_TYPE_NONE;

       if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
         call = mc_get_call_type(req);
       }
       if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
         call = mc_get_call_type(req);
       }


@@ -364,8 +421,10 @@ void MC_modelcheck_comm_determinism(void)
       SIMIX_simcall_handle(req, value);    /* After this call req is no longer useful */
 
       MC_SET_MC_HEAP;
       SIMIX_simcall_handle(req, value);    /* After this call req is no longer useful */
 
       MC_SET_MC_HEAP;

-      current_pattern = !initial_global_state->initial_communications_pattern_done ? initial_communications_pattern : communications_pattern; 
-      mc_update_comm_pattern(call, req, value, current_pattern);
+      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;
 
       /* Wait for requests (schedules processes) */
       MC_SET_STD_HEAP;
 
       /* Wait for requests (schedules processes) */


@@ -376,7 +435,7 @@ void MC_modelcheck_comm_determinism(void)
 
       next_state = MC_state_new();
 
 
       next_state = MC_state_new();
 

-      if ((visited_state = is_visited_state()) == NULL) {
+      if ((visited_state = is_visited_state(next_state)) == NULL) {

 
         /* Get enabled processes and insert them 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 */
         xbt_swag_foreach(process, simix_global->process_list) {


@@ -386,14 +445,12 @@ void MC_modelcheck_comm_determinism(void)
         }
 
         if (dot_output != NULL)
         }
 
         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)
 
       } else {
 
         if (dot_output != NULL)

-          fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,
-                  visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, 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);

 
       }
 
 
       }
 


@@ -416,49 +473,13 @@ void MC_modelcheck_comm_determinism(void)
 
       MC_SET_MC_HEAP;
 
 
       MC_SET_MC_HEAP;
 

-      if (initial_global_state->initial_communications_pattern_done) {
-        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 (per process): **");
-            print_communications_pattern(initial_communications_pattern);
-            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 (_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: **");
-            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->initial_communications_pattern_done) 

         initial_global_state->initial_communications_pattern_done = 1;
         initial_global_state->initial_communications_pattern_done = 1;

-      }

 
       /* Trash the current state, no longer needed */
       xbt_fifo_shift(mc_stack);
 
       /* 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;
 
 
       MC_SET_STD_HEAP;
 


@@ -473,23 +494,20 @@ void MC_modelcheck_comm_determinism(void)
       MC_SET_MC_HEAP;
 
       while ((state = xbt_fifo_shift(mc_stack)) != NULL) {
       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 */
           /* 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;
 
           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 {
           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);

         }
       }
 
         }
       }
 

diff --git a/src/mc/mc_comm_pattern.h b/src/mc/mc_comm_pattern.h
index cb45a66..667f24e 100644 (file)
--- a/src/mc/mc_comm_pattern.h
+++ b/src/mc/mc_comm_pattern.h
@@ -27,22 +27,36 @@ typedef struct s_mc_comm_pattern{
   char *rdv;
   ssize_t data_size;
   void *data;
   char *rdv;
   ssize_t data_size;
   void *data;

+  int index;

 } s_mc_comm_pattern_t, *mc_comm_pattern_t;
 
 } s_mc_comm_pattern_t, *mc_comm_pattern_t;
 

+typedef struct s_mc_list_comm_pattern{
+  unsigned int index_comm;
+  xbt_dynar_t list;
+}s_mc_list_comm_pattern_t, *mc_list_comm_pattern_t;
+

 extern xbt_dynar_t initial_communications_pattern;
 extern xbt_dynar_t initial_communications_pattern;

-extern xbt_dynar_t communications_pattern;

 extern xbt_dynar_t incomplete_communications_pattern;
 
 extern xbt_dynar_t incomplete_communications_pattern;
 

-// Can we use the SIMIX syscall for this?
-typedef enum mc_call_type {
+typedef enum {

   MC_CALL_TYPE_NONE,
   MC_CALL_TYPE_SEND,
   MC_CALL_TYPE_RECV,
   MC_CALL_TYPE_WAIT,
   MC_CALL_TYPE_WAITANY,
   MC_CALL_TYPE_NONE,
   MC_CALL_TYPE_SEND,
   MC_CALL_TYPE_RECV,
   MC_CALL_TYPE_WAIT,
   MC_CALL_TYPE_WAITANY,

-} mc_call_type;
+} e_mc_call_type_t;
+
+typedef enum {
+  NONE_DIFF,
+  TYPE_DIFF,
+  RDV_DIFF,
+  SRC_PROC_DIFF,
+  DST_PROC_DIFF,
+  DATA_SIZE_DIFF,
+  DATA_DIFF,
+} e_mc_comm_pattern_difference_t;

 
 

-static inline mc_call_type mc_get_call_type(smx_simcall_t req)
+static inline e_mc_call_type_t mc_get_call_type(smx_simcall_t req)

 {
   switch(req->call) {
   case SIMCALL_COMM_ISEND:
 {
   switch(req->call) {
   case SIMCALL_COMM_ISEND:


@@ -58,9 +72,11 @@ static inline mc_call_type mc_get_call_type(smx_simcall_t req)
   }
 }
 
   }
 }
 

-void get_comm_pattern(xbt_dynar_t communications_pattern, smx_simcall_t request, mc_call_type call_type);
-void mc_update_comm_pattern(mc_call_type call_type, smx_simcall_t request, int value, xbt_dynar_t current_pattern);
-void complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm);
+void get_comm_pattern(xbt_dynar_t communications_pattern, smx_simcall_t request, e_mc_call_type_t call_type);
+void handle_comm_pattern(e_mc_call_type_t call_type, smx_simcall_t request, int value, xbt_dynar_t current_pattern, int backtracking);
+void comm_pattern_free_voidp(void *p);
+void list_comm_pattern_free_voidp(void *p);
+void complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm, int backtracking);

 void MC_pre_modelcheck_comm_determinism(void);
 void MC_modelcheck_comm_determinism(void);
 
 void MC_pre_modelcheck_comm_determinism(void);
 void MC_modelcheck_comm_determinism(void);
 

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 19f84ef..3776138 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -194,9 +194,9 @@ void MC_init()
 
     /* Main MC state: */
     MC_ignore_global_variable("mc_model_checker");
 
     /* Main MC state: */
     MC_ignore_global_variable("mc_model_checker");

-    MC_ignore_global_variable("communications_pattern");

     MC_ignore_global_variable("initial_communications_pattern");
     MC_ignore_global_variable("incomplete_communications_pattern");
     MC_ignore_global_variable("initial_communications_pattern");
     MC_ignore_global_variable("incomplete_communications_pattern");

+    MC_ignore_global_variable("nb_comm_pattern");

 
     /* MC __thread variables: */
     MC_ignore_global_variable("mc_diff_info");
 
     /* MC __thread variables: */
     MC_ignore_global_variable("mc_diff_info");


@@ -370,7 +370,8 @@ int MC_deadlock_check()
   return deadlock;
 }
 
   return deadlock;
 }
 

-void mc_update_comm_pattern(mc_call_type call_type, smx_simcall_t req, int value, xbt_dynar_t pattern) {
+void handle_comm_pattern(e_mc_call_type_t call_type, smx_simcall_t req, int value, xbt_dynar_t pattern, int backtracking) {
+

   switch(call_type) {
   case MC_CALL_TYPE_NONE:
     break;
   switch(call_type) {
   case MC_CALL_TYPE_NONE:
     break;


@@ -379,6 +380,7 @@ void mc_update_comm_pattern(mc_call_type call_type, smx_simcall_t req, int value
     get_comm_pattern(pattern, req, call_type);
     break;
   case MC_CALL_TYPE_WAIT:
     get_comm_pattern(pattern, req, call_type);
     break;
   case MC_CALL_TYPE_WAIT:

+  case MC_CALL_TYPE_WAITANY:

     {
       smx_synchro_t current_comm = NULL;
       if (call_type == MC_CALL_TYPE_WAIT)
     {
       smx_synchro_t current_comm = NULL;
       if (call_type == MC_CALL_TYPE_WAIT)


@@ -387,12 +389,51 @@ void mc_update_comm_pattern(mc_call_type call_type, smx_simcall_t req, int value
         current_comm = xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value, smx_synchro_t);
       // First wait only must be considered:
       if (current_comm->comm.refcount == 1)
         current_comm = xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value, smx_synchro_t);
       // First wait only must be considered:
       if (current_comm->comm.refcount == 1)

-        complete_comm_pattern(pattern, current_comm);
+        complete_comm_pattern(pattern, current_comm, backtracking);

       break;
     }
   default:
     xbt_die("Unexpected call type %i", (int)call_type);
   }
       break;
     }
   default:
     xbt_die("Unexpected call type %i", (int)call_type);
   }

+  
+}
+
+static void MC_restore_communications_pattern(mc_state_t state) {
+  mc_list_comm_pattern_t list_process_comm;
+  unsigned int cursor, cursor2;
+  xbt_dynar_foreach(initial_communications_pattern, cursor, list_process_comm){
+    list_process_comm->index_comm = (int)xbt_dynar_get_as(state->index_comm, cursor, int);
+  }
+  mc_comm_pattern_t comm;
+  cursor = 0;
+  xbt_dynar_t initial_incomplete_process_comms, incomplete_process_comms;
+  for(int i=0; i<simix_process_maxpid; i++){
+    initial_incomplete_process_comms = xbt_dynar_get_as(incomplete_communications_pattern, i, xbt_dynar_t);
+    xbt_dynar_reset(initial_incomplete_process_comms);
+    incomplete_process_comms = xbt_dynar_get_as(state->incomplete_comm_pattern, i, xbt_dynar_t);
+    xbt_dynar_foreach(incomplete_process_comms, cursor2, comm) {
+      mc_comm_pattern_t copy_comm = xbt_new0(s_mc_comm_pattern_t, 1);
+      copy_comm->index = comm->index;
+      copy_comm->type = comm->type;
+      copy_comm->comm = comm->comm;
+      copy_comm->rdv = strdup(comm->rdv);
+      copy_comm->data_size = -1;
+      copy_comm->data = NULL;
+      if(comm->type == SIMIX_COMM_SEND){
+        copy_comm->src_proc = comm->src_proc;
+        copy_comm->src_host = comm->src_host;
+        if(comm->data != NULL){
+          copy_comm->data_size = comm->data_size;
+          copy_comm->data = xbt_malloc0(comm->data_size);
+          memcpy(copy_comm->data, comm->data, comm->data_size);
+        }
+      }else{
+        copy_comm->dst_proc = comm->dst_proc;
+        copy_comm->dst_host = comm->dst_host;
+      }
+      xbt_dynar_push(initial_incomplete_process_comms, &copy_comm);
+    }
+  }

 }
 
 /**
 }
 
 /**


@@ -749,11 +790,9 @@ void MC_print_statistics(mc_stats_t stats)
   }
   if (initial_global_state != NULL) {
     if (_sg_mc_comms_determinism)
   }
   if (initial_global_state != NULL) {
     if (_sg_mc_comms_determinism)

-      XBT_INFO("Communication-deterministic : %s",
-               !initial_global_state->comm_deterministic ? "No" : "Yes");
+      XBT_INFO("Communication-deterministic : %s", !initial_global_state->comm_deterministic ? "No" : "Yes");

     if (_sg_mc_send_determinism)
     if (_sg_mc_send_determinism)

-      XBT_INFO("Send-deterministic : %s",
-               !initial_global_state->send_deterministic ? "No" : "Yes");
+      XBT_INFO("Send-deterministic : %s", !initial_global_state->send_deterministic ? "No" : "Yes");

   }
   mmalloc_set_current_heap(previous_heap);
 }
   }
   mmalloc_set_current_heap(previous_heap);
 }

diff --git a/src/mc/mc_state.c b/src/mc/mc_state.c
index e9b4b04..1f3abce 100644 (file)
--- a/src/mc/mc_state.c
+++ b/src/mc/mc_state.c
@@ -9,6 +9,52 @@
 #include "mc_state.h"
 #include "mc_request.h"
 #include "mc_private.h"
 #include "mc_state.h"
 #include "mc_request.h"
 #include "mc_private.h"

+#include "mc_comm_pattern.h"
+
+static void copy_incomplete_communications_pattern(mc_state_t state) {
+  int i;
+  xbt_dynar_t incomplete_process_comms;
+  mc_comm_pattern_t comm;
+  unsigned int cursor;
+  state->incomplete_comm_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp);
+  for (i=0; i<simix_process_maxpid; i++) {
+    incomplete_process_comms = xbt_dynar_get_as(incomplete_communications_pattern, i, xbt_dynar_t);
+    xbt_dynar_t incomplete_process_comms_copy = xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp);
+    xbt_dynar_foreach(incomplete_process_comms, cursor, comm) {
+      mc_comm_pattern_t copy_comm = xbt_new0(s_mc_comm_pattern_t, 1);
+      copy_comm->index = comm->index;
+      copy_comm->type = comm->type;
+      copy_comm->comm = comm->comm;
+      copy_comm->rdv = strdup(comm->rdv);
+      copy_comm->data_size = -1;
+      copy_comm->data = NULL;
+      if(comm->type == SIMIX_COMM_SEND){
+        copy_comm->src_proc = comm->src_proc;
+        copy_comm->src_host = comm->src_host;
+        if (comm->data != NULL) {
+          copy_comm->data_size = comm->data_size;
+          copy_comm->data = xbt_malloc0(comm->data_size);
+          memcpy(copy_comm->data, comm->data, comm->data_size);
+        }
+      }else{
+        copy_comm->dst_proc = comm->dst_proc;
+        copy_comm->dst_host = comm->dst_host;
+      }
+      xbt_dynar_push(incomplete_process_comms_copy, &copy_comm);
+    }
+    xbt_dynar_insert_at(state->incomplete_comm_pattern, i, &incomplete_process_comms_copy);
+  }
+}
+
+static void copy_index_communications_pattern(mc_state_t state) {
+
+  state->index_comm = xbt_dynar_new(sizeof(unsigned int), NULL);
+  mc_list_comm_pattern_t list_process_comm;
+  unsigned int cursor;
+  xbt_dynar_foreach(initial_communications_pattern, cursor, list_process_comm){
+    xbt_dynar_push_as(state->index_comm, unsigned int, list_process_comm->index_comm);
+  }
+}

 
 /**
  * \brief Creates a state data structure used by the exploration algorithm
 
 /**
  * \brief Creates a state data structure used by the exploration algorithm

diff --git a/src/mc/mc_visited.c b/src/mc/mc_visited.c
index 8ac5d0f..0c3c971 100644 (file)
--- a/src/mc/mc_visited.c
+++ b/src/mc/mc_visited.c
@@ -208,20 +208,25 @@ int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max)
  * \brief Checks whether a given state has already been visited by the algorithm.
  */
 
  * \brief Checks whether a given state has already been visited by the algorithm.
  */
 

-mc_visited_state_t is_visited_state()
+mc_visited_state_t is_visited_state(mc_state_t graph_state)

 {
 
   if (_sg_mc_visited == 0)
     return NULL;
 
 {
 
   if (_sg_mc_visited == 0)
     return NULL;
 

+  int partial_comm = 0;
+

   /* If comm determinism verification, we cannot stop the exploration if some 
      communications are not finished (at least, data are transfered). These communications 
   /* If comm determinism verification, we cannot stop the exploration if some 
      communications are not finished (at least, data are transfered). These communications 

-     are incomplete and they cannot be analyzed and compared with the initial pattern */
+     are incomplete and they cannot be analyzed and compared with the initial pattern. */

   if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
     int current_process = 1;
     while (current_process < simix_process_maxpid) {
   if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
     int current_process = 1;
     while (current_process < simix_process_maxpid) {

-      if (!xbt_dynar_is_empty((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t)))
-        return NULL;
+      if (!xbt_dynar_is_empty((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t))){
+        XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
+        partial_comm = 1;
+        break;
+      }

       current_process++;
     }
   }
       current_process++;
     }
   }