X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/3bda7845c0cceaaeedd5d0371434927c8cf6231d..c4f1fe5c9bd8fa83fd0cdf873f27634930e02d95:/src/mc/mc_checkpoint.cpp

diff --git a/src/mc/mc_checkpoint.cpp b/src/mc/mc_checkpoint.cpp
index f458f72a84..9aa90a6977 100644
--- a/src/mc/mc_checkpoint.cpp
+++ b/src/mc/mc_checkpoint.cpp
@@ -11,7 +11,7 @@
 #include <dirent.h>
 
 #include "src/internal_config.h"
-#include "mc_private.h"
+#include "src/mc/mc_private.h"
 #include "xbt/module.h"
 #include <xbt/mmalloc.h>
 #include "src/smpi/private.h"
@@ -24,15 +24,15 @@
 #include <libunwind.h>
 #include <libelf.h>
 
-#include "mc_private.h"
+#include "src/mc/mc_private.h"
 #include <mc/mc.h>
 
-#include "mc_snapshot.h"
-#include "mc_object_info.h"
-#include "mc_mmu.h"
-#include "mc_unw.h"
-#include "mc_protocol.h"
-#include "mc_smx.h"
+#include "src/mc/mc_snapshot.h"
+#include "src/mc/mc_object_info.h"
+#include "src/mc/mc_mmu.h"
+#include "src/mc/mc_unw.h"
+#include "src/mc/mc_protocol.h"
+#include "src/mc/mc_smx.h"
 #include "mc_hash.hpp"
 
 #include "src/mc/ObjectInformation.hpp"
@@ -139,7 +139,8 @@ static void MC_snapshot_add_region(int index, mc_snapshot_t snapshot,
 
   simgrid::mc::RegionSnapshot region;
 #ifdef HAVE_SMPI
-  const bool privatization_aware = object_info && object_info->privatized();
+  const bool privatization_aware = object_info
+    && mc_model_checker->process().privatized(*object_info);
   if (privatization_aware && MC_smpi_process_count())
     region = simgrid::mc::privatized_region(
       type, start_addr, permanent_addr, size, ref_region);
@@ -179,7 +180,7 @@ static void MC_get_memory_regions(simgrid::mc::Process* process, mc_snapshot_t s
     process->get_malloc_info());
 
 #ifdef HAVE_SMPI
-  if (smpi_privatize_global_variables && MC_smpi_process_count()) {
+  if (mc_model_checker->process().privatized() && MC_smpi_process_count()) {
     // snapshot->privatization_index = smpi_loaded_page
     mc_model_checker->process().read_variable(
       "smpi_loaded_page", &snapshot->privatization_index,
@@ -416,32 +417,28 @@ static std::vector<s_mc_snapshot_stack_t> MC_take_snapshot_stacks(mc_snapshot_t
 {
   std::vector<s_mc_snapshot_stack_t> res;
 
-  unsigned int cursor = 0;
-  stack_region_t current_stack;
-
-  // FIXME, cross-process support (stack_areas)
-  xbt_dynar_foreach(stacks_areas, cursor, current_stack) {
+  for (auto const& stack : mc_model_checker->process().stack_areas()) {
     s_mc_snapshot_stack_t st;
 
     // Read the context from remote process:
     unw_context_t context;
     mc_model_checker->process().read_bytes(
-      &context, sizeof(context), remote(current_stack->context));
+      &context, sizeof(context), remote(stack.context));
 
     if (mc_unw_init_context(&st.context, &mc_model_checker->process(),
       &context) < 0) {
       xbt_die("Could not initialise the libunwind context.");
     }
     st.stack_frames = MC_unwind_stack_frames(&st.context);
-    st.local_variables = MC_get_local_variables_values(st.stack_frames, current_stack->process_index);
-    st.process_index = current_stack->process_index;
+    st.local_variables = MC_get_local_variables_values(st.stack_frames, stack.process_index);
+    st.process_index = stack.process_index;
 
     unw_word_t sp = st.stack_frames[0].sp;
 
     res.push_back(std::move(st));
 
     size_t stack_size =
-      (char*) current_stack->address + current_stack->size - (char*) sp;
+      (char*) stack.address + stack.size - (char*) sp;
     (*snapshot)->stack_sizes.push_back(stack_size);
   }
 
@@ -449,28 +446,6 @@ static std::vector<s_mc_snapshot_stack_t> MC_take_snapshot_stacks(mc_snapshot_t
 
 }
 
-static std::vector<s_mc_heap_ignore_region_t> MC_take_snapshot_ignore()
-{
-  std::vector<s_mc_heap_ignore_region_t> res;
-
-  if (mc_heap_comparison_ignore == NULL)
-    return std::move(res);
-
-  unsigned int cursor = 0;
-  mc_heap_ignore_region_t current_region;
-
-  xbt_dynar_foreach(mc_heap_comparison_ignore, cursor, current_region) {
-    s_mc_heap_ignore_region_t new_region;
-    new_region.address = current_region->address;
-    new_region.size = current_region->size;
-    new_region.block = current_region->block;
-    new_region.fragment = current_region->fragment;
-    res.push_back(std::move(new_region));
-  }
-
-  return std::move(res);
-}
-
 static void MC_snapshot_handle_ignore(mc_snapshot_t snapshot)
 {
   xbt_assert(snapshot->process());
@@ -607,7 +582,7 @@ mc_snapshot_t MC_take_snapshot(int num_state)
   if (use_soft_dirty)
     mc_process->reset_soft_dirty();
 
-  snapshot->to_ignore = MC_take_snapshot_ignore();
+  snapshot->to_ignore = mc_model_checker->process().ignored_heap();
 
   if (_sg_mc_visited > 0 || strcmp(_sg_mc_property_file, "")) {
     snapshot->stacks =
@@ -639,13 +614,11 @@ void MC_restore_snapshot_regions(mc_snapshot_t snapshot)
 #ifdef HAVE_SMPI
   // TODO, send a message to implement this in the MCed process
   if(snapshot->privatization_index >= 0) {
-    // We just rewrote the global variables.
-    // The privatisation segment SMPI thinks
-    // is mapped might be inconsistent with the segment which
-    // is really mapped in memory (kernel state).
-    // We ask politely SMPI to map the segment anyway,
-    // even if it thinks it is the current one:
-    smpi_really_switch_data_segment(snapshot->privatization_index);
+    // Fix the privatization mmap:
+    s_mc_restore_message message;
+    message.type = MC_MESSAGE_RESTORE;
+    message.index = snapshot->privatization_index;
+    mc_model_checker->process().send_message(message);
   }
 #endif
 }