From 95f6f24c739bd20e274a8af9b9e998dff826986d Mon Sep 17 00:00:00 2001 From: Martin Quinson Date: Sun, 12 Mar 2023 23:31:40 +0100 Subject: [PATCH] move wait_for_requests() from ModelChecker to RemoteApp --- src/mc/ModelChecker.cpp | 11 ----------- src/mc/ModelChecker.hpp | 4 ++-- src/mc/api/RemoteApp.cpp | 33 +++++++++++++++++++++----------- src/mc/api/RemoteApp.hpp | 1 + src/mc/api/State.cpp | 3 ++- src/mc/transition/Transition.cpp | 3 ++- 6 files changed, 29 insertions(+), 26 deletions(-) diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp index c95d4bf00f..69d1d204ba 100644 --- a/src/mc/ModelChecker.cpp +++ b/src/mc/ModelChecker.cpp @@ -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 = {}; diff --git a/src/mc/ModelChecker.hpp b/src/mc/ModelChecker.hpp index 5fc0052444..40ad462760 100644 --- a/src/mc/ModelChecker.hpp +++ b/src/mc/ModelChecker.hpp @@ -28,10 +28,10 @@ public: explicit ModelChecker(std::unique_ptr 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); diff --git a/src/mc/api/RemoteApp.cpp b/src/mc/api/RemoteApp.cpp index 842961a11c..6b53a00f39 100644 --- a/src/mc/api/RemoteApp.cpp +++ b/src/mc/api/RemoteApp.cpp @@ -135,7 +135,7 @@ RemoteApp::RemoteApp(const std::vector& args) model_checker_->start(); /* Take the initial snapshot */ - model_checker_->wait_for_requests(); + wait_for_requests(); initial_snapshot_ = std::make_shared(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& 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& whereto) const std::vector 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(received) == size); } @@ -217,7 +217,7 @@ void RemoteApp::get_actors_status(std::map& whereto) const std::vector 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(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& 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, diff --git a/src/mc/api/RemoteApp.hpp b/src/mc/api/RemoteApp.hpp index f1c60f70f4..ed1d7ee0e1 100644 --- a/src/mc/api/RemoteApp.hpp +++ b/src/mc/api/RemoteApp.hpp @@ -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; diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp index 6b49c65faa..77973c91c5 100644 --- a/src/mc/api/State.cpp +++ b/src/mc/api/State.cpp @@ -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 @@ -133,6 +134,6 @@ void State::execute_next(aid_t next) auto executed_transition = std::unique_ptr(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 diff --git a/src/mc/transition/Transition.cpp b/src/mc/transition/Transition.cpp index 2c20b73430..8ad38774eb 100644 --- a/src/mc/transition/Transition.cpp +++ b/src/mc/transition/Transition.cpp @@ -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 } -- 2.20.1