model-checker : use the right heap

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

diff --git a/src/mc/mc_comm_determinism.c b/src/mc/mc_comm_determinism.c
index d5b086c..37a6f90 100644 (file)
--- a/src/mc/mc_comm_determinism.c
+++ b/src/mc/mc_comm_determinism.c
@@ -217,7 +217,53 @@ 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();
+
+  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;
@@ -347,7 +393,7 @@ 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");
+        XBT_DEBUG("State already visited, exploration stopped on this path.");
       } else {
         XBT_DEBUG("There are no more processes to interleave. (depth %d)",
                   xbt_fifo_size(mc_stack) + 1);
@@ -369,6 +415,7 @@ static void MC_modelcheck_comm_determinism(void)
             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) {
@@ -383,6 +430,7 @@ static void MC_modelcheck_comm_determinism(void)
             XBT_INFO("Communications pattern counter-example:");
             print_communications_pattern(communications_pattern);
             MC_print_statistics(mc_stats);
+            MC_SET_STD_HEAP;
             return;
           }
         } else {
@@ -408,6 +456,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 +488,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();
-
-}