From: Martin Quinson Date: Sat, 5 Feb 2022 22:57:33 +0000 (+0100) Subject: Don't compute the dependencies locally in the checker, but through the observers... X-Git-Tag: v3.31~494 X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/d89ca681772fdaafdd69049d4d66676a4e98de38 Don't compute the dependencies locally in the checker, but through the observers over the network --- diff --git a/src/kernel/actor/SimcallObserver.cpp b/src/kernel/actor/SimcallObserver.cpp index e0b4a5517a..8d13441662 100644 --- a/src/kernel/actor/SimcallObserver.cpp +++ b/src/kernel/actor/SimcallObserver.cpp @@ -323,8 +323,10 @@ std::string ActivityWaitSimcall::to_string(int times_considered) const { std::string res = SimcallObserver::to_string(times_considered); auto* comm = dynamic_cast(activity_); - if (comm == nullptr) - xbt_die("Only Comms are supported here for now"); + if (comm == nullptr) { + res += "ActivityWait on non-Comm (FIXME)"; // FIXME + return res; + } if (times_considered == -1) { res += "WaitTimeout(comm=" + (XBT_LOG_ISENABLED(mc_observer, xbt_log_priority_verbose) diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp index c4cbd9a0c1..fb1bb57d1e 100644 --- a/src/mc/ModelChecker.cpp +++ b/src/mc/ModelChecker.cpp @@ -308,17 +308,29 @@ void ModelChecker::wait_for_requests() checker_side_.dispatch(); } -void ModelChecker::handle_simcall(Transition const& transition) +RemotePtr ModelChecker::handle_simcall(Transition const& transition) { - s_mc_message_simcall_handle_t m; + s_mc_message_simcall_execute_t m; memset(&m, 0, sizeof(m)); - m.type = MessageType::SIMCALL_HANDLE; + m.type = MessageType::SIMCALL_EXECUTE; m.aid_ = transition.aid_; m.times_considered_ = transition.times_considered_; checker_side_.get_channel().send(m); + + 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) && answer.type == MessageType::SIMCALL_EXECUTE_ANSWER, + "Received unexpected message %s (%i, size=%i) " + "expected MessageType::SIMCALL_EXECUTE_ANSWER (%i, size=%i)", + to_c_str(answer.type), (int)answer.type, (int)s, (int)MessageType::SIMCALL_EXECUTE_ANSWER, + (int)sizeof(answer)); + this->remote_process_->clear_cache(); if (this->remote_process_->running()) - checker_side_.dispatch(); + checker_side_.dispatch(); // The app may send messages while processing the transition + + return remote(answer.observer); } bool ModelChecker::simcall_is_visible(aid_t aid) { @@ -345,6 +357,30 @@ bool ModelChecker::simcall_is_visible(aid_t aid) return answer.value; } +bool ModelChecker::requests_are_dependent(RemotePtr obs1, + RemotePtr obs2) const +{ + xbt_assert(mc_model_checker != nullptr, "This should be called from the checker side"); + + s_mc_message_simcalls_dependent_t m; + memset(&m, 0, sizeof(m)); + m.type = MessageType::SIMCALLS_DEPENDENT; + m.obs1 = obs1.local(); + m.obs2 = obs2.local(); + checker_side_.get_channel().send(m); + + s_mc_message_simcalls_dependent_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) && answer.type == MessageType::SIMCALLS_DEPENDENT_ANSWER, + "Received unexpected message %s (%i, size=%i) " + "expected MessageType::SIMCALLS_DEPENDENT_ANSWER (%i, size=%i)", + to_c_str(answer.type), (int)answer.type, (int)s, (int)MessageType::SIMCALLS_DEPENDENT_ANSWER, + (int)sizeof(answer)); + + return answer.value; +} + std::string ModelChecker::simcall_to_string(MessageType type, aid_t aid, int times_considered) { xbt_assert(mc_model_checker != nullptr, "This should be called from the checker side"); diff --git a/src/mc/ModelChecker.hpp b/src/mc/ModelChecker.hpp index ba10b86960..486145a670 100644 --- a/src/mc/ModelChecker.hpp +++ b/src/mc/ModelChecker.hpp @@ -7,6 +7,7 @@ #define SIMGRID_MC_MODEL_CHECKER_HPP #include "src/mc/remote/CheckerSide.hpp" +#include "src/mc/remote/RemotePtr.hpp" #include "src/mc/sosp/PageStore.hpp" #include "xbt/base.h" #include "xbt/string.hpp" @@ -49,10 +50,12 @@ public: void shutdown(); void resume(); void wait_for_requests(); - void handle_simcall(Transition const& transition); + RemotePtr handle_simcall(Transition const& transition); /* Interactions with the simcall observer */ bool simcall_is_visible(aid_t aid); + bool requests_are_dependent(RemotePtr obs1, + RemotePtr obs2) const; std::string simcall_to_string(aid_t aid, int times_considered); std::string simcall_dot_label(aid_t aid, int times_considered); diff --git a/src/mc/Session.cpp b/src/mc/Session.cpp index b3470c12a6..37a048762b 100644 --- a/src/mc/Session.cpp +++ b/src/mc/Session.cpp @@ -107,10 +107,11 @@ void Session::take_initial_snapshot() initial_snapshot_ = std::make_shared(0); } -void Session::execute(Transition const& transition) const +simgrid::mc::RemotePtr Session::execute(Transition const& transition) const { - model_checker_->handle_simcall(transition); + simgrid::mc::RemotePtr res = model_checker_->handle_simcall(transition); model_checker_->wait_for_requests(); + return res; } void Session::restore_initial_state() const diff --git a/src/mc/Session.hpp b/src/mc/Session.hpp index a639246591..c962d1f403 100644 --- a/src/mc/Session.hpp +++ b/src/mc/Session.hpp @@ -8,6 +8,7 @@ #include "simgrid/forward.h" #include "src/mc/ModelChecker.hpp" +#include "src/mc/remote/RemotePtr.hpp" #include @@ -45,7 +46,7 @@ public: void close(); void take_initial_snapshot(); - void execute(Transition const& transition) const; + simgrid::mc::RemotePtr execute(Transition const& transition) const; void log_state() const; void restore_initial_state() const; diff --git a/src/mc/api.cpp b/src/mc/api.cpp index 219547cee5..f3e5b16171 100644 --- a/src/mc/api.cpp +++ b/src/mc/api.cpp @@ -125,16 +125,12 @@ simgrid::mc::ActorInformation* Api::actor_info_cast(smx_actor_t actor) const return process_info; } -bool Api::simcall_check_dependency(smx_simcall_t req1, smx_simcall_t req2) const -{ - // FIXME: this should be removed now - /* Make sure that req1 and req2 are in alphabetic order */ - if (req1->call_ > req2->call_) { - auto temp = req1; - req1 = req2; - req2 = temp; - } - return true; +bool Api::requests_are_dependent(RemotePtr obs1, + RemotePtr obs2) const +{ + xbt_assert(mc_model_checker != nullptr, "Must be called from MCer"); + + return mc_model_checker->requests_are_dependent(obs1, obs2); } xbt::string const& Api::get_actor_host_name(smx_actor_t actor) const @@ -563,11 +559,11 @@ void Api::s_close() const session_singleton->close(); } -void Api::execute(Transition& transition, smx_simcall_t simcall) const +RemotePtr Api::execute(Transition& transition, smx_simcall_t simcall) const { /* FIXME: once all simcalls have observers, kill the simcall parameter and use mc_model_checker->simcall_to_string() */ transition.textual = request_to_string(simcall, transition.times_considered_); - session_singleton->execute(transition); + return session_singleton->execute(transition); } void Api::automaton_load(const char* file) const diff --git a/src/mc/api.hpp b/src/mc/api.hpp index 6989844e9d..500967aa93 100644 --- a/src/mc/api.hpp +++ b/src/mc/api.hpp @@ -111,12 +111,13 @@ public: std::list get_enabled_transitions(simgrid::mc::State* state) const; // SIMCALL APIs + bool requests_are_dependent(RemotePtr obs1, + RemotePtr obs2) const; std::string request_to_string(smx_simcall_t req, int value) const; std::string request_get_dot_output(smx_simcall_t req, int value) const; smx_actor_t simcall_get_issuer(s_smx_simcall const* req) const; RemotePtr get_mbox_remote_addr(smx_simcall_t const req) const; RemotePtr get_comm_remote_addr(smx_simcall_t const req) const; - bool simcall_check_dependency(smx_simcall_t const req1, smx_simcall_t const req2) const; #if HAVE_SMPI int get_smpi_request_tag(smx_simcall_t const& simcall, simgrid::simix::Simcall type) const; @@ -132,7 +133,7 @@ public: // SESSION APIs void s_close() const; - void execute(Transition& transition, smx_simcall_t simcall) const; + RemotePtr execute(Transition& transition, smx_simcall_t simcall) const; // AUTOMATION APIs #if SIMGRID_HAVE_MC diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp index a4610dc70d..edabda4cbb 100644 --- a/src/mc/checker/SafetyChecker.cpp +++ b/src/mc/checker/SafetyChecker.cpp @@ -90,7 +90,8 @@ void SafetyChecker::run() // Backtrack if we reached the maximum depth if (stack_.size() > (std::size_t)_sg_mc_max_depth) { if (reductionMode_ == ReductionMode::dpor) { - XBT_ERROR("/!\\ Max depth reached! THIS WILL PROBABLY BREAK the dpor reduction /!\\"); + XBT_ERROR("/!\\ Max depth of %d reached! THIS WILL PROBABLY BREAK the dpor reduction /!\\", + _sg_mc_max_depth.get()); XBT_ERROR("/!\\ If bad things happen, disable dpor with --cfg=model-check/reduction:none /!\\"); } else XBT_WARN("/!\\ Max depth reached ! /!\\ "); @@ -114,7 +115,7 @@ void SafetyChecker::run() // req is now the transition of the process that was selected to be executed if (req == nullptr) { - XBT_DEBUG("There remains %zu actors, but no more processes to interleave. (depth %zu)", + XBT_DEBUG("There remains %zu actors, but none to interleave (depth %zu).", mc_model_checker->get_remote_process().actors().size(), stack_.size() + 1); if (mc_model_checker->get_remote_process().actors().empty()) @@ -134,11 +135,13 @@ void SafetyChecker::run() api::get().mc_inc_executed_trans(); /* Actually answer the request: let execute the selected request (MCed does one step) */ - api::get().execute(state->transition_, &state->executed_req_); + RemotePtr remote_observer = + api::get().execute(state->transition_, &state->executed_req_); /* Create the new expanded state (copy the state of MCed into our MCer data) */ ++expanded_states_count_; auto next_state = std::make_unique(expanded_states_count_); + next_state->remote_observer_ = remote_observer; if (_sg_mc_termination) this->check_non_termination(next_state.get()); @@ -197,7 +200,7 @@ void SafetyChecker::backtrack() XBT_DEBUG("Simcall %s and %s with same issuer", SIMIX_simcall_name(state->executed_req_), SIMIX_simcall_name(prev_state->executed_req_)); break; - } else if (api::get().simcall_check_dependency(&state->internal_req_, &prev_state->internal_req_)) { + } else if (api::get().requests_are_dependent(state->remote_observer_, state->remote_observer_)) { if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) { XBT_DEBUG("Dependent Transitions:"); int value = prev_state->transition_.times_considered_; diff --git a/src/mc/mc_state.hpp b/src/mc/mc_state.hpp index 612fc4ccd5..6892324f1d 100644 --- a/src/mc/mc_state.hpp +++ b/src/mc/mc_state.hpp @@ -27,6 +27,9 @@ public: /** The simcall which was executed, going out of that state */ s_smx_simcall executed_req_; + /** Observer of the transition leading to that sate */ + RemotePtr remote_observer_; + /* Internal translation of the executed_req simcall * * Simcall::COMM_TESTANY is translated to a Simcall::COMM_TEST diff --git a/src/mc/remote/AppSide.cpp b/src/mc/remote/AppSide.cpp index 5ad3e5422e..4e1221dfca 100644 --- a/src/mc/remote/AppSide.cpp +++ b/src/mc/remote/AppSide.cpp @@ -93,13 +93,24 @@ void AppSide::handle_deadlock_check(const s_mc_message_t*) const s_mc_message_int_t answer{MessageType::DEADLOCK_CHECK_REPLY, deadlock}; xbt_assert(channel_.send(answer) == 0, "Could not send response"); } -void AppSide::handle_simcall_execute(const s_mc_message_simcall_handle_t* message) const +void AppSide::handle_simcall_execute(const s_mc_message_simcall_execute_t* message) const { kernel::actor::ActorImpl* actor = kernel::actor::ActorImpl::by_pid(message->aid_); xbt_assert(actor != nullptr, "Invalid pid %ld", message->aid_); - if (actor->simcall_.observer_ != nullptr) - actor->observer_stack_.push_back(actor->simcall_.observer_->clone()); + simgrid::kernel::actor::SimcallObserver* observer = nullptr; + if (actor->simcall_.observer_ != nullptr) { + observer = actor->simcall_.observer_->clone(); + actor->observer_stack_.push_back(observer); + } + // Finish the RPC from the server: we need to return a pointer to the observer, saved in a stable storage + s_mc_message_simcall_execute_answer_t answer{MessageType::SIMCALL_EXECUTE_ANSWER, observer}; + XBT_DEBUG("send SIMCALL_EXECUTE_ANSWER(%p)", observer); + xbt_assert(channel_.send(answer) == 0, "Could not send response"); + + // The client may send some messages to the server while processing the transition actor->simcall_handle(message->times_considered_); + + // Say the server that the transition is over and that it should proceed xbt_assert(channel_.send(MessageType::WAITING) == 0, "Could not send MESSAGE_WAITING to model-checker"); } @@ -136,9 +147,9 @@ void AppSide::handle_messages() const assert_msg_size("MESSAGE_CONTINUE", s_mc_message_t); return; - case MessageType::SIMCALL_HANDLE: - assert_msg_size("SIMCALL_HANDLE", s_mc_message_simcall_handle_t); - handle_simcall_execute((s_mc_message_simcall_handle_t*)message_buffer.data()); + case MessageType::SIMCALL_EXECUTE: + assert_msg_size("SIMCALL_EXECUTE", s_mc_message_simcall_execute_t); + handle_simcall_execute((s_mc_message_simcall_execute_t*)message_buffer.data()); break; case MessageType::SIMCALL_IS_VISIBLE: { @@ -170,6 +181,26 @@ void AppSide::handle_messages() const break; } + case MessageType::SIMCALLS_DEPENDENT: { + assert_msg_size("SIMCALLS_DEPENDENT", s_mc_message_simcalls_dependent_t); + auto msg_simcalls = (s_mc_message_simcalls_dependent_t*)message_buffer.data(); + auto* obs1 = msg_simcalls->obs1; + auto* obs2 = msg_simcalls->obs2; + bool res = true; + + if (obs1 != nullptr && obs2 != nullptr) + res = obs1->depends(obs2); + + XBT_DEBUG("return SIMCALLS_DEPENDENT(%s, %s) = %s", obs1->to_string(0).c_str(), obs2->to_string(0).c_str(), + (res ? "true" : "false")); + + // Send result: + s_mc_message_simcalls_dependent_answer_t answer{MessageType::SIMCALLS_DEPENDENT_ANSWER, {0}}; + answer.value = res; + xbt_assert(channel_.send(answer) == 0, "Could not send response"); + break; + } + case MessageType::SIMCALL_DOT_LABEL: { assert_msg_size("SIMCALL_DOT_LABEL", s_mc_message_simcall_to_string_t); auto msg_simcall = (s_mc_message_simcall_to_string_t*)message_buffer.data(); diff --git a/src/mc/remote/AppSide.hpp b/src/mc/remote/AppSide.hpp index 544219cb90..641ceae1bf 100644 --- a/src/mc/remote/AppSide.hpp +++ b/src/mc/remote/AppSide.hpp @@ -31,7 +31,7 @@ public: private: void handle_deadlock_check(const s_mc_message_t* msg) const; - void handle_simcall_execute(const s_mc_message_simcall_handle_t* message) const; + void handle_simcall_execute(const s_mc_message_simcall_execute_t* message) const; void handle_actor_enabled(const s_mc_message_actor_enabled_t* msg) const; public: diff --git a/src/mc/remote/RemoteProcess.cpp b/src/mc/remote/RemoteProcess.cpp index 538939b365..fcde1d3f42 100644 --- a/src/mc/remote/RemoteProcess.cpp +++ b/src/mc/remote/RemoteProcess.cpp @@ -556,7 +556,7 @@ void RemoteProcess::dump_stack() const if (unw_init_remote(&cursor, as, context) != 0) { _UPT_destroy(context); unw_destroy_addr_space(as); - XBT_ERROR("Could not initialiez ptrace cursor"); + XBT_ERROR("Could not initialize ptrace cursor"); return; } diff --git a/src/mc/remote/mc_protocol.h b/src/mc/remote/mc_protocol.h index de67c9dbe5..112cddf107 100644 --- a/src/mc/remote/mc_protocol.h +++ b/src/mc/remote/mc_protocol.h @@ -29,9 +29,10 @@ namespace simgrid { namespace mc { XBT_DECLARE_ENUM_CLASS(MessageType, NONE, INITIAL_ADDRESSES, CONTINUE, IGNORE_HEAP, UNIGNORE_HEAP, IGNORE_MEMORY, - STACK_REGION, REGISTER_SYMBOL, DEADLOCK_CHECK, DEADLOCK_CHECK_REPLY, WAITING, SIMCALL_HANDLE, - SIMCALL_IS_VISIBLE, SIMCALL_IS_VISIBLE_ANSWER, SIMCALL_TO_STRING, SIMCALL_TO_STRING_ANSWER, - SIMCALL_DOT_LABEL, ASSERTION_FAILED, ACTOR_ENABLED, ACTOR_ENABLED_REPLY, FINALIZE); + STACK_REGION, REGISTER_SYMBOL, DEADLOCK_CHECK, DEADLOCK_CHECK_REPLY, WAITING, SIMCALL_EXECUTE, + SIMCALL_EXECUTE_ANSWER, SIMCALL_IS_VISIBLE, SIMCALL_IS_VISIBLE_ANSWER, SIMCALL_TO_STRING, + SIMCALL_TO_STRING_ANSWER, SIMCALLS_DEPENDENT, SIMCALLS_DEPENDENT_ANSWER, SIMCALL_DOT_LABEL, + ASSERTION_FAILED, ACTOR_ENABLED, ACTOR_ENABLED_REPLY, FINALIZE); } // namespace mc } // namespace simgrid @@ -94,11 +95,15 @@ struct s_mc_message_register_symbol_t { }; /* Server -> client */ -struct s_mc_message_simcall_handle_t { +struct s_mc_message_simcall_execute_t { simgrid::mc::MessageType type; aid_t aid_; int times_considered_; }; +struct s_mc_message_simcall_execute_answer_t { + simgrid::mc::MessageType type; + simgrid::kernel::actor::SimcallObserver* observer; +}; struct s_mc_message_restore_t { simgrid::mc::MessageType type; @@ -130,5 +135,15 @@ struct s_mc_message_simcall_to_string_answer_t { // MessageType::SIMCALL_TO_STRI char value[1024]; }; +struct s_mc_message_simcalls_dependent_t { // MessageType::SIMCALLS_DEPENDENT + simgrid::mc::MessageType type; + simgrid::kernel::actor::SimcallObserver* obs1; + simgrid::kernel::actor::SimcallObserver* obs2; +}; +struct s_mc_message_simcalls_dependent_answer_t { // MessageType::SIMCALLS_DEPENDENT_ANSWER + simgrid::mc::MessageType type; + bool value; +}; + #endif // __cplusplus #endif