Merge branch 'master' of git+ssh://scm.gforge.inria.fr//gitroot/simgrid/simgrid

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

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 524056e..cdbec20 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -30,7 +30,7 @@ e_mc_reduce_t mc_reduce_kind = e_mc_reduce_unset;
 int _sg_do_model_check = 0;
 int _sg_mc_checkpoint = 0;
 int _sg_mc_sparse_checkpoint = 0;
-int _sg_mc_soft_dirty = 1;
+int _sg_mc_soft_dirty = 0;
 char *_sg_mc_property_file = NULL;
 int _sg_mc_timeout = 0;
 int _sg_mc_hash = 0;
@@ -481,7 +481,7 @@ void MC_wait_for_requests(void)
     xbt_dynar_foreach(simix_global->process_that_ran, iter, process) {
       req = &process->simcall;
       if (req->call != SIMCALL_NONE && !MC_request_is_visible(req))
-        SIMIX_simcall_pre(req, 0);
+        SIMIX_simcall_enter(req, 0);
     }
   }
 }
@@ -576,7 +576,8 @@ void MC_replay(xbt_fifo_t stack, int start)
     if (mc_reduce_kind == e_mc_reduce_dpor) {
       MC_SET_MC_HEAP;
       char *key = bprintf("%lu", saved_req->issuer->pid);
-      xbt_dict_remove(first_enabled_state, key);
+      if(xbt_dict_get_or_null(first_enabled_state, key))
+         xbt_dict_remove(first_enabled_state, key);
       xbt_free(key);
       MC_SET_STD_HEAP;
     }
@@ -605,7 +606,7 @@ void MC_replay(xbt_fifo_t stack, int start)
           call = 4;
       }
 
-      SIMIX_simcall_pre(req, value);
+      SIMIX_simcall_enter(req, value);
 
       if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
         MC_SET_MC_HEAP;
@@ -669,12 +670,7 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
 
   initial_global_state->raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
 
-  int value;
-  char *req_str;
-  smx_simcall_t req = NULL, saved_req = NULL;
   xbt_fifo_item_t item;
-  mc_state_t state;
-  mc_pair_t pair;
   int depth = 1;
 
   XBT_DEBUG("**** Begin Replay ****");
@@ -687,14 +683,17 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
   if (!initial_global_state->raw_mem_set)
     MC_SET_STD_HEAP;
 
-  if (all_stack) {
-
-    item = xbt_fifo_get_last_item(stack);
+    /* Traverse the stack from the initial state and re-execute the transitions */
+    for (item = xbt_fifo_get_last_item(stack);
+         all_stack ? depth <= xbt_fifo_size(stack) : item != xbt_fifo_get_first_item(stack);
+         item = xbt_fifo_get_prev_item(item)) {
 
-    while (depth <= xbt_fifo_size(stack)) {
+      mc_pair_t pair = (mc_pair_t) xbt_fifo_get_item_content(item);
 
-      pair = (mc_pair_t) xbt_fifo_get_item_content(item);
-      state = (mc_state_t) pair->graph_state;
+      mc_state_t state = (mc_state_t) pair->graph_state;
+      smx_simcall_t req = NULL, saved_req = NULL;
+      int value;
+      char *req_str;
 
       if (pair->requests > 0) {
 
@@ -702,7 +701,7 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
         //XBT_DEBUG("SavedReq->call %u", saved_req->call);
 
         if (saved_req != NULL) {
-          /* because we got a copy of the executed request, we have to fetch the  
+          /* because we got a copy of the executed request, we have to fetch the
              real one, pointed by the request field of the issuer process */
           req = &saved_req->issuer->simcall;
           //XBT_DEBUG("Req->call %u", req->call);
@@ -716,60 +715,17 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
 
         }
 
-        SIMIX_simcall_pre(req, value);
+        SIMIX_simcall_enter(req, value);
         MC_wait_for_requests();
       }
 
-      depth++;
-
       /* Update statistics */
       mc_stats->visited_pairs++;
       mc_stats->executed_transitions++;
 
-      item = xbt_fifo_get_prev_item(item);
-    }
-
-  } else {
-
-    /* Traverse the stack from the initial state and re-execute the transitions */
-    for (item = xbt_fifo_get_last_item(stack);
-         item != xbt_fifo_get_first_item(stack);
-         item = xbt_fifo_get_prev_item(item)) {
-
-      pair = (mc_pair_t) xbt_fifo_get_item_content(item);
-      state = (mc_state_t) pair->graph_state;
-
-      if (pair->requests > 0) {
-
-        saved_req = MC_state_get_executed_request(state, &value);
-        //XBT_DEBUG("SavedReq->call %u", saved_req->call);
-
-        if (saved_req != NULL) {
-          /* because we got a copy of the executed request, we have to fetch the  
-             real one, pointed by the request field of the issuer process */
-          req = &saved_req->issuer->simcall;
-          //XBT_DEBUG("Req->call %u", req->call);
-
-          /* Debug information */
-          if (XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)) {
-            req_str = MC_request_to_string(req, value);
-            XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
-            xbt_free(req_str);
-          }
-
-        }
-
-        SIMIX_simcall_pre(req, value);
-        MC_wait_for_requests();
-      }
-
       depth++;
 
-      /* Update statistics */
-      mc_stats->visited_pairs++;
-      mc_stats->executed_transitions++;
     }
-  }
 
   XBT_DEBUG("**** End Replay ****");
 
@@ -899,6 +855,8 @@ void MC_dump_stack_liveness(xbt_fifo_t stack)
 
 void MC_print_statistics(mc_stats_t stats)
 {
+  xbt_mheap_t previous_heap = mmalloc_get_current_heap();
+
   if (stats->expanded_pairs == 0) {
     XBT_INFO("Expanded states = %lu", stats->expanded_states);
     XBT_INFO("Visited states = %lu", stats->visited_states);
@@ -920,7 +878,7 @@ void MC_print_statistics(mc_stats_t stats)
       XBT_INFO("Send-deterministic : %s",
                !initial_global_state->send_deterministic ? "No" : "Yes");
   }
-  MC_SET_STD_HEAP;
+  mmalloc_set_current_heap(previous_heap);
 }
 
 void MC_assert(int prop)