Move the memory handling of RemoteProcessMemory singleton from ModelChecker to Checke...

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index 0a1a077..a1b1a81 100644 (file)
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -25,9 +25,4 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_ModelChecker, mc, "ModelChecker");
 
 namespace simgrid::mc {
 
-ModelChecker::ModelChecker(std::unique_ptr<RemoteProcessMemory> remote_memory)
-    : remote_process_memory_(std::move(remote_memory))
-{
-}
-
 } // namespace simgrid::mc

diff --git a/src/mc/ModelChecker.hpp b/src/mc/ModelChecker.hpp
index 41aa6cb..d881e64 100644 (file)
--- a/src/mc/ModelChecker.hpp
+++ b/src/mc/ModelChecker.hpp
@@ -18,14 +18,11 @@ namespace simgrid::mc {
 /** State of the model-checker (global variables for the model checker)
  */
 class ModelChecker {
-  std::unique_ptr<RemoteProcessMemory> remote_process_memory_;
 
 public:
   ModelChecker(ModelChecker const&) = delete;
   ModelChecker& operator=(ModelChecker const&) = delete;
-  explicit ModelChecker(std::unique_ptr<RemoteProcessMemory> remote_simulation);
-
-  RemoteProcessMemory& get_remote_process_memory() { return *remote_process_memory_; }
+  explicit ModelChecker()                      = default;
 };
 
 } // namespace simgrid::mc

diff --git a/src/mc/api/RemoteApp.cpp b/src/mc/api/RemoteApp.cpp
index dd249a2..c680ae4 100644 (file)
--- a/src/mc/api/RemoteApp.cpp
+++ b/src/mc/api/RemoteApp.cpp
@@ -126,16 +126,15 @@ RemoteApp::RemoteApp(const std::vector<char*>& args)
   xbt_assert(mc_model_checker == nullptr, "Did you manage to start the MC twice in this process?");
 
   auto memory      = std::make_unique<simgrid::mc::RemoteProcessMemory>(pid);
-  model_checker_   = std::make_unique<simgrid::mc::ModelChecker>(std::move(memory));
+  model_checker_   = std::make_unique<simgrid::mc::ModelChecker>();
   mc_model_checker = model_checker_.get();
-  checker_side_    = std::make_unique<simgrid::mc::CheckerSide>(sockets[1], model_checker_.get());
+  checker_side_    = std::make_unique<simgrid::mc::CheckerSide>(sockets[1], std::move(memory), model_checker_.get());
 
   start();
 
   /* Take the initial snapshot */
   wait_for_requests();
-  initial_snapshot_ =
-      std::make_shared<simgrid::mc::Snapshot>(0, page_store_, model_checker_->get_remote_process_memory());
+  initial_snapshot_ = std::make_shared<simgrid::mc::Snapshot>(0, page_store_, checker_side_->get_remote_memory());
 }
 
 RemoteApp::~RemoteApp()
@@ -175,7 +174,7 @@ void RemoteApp::start()
 }
 void RemoteApp::restore_initial_state() const
 {
-  this->initial_snapshot_->restore(model_checker_->get_remote_process_memory());
+  this->initial_snapshot_->restore(checker_side_->get_remote_memory());
 }
 
 unsigned long RemoteApp::get_maxpid() const

diff --git a/src/mc/api/RemoteApp.hpp b/src/mc/api/RemoteApp.hpp
index 77e07f6..948cb53 100644 (file)
--- a/src/mc/api/RemoteApp.hpp
+++ b/src/mc/api/RemoteApp.hpp
@@ -68,7 +68,7 @@ public:
   Transition* handle_simcall(aid_t aid, int times_considered, bool new_transition);
 
   /* Get the memory of the remote process */
-  RemoteProcessMemory& get_remote_process_memory() { return model_checker_->get_remote_process_memory(); }
+  RemoteProcessMemory& get_remote_process_memory() { return checker_side_->get_remote_memory(); }
 
   PageStore& get_page_store() { return page_store_; }
 };

