[mc] Fix privatisation support

It was broken (TODO) since the switch to split-process MC.

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index f0f65af..2c7dac5 100644 (file)
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -6,6 +6,8 @@
 
 #include <cassert>
 
+#include "simgrid/sg_config.h" // sg_cfg_get_boolean
+
 #include "ModelChecker.hpp"
 #include "PageStore.hpp"
 
@@ -20,6 +22,8 @@ ModelChecker::ModelChecker(pid_t pid, int socket) :
   process_(pid, socket),
   parent_snapshot_(nullptr)
 {
+  // TODO, avoid direct dependency on sg_cfg
+  process_.privatized(sg_cfg_get_boolean("smpi/privatize_global_variables"));
 }
 
 ModelChecker::~ModelChecker()

diff --git a/src/mc/ObjectInformation.hpp b/src/mc/ObjectInformation.hpp
index d589dac..7902e3d 100644 (file)
--- a/src/mc/ObjectInformation.hpp
+++ b/src/mc/ObjectInformation.hpp
@@ -88,15 +88,6 @@ public:
     return this->flags & simgrid::mc::ObjectInformation::Executable;
   }
 
-  bool privatized() const
-  {
-#ifdef HAVE_SMPI
-    return this->executable() && smpi_privatize_global_variables;
-#else
-    return false;
-#endif
-  }
-
   void* base_address() const;
 
   simgrid::mc::Frame* find_function(const void *ip) const;

diff --git a/src/mc/Process.cpp b/src/mc/Process.cpp
index 78f4b45..46ef37c 100644 (file)
--- a/src/mc/Process.cpp
+++ b/src/mc/Process.cpp
@@ -220,6 +220,7 @@ Process::Process(pid_t pid, int sockfd) : AddressSpace(this)
   process->init_memory_map_info();
   process->clear_refs_fd_ = -1;
   process->pagemap_fd_ = -1;
+  process->privatized_ = false;
 
   int fd = open_vm(process->pid_, O_RDWR);
   if (fd<0)
@@ -522,7 +523,7 @@ const void *Process::read_bytes(void* buffer, std::size_t size,
       this->find_object_info_rw((void*)address.address());
     // Segment overlap is not handled.
 #ifdef HAVE_SMPI
-    if (info.get() && info.get()->privatized()) {
+    if (info.get() && this->privatized(*info)) {
       if (process_index < 0)
         xbt_die("Missing process index");
       if (process_index >= (int) MC_smpi_process_count())

diff --git a/src/mc/Process.hpp b/src/mc/Process.hpp
index af42a12..526bb42 100644 (file)
--- a/src/mc/Process.hpp
+++ b/src/mc/Process.hpp
@@ -35,6 +35,8 @@
 #include "AddressSpace.hpp"
 #include "mc_protocol.h"
 
+#include "ObjectInformation.hpp"
+
 // Those flags are used to track down which cached information
 // is still up to date and which information needs to be updated.
 typedef int mc_process_cache_flags_t;
@@ -154,6 +156,16 @@ public:
   void reset_soft_dirty();
   void read_pagemap(uint64_t* pagemap, size_t start_page, size_t page_count);
 
+  bool privatized(ObjectInformation const& info) const
+  {
+    return privatized_ && info.executable();
+  }
+  bool privatized() const
+  {
+    return privatized_;
+  }
+  void privatized(bool privatized) { privatized_ = privatized; }
+
 private:
   void init_memory_map_info();
   void refresh_heap();
@@ -169,6 +181,7 @@ private:
   std::vector<IgnoredRegion> ignored_regions_;
   int clear_refs_fd_;
   int pagemap_fd_;
+  bool privatized_;
 public: // object info
   // TODO, make private (first, objectify simgrid::mc::ObjectInformation*)
   std::vector<std::shared_ptr<simgrid::mc::ObjectInformation>> object_infos;

diff --git a/src/mc/mc_checkpoint.cpp b/src/mc/mc_checkpoint.cpp
index 763e116..d583acd 100644 (file)
--- a/src/mc/mc_checkpoint.cpp
+++ b/src/mc/mc_checkpoint.cpp
@@ -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,
@@ -641,13 +642,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
 }

diff --git a/src/mc/mc_client.cpp b/src/mc/mc_client.cpp
index 5ed0cf3..1ddca91 100644 (file)
--- a/src/mc/mc_client.cpp
+++ b/src/mc/mc_client.cpp
@@ -118,6 +118,16 @@ void MC_client_handle_messages(void)
       }
       break;
 
+    case MC_MESSAGE_RESTORE:
+      {
+        s_mc_restore_message_t message;
+        if (s != sizeof(message))
+          xbt_die("Unexpected size for SIMCALL_HANDLE");
+        memcpy(&message, message_buffer, sizeof(message));
+        smpi_really_switch_data_segment(message.index);
+      }
+      break;
+
     default:
       xbt_die("%s received unexpected message %s (%i)",
         MC_mode_name(mc_mode),

diff --git a/src/mc/mc_protocol.cpp b/src/mc/mc_protocol.cpp
index 09b3227..d5fc228 100644 (file)
--- a/src/mc/mc_protocol.cpp
+++ b/src/mc/mc_protocol.cpp
@@ -6,6 +6,7 @@
 
 #include <errno.h>
 #include <string.h>
+#include <stdio.h> // perror
 
 #include <sys/types.h>
 #include <sys/socket.h>

diff --git a/src/mc/mc_protocol.h b/src/mc/mc_protocol.h
index 1c39fa7..744b333 100644 (file)
--- a/src/mc/mc_protocol.h
+++ b/src/mc/mc_protocol.h
@@ -49,6 +49,8 @@ typedef enum {
   MC_MESSAGE_WAITING,
   MC_MESSAGE_SIMCALL_HANDLE,
   MC_MESSAGE_ASSERTION_FAILED,
+  // MCer request to finish the restoration:
+  MC_MESSAGE_RESTORE,
 } e_mc_message_type;
 
 #define MC_MESSAGE_LENGTH 512
@@ -103,6 +105,11 @@ typedef struct s_mc_register_symbol_message {
   void* data;
 } s_mc_register_symbol_message_t, * mc_register_symbol_message_t;
 
+typedef struct s_mc_restore_message {
+  e_mc_message_type type;
+  int index;
+} s_mc_restore_message_t, *mc_restore_message_t;
+
 XBT_PRIVATE int MC_protocol_send(int socket, const void* message, size_t size);
 XBT_PRIVATE int MC_protocol_send_simple_message(int socket, e_mc_message_type type);
 XBT_PRIVATE int MC_protocol_hello(int socket);