Move the PageStore from ModelChecker to RemoteApp

diff --git a/src/mc/ModelChecker.hpp b/src/mc/ModelChecker.hpp
index d32bd26..ccbee43 100644 (file)
--- a/src/mc/ModelChecker.hpp
+++ b/src/mc/ModelChecker.hpp
@@ -19,8 +19,6 @@ namespace simgrid::mc {
  */
 class ModelChecker {
   CheckerSide checker_side_;
-  // This is the parent snapshot of the current state:
-  PageStore page_store_{500};
   std::unique_ptr<RemoteProcess> remote_process_;
   Exploration* exploration_ = nullptr;
 
@@ -31,7 +29,6 @@ public:
 
   RemoteProcess& get_remote_process() { return *remote_process_; }
   Channel& channel() { return checker_side_.get_channel(); }
-  PageStore& page_store() { return page_store_; }
 
   void start();
   void shutdown();

diff --git a/src/mc/VisitedState.cpp b/src/mc/VisitedState.cpp
index e067dfb..ac9e191 100644 (file)
--- a/src/mc/VisitedState.cpp
+++ b/src/mc/VisitedState.cpp
@@ -18,10 +18,12 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_VisitedState, mc, "Logging specific to state
 namespace simgrid::mc {
 
 /** @brief Save the current state */
-VisitedState::VisitedState(unsigned long state_number, unsigned int actor_count, std::size_t heap_bytes_used)
-    : heap_bytes_used_(heap_bytes_used), actor_count_(actor_count), num_(state_number)
+VisitedState::VisitedState(unsigned long state_number, unsigned int actor_count, RemoteApp& remote_app)
+    : heap_bytes_used_(remote_app.get_remote_process().get_remote_heap_bytes())
+    , actor_count_(actor_count)
+    , num_(state_number)
 {
-  this->system_state_    = std::make_shared<simgrid::mc::Snapshot>(state_number);
+  this->system_state_ = std::make_shared<simgrid::mc::Snapshot>(state_number, remote_app.get_page_store());
 }
 
 void VisitedStates::prune()
@@ -40,10 +42,10 @@ void VisitedStates::prune()
 
 /** @brief Checks whether a given state has already been visited by the algorithm. */
 std::unique_ptr<simgrid::mc::VisitedState>
-VisitedStates::addVisitedState(unsigned long state_number, simgrid::mc::State* graph_state, std::size_t heap_bytes_used)
+VisitedStates::addVisitedState(unsigned long state_number, simgrid::mc::State* graph_state, RemoteApp& remote_app)
 {
   auto new_state =
-      std::make_unique<simgrid::mc::VisitedState>(state_number, graph_state->get_actor_count(), heap_bytes_used);
+      std::make_unique<simgrid::mc::VisitedState>(state_number, graph_state->get_actor_count(), remote_app);
 
   graph_state->set_system_state(new_state->system_state_);
   XBT_DEBUG("Snapshot %p of visited state %ld (exploration stack state %ld)", new_state->system_state_.get(),

diff --git a/src/mc/VisitedState.hpp b/src/mc/VisitedState.hpp
index e3de838..b2f2694 100644 (file)
--- a/src/mc/VisitedState.hpp
+++ b/src/mc/VisitedState.hpp
@@ -22,15 +22,15 @@ public:
   long num_;               // unique id of that state in the storage of all stored IDs
   long original_num_ = -1; // num field of the VisitedState to which I was declared equal to (used for dot_output)
 
-  explicit VisitedState(unsigned long state_number, unsigned int actor_count, std::size_t heap_bytes_used);
+  explicit VisitedState(unsigned long state_number, unsigned int actor_count, RemoteApp& remote_app);
 };
 
 class XBT_PRIVATE VisitedStates {
   std::vector<std::unique_ptr<simgrid::mc::VisitedState>> states_;
 public:
   void clear() { states_.clear(); }
-  std::unique_ptr<simgrid::mc::VisitedState>
-  addVisitedState(unsigned long state_number, simgrid::mc::State* graph_state, std::size_t heap_bytes_used);
+  std::unique_ptr<simgrid::mc::VisitedState> addVisitedState(unsigned long state_number,
+                                                             simgrid::mc::State* graph_state, RemoteApp& remote_app);
 
 private:
   void prune();

diff --git a/src/mc/api/RemoteApp.cpp b/src/mc/api/RemoteApp.cpp
index 9007e82..a6fd5ab 100644 (file)
--- a/src/mc/api/RemoteApp.cpp
+++ b/src/mc/api/RemoteApp.cpp
@@ -136,7 +136,7 @@ RemoteApp::RemoteApp(const std::vector<char*>& args)
 
   /* Take the initial snapshot */
   model_checker_->wait_for_requests();
-  initial_snapshot_ = std::make_shared<simgrid::mc::Snapshot>(0);
+  initial_snapshot_ = std::make_shared<simgrid::mc::Snapshot>(0, page_store_);
 }
 
 RemoteApp::~RemoteApp()

diff --git a/src/mc/api/RemoteApp.hpp b/src/mc/api/RemoteApp.hpp
index 2f244b6..f920da6 100644 (file)
--- a/src/mc/api/RemoteApp.hpp
+++ b/src/mc/api/RemoteApp.hpp
@@ -26,6 +26,7 @@ namespace simgrid::mc {
 class XBT_PUBLIC RemoteApp {
 private:
   std::unique_ptr<ModelChecker> model_checker_;
+  PageStore page_store_{500};
   std::shared_ptr<simgrid::mc::Snapshot> initial_snapshot_;
 
   // No copy:
@@ -57,6 +58,8 @@ public:
 
   /* Get the remote process */
   RemoteProcess& get_remote_process() { return model_checker_->get_remote_process(); }
+
+  PageStore& get_page_store() { return page_store_; }
 };
 } // namespace simgrid::mc
 

diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp
index 14f0208..6b49c65 100644 (file)
--- a/src/mc/api/State.cpp
+++ b/src/mc/api/State.cpp
@@ -14,17 +14,16 @@ namespace simgrid::mc {
 
 long State::expended_states_ = 0;
 
-State::State(const RemoteApp& remote_app) : num_(++expended_states_)
+State::State(RemoteApp& remote_app) : num_(++expended_states_)
 {
   remote_app.get_actors_status(actors_to_run_);
 
   /* Stateful model checking */
-  if ((_sg_mc_checkpoint > 0 && (num_ % _sg_mc_checkpoint == 0)) || _sg_mc_termination) {
-    system_state_ = std::make_shared<simgrid::mc::Snapshot>(num_);
-  }
+  if ((_sg_mc_checkpoint > 0 && (num_ % _sg_mc_checkpoint == 0)) || _sg_mc_termination)
+    system_state_ = std::make_shared<simgrid::mc::Snapshot>(num_, remote_app.get_page_store());
 }
 
-State::State(const RemoteApp& remote_app, const State* previous_state)
+State::State(RemoteApp& remote_app, const State* previous_state)
     : default_transition_(std::make_unique<Transition>()), num_(++expended_states_)
 {
 
@@ -34,7 +33,7 @@ State::State(const RemoteApp& remote_app, const State* previous_state)
 
   /* Stateful model checking */
   if ((_sg_mc_checkpoint > 0 && (num_ % _sg_mc_checkpoint == 0)) || _sg_mc_termination) {
-    system_state_ = std::make_shared<simgrid::mc::Snapshot>(num_);
+    system_state_ = std::make_shared<simgrid::mc::Snapshot>(num_, remote_app.get_page_store());
   }
 
   /* For each actor in the previous sleep set, keep it if it is not dependent with current transition.

diff --git a/src/mc/api/State.hpp b/src/mc/api/State.hpp
index f96d540..5eb96fe 100644 (file)
--- a/src/mc/api/State.hpp
+++ b/src/mc/api/State.hpp
@@ -48,8 +48,8 @@ class XBT_PRIVATE State : public xbt::Extendable<State> {
   std::map<aid_t, Transition> sleep_set_;
   
 public:
-  explicit State(const RemoteApp& remote_app);
-  explicit State(const RemoteApp& remote_app, const State* previous_state);
+  explicit State(RemoteApp& remote_app);
+  explicit State(RemoteApp& remote_app, const State* previous_state);
   /* Returns a positive number if there is another transition to pick, or -1 if not */
   aid_t next_transition() const;
 

diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index 4c3657f..386c43c 100644 (file)
--- a/src/mc/explo/DFSExplorer.cpp
+++ b/src/mc/explo/DFSExplorer.cpp
@@ -179,8 +179,7 @@ void DFSExplorer::run()
 
     /* Check whether we already explored next_state in the past (but only if interested in state-equality reduction) */
     if (_sg_mc_max_visited_states > 0)
-      visited_state_ = visited_states_.addVisitedState(next_state->get_num(), next_state.get(),
-                                                       get_remote_app().get_remote_process().get_remote_heap_bytes());
+      visited_state_ = visited_states_.addVisitedState(next_state->get_num(), next_state.get(), get_remote_app());
 
     /* If this is a new state (or if we don't care about state-equality reduction) */
     if (visited_state_ == nullptr) {

diff --git a/src/mc/explo/LivenessChecker.cpp b/src/mc/explo/LivenessChecker.cpp
index 7aef933..c0929f1 100644 (file)
--- a/src/mc/explo/LivenessChecker.cpp
+++ b/src/mc/explo/LivenessChecker.cpp
@@ -19,12 +19,13 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc, "Logging specific to algorithms
 namespace simgrid::mc {
 
 VisitedPair::VisitedPair(int pair_num, xbt_automaton_state_t prop_state,
-                         std::shared_ptr<const std::vector<int>> atomic_propositions, std::shared_ptr<State> app_state)
+                         std::shared_ptr<const std::vector<int>> atomic_propositions, std::shared_ptr<State> app_state,
+                         RemoteApp& remote_app)
     : num(pair_num), prop_state_(prop_state)
 {
   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));
+    this->app_state_->set_system_state(std::make_shared<Snapshot>(pair_num, remote_app.get_page_store()));
   this->heap_bytes_used     = mc_model_checker->get_remote_process().get_remote_heap_bytes();
   this->actor_count_        = app_state_->get_actor_count();
   this->other_num           = -1;
@@ -59,8 +60,8 @@ std::shared_ptr<const std::vector<int>> LivenessChecker::get_proposition_values(
 
 std::shared_ptr<VisitedPair> LivenessChecker::insert_acceptance_pair(simgrid::mc::Pair* pair)
 {
-  auto new_pair =
-      std::make_shared<VisitedPair>(pair->num, pair->prop_state_, pair->atomic_propositions, pair->app_state_);
+  auto new_pair = std::make_shared<VisitedPair>(pair->num, pair->prop_state_, pair->atomic_propositions,
+                                                pair->app_state_, get_remote_app());
 
   auto [res_begin,
         res_end] = boost::range::equal_range(acceptance_pairs_, new_pair.get(), [](auto const& a, auto const& b) {
@@ -137,8 +138,8 @@ int LivenessChecker::insert_visited_pair(std::shared_ptr<VisitedPair> visited_pa
     return -1;
 
   if (visited_pair == nullptr)
-    visited_pair =
-        std::make_shared<VisitedPair>(pair->num, pair->prop_state_, pair->atomic_propositions, pair->app_state_);
+    visited_pair = std::make_shared<VisitedPair>(pair->num, pair->prop_state_, pair->atomic_propositions,
+                                                 pair->app_state_, get_remote_app());
 
   auto [range_begin,
         range_end] = boost::range::equal_range(visited_pairs_, visited_pair.get(), [](auto const& a, auto const& b) {

diff --git a/src/mc/explo/LivenessChecker.hpp b/src/mc/explo/LivenessChecker.hpp
index 50307ca..0b366e8 100644 (file)
--- a/src/mc/explo/LivenessChecker.hpp
+++ b/src/mc/explo/LivenessChecker.hpp
@@ -45,7 +45,8 @@ public:
   int actor_count_;
 
   VisitedPair(int pair_num, xbt_automaton_state_t prop_state,
-              std::shared_ptr<const std::vector<int>> atomic_propositions, std::shared_ptr<State> app_state);
+              std::shared_ptr<const std::vector<int>> atomic_propositions, std::shared_ptr<State> app_state,
+              RemoteApp& remote_app);
 };
 
 class XBT_PRIVATE LivenessChecker : public Exploration {

diff --git a/src/mc/sosp/Region.cpp b/src/mc/sosp/Region.cpp
index 426a6cb..bb98737 100644 (file)
--- a/src/mc/sosp/Region.cpp
+++ b/src/mc/sosp/Region.cpp
@@ -17,13 +17,13 @@
 
 namespace simgrid::mc {
 
-Region::Region(RegionType region_type, void* start_addr, size_t size)
+Region::Region(PageStore& store, RegionType region_type, void* start_addr, size_t size)
     : region_type_(region_type), start_addr_(start_addr), size_(size)
 {
   xbt_assert((((uintptr_t)start_addr) & (xbt_pagesize - 1)) == 0, "Start address not at the beginning of a page");
 
-  chunks_ = ChunkedData(mc_model_checker->page_store(), mc_model_checker->get_remote_process(),
-                        RemotePtr<void>(start_addr), mmu::chunk_count(size));
+  chunks_ =
+      ChunkedData(store, mc_model_checker->get_remote_process(), RemotePtr<void>(start_addr), mmu::chunk_count(size));
 }
 
 /** @brief Restore a region from a snapshot

diff --git a/src/mc/sosp/Region.hpp b/src/mc/sosp/Region.hpp
index ad428e7..01af81c 100644 (file)
--- a/src/mc/sosp/Region.hpp
+++ b/src/mc/sosp/Region.hpp
@@ -35,7 +35,7 @@ private:
   ChunkedData chunks_;
 
 public:
-  Region(RegionType type, void* start_addr, size_t size);
+  Region(PageStore& store, RegionType type, void* start_addr, size_t size);
   Region(Region const&) = delete;
   Region& operator=(Region const&) = delete;
   Region(Region&& that)            = delete;

diff --git a/src/mc/sosp/Snapshot.cpp b/src/mc/sosp/Snapshot.cpp
index ed39417..afe91c6 100644 (file)
--- a/src/mc/sosp/Snapshot.cpp
+++ b/src/mc/sosp/Snapshot.cpp
@@ -197,7 +197,8 @@ void Snapshot::ignore_restore() const
     get_remote_process()->write_bytes(ignored_data.data.data(), ignored_data.data.size(), remote(ignored_data.start));
 }
 
-Snapshot::Snapshot(long num_state, RemoteProcess* process) : AddressSpace(process), num_state_(num_state)
+Snapshot::Snapshot(long num_state, PageStore& store, RemoteProcess* process)
+    : AddressSpace(process), page_store_(store), num_state_(num_state)
 {
   XBT_DEBUG("Taking snapshot %ld", num_state);
 
@@ -223,7 +224,7 @@ void Snapshot::add_region(RegionType type, ObjectInformation* object_info, void*
   else if (type == RegionType::Heap)
     xbt_assert(not object_info, "Unexpected object info for heap region.");
 
-  auto* region = new Region(type, start_addr, size);
+  auto* region = new Region(page_store_, type, start_addr, size);
   region->object_info(object_info);
   snapshot_regions_.push_back(std::unique_ptr<Region>(region));
 }

diff --git a/src/mc/sosp/Snapshot.hpp b/src/mc/sosp/Snapshot.hpp
index 4a64390..baf06f5 100644 (file)
--- a/src/mc/sosp/Snapshot.hpp
+++ b/src/mc/sosp/Snapshot.hpp
@@ -58,9 +58,11 @@ namespace simgrid::mc {
 using hash_type = std::uint64_t;
 
 class XBT_PRIVATE Snapshot final : public AddressSpace {
+  PageStore& page_store_;
+
 public:
   /* Initialization */
-  Snapshot(long num_state, RemoteProcess* process = &mc_model_checker->get_remote_process());
+  Snapshot(long num_state, PageStore& store, RemoteProcess* process = &mc_model_checker->get_remote_process());
 
   /* Regular use */
   bool on_heap(const void* address) const

diff --git a/src/mc/sosp/Snapshot_test.cpp b/src/mc/sosp/Snapshot_test.cpp
index ff2ff0b..c7a1804 100644 (file)
--- a/src/mc/sosp/Snapshot_test.cpp
+++ b/src/mc/sosp/Snapshot_test.cpp
@@ -15,6 +15,8 @@
 /**************** Class BOOST_tests *************************/
 using simgrid::mc::Region;
 class snap_test_helper {
+  static simgrid::mc::PageStore page_store_;
+
 public:
   static void init_memory(void* mem, size_t size);
   static void Init();
@@ -43,6 +45,7 @@ public:
 
 // static member variables init.
 std::unique_ptr<simgrid::mc::RemoteProcess> snap_test_helper::process = nullptr;
+simgrid::mc::PageStore snap_test_helper::page_store_(500);
 
 void snap_test_helper::init_memory(void* mem, size_t size)
 {
@@ -72,11 +75,11 @@ 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(simgrid::mc::RegionType::Data, source, byte_size);
+  auto* region0 = new simgrid::mc::Region(page_store_, 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(simgrid::mc::RegionType::Data, source, byte_size);
+  auto* region = new simgrid::mc::Region(page_store_, 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");
@@ -158,7 +161,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(simgrid::mc::RegionType::Data, ret.src, ret.size);
+  const simgrid::mc::Region region2(page_store_, 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);