Put everything in position to re-fork the verified App

If you pass "need_memory_introspection = false" to the Exploration
constructor, then the application is re-forked systematically instead
of taking snapshot that are then restored.

But it's still in progress, in the sense that the memory is still
introspected even if we don't need it. The network protocol still
needs to be changed so that the memory info are asked only if
"need_memory_introspection = true" and not otherwise.

For the time being, using reforks is very memory intensive for some
reason, and my computers gets to its knees when running the tests.
Until after the OOM killer saves me by cleaning stuff.

diff --git a/src/mc/api/RemoteApp.cpp b/src/mc/api/RemoteApp.cpp
index 2ddd5c0..e57e931 100644 (file)
--- a/src/mc/api/RemoteApp.cpp
+++ b/src/mc/api/RemoteApp.cpp
@@ -29,11 +29,15 @@ XBT_LOG_EXTERNAL_CATEGORY(mc_global);
 
 namespace simgrid::mc {
 
-RemoteApp::RemoteApp(const std::vector<char*>& args)
+RemoteApp::RemoteApp(const std::vector<char*>& args, bool need_memory_introspection)
 {
-  checker_side_ = std::make_unique<simgrid::mc::CheckerSide>(args);
+  for (auto* arg : args)
+    app_args_.push_back(arg);
 
-  initial_snapshot_ = std::make_shared<simgrid::mc::Snapshot>(0, page_store_, checker_side_->get_remote_memory());
+  checker_side_ = std::make_unique<simgrid::mc::CheckerSide>(app_args_);
+
+  if (need_memory_introspection)
+    initial_snapshot_ = std::make_shared<simgrid::mc::Snapshot>(0, page_store_, checker_side_->get_remote_memory());
 }
 
 RemoteApp::~RemoteApp()
@@ -42,9 +46,15 @@ RemoteApp::~RemoteApp()
   shutdown();
 }
 
-void RemoteApp::restore_initial_state() const
+void RemoteApp::restore_initial_state()
 {
-  this->initial_snapshot_->restore(checker_side_->get_remote_memory());
+  if (initial_snapshot_ == nullptr) { // No memory introspection
+    shutdown();
+    checker_side_.reset(
+        nullptr); // We need to destroy the existing CheckerSide before creating the new one, or libevent gets crazy
+    checker_side_.reset(new simgrid::mc::CheckerSide(app_args_));
+  } else
+    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 d6e5eee..5ad3559 100644 (file)
--- a/src/mc/api/RemoteApp.hpp
+++ b/src/mc/api/RemoteApp.hpp
@@ -30,6 +30,8 @@ private:
   PageStore page_store_{500};
   std::shared_ptr<simgrid::mc::Snapshot> initial_snapshot_;
 
+  std::vector<char*> app_args_;
+
   // No copy:
   RemoteApp(RemoteApp const&) = delete;
   RemoteApp& operator=(RemoteApp const&) = delete;
@@ -42,11 +44,11 @@ public:
    *
    *  The code is expected to `exec` the model-checked application.
    */
-  explicit RemoteApp(const std::vector<char*>& args);
+  explicit RemoteApp(const std::vector<char*>& args, bool need_memory_introspection);
 
   ~RemoteApp();
 
-  void restore_initial_state() const;
+  void restore_initial_state();
   void wait_for_requests();
 
   /** Ask to the application to check for a deadlock. If so, do an error message and throw a DeadlockError. */

diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index 9839611..99379b8 100644 (file)
--- a/src/mc/explo/DFSExplorer.cpp
+++ b/src/mc/explo/DFSExplorer.cpp
@@ -297,7 +297,7 @@ void DFSExplorer::backtrack()
   } // If no backtracing point, then the stack is empty and the exploration is over
 }
 
-DFSExplorer::DFSExplorer(const std::vector<char*>& args, bool with_dpor) : Exploration(args)
+DFSExplorer::DFSExplorer(const std::vector<char*>& args, bool with_dpor) : Exploration(args, true)
 {
   if (with_dpor)
     reduction_mode_ = ReductionMode::dpor;

diff --git a/src/mc/explo/Exploration.cpp b/src/mc/explo/Exploration.cpp
index 1dbe4c4..463a5e3 100644 (file)
--- a/src/mc/explo/Exploration.cpp
+++ b/src/mc/explo/Exploration.cpp
@@ -20,7 +20,8 @@ static simgrid::config::Flag<std::string> cfg_dot_output_file{
 
 Exploration* Exploration::instance_ = nullptr; // singleton instance
 
-Exploration::Exploration(const std::vector<char*>& args) : remote_app_(std::make_unique<RemoteApp>(args))
+Exploration::Exploration(const std::vector<char*>& args, bool need_memory_introspection)
+    : remote_app_(std::make_unique<RemoteApp>(args, need_memory_introspection))
 {
   xbt_assert(instance_ == nullptr, "Cannot have more than one exploration instance");
   instance_ = this;

diff --git a/src/mc/explo/Exploration.hpp b/src/mc/explo/Exploration.hpp
index c027256..7a30470 100644 (file)
--- a/src/mc/explo/Exploration.hpp
+++ b/src/mc/explo/Exploration.hpp
@@ -34,7 +34,7 @@ class Exploration : public xbt::Extendable<Exploration> {
   FILE* dot_output_ = nullptr;
 
 public:
-  explicit Exploration(const std::vector<char*>& args);
+  explicit Exploration(const std::vector<char*>& args, bool need_memory_introspection);
   virtual ~Exploration();
 
   static Exploration* get_instance() { return instance_; }

diff --git a/src/mc/explo/LivenessChecker.cpp b/src/mc/explo/LivenessChecker.cpp
index 7290930..ea293ae 100644 (file)
--- a/src/mc/explo/LivenessChecker.cpp
+++ b/src/mc/explo/LivenessChecker.cpp
@@ -180,7 +180,7 @@ void LivenessChecker::purge_visited_pairs()
   }
 }
 
-LivenessChecker::LivenessChecker(const std::vector<char*>& args) : Exploration(args) {}
+LivenessChecker::LivenessChecker(const std::vector<char*>& args) : Exploration(args, true) {}
 LivenessChecker::~LivenessChecker()
 {
   xbt_automaton_free(property_automaton_);

diff --git a/src/mc/explo/UdporChecker.cpp b/src/mc/explo/UdporChecker.cpp
index 1506a16..17cca8d 100644 (file)
--- a/src/mc/explo/UdporChecker.cpp
+++ b/src/mc/explo/UdporChecker.cpp
@@ -13,7 +13,7 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_udpor, mc, "Logging specific to verification
 
 namespace simgrid::mc::udpor {
 
-UdporChecker::UdporChecker(const std::vector<char*>& args) : Exploration(args)
+UdporChecker::UdporChecker(const std::vector<char*>& args) : Exploration(args, true)
 {
   // Initialize the map
 }

diff --git a/src/mc/remote/CheckerSide.cpp b/src/mc/remote/CheckerSide.cpp
index bd7b16b..54c8563 100644 (file)
--- a/src/mc/remote/CheckerSide.cpp
+++ b/src/mc/remote/CheckerSide.cpp
@@ -126,6 +126,8 @@ static void wait_application_process(pid_t pid)
 
 void CheckerSide::setup_events()
 {
+  if (base_ != nullptr)
+    event_base_free(base_.get());
   auto* base = event_base_new();
   base_.reset(base);
 

diff --git a/src/mc/remote/CheckerSide.hpp b/src/mc/remote/CheckerSide.hpp
index 2461d33..40e74c5 100644 (file)
--- a/src/mc/remote/CheckerSide.hpp
+++ b/src/mc/remote/CheckerSide.hpp
@@ -18,12 +18,16 @@ namespace simgrid::mc {
 /* CheckerSide: All what the checker needs to interact with a given application process */
 
 class CheckerSide {
+  void (*const free_event_fun)(event*) = [](event* evt) {
+    event_del(evt);
+    event_free(evt);
+  };
+  std::unique_ptr<event, decltype(&event_free)> socket_event_{nullptr, free_event_fun};
+  std::unique_ptr<event, decltype(&event_free)> signal_event_{nullptr, free_event_fun};
   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_;
 
+  Channel channel_;
   bool running_ = false;
   pid_t pid_;