From: Marion Guthmuller <marion.guthmuller@inria.fr>
Date: Fri, 30 May 2014 21:51:41 +0000 (+0200)
Subject: model-checker : fix comm determinism detection mechanisms
X-Git-Tag: v3_12~956^2~18
X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/48af4c8427d171d3e05d39116b02e441f2391374?ds=sidebyside

model-checker : fix comm determinism detection mechanisms
---

diff --git a/src/mc/mc_comm_determinism.c b/src/mc/mc_comm_determinism.c
index d5b086ce2f..d034675fc5 100644
--- a/src/mc/mc_comm_determinism.c
+++ b/src/mc/mc_comm_determinism.c
@@ -217,7 +217,58 @@ void complete_comm_pattern(xbt_dynar_t list, smx_action_t comm)
 
 /************************ 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;
+
+  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;
+
+}
+
+void MC_modelcheck_comm_determinism(void)
 {
 
   char *req_str = NULL;
@@ -408,6 +459,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 +491,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();
-
-}
diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index c9e8c6ef8c..72ab53686c 100644
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -316,16 +316,22 @@ static void MC_modelcheck_comm_determinism_init(void)
   /* Create exploration stack */
   mc_stack = xbt_fifo_new();
 
+  MC_SET_STD_HEAP;
+
+  MC_pre_modelcheck_comm_determinism();
+
+  MC_SET_MC_HEAP;
   initial_global_state = xbt_new0(s_mc_global_t, 1);
   initial_global_state->snapshot = MC_take_snapshot(0);
   initial_global_state->initial_communications_pattern_done = 0;
   initial_global_state->comm_deterministic = 1;
   initial_global_state->send_deterministic = 1;
+  MC_SET_STD_HEAP;
 
-  if (!mc_mem_set)
-    MC_SET_STD_HEAP;
+  MC_modelcheck_comm_determinism();
 
-  MC_pre_modelcheck_comm_determinism();
+  if(mc_mem_set)
+    MC_SET_MC_HEAP;
 
 }
 
diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index e7a2703122..3ff124f0c1 100644
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -586,6 +586,7 @@ extern xbt_dynar_t incomplete_communications_pattern;
 void get_comm_pattern(xbt_dynar_t communications_pattern, smx_simcall_t request, int call);
 void complete_comm_pattern(xbt_dynar_t list, smx_action_t comm);
 void MC_pre_modelcheck_comm_determinism(void);
+void MC_modelcheck_comm_determinism(void);
 
 /* *********** Sets *********** */