Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
move wait_for_requests() from ModelChecker to RemoteApp
authorMartin Quinson <martin.quinson@ens-rennes.fr>
Sun, 12 Mar 2023 22:31:40 +0000 (23:31 +0100)
committerMartin Quinson <martin.quinson@ens-rennes.fr>
Sun, 12 Mar 2023 22:31:40 +0000 (23:31 +0100)
src/mc/ModelChecker.cpp
src/mc/ModelChecker.hpp
src/mc/api/RemoteApp.cpp
src/mc/api/RemoteApp.hpp
src/mc/api/State.cpp
src/mc/transition/Transition.cpp

index c95d4bf..69d1d20 100644 (file)
@@ -278,17 +278,6 @@ void ModelChecker::handle_waitpid()
   }
 }
 
-void ModelChecker::wait_for_requests()
-{
-  /* Resume the application */
-  if (checker_side_.get_channel().send(MessageType::CONTINUE) != 0)
-    throw xbt::errno_error();
-  remote_process_memory_->clear_cache();
-
-  if (this->get_remote_process_memory().running())
-    checker_side_.dispatch();
-}
-
 Transition* ModelChecker::handle_simcall(aid_t aid, int times_considered, bool new_transition)
 {
   s_mc_message_simcall_execute_t m = {};
index 5fc0052..40ad462 100644 (file)
@@ -28,10 +28,10 @@ public:
   explicit ModelChecker(std::unique_ptr<RemoteProcessMemory> remote_simulation, int sockfd);
 
   RemoteProcessMemory& get_remote_process_memory() { return *remote_process_memory_; }
-  Channel& channel() { return checker_side_.get_channel(); }
+  Channel& get_channel() { return checker_side_.get_channel(); }
+  void channel_handle_events() { checker_side_.dispatch(); }
 
   void start();
-  void wait_for_requests();
 
   /** Let the application take a transition. A new Transition is created iff the last parameter is true */
   Transition* handle_simcall(aid_t aid, int times_considered, bool new_transition);
index 842961a..6b53a00 100644 (file)
@@ -135,7 +135,7 @@ RemoteApp::RemoteApp(const std::vector<char*>& args)
   model_checker_->start();
 
   /* Take the initial snapshot */
-  model_checker_->wait_for_requests();
+  wait_for_requests();
   initial_snapshot_ = std::make_shared<simgrid::mc::Snapshot>(0, page_store_);
 }
 
@@ -159,9 +159,9 @@ unsigned long RemoteApp::get_maxpid() const
   // note: we could maybe cache it and count the actor creation on checker side too.
   // But counting correctly accross state checkpoint/restore would be annoying.
 
-  model_checker_->channel().send(MessageType::ACTORS_MAXPID);
+  model_checker_->get_channel().send(MessageType::ACTORS_MAXPID);
   s_mc_message_int_t answer;
-  ssize_t answer_size = model_checker_->channel().receive(answer);
+  ssize_t answer_size = model_checker_->get_channel().receive(answer);
   xbt_assert(answer_size != -1, "Could not receive message");
   xbt_assert(answer_size == sizeof answer, "Broken message (size=%zd; expected %zu)", answer_size, sizeof answer);
   xbt_assert(answer.type == MessageType::ACTORS_MAXPID_REPLY,
@@ -180,10 +180,10 @@ void RemoteApp::get_actors_status(std::map<aid_t, ActorState>& whereto) const
   //                    <----- send ACTORS_STATUS_REPLY
   //                    <----- send `N` `s_mc_message_actors_status_one_t` structs
   //                    <----- send `M` `s_mc_message_simcall_probe_one_t` structs
-  model_checker_->channel().send(MessageType::ACTORS_STATUS);
+  model_checker_->get_channel().send(MessageType::ACTORS_STATUS);
 
   s_mc_message_actors_status_answer_t answer;
-  ssize_t answer_size = model_checker_->channel().receive(answer);
+  ssize_t answer_size = model_checker_->get_channel().receive(answer);
   xbt_assert(answer_size != -1, "Could not receive message");
   xbt_assert(answer_size == sizeof answer, "Broken message (size=%zd; expected %zu)", answer_size, sizeof answer);
   xbt_assert(answer.type == MessageType::ACTORS_STATUS_REPLY,
@@ -201,7 +201,7 @@ void RemoteApp::get_actors_status(std::map<aid_t, ActorState>& whereto) const
   std::vector<s_mc_message_actors_status_one_t> status(answer.count);
   if (answer.count > 0) {
     size_t size      = status.size() * sizeof(s_mc_message_actors_status_one_t);
-    ssize_t received = model_checker_->channel().receive(status.data(), size);
+    ssize_t received = model_checker_->get_channel().receive(status.data(), size);
     xbt_assert(static_cast<size_t>(received) == size);
   }
 
@@ -217,7 +217,7 @@ void RemoteApp::get_actors_status(std::map<aid_t, ActorState>& whereto) const
   std::vector<s_mc_message_simcall_probe_one_t> probes(answer.transition_count);
   if (answer.transition_count > 0) {
     for (auto& probe : probes) {
-      ssize_t received = model_checker_->channel().receive(probe);
+      ssize_t received = model_checker_->get_channel().receive(probe);
       xbt_assert(received >= 0, "Could not receive response to ACTORS_PROBE message (%s)", strerror(errno));
       xbt_assert(static_cast<size_t>(received) == sizeof probe,
                  "Could not receive response to ACTORS_PROBE message (%zd bytes received != %zu bytes expected",
@@ -248,9 +248,9 @@ void RemoteApp::get_actors_status(std::map<aid_t, ActorState>& whereto) const
 
 void RemoteApp::check_deadlock() const
 {
-  xbt_assert(model_checker_->channel().send(MessageType::DEADLOCK_CHECK) == 0, "Could not check deadlock state");
+  xbt_assert(model_checker_->get_channel().send(MessageType::DEADLOCK_CHECK) == 0, "Could not check deadlock state");
   s_mc_message_int_t message;
-  ssize_t received = model_checker_->channel().receive(message);
+  ssize_t received = model_checker_->get_channel().receive(message);
   xbt_assert(received != -1, "Could not receive message");
   xbt_assert(received == sizeof message, "Broken message (size=%zd; expected %zu)", received, sizeof message);
   xbt_assert(message.type == MessageType::DEADLOCK_CHECK_REPLY,
@@ -269,6 +269,17 @@ void RemoteApp::check_deadlock() const
   }
 }
 
+void RemoteApp::wait_for_requests()
+{
+  /* Resume the application */
+  if (model_checker_->get_channel().send(MessageType::CONTINUE) != 0)
+    throw xbt::errno_error();
+  get_remote_process_memory().clear_cache();
+
+  if (this->get_remote_process_memory().running())
+    model_checker_->channel_handle_events();
+}
+
 void RemoteApp::shutdown()
 {
   XBT_DEBUG("Shutting down model-checker");
@@ -287,10 +298,10 @@ 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");
+  xbt_assert(model_checker_->get_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);
+  ssize_t s = model_checker_->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,
index f1c60f7..ed1d7ee 100644 (file)
@@ -46,6 +46,7 @@ public:
   ~RemoteApp();
 
   void restore_initial_state() const;
+  void wait_for_requests();
 
   /** Ask to the application to check for a deadlock. If so, do an error message and throw a DeadlockError. */
   void check_deadlock() const;
index 6b49c65..77973c9 100644 (file)
@@ -4,6 +4,7 @@
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
 #include "src/mc/api/State.hpp"
+#include "src/mc/explo/Exploration.hpp"
 #include "src/mc/mc_config.hpp"
 
 #include <boost/range/algorithm.hpp>
@@ -133,6 +134,6 @@ void State::execute_next(aid_t next)
   auto executed_transition = std::unique_ptr<Transition>(just_executed);
   actor_state.set_transition(std::move(executed_transition), times_considered);
 
-  mc_model_checker->wait_for_requests();
+  mc_model_checker->get_exploration()->get_remote_app().wait_for_requests();
 }
 } // namespace simgrid::mc
index 2c20b73..8ad3877 100644 (file)
@@ -11,6 +11,7 @@
 
 #if SIMGRID_HAVE_MC
 #include "src/mc/ModelChecker.hpp"
+#include "src/mc/explo/Exploration.hpp"
 #include "src/mc/transition/TransitionActorJoin.hpp"
 #include "src/mc/transition/TransitionAny.hpp"
 #include "src/mc/transition/TransitionComm.hpp"
@@ -50,7 +51,7 @@ void Transition::replay() const
 
 #if SIMGRID_HAVE_MC
   mc_model_checker->handle_simcall(aid_, times_considered_, false);
-  mc_model_checker->wait_for_requests();
+  mc_model_checker->get_exploration()->get_remote_app().wait_for_requests();
 #endif
 }