Make a global singleton of Exploration, to kill ModelChecker

Having global singletons is far from optimal, but it's a bit like the
EngineImpl singleton in the model-checker process.

This will allow to kill the ModelChecker class which responsabilities
were split between RemoteApp and Exploration.

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index cec73c6..a9e0e99 100644 (file)
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -99,7 +99,7 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size)
       return false;
 
     case MessageType::ASSERTION_FAILED:
-      exploration_->report_assertion_failure();
+      Exploration::get_instance()->report_assertion_failure();
       break;
 
     default:
@@ -132,7 +132,7 @@ void ModelChecker::handle_waitpid(pid_t pid_to_wait)
         xbt_assert(ptrace(PTRACE_GETEVENTMSG, pid_to_wait, 0, &eventmsg) != -1, "Could not get exit status");
         status = static_cast<int>(eventmsg);
         if (WIFSIGNALED(status))
-          exploration_->report_crash(status);
+          Exploration::get_instance()->report_crash(status);
       }
 #endif
 
@@ -149,7 +149,7 @@ void ModelChecker::handle_waitpid(pid_t pid_to_wait)
       }
 
       else if (WIFSIGNALED(status)) {
-        exploration_->report_crash(status);
+        Exploration::get_instance()->report_crash(status);
       } else if (WIFEXITED(status)) {
         XBT_DEBUG("Child process is over");
         this->get_remote_process_memory().terminate();

diff --git a/src/mc/ModelChecker.hpp b/src/mc/ModelChecker.hpp
index 7b91263..58654af 100644 (file)
--- a/src/mc/ModelChecker.hpp
+++ b/src/mc/ModelChecker.hpp
@@ -19,7 +19,6 @@ namespace simgrid::mc {
  */
 class ModelChecker {
   std::unique_ptr<RemoteProcessMemory> remote_process_memory_;
-  Exploration* exploration_ = nullptr;
 
 public:
   ModelChecker(ModelChecker const&) = delete;
@@ -28,9 +27,6 @@ public:
 
   RemoteProcessMemory& get_remote_process_memory() { return *remote_process_memory_; }
 
-  Exploration* get_exploration() const { return exploration_; }
-  void set_exploration(Exploration* exploration) { exploration_ = exploration; }
-
   void handle_waitpid(pid_t pid_to_wait);                // FIXME move to RemoteApp
   bool handle_message(const char* buffer, ssize_t size); // FIXME move to RemoteApp
 };

diff --git a/src/mc/api/RemoteApp.cpp b/src/mc/api/RemoteApp.cpp
index 6c109d4..dd249a2 100644 (file)
--- a/src/mc/api/RemoteApp.cpp
+++ b/src/mc/api/RemoteApp.cpp
@@ -282,13 +282,14 @@ void RemoteApp::check_deadlock() const
              to_c_str(message.type), (int)message.type, (int)MessageType::DEADLOCK_CHECK_REPLY);
 
   if (message.value != 0) {
+    auto* explo = Exploration::get_instance();
     XBT_CINFO(mc_global, "Counter-example execution trace:");
-    for (auto const& frame : model_checker_->get_exploration()->get_textual_trace())
+    for (auto const& frame : explo->get_textual_trace())
       XBT_CINFO(mc_global, "  %s", frame.c_str());
     XBT_INFO("You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with "
              "--cfg=model-check/replay:'%s'",
-             model_checker_->get_exploration()->get_record_trace().to_string().c_str());
-    model_checker_->get_exploration()->log_state();
+             explo->get_record_trace().to_string().c_str());
+    explo->log_state();
     throw DeadlockError();
   }
 }

diff --git a/src/mc/explo/Exploration.cpp b/src/mc/explo/Exploration.cpp
index 0e44b04..02a0016 100644 (file)
--- a/src/mc/explo/Exploration.cpp
+++ b/src/mc/explo/Exploration.cpp
@@ -18,9 +18,12 @@ namespace simgrid::mc {
 static simgrid::config::Flag<std::string> cfg_dot_output_file{
     "model-check/dot-output", "Name of dot output file corresponding to graph state", ""};
 
+Exploration* Exploration::instance_ = nullptr; // singleton instance
+
 Exploration::Exploration(const std::vector<char*>& args) : remote_app_(std::make_unique<RemoteApp>(args))
 {
-  mc_model_checker->set_exploration(this);
+  xbt_assert(instance_ == nullptr, "Cannot have more than one exploration instance");
+  instance_ = this;
 
   if (not cfg_dot_output_file.get().empty()) {
     dot_output_ = fopen(cfg_dot_output_file.get().c_str(), "w");

diff --git a/src/mc/explo/Exploration.hpp b/src/mc/explo/Exploration.hpp
index ee3c452..c027256 100644 (file)
--- a/src/mc/explo/Exploration.hpp
+++ b/src/mc/explo/Exploration.hpp
@@ -29,6 +29,7 @@ namespace simgrid::mc {
 // abstract
 class Exploration : public xbt::Extendable<Exploration> {
   std::unique_ptr<RemoteApp> remote_app_;
+  static Exploration* instance_;
 
   FILE* dot_output_ = nullptr;
 
@@ -36,6 +37,7 @@ public:
   explicit Exploration(const std::vector<char*>& args);
   virtual ~Exploration();
 
+  static Exploration* get_instance() { return instance_; }
   // No copy:
   Exploration(Exploration const&) = delete;
   Exploration& operator=(Exploration const&) = delete;