Move 2 functions from mc::ModelChecker to mc::RemoteApp

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index 60f4970..8804000 100644 (file)
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -105,19 +105,6 @@ void ModelChecker::setup_ignore()
   process.ignore_global_variable("counter");
 }
 
-void ModelChecker::shutdown()
-{
-  XBT_DEBUG("Shutting down model-checker");
-
-  RemoteProcessMemory& process = get_remote_process_memory();
-  if (process.running()) {
-    XBT_DEBUG("Killing process");
-    finalize_app(true);
-    kill(process.pid(), SIGKILL);
-    process.terminate();
-  }
-}
-
 void ModelChecker::resume()
 {
   if (checker_side_.get_channel().send(MessageType::CONTINUE) != 0)
@@ -244,7 +231,7 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size)
 /** Terminate the model-checker application */
 void ModelChecker::exit(int status)
 {
-  shutdown();
+  get_exploration()->get_remote_app().shutdown();
   ::exit(status);
 }
 
@@ -339,20 +326,4 @@ Transition* ModelChecker::handle_simcall(aid_t aid, int times_considered, bool n
     return nullptr;
 }
 
-void ModelChecker::finalize_app(bool terminate_asap)
-{
-  s_mc_message_int_t m = {};
-  m.type  = MessageType::FINALIZE;
-  m.value = terminate_asap;
-  xbt_assert(checker_side_.get_channel().send(m) == 0, "Could not ask the app to finalize on need");
-
-  s_mc_message_t answer;
-  ssize_t s = checker_side_.get_channel().receive(answer);
-  xbt_assert(s != -1, "Could not receive answer to FINALIZE");
-  xbt_assert(s == sizeof answer, "Broken message (size=%zd; expected %zu)", s, sizeof answer);
-  xbt_assert(answer.type == MessageType::FINALIZE_REPLY,
-             "Received unexpected message %s (%i); expected MessageType::FINALIZE_REPLY (%i)", to_c_str(answer.type),
-             (int)answer.type, (int)MessageType::FINALIZE_REPLY);
-}
-
 } // namespace simgrid::mc

diff --git a/src/mc/ModelChecker.hpp b/src/mc/ModelChecker.hpp
index 5f7c53b..5554144 100644 (file)
--- a/src/mc/ModelChecker.hpp
+++ b/src/mc/ModelChecker.hpp
@@ -31,7 +31,6 @@ public:
   Channel& channel() { return checker_side_.get_channel(); }
 
   void start();
-  void shutdown();
   void resume();
   void wait_for_requests();
 
@@ -41,8 +40,6 @@ public:
   /* Interactions with the simcall observer */
   XBT_ATTRIB_NORETURN void exit(int status);
 
-  void finalize_app(bool terminate_asap = false);
-
   Exploration* get_exploration() const { return exploration_; }
   void set_exploration(Exploration* exploration) { exploration_ = exploration; }
 

diff --git a/src/mc/api/RemoteApp.cpp b/src/mc/api/RemoteApp.cpp
index b31650f..842961a 100644 (file)
--- a/src/mc/api/RemoteApp.cpp
+++ b/src/mc/api/RemoteApp.cpp
@@ -143,7 +143,7 @@ RemoteApp::~RemoteApp()
 {
   initial_snapshot_ = nullptr;
   if (model_checker_) {
-    model_checker_->shutdown();
+    shutdown();
     model_checker_   = nullptr;
     mc_model_checker = nullptr;
   }
@@ -268,4 +268,34 @@ void RemoteApp::check_deadlock() const
     throw DeadlockError();
   }
 }
+
+void RemoteApp::shutdown()
+{
+  XBT_DEBUG("Shutting down model-checker");
+
+  RemoteProcessMemory& process = get_remote_process_memory();
+  if (process.running()) {
+    XBT_DEBUG("Killing process");
+    finalize_app(true);
+    kill(process.pid(), SIGKILL);
+    process.terminate();
+  }
+}
+
+void RemoteApp::finalize_app(bool terminate_asap)
+{
+  s_mc_message_int_t m = {};
+  m.type               = MessageType::FINALIZE;
+  m.value              = terminate_asap;
+  xbt_assert(model_checker_->channel().send(m) == 0, "Could not ask the app to finalize on need");
+
+  s_mc_message_t answer;
+  ssize_t s = model_checker_->channel().receive(answer);
+  xbt_assert(s != -1, "Could not receive answer to FINALIZE");
+  xbt_assert(s == sizeof answer, "Broken message (size=%zd; expected %zu)", s, sizeof answer);
+  xbt_assert(answer.type == MessageType::FINALIZE_REPLY,
+             "Received unexpected message %s (%i); expected MessageType::FINALIZE_REPLY (%i)", to_c_str(answer.type),
+             (int)answer.type, (int)MessageType::FINALIZE_REPLY);
+}
+
 } // namespace simgrid::mc

diff --git a/src/mc/api/RemoteApp.hpp b/src/mc/api/RemoteApp.hpp
index 975502e..f1c60f7 100644 (file)
--- a/src/mc/api/RemoteApp.hpp
+++ b/src/mc/api/RemoteApp.hpp
@@ -50,6 +50,11 @@ public:
   /** Ask to the application to check for a deadlock. If so, do an error message and throw a DeadlockError. */
   void check_deadlock() const;
 
+  /** Ask the application to run post-mortem analysis, and maybe to stop ASAP */
+  void finalize_app(bool terminate_asap = false);
+  /** Forcefully kill the application (after running post-mortem analysis)*/
+  void shutdown();
+
   /** Retrieve the max PID of the running actors */
   unsigned long get_maxpid() const;
 

diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index d2aa4f4..4602fdf 100644 (file)
--- a/src/mc/explo/DFSExplorer.cpp
+++ b/src/mc/explo/DFSExplorer.cpp
@@ -135,7 +135,7 @@ void DFSExplorer::run()
                 stack_.size() + 1);
       
       if (state->get_actor_count() == 0) {
-        mc_model_checker->finalize_app();
+        get_remote_app().finalize_app();
         XBT_VERB("Execution came to an end at %s (state: %ld, depth: %zu)", get_record_trace().to_string().c_str(),
                  state->get_num(), stack_.size());