diff --git a/src/mc/explo/LivenessChecker.cpp b/src/mc/explo/LivenessChecker.cpp
index 2ce38b8..7290930 100644 (file)
--- a/src/mc/explo/LivenessChecker.cpp
+++ b/src/mc/explo/LivenessChecker.cpp
@@ -23,7 +23,7 @@ VisitedPair::VisitedPair(int pair_num, xbt_automaton_state_t prop_state,
                          RemoteApp& remote_app)
     : num(pair_num), prop_state_(prop_state)
 {
-  auto& memory     = mc_model_checker->get_remote_process_memory();
+  auto& memory     = remote_app.get_remote_process_memory();
   this->app_state_ = std::move(app_state);
   if (not this->app_state_->get_system_state())
     this->app_state_->set_system_state(std::make_shared<Snapshot>(pair_num, remote_app.get_page_store(), memory));

diff --git a/src/mc/remote/CheckerSide.cpp b/src/mc/remote/CheckerSide.cpp
index cf0d9e0..5f04d15 100644 (file)
--- a/src/mc/remote/CheckerSide.cpp
+++ b/src/mc/remote/CheckerSide.cpp
@@ -13,7 +13,8 @@
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_checkerside, mc, "MC communication with the application");
 
 namespace simgrid::mc {
-CheckerSide::CheckerSide(int sockfd, ModelChecker* mc) : channel_(sockfd)
+CheckerSide::CheckerSide(int sockfd, std::unique_ptr<RemoteProcessMemory> memory, ModelChecker* mc)
+    : remote_memory_(std::move(memory)), channel_(sockfd)
 {
   auto* base = event_base_new();
   base_.reset(base);
@@ -31,7 +32,7 @@ CheckerSide::CheckerSide(int sockfd, ModelChecker* mc) : channel_(sockfd)
               throw simgrid::xbt::errno_error();
           }
 
-          if (not mc_model_checker->get_remote_process_memory().handle_message(buffer.data(), size))
+          if (not checker->get_remote_memory().handle_message(buffer.data(), size))
             checker->break_loop();
         } else {
           xbt_die("Unexpected event");
@@ -44,17 +45,17 @@ CheckerSide::CheckerSide(int sockfd, ModelChecker* mc) : channel_(sockfd)
   auto* signal_event = event_new(
       base, SIGCHLD, EV_SIGNAL | EV_PERSIST,
       [](evutil_socket_t sig, short events, void* arg) {
-        auto mc = static_cast<simgrid::mc::ModelChecker*>(arg);
+        auto checker = static_cast<simgrid::mc::CheckerSide*>(arg);
         if (events == EV_SIGNAL) {
           if (sig == SIGCHLD)
-            mc->get_remote_process_memory().handle_waitpid();
+            checker->get_remote_memory().handle_waitpid();
           else
             xbt_die("Unexpected signal: %d", sig);
         } else {
           xbt_die("Unexpected event");
         }
       },
-      mc);
+      this);
   event_add(signal_event, nullptr);
   signal_event_.reset(signal_event);
 }

diff --git a/src/mc/remote/CheckerSide.hpp b/src/mc/remote/CheckerSide.hpp
index 81b4f9a..2d0aa94 100644 (file)
--- a/src/mc/remote/CheckerSide.hpp
+++ b/src/mc/remote/CheckerSide.hpp
@@ -19,11 +19,11 @@ class CheckerSide {
   std::unique_ptr<event_base, decltype(&event_base_free)> base_{nullptr, &event_base_free};
   std::unique_ptr<event, decltype(&event_free)> socket_event_{nullptr, &event_free};
   std::unique_ptr<event, decltype(&event_free)> signal_event_{nullptr, &event_free};
-
+  std::unique_ptr<RemoteProcessMemory> remote_memory_;
   Channel channel_;
 
 public:
-  explicit CheckerSide(int sockfd, ModelChecker* mc);
+  explicit CheckerSide(int sockfd, std::unique_ptr<RemoteProcessMemory> mem, ModelChecker* mc);
 
   // No copy:
   CheckerSide(CheckerSide const&) = delete;
@@ -32,6 +32,7 @@ public:
 
   Channel const& get_channel() const { return channel_; }
   Channel& get_channel() { return channel_; }
+  RemoteProcessMemory& get_remote_memory() { return *remote_memory_.get(); }
 
   void dispatch_events() const;
   void break_loop() const;

diff --git a/src/mc/sosp/Snapshot_test.cpp b/src/mc/sosp/Snapshot_test.cpp
index 974ad35..a5cefbc 100644 (file)
--- a/src/mc/sosp/Snapshot_test.cpp
+++ b/src/mc/sosp/Snapshot_test.cpp
@@ -16,6 +16,7 @@
 using simgrid::mc::Region;
 class snap_test_helper {
   static simgrid::mc::PageStore page_store_;
+  static std::unique_ptr<simgrid::mc::RemoteProcessMemory> memory_;
 
 public:
   static void init_memory(void* mem, size_t size);
@@ -34,15 +35,12 @@ public:
   static void compare_region_parts();
   static void read_pointer();
 
-  static void cleanup()
-  {
-    delete mc_model_checker;
-    mc_model_checker = nullptr;
-  }
+  static void cleanup() { memory_ = nullptr; }
 };
 
 // static member variables init.
 simgrid::mc::PageStore snap_test_helper::page_store_(500);
+std::unique_ptr<simgrid::mc::RemoteProcessMemory> snap_test_helper::memory_ = nullptr;
 
 void snap_test_helper::init_memory(void* mem, size_t size)
 {
@@ -57,9 +55,8 @@ void snap_test_helper::Init()
   REQUIRE(xbt_pagesize == getpagesize());
   REQUIRE(1 << xbt_pagebits == xbt_pagesize);
 
-  auto memory = std::make_unique<simgrid::mc::RemoteProcessMemory>(getpid());
-  memory->init(nullptr);
-  mc_model_checker = new ::simgrid::mc::ModelChecker(std::move(memory));
+  memory_ = std::make_unique<simgrid::mc::RemoteProcessMemory>(getpid());
+  memory_->init(nullptr);
 }
 
 snap_test_helper::prologue_return snap_test_helper::prologue(int n)
@@ -72,13 +69,12 @@ snap_test_helper::prologue_return snap_test_helper::prologue(int n)
 
   // Init memory and take snapshots:
   init_memory(source, byte_size);
-  auto* region0 = new simgrid::mc::Region(page_store_, mc_model_checker->get_remote_process_memory(),
-                                          simgrid::mc::RegionType::Data, source, byte_size);
+  auto* region0 =
+      new simgrid::mc::Region(page_store_, *memory_.get(), simgrid::mc::RegionType::Data, source, byte_size);
   for (int i = 0; i < n; i += 2) {
     init_memory((char*)source + i * xbt_pagesize, xbt_pagesize);
   }
-  auto* region = new simgrid::mc::Region(page_store_, mc_model_checker->get_remote_process_memory(),
-                                         simgrid::mc::RegionType::Data, source, byte_size);
+  auto* region = new simgrid::mc::Region(page_store_, *memory_.get(), simgrid::mc::RegionType::Data, source, byte_size);
 
   void* destination = mmap(nullptr, byte_size, PROT_READ | PROT_WRITE, MAP_PRIVATE | MAP_ANONYMOUS, -1, 0);
   INFO("Could not allocate destination memory");
@@ -160,8 +156,7 @@ void snap_test_helper::read_pointer()
 {
   prologue_return ret = prologue(1);
   memcpy(ret.src, &mc_model_checker, sizeof(void*));
-  const simgrid::mc::Region region2(page_store_, mc_model_checker->get_remote_process_memory(),
-                                    simgrid::mc::RegionType::Data, ret.src, ret.size);
+  const simgrid::mc::Region region2(page_store_, *memory_.get(), simgrid::mc::RegionType::Data, ret.src, ret.size);
   INFO("Mismtach in MC_region_read_pointer()");
   REQUIRE(MC_region_read_pointer(&region2, ret.src) == mc_model_checker);