Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Move handle_simcall from ModelChecker to RemoteApp
authorMartin Quinson <martin.quinson@ens-rennes.fr>
Fri, 17 Mar 2023 21:13:40 +0000 (22:13 +0100)
committerMartin Quinson <martin.quinson@ens-rennes.fr>
Fri, 17 Mar 2023 21:43:13 +0000 (22:43 +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 10f0ba3..20d6be5 100644 (file)
@@ -215,31 +215,4 @@ void ModelChecker::handle_waitpid()
   }
 }
 
-Transition* ModelChecker::handle_simcall(aid_t aid, int times_considered, bool new_transition)
-{
-  s_mc_message_simcall_execute_t m = {};
-  m.type              = MessageType::SIMCALL_EXECUTE;
-  m.aid_              = aid;
-  m.times_considered_ = times_considered;
-  checker_side_.get_channel().send(m);
-
-  this->remote_process_memory_->clear_cache();
-  if (this->remote_process_memory_->running())
-    checker_side_.dispatch(); // The app may send messages while processing the transition
-
-  s_mc_message_simcall_execute_answer_t answer;
-  ssize_t s = checker_side_.get_channel().receive(answer);
-  xbt_assert(s != -1, "Could not receive message");
-  xbt_assert(s == sizeof answer, "Broken message (size=%zd; expected %zu)", s, sizeof answer);
-  xbt_assert(answer.type == MessageType::SIMCALL_EXECUTE_ANSWER,
-             "Received unexpected message %s (%i); expected MessageType::SIMCALL_EXECUTE_ANSWER (%i)",
-             to_c_str(answer.type), (int)answer.type, (int)MessageType::SIMCALL_EXECUTE_ANSWER);
-
-  if (new_transition) {
-    std::stringstream stream(answer.buffer.data());
-    return deserialize_transition(aid, times_considered, stream);
-  } else
-    return nullptr;
-}
-
 } // namespace simgrid::mc
index 0d51e9e..50f3779 100644 (file)
@@ -33,9 +33,6 @@ public:
 
   void start();
 
-  /** 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);
-
   Exploration* get_exploration() const { return exploration_; }
   void set_exploration(Exploration* exploration) { exploration_ = exploration; }
 
index 6782fa3..d7fa977 100644 (file)
@@ -283,6 +283,33 @@ void RemoteApp::shutdown()
   }
 }
 
+Transition* RemoteApp::handle_simcall(aid_t aid, int times_considered, bool new_transition)
+{
+  s_mc_message_simcall_execute_t m = {};
+  m.type                           = MessageType::SIMCALL_EXECUTE;
+  m.aid_                           = aid;
+  m.times_considered_              = times_considered;
+  model_checker_->get_channel().send(m);
+
+  get_remote_process_memory().clear_cache();
+  if (this->get_remote_process_memory().running())
+    model_checker_->channel_handle_events(); // The app may send messages while processing the transition
+
+  s_mc_message_simcall_execute_answer_t answer;
+  ssize_t s = model_checker_->get_channel().receive(answer);
+  xbt_assert(s != -1, "Could not receive message");
+  xbt_assert(s == sizeof answer, "Broken message (size=%zd; expected %zu)", s, sizeof answer);
+  xbt_assert(answer.type == MessageType::SIMCALL_EXECUTE_ANSWER,
+             "Received unexpected message %s (%i); expected MessageType::SIMCALL_EXECUTE_ANSWER (%i)",
+             to_c_str(answer.type), (int)answer.type, (int)MessageType::SIMCALL_EXECUTE_ANSWER);
+
+  if (new_transition) {
+    std::stringstream stream(answer.buffer.data());
+    return deserialize_transition(aid, times_considered, stream);
+  } else
+    return nullptr;
+}
+
 void RemoteApp::finalize_app(bool terminate_asap)
 {
   s_mc_message_int_t m = {};
index ed1d7ee..58531fa 100644 (file)
@@ -62,6 +62,9 @@ public:
   /* Get the list of actors that are ready to run at that step. Usually shorter than maxpid */
   void get_actors_status(std::map<aid_t, simgrid::mc::ActorState>& whereto) const;
 
+  /** 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);
+
   /* Get the memory of the remote process */
   RemoteProcessMemory& get_remote_process_memory() { return model_checker_->get_remote_process_memory(); }
 
index 6577e1b..e81998b 100644 (file)
@@ -118,7 +118,8 @@ void State::execute_next(aid_t next)
 
   // 2. Execute the actor according to the preparation above
   Transition::executed_transitions_++;
-  auto* just_executed = mc_model_checker->handle_simcall(next, times_considered, true);
+  auto* just_executed =
+      mc_model_checker->get_exploration()->get_remote_app().handle_simcall(next, times_considered, true);
   xbt_assert(just_executed->type_ == expected_executed_transition->type_,
              "The transition that was just executed by actor %ld, viz:\n"
              "%s\n"
index 8ad3877..1b6f8c3 100644 (file)
@@ -50,7 +50,7 @@ void Transition::replay() const
   replayed_transitions_++;
 
 #if SIMGRID_HAVE_MC
-  mc_model_checker->handle_simcall(aid_, times_considered_, false);
+  mc_model_checker->get_exploration()->get_remote_app().handle_simcall(aid_, times_considered_, false);
   mc_model_checker->get_exploration()->get_remote_app().wait_for_requests();
 #endif
 }