From: Martin Quinson Date: Sat, 30 Jul 2022 21:56:43 +0000 (+0200) Subject: Finally kill mc::RemoteProcess::actors(). We now communicate the data over the wire... X-Git-Tag: v3.32~113 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/bb1c2f879c11304682a40b3eaea20bbfe911cddf Finally kill mc::RemoteProcess::actors(). We now communicate the data over the wire instead of reading it directly --- diff --git a/src/mc/Session.cpp b/src/mc/Session.cpp index f5d8944889..3f19003dca 100644 --- a/src/mc/Session.cpp +++ b/src/mc/Session.cpp @@ -134,17 +134,29 @@ void Session::close() } } -bool Session::actor_is_enabled(aid_t pid) const +void Session::get_actors_status(std::map& whereto) { - s_mc_message_actor_enabled_t msg; + s_mc_message_t msg; memset(&msg, 0, sizeof msg); - msg.type = simgrid::mc::MessageType::ACTOR_ENABLED; - msg.aid = pid; + msg.type = simgrid::mc::MessageType::ACTORS_STATUS; model_checker_->channel().send(msg); - std::array buff; - ssize_t received = model_checker_->channel().receive(buff.data(), buff.size(), true); - xbt_assert(received == sizeof(s_mc_message_int_t), "Unexpected size in answer to ACTOR_ENABLED"); - return ((s_mc_message_int_t*)buff.data())->value; + + s_mc_message_actors_status_answer_t answer; + ssize_t received = model_checker_->channel().receive(answer); + xbt_assert(received != -1, "Could not receive message"); + xbt_assert(received == sizeof(answer) && answer.type == MessageType::ACTORS_STATUS_REPLY, + "Received unexpected message %s (%i, size=%i) " + "expected MessageType::ACTORS_STATUS_REPLY (%i, size=%i)", + to_c_str(answer.type), (int)answer.type, (int)received, (int)MessageType::ACTORS_STATUS_REPLY, + (int)sizeof(answer)); + + s_mc_message_actors_status_one_t status[answer.count]; + received = model_checker_->channel().receive(&status, sizeof(status)); + xbt_assert(static_cast(received) == sizeof(status)); + + whereto.clear(); + for (auto const& actor : status) + whereto.insert(std::make_pair(actor.aid, ActorState(actor.aid, actor.enabled, actor.max_considered))); } void Session::check_deadlock() const diff --git a/src/mc/Session.hpp b/src/mc/Session.hpp index b84e6fec73..c895a34258 100644 --- a/src/mc/Session.hpp +++ b/src/mc/Session.hpp @@ -6,6 +6,7 @@ #ifndef SIMGRID_MC_SESSION_HPP #define SIMGRID_MC_SESSION_HPP +#include "mc_pattern.hpp" #include "simgrid/forward.h" #include "src/mc/ModelChecker.hpp" #include "src/mc/remote/RemotePtr.hpp" @@ -52,7 +53,7 @@ public: void log_state() const; - bool actor_is_enabled(aid_t pid) const; + void get_actors_status(std::map& whereto); }; } // namespace simgrid::mc diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp index 79213e7cb3..1ba81a2754 100644 --- a/src/mc/api/State.cpp +++ b/src/mc/api/State.cpp @@ -17,15 +17,7 @@ long State::expended_states_ = 0; State::State(Session& session) : num_(++expended_states_) { - auto actors = mc_model_checker->get_remote_process().actors(); - - for (unsigned int i = 0; i < actors.size(); i++) { - auto remote_actor = actors[i].copy.get_buffer(); - aid_t aid = remote_actor->get_pid(); - - actors_to_run_.insert( - std::make_pair(aid, ActorState(aid, session.actor_is_enabled(aid), remote_actor->simcall_.mc_max_consider_))); - } + session.get_actors_status(actors_to_run_); transition_.reset(new Transition()); /* Stateful model checking */ diff --git a/src/mc/remote/AppSide.cpp b/src/mc/remote/AppSide.cpp index 929c97cd5d..8ed73b4d9a 100644 --- a/src/mc/remote/AppSide.cpp +++ b/src/mc/remote/AppSide.cpp @@ -122,13 +122,6 @@ void AppSide::handle_simcall_execute(const s_mc_message_simcall_execute_t* messa xbt_assert(channel_.send(answer) == 0, "Could not send response"); } -void AppSide::handle_actor_enabled(const s_mc_message_actor_enabled_t* msg) const -{ - bool res = mc::actor_is_enabled(kernel::EngineImpl::get_instance()->get_actor_by_pid(msg->aid)); - s_mc_message_int_t answer{MessageType::ACTOR_ENABLED_REPLY, res}; - xbt_assert(channel_.send(answer) == 0, "Could not send ACTOR_ENABLED_REPLY"); -} - void AppSide::handle_finalize(const s_mc_message_int_t* msg) const { bool terminate_asap = msg->value; @@ -143,12 +136,32 @@ void AppSide::handle_finalize(const s_mc_message_int_t* msg) const #endif } coverage_checkpoint(); - xbt_assert(channel_.send(MessageType::DEADLOCK_CHECK_REPLY) == 0, // DEADLOCK_CHECK_REPLY, really? + xbt_assert(channel_.send(MessageType::DEADLOCK_CHECK_REPLY) == + 0, // DEADLOCK_CHECK_REPLY because I'm too lazy to create another message type with no content (FIXME) "Could not answer to FINALIZE"); std::fflush(stdout); if (terminate_asap) ::_Exit(0); } +void AppSide::handle_actors_status() const +{ + auto const& actor_list = kernel::EngineImpl::get_instance()->get_actor_list(); + int count = actor_list.size(); + + struct s_mc_message_actors_status_answer_t answer { + MessageType::ACTORS_STATUS_REPLY, count + }; + s_mc_message_actors_status_one_t status[count]; + int i = 0; + for (auto const& [aid, actor] : actor_list) { + status[i].aid = aid; + status[i].enabled = mc::actor_is_enabled(actor); + status[i].max_considered = actor->simcall_.observer_->get_max_consider(); + i++; + } + xbt_assert(channel_.send(answer) == 0, "Could not send ACTORS_STATUS_REPLY msg"); + xbt_assert(channel_.send(status, sizeof(status)) == 0, "Could not send ACTORS_STATUS_REPLY data"); +} #define assert_msg_size(_name_, _type_) \ xbt_assert(received_size == sizeof(_type_), "Unexpected size for " _name_ " (%zd != %zu)", received_size, \ @@ -180,16 +193,16 @@ void AppSide::handle_messages() const handle_simcall_execute((s_mc_message_simcall_execute_t*)message_buffer.data()); break; - case MessageType::ACTOR_ENABLED: - assert_msg_size("ACTOR_ENABLED", s_mc_message_actor_enabled_t); - handle_actor_enabled((s_mc_message_actor_enabled_t*)message_buffer.data()); - break; - case MessageType::FINALIZE: assert_msg_size("FINALIZE", s_mc_message_int_t); handle_finalize((s_mc_message_int_t*)message_buffer.data()); break; + case MessageType::ACTORS_STATUS: + assert_msg_size("ACTORS_STATUS", s_mc_message_t); + handle_actors_status(); + break; + default: xbt_die("Received unexpected message %s (%i)", to_c_str(message->type), static_cast(message->type)); break; diff --git a/src/mc/remote/AppSide.hpp b/src/mc/remote/AppSide.hpp index 393f1ea4d4..6fe23a33ec 100644 --- a/src/mc/remote/AppSide.hpp +++ b/src/mc/remote/AppSide.hpp @@ -31,8 +31,8 @@ public: private: void handle_deadlock_check(const s_mc_message_t* msg) 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; void handle_finalize(const s_mc_message_int_t* msg) const; + void handle_actors_status() const; public: Channel const& get_channel() const { return channel_; } diff --git a/src/mc/remote/RemoteProcess.cpp b/src/mc/remote/RemoteProcess.cpp index 4411375eef..afda96232e 100644 --- a/src/mc/remote/RemoteProcess.cpp +++ b/src/mc/remote/RemoteProcess.cpp @@ -410,40 +410,6 @@ void RemoteProcess::ignore_local_variable(const char* var_name, const char* fram info->remove_local_variable(var_name, frame_name); } -/** Load the remote list of actors into the Checker process - * - * FIXME: This shall die alltogether and be reimplemented with a networked communication to not suppose anything about - * the memory layout of the checked App if avoidable. - * - * Liveness checking will always require to explore the memory of the App, but safety checking doesn't. - */ - -std::vector& RemoteProcess::actors() -{ - if (not(this->cache_flags_ & RemoteProcess::cache_simix_processes)) { - smx_actors_infos.clear(); - - s_xbt_dynar_t dynar; - read_bytes(&dynar, sizeof(dynar), actors_addr_); - - auto* data = static_cast(::operator new(dynar.elmsize* dynar.used)); - read_bytes(data, dynar.elmsize * dynar.used, simgrid::mc::RemotePtr(dynar.data)); - - // Load each element of the vector from the MCed process: - for (unsigned int i = 0; i < dynar.used; ++i) { - simgrid::mc::ActorInformation info; - - info.address = simgrid::mc::RemotePtr(data[i]); - read_bytes(&info.copy, sizeof(info.copy), simgrid::mc::remote(data[i])); - smx_actors_infos.push_back(std::move(info)); - } - ::operator delete(data); - - this->cache_flags_ |= RemoteProcess::cache_simix_processes; - } - return smx_actors_infos; -} - void RemoteProcess::dump_stack() const { unw_addr_space_t as = unw_create_addr_space(&_UPT_accessors, BYTE_ORDER); diff --git a/src/mc/remote/RemoteProcess.hpp b/src/mc/remote/RemoteProcess.hpp index 02c4fba62b..64b2ff7b3a 100644 --- a/src/mc/remote/RemoteProcess.hpp +++ b/src/mc/remote/RemoteProcess.hpp @@ -71,7 +71,6 @@ private: static constexpr int cache_none = 0; static constexpr int cache_heap = 1; static constexpr int cache_malloc = 2; - static constexpr int cache_simix_processes = 4; public: explicit RemoteProcess(pid_t pid); @@ -171,8 +170,6 @@ private: RemotePtr actors_addr_; public: - std::vector& actors(); - unsigned long get_maxpid() const { return this->read(maxpid_addr_); } void dump_stack() const; diff --git a/src/mc/remote/mc_protocol.h b/src/mc/remote/mc_protocol.h index c04acc1c03..6a8b5adeeb 100644 --- a/src/mc/remote/mc_protocol.h +++ b/src/mc/remote/mc_protocol.h @@ -25,8 +25,7 @@ namespace simgrid::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_EXECUTE, - SIMCALL_EXECUTE_ANSWER, ASSERTION_FAILED, ACTOR_ENABLED, ACTOR_ENABLED_REPLY, FINALIZE); - + SIMCALL_EXECUTE_ANSWER, ASSERTION_FAILED, ACTORS_STATUS, ACTORS_STATUS_REPLY, FINALIZE); } // namespace simgrid::mc constexpr unsigned MC_MESSAGE_LENGTH = 512; @@ -102,9 +101,15 @@ struct s_mc_message_restore_t { int index; }; -struct s_mc_message_actor_enabled_t { +struct s_mc_message_actors_status_answer_t { simgrid::mc::MessageType type; - aid_t aid; // actor ID + int count; +}; +struct s_mc_message_actors_status_one_t { // an array of `s_mc_message_actors_status_one_t[count]` is sent right after + // after a s_mc_message_actors_status_answer_t + aid_t aid; + bool enabled; + int max_considered; }; #endif // __cplusplus