model-checker : communications determinism with visited state equality reduction

[simgrid.git] / src / mc / mc_global.c

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 6c3b742..3776138 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -13,9 +13,6 @@
 #include <sys/time.h>
 #include <sys/mman.h>
 #include <libgen.h>
-
-#define UNW_LOCAL_ONLY
-#include <libunwind.h>
 #endif
 
 #include "simgrid/sg_config.h"
@@ -26,6 +23,9 @@
 #include "xbt/dict.h"
 
 #ifdef HAVE_MC
+#define UNW_LOCAL_ONLY
+#include <libunwind.h>
+
 #include "../xbt/mmalloc/mmprivate.h"
 #include "mc_object_info.h"
 #include "mc_comm_pattern.h"
@@ -194,9 +194,9 @@ void MC_init()
 
     /* 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("nb_comm_pattern");
 
     /* MC __thread variables: */
     MC_ignore_global_variable("mc_diff_info");
@@ -370,7 +370,8 @@ int MC_deadlock_check()
   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;
@@ -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:
+  case MC_CALL_TYPE_WAITANY:
     {
       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)
-        complete_comm_pattern(pattern, current_comm);
+        complete_comm_pattern(pattern, current_comm, backtracking);
       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)
-      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)
-      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);
 }