From: Martin Quinson Date: Fri, 11 Feb 2022 00:48:24 +0000 (+0100) Subject: Big bang in MC: app's observers are serialized, to become transitions in checker X-Git-Tag: v3.31~455 X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/1d1294418fcdb34a66a0569033b173274db14fe8 Big bang in MC: app's observers are serialized, to become transitions in checker Instead of interacting with the observers over the network, we now transfer over the wire (a simplified copy of) the observer to the checker. This was necessary because the lifetime of the Observer (or of its components) was sometimes too short: it happened that the Actor refered to by the Observer was not existing anymore at the end of the simulation when the depend relation was evaluated. Or something like that, I'm not sure. Another argument for this change was that UDPOR reduction sometimes need to evaluate the dependency between transitions that are not in the same history (in the same run of the application), so we really need to carry the transition over to let them live in the checker. Note that we are not copying every information of the observer over, only the ones that are relevant to the model-checker. Finally, this change is still ongoing: - not all observers are serialized over the wire yet - the depends() are not implemented in the Transition yet - the network protocol is utterly inefficient, and we probably need to move to FlatBuffer or something like that. - a lot of dead code remains Sorry for the mess, it's progressing rather slowly... --- diff --git a/src/kernel/activity/MailboxImpl.cpp b/src/kernel/activity/MailboxImpl.cpp index 4c672cbfaf..febedbe200 100644 --- a/src/kernel/activity/MailboxImpl.cpp +++ b/src/kernel/activity/MailboxImpl.cpp @@ -18,6 +18,8 @@ namespace simgrid { namespace kernel { namespace activity { +unsigned MailboxImpl::next_id_ = 0; + /** @brief set the receiver of the mailbox to allow eager sends * @param actor The receiving dude */ diff --git a/src/kernel/activity/MailboxImpl.hpp b/src/kernel/activity/MailboxImpl.hpp index 594e4b07dc..e82979ed5e 100644 --- a/src/kernel/activity/MailboxImpl.hpp +++ b/src/kernel/activity/MailboxImpl.hpp @@ -36,10 +36,14 @@ class MailboxImpl { friend s4u::Mailbox* s4u::Mailbox::by_name(const std::string& name); friend mc::CommunicationDeterminismChecker; - explicit MailboxImpl(const std::string& name) : piface_(this), name_(name) {} + static unsigned next_id_; // Next ID to be given + unsigned id_; + explicit MailboxImpl(const std::string& name) : piface_(this), name_(name), id_(next_id_++) {} public: /** @brief Public interface */ + unsigned get_id() { return id_; } + const s4u::Mailbox* get_iface() const { return &piface_; } s4u::Mailbox* get_iface() { return &piface_; } diff --git a/src/kernel/actor/SimcallObserver.cpp b/src/kernel/actor/SimcallObserver.cpp index a2df655c76..f2818db656 100644 --- a/src/kernel/actor/SimcallObserver.cpp +++ b/src/kernel/actor/SimcallObserver.cpp @@ -6,10 +6,13 @@ #include "src/kernel/actor/SimcallObserver.hpp" #include "simgrid/s4u/Host.hpp" #include "src/kernel/activity/CommImpl.hpp" +#include "src/kernel/activity/MailboxImpl.hpp" #include "src/kernel/activity/MutexImpl.hpp" #include "src/kernel/actor/ActorImpl.hpp" #include "src/mc/mc_config.hpp" +#include + XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_observer, mc, "Logging specific to MC simcall observation"); namespace simgrid { @@ -48,11 +51,12 @@ bool MutexSimcall::depends(SimcallObserver* other) return true; // Depend on things we don't know for sure that they are independent } -std::string SimcallObserver::to_string(int /*times_considered*/) const +/* +std::string SimcallObserver::to_string(int) const { return simgrid::xbt::string_printf("[(%ld)%s (%s)] ", issuer_->get_pid(), issuer_->get_host()->get_cname(), issuer_->get_cname()); -} +}*/ std::string SimcallObserver::dot_label(int /*times_considered*/) const { @@ -61,11 +65,6 @@ std::string SimcallObserver::dot_label(int /*times_considered*/) const return xbt::string_printf("[(%ld)] ", issuer_->get_pid()); } -std::string RandomSimcall::to_string(int times_considered) const -{ - return SimcallObserver::to_string(times_considered) + "MC_RANDOM(" + std::to_string(times_considered) + ")"; -} - std::string RandomSimcall::dot_label(int times_considered) const { return SimcallObserver::dot_label(times_considered) + "MC_RANDOM(" + std::to_string(next_value_) + ")"; @@ -82,16 +81,12 @@ int RandomSimcall::get_max_consider() const return max_ - min_ + 1; } -std::string MutexUnlockSimcall::to_string(int times_considered) const -{ - return SimcallObserver::to_string(times_considered) + "Mutex UNLOCK"; -} - std::string MutexUnlockSimcall::dot_label(int times_considered) const { return SimcallObserver::dot_label(times_considered) + "Mutex UNLOCK"; } +/* std::string MutexLockSimcall::to_string(int times_considered) const { auto mutex = get_mutex(); @@ -100,7 +95,7 @@ std::string MutexLockSimcall::to_string(int times_considered) const res += ", owner = " + std::to_string(mutex->get_owner() ? mutex->get_owner()->get_pid() : -1); res += ", sleeping = n/a)"; return res; -} +}*/ std::string MutexLockSimcall::dot_label(int times_considered) const { @@ -112,13 +107,6 @@ bool MutexLockSimcall::is_enabled() const return not blocking_ || get_mutex()->get_owner() == nullptr || get_mutex()->get_owner() == get_issuer(); } -std::string ConditionWaitSimcall::to_string(int times_considered) const -{ - std::string res = SimcallObserver::to_string(times_considered) + "Condition WAIT"; - res += "(" + (timeout_ == -1.0 ? "" : std::to_string(timeout_)) + ")"; - return res; -} - std::string ConditionWaitSimcall::dot_label(int times_considered) const { return SimcallObserver::dot_label(times_considered) + "Condition WAIT"; @@ -134,13 +122,6 @@ bool ConditionWaitSimcall::is_enabled() const return true; } -std::string SemAcquireSimcall::to_string(int times_considered) const -{ - std::string res = SimcallObserver::to_string(times_considered) + "Sem ACQUIRE"; - res += "(" + (timeout_ == -1.0 ? "" : std::to_string(timeout_)) + ")"; - return res; -} - std::string SemAcquireSimcall::dot_label(int times_considered) const { return SimcallObserver::dot_label(times_considered) + "Sem ACQUIRE"; @@ -172,6 +153,7 @@ void ActivityTestanySimcall::prepare(int times_considered) next_value_ = times_considered; } +/* std::string ActivityTestanySimcall::to_string(int times_considered) const { std::string res = SimcallObserver::to_string(times_considered); @@ -182,7 +164,7 @@ std::string ActivityTestanySimcall::to_string(int times_considered) const } return res; -} +}*/ std::string ActivityTestanySimcall::dot_label(int times_considered) const { @@ -236,7 +218,24 @@ bool ActivityTestSimcall::depends(SimcallObserver* other) return true; } +void ActivityWaitSimcall::serialize(Simcall& type, char* buffer) +{ + std::stringstream stream; + if (auto* comm = dynamic_cast(activity_)) { + type = Simcall::COMM_WAIT; + stream << timeout_ << ' ' << comm; + stream << ' ' << (comm->src_actor_ != nullptr ? comm->src_actor_->get_pid() : -1); + stream << ' ' << (comm->dst_actor_ != nullptr ? comm->dst_actor_->get_pid() : -1); + stream << ' ' << (comm->get_mailbox() != nullptr ? comm->get_mailbox()->get_id() : 666); + stream << ' ' << (void*)comm->src_buff_ << ' ' << (void*)comm->dst_buff_ << ' ' << comm->src_buff_size_; + strcpy(buffer, stream.str().c_str()); + } else { + type = Simcall::UNKNOWN; + strcpy(buffer, stream.str().c_str()); + } +} +/* std::string ActivityTestSimcall::to_string(int times_considered) const { std::string res = SimcallObserver::to_string(times_considered) + "Test "; @@ -259,7 +258,7 @@ std::string ActivityTestSimcall::to_string(int times_considered) const } else xbt_die("Only Comms are supported here for now"); return res; -} +}*/ std::string ActivityTestSimcall::dot_label(int times_considered) const { @@ -324,32 +323,6 @@ bool ActivityWaitSimcall::depends(SimcallObserver* other) return true; } -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) { - 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) - ? xbt::string_printf("%p)", comm) - : "(verbose only))"); - } else { - res += "Wait(comm="; - - auto src = comm->src_actor_; - auto dst = comm->dst_actor_; - res += - XBT_LOG_ISENABLED(mc_observer, xbt_log_priority_verbose) ? xbt::string_printf("%p", comm) : "(verbose only) "; - res += xbt::string_printf("[(%ld)%s (%s) ", src->get_pid(), src->get_host()->get_cname(), src->get_cname()) + - "-> " + xbt::string_printf("(%ld)%s (%s)])", dst->get_pid(), dst->get_host()->get_cname(), dst->get_cname()); - } - return res; -} - std::string ActivityWaitSimcall::dot_label(int times_considered) const { std::string res = SimcallObserver::dot_label(times_considered); @@ -401,23 +374,6 @@ void ActivityWaitanySimcall::prepare(int times_considered) next_value_ = times_considered; } -std::string ActivityWaitanySimcall::to_string(int times_considered) const -{ - std::string res = SimcallObserver::to_string(times_considered) + "WaitAny("; - size_t count = activities_.size(); - if (count > 0) { - if (auto* comm = dynamic_cast(activities_[times_considered])) - res += "comm=" + - (XBT_LOG_ISENABLED(mc_observer, xbt_log_priority_verbose) ? xbt::string_printf("%p", comm) - : "(verbose only)") + - xbt::string_printf("(%d of %zu))", times_considered + 1, count); - else - xbt_die("Only Comms are supported here for now"); - } else - res += "comm at idx " + std::to_string(times_considered) + ")"; - return res; -} - bool CommIsendSimcall::depends(SimcallObserver* other) { if (get_issuer() == other->get_issuer()) @@ -457,18 +413,20 @@ bool CommIsendSimcall::depends(SimcallObserver* other) return true; } +void CommIsendSimcall::serialize(Simcall& type, char* buffer) +{ + type = Simcall::ISEND; + std::stringstream stream; + stream << mbox_->get_id() << ' ' << (void*)src_buff_ << ' ' << src_buff_size_; + strcpy(buffer, stream.str().c_str()); +} -std::string CommIsendSimcall::to_string(int times_considered) const +void CommIrecvSimcall::serialize(Simcall& type, char* buffer) { - std::string res = SimcallObserver::to_string(times_considered) + "iSend("; - res += xbt::string_printf("src=(%ld)%s (%s)", get_issuer()->get_pid(), get_issuer()->get_host()->get_cname(), - get_issuer()->get_cname()); - res += ", buff=" + (XBT_LOG_ISENABLED(mc_observer, xbt_log_priority_verbose) ? xbt::string_printf("%p", src_buff_) - : "(verbose only)"); - res += ", size=" + - (XBT_LOG_ISENABLED(mc_observer, xbt_log_priority_verbose) ? std::to_string(src_buff_size_) : "(verbose only)"); - res += ")"; - return res; + type = Simcall::IRECV; + std::stringstream stream; + stream << mbox_->get_id() << dst_buff_; + strcpy(buffer, stream.str().c_str()); } bool CommIrecvSimcall::depends(SimcallObserver* other) @@ -511,6 +469,7 @@ bool CommIrecvSimcall::depends(SimcallObserver* other) return true; } +/* std::string CommIrecvSimcall::to_string(int times_considered) const { std::string res = SimcallObserver::to_string(times_considered) + "iRecv("; @@ -523,6 +482,7 @@ std::string CommIrecvSimcall::to_string(int times_considered) const res += ")"; return res; } +*/ } // namespace actor } // namespace kernel diff --git a/src/kernel/actor/SimcallObserver.hpp b/src/kernel/actor/SimcallObserver.hpp index ad6e824da3..74763346f1 100644 --- a/src/kernel/actor/SimcallObserver.hpp +++ b/src/kernel/actor/SimcallObserver.hpp @@ -8,6 +8,7 @@ #include "simgrid/forward.h" #include "xbt/asserts.h" +#include "xbt/utility.hpp" #include @@ -19,6 +20,9 @@ class SimcallObserver { ActorImpl* const issuer_; public: + XBT_DECLARE_ENUM_CLASS(Simcall, UNKNOWN, RANDOM, ISEND, IRECV, COMM_WAIT, COMM_TEST); + + SimcallObserver() = default; explicit SimcallObserver(ActorImpl* issuer) : issuer_(issuer) {} ActorImpl* get_issuer() const { return issuer_; } /** Whether this transition can currently be taken without blocking. @@ -56,10 +60,12 @@ public: /** Computes the dependency relation */ virtual bool depends(SimcallObserver* other); + /** Serialize to the given buffer */ + virtual void serialize(Simcall& type, char* buffer) { type = Simcall::UNKNOWN; } + /** Some simcalls may only be observable under some conditions. * Most simcalls are not visible from the MC because they don't have an observer at all. */ virtual bool is_visible() const { return true; } - virtual std::string to_string(int times_considered) const = 0; virtual std::string dot_label(int times_considered) const = 0; }; @@ -67,6 +73,7 @@ template class ResultingSimcall : public SimcallObserver { T result_; public: + ResultingSimcall() = default; ResultingSimcall(ActorImpl* actor, T default_result) : SimcallObserver(actor), result_(default_result) {} void set_result(T res) { result_ = res; } T get_result() const { return result_; } @@ -88,9 +95,9 @@ public: res->next_value_ = next_value_; return res; } + void serialize(Simcall& type, char* buffer) override { type = Simcall::RANDOM; } int get_max_consider() const override; void prepare(int times_considered) override; - std::string to_string(int times_considered) const override; std::string dot_label(int times_considered) const override; int get_value() const { return next_value_; } bool depends(SimcallObserver* other) override; @@ -110,7 +117,6 @@ class MutexUnlockSimcall : public MutexSimcall { public: SimcallObserver* clone() override { return new MutexUnlockSimcall(get_issuer(), get_mutex()); } - std::string to_string(int times_considered) const override; std::string dot_label(int times_considered) const override; }; @@ -124,7 +130,6 @@ public: } SimcallObserver* clone() override { return new MutexLockSimcall(get_issuer(), get_mutex(), blocking_); } bool is_enabled() const override; - std::string to_string(int times_considered) const override; std::string dot_label(int times_considered) const override; }; @@ -142,7 +147,6 @@ public: SimcallObserver* clone() override { return new ConditionWaitSimcall(get_issuer(), cond_, mutex_, timeout_); } bool is_enabled() const override; bool is_visible() const override { return false; } - std::string to_string(int times_considered) const override; std::string dot_label(int times_considered) const override; activity::ConditionVariableImpl* get_cond() const { return cond_; } activity::MutexImpl* get_mutex() const { return mutex_; } @@ -161,7 +165,6 @@ public: SimcallObserver* clone() override { return new SemAcquireSimcall(get_issuer(), sem_, timeout_); } bool is_enabled() const override; bool is_visible() const override { return false; } - std::string to_string(int times_considered) const override; std::string dot_label(int times_considered) const override; activity::SemaphoreImpl* get_sem() const { return sem_; } double get_timeout() const { return timeout_; } @@ -178,7 +181,6 @@ public: SimcallObserver* clone() override { return new ActivityTestSimcall(get_issuer(), activity_); } bool is_visible() const override { return true; } bool depends(SimcallObserver* other) override; - std::string to_string(int times_considered) const override; std::string dot_label(int times_considered) const override; activity::ActivityImpl* get_activity() const { return activity_; } }; @@ -196,7 +198,6 @@ public: bool is_visible() const override { return true; } int get_max_consider() const override; void prepare(int times_considered) override; - std::string to_string(int times_considered) const override; std::string dot_label(int times_considered) const override; const std::vector& get_activities() const { return activities_; } int get_value() const { return next_value_; } @@ -212,10 +213,10 @@ public: { } SimcallObserver* clone() override { return new ActivityWaitSimcall(get_issuer(), activity_, timeout_); } + void serialize(Simcall& type, char* buffer); bool is_visible() const override { return true; } bool is_enabled() const override; bool depends(SimcallObserver* other) override; - std::string to_string(int times_considered) const override; std::string dot_label(int times_considered) const override; activity::ActivityImpl* get_activity() const { return activity_; } void set_activity(activity::ActivityImpl* activity) { activity_ = activity; } @@ -237,7 +238,6 @@ public: bool is_visible() const override { return true; } void prepare(int times_considered) override; int get_max_consider() const override; - std::string to_string(int times_considered) const override; std::string dot_label(int times_considered) const override; const std::vector& get_activities() const { return activities_; } double get_timeout() const { return timeout_; } @@ -276,6 +276,7 @@ public: , copy_data_fun_(copy_data_fun) { } + void serialize(Simcall& type, char* buffer) override; CommIsendSimcall* clone() override { return new CommIsendSimcall(get_issuer(), mbox_, payload_size_, rate_, src_buff_, src_buff_size_, match_fun_, @@ -283,7 +284,6 @@ public: } bool is_visible() const override { return true; } bool depends(SimcallObserver* other) override; - std::string to_string(int times_considered) const override; std::string dot_label(int times_considered) const override { return SimcallObserver::dot_label(times_considered) + "iSend"; @@ -326,9 +326,9 @@ public: return new CommIrecvSimcall(get_issuer(), mbox_, dst_buff_, dst_buff_size_, match_fun_, copy_data_fun_, payload_, rate_); } + void serialize(Simcall& type, char* buffer) override; bool is_visible() const override { return true; } bool depends(SimcallObserver* other) override; - std::string to_string(int times_considered) const override; std::string dot_label(int times_considered) const override { return SimcallObserver::dot_label(times_considered) + "iRecv"; diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp index 10881de354..b2a8f146c4 100644 --- a/src/mc/ModelChecker.cpp +++ b/src/mc/ModelChecker.cpp @@ -308,7 +308,7 @@ void ModelChecker::wait_for_requests() checker_side_.dispatch(); } -RemotePtr ModelChecker::handle_simcall(Transition const& transition) +Transition* ModelChecker::handle_simcall(Transition const& transition, bool new_transition) { s_mc_message_simcall_execute_t m; memset(&m, 0, sizeof(m)); @@ -330,7 +330,10 @@ RemotePtr ModelChecker::handle_simcall( if (this->remote_process_->running()) checker_side_.dispatch(); // The app may send messages while processing the transition - return remote(answer.observer); + if (new_transition) + return recv_transition(transition.aid_, transition.times_considered_, answer.simcall, answer.buffer); + else + return nullptr; } bool ModelChecker::simcall_is_visible(aid_t aid) { @@ -357,40 +360,13 @@ 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(); - - if (m.obs1 == nullptr || m.obs2 == nullptr) - return true; - 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) +std::string ModelChecker::simcall_dot_label(aid_t aid, int times_considered) { xbt_assert(mc_model_checker != nullptr, "This should be called from the checker side"); s_mc_message_simcall_to_string_t m; memset(&m, 0, sizeof(m)); - m.type = type; + m.type = MessageType::SIMCALL_DOT_LABEL; m.aid = aid; m.time_considered = times_considered; checker_side_.get_channel().send(m); @@ -398,27 +374,14 @@ std::string ModelChecker::simcall_to_string(MessageType type, aid_t aid, int tim s_mc_message_simcall_to_string_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_TO_STRING_ANSWER, + xbt_assert(s == sizeof(answer) && answer.type == MessageType::SIMCALL_DOT_LABEL_ANSWER, "Received unexpected message %s (%i, size=%i) " "expected MessageType::SIMCALL_TO_STRING_ANSWER (%i, size=%i)", - to_c_str(answer.type), (int)answer.type, (int)s, (int)MessageType::SIMCALL_TO_STRING_ANSWER, + to_c_str(answer.type), (int)answer.type, (int)s, (int)MessageType::SIMCALL_DOT_LABEL_ANSWER, (int)sizeof(answer)); - return std::string(answer.value); -} - -std::string ModelChecker::simcall_to_string(aid_t aid, int times_considered) -{ - std::string answer = simcall_to_string(MessageType::SIMCALL_TO_STRING, aid, times_considered); - XBT_DEBUG("to_string(%ld) is returning %s", aid, answer.c_str()); - return answer; -} - -std::string ModelChecker::simcall_dot_label(aid_t aid, int times_considered) -{ - std::string answer = simcall_to_string(MessageType::SIMCALL_DOT_LABEL, aid, times_considered); - XBT_DEBUG("dot_label(%ld) is returning %s", aid, answer.c_str()); - return answer; + XBT_DEBUG("dot_label(%ld) is returning %s", aid, answer.value); + return answer.value; } void ModelChecker::finalize_app(bool terminate_asap) diff --git a/src/mc/ModelChecker.hpp b/src/mc/ModelChecker.hpp index 974c82f245..e7bff26a87 100644 --- a/src/mc/ModelChecker.hpp +++ b/src/mc/ModelChecker.hpp @@ -50,13 +50,10 @@ public: void shutdown(); void resume(); void wait_for_requests(); - RemotePtr handle_simcall(Transition const& transition); + Transition* handle_simcall(Transition const& transition, bool new_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); XBT_ATTRIB_NORETURN void exit(int status); diff --git a/src/mc/Transition.cpp b/src/mc/Transition.cpp index 61623be629..5bba8c43eb 100644 --- a/src/mc/Transition.cpp +++ b/src/mc/Transition.cpp @@ -10,38 +10,103 @@ #include "src/mc/remote/RemoteProcess.hpp" #include "xbt/asserts.h" +#include + XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_transition, mc, "Logging specific to MC transitions"); namespace simgrid { namespace mc { unsigned long Transition::executed_transitions_ = 0; +unsigned long Transition::replayed_transitions_ = 0; -std::string Transition::to_string() const +std::string Transition::to_string(bool verbose) { xbt_assert(mc_model_checker != nullptr, "Must be called from MCer"); return textual_; } -const char* Transition::to_cstring() const +const char* Transition::to_cstring(bool verbose) { xbt_assert(mc_model_checker != nullptr, "Must be called from MCer"); + to_string(); return textual_.c_str(); } void Transition::init(aid_t aid, int times_considered) { aid_ = aid; times_considered_ = times_considered; - textual_ = mc_model_checker->simcall_to_string(aid_, times_considered_); } -RemotePtr Transition::replay() const +void Transition::replay() const { - executed_transitions_++; + replayed_transitions_++; - simgrid::mc::RemotePtr res = mc_model_checker->handle_simcall(*this); + mc_model_checker->handle_simcall(*this, false); mc_model_checker->wait_for_requests(); +} + +CommWaitTransition::CommWaitTransition(aid_t issuer, int times_considered, char* buffer) + : Transition(issuer, times_considered) +{ + std::stringstream stream(buffer); + stream >> timeout_ >> comm_ >> sender_ >> receiver_ >> mbox_ >> src_buff_ >> dst_buff_ >> size_; +} +std::string CommWaitTransition::to_string(bool verbose) +{ + textual_ = Transition::to_string(verbose); + textual_ += xbt::string_printf("[src=%ld -> dst=%ld, mbox=%u, tout=%f", sender_, receiver_, mbox_, timeout_); + if (verbose) { + textual_ += ", src_buff=" + xbt::string_printf("%p", src_buff_) + ", size=" + std::to_string(size_); + textual_ += ", dst_buff=" + xbt::string_printf("%p", dst_buff_); + } + textual_ += "]"; + return textual_; +} + +CommRecvTransition::CommRecvTransition(aid_t issuer, int times_considered, char* buffer) + : Transition(issuer, times_considered) +{ + std::stringstream stream(buffer); + stream >> mbox_ >> dst_buff_; +} +std::string CommRecvTransition::to_string(bool verbose) +{ + textual_ = xbt::string_printf("iRecv(recver=%ld mbox=%u", aid_, mbox_); + if (verbose) + textual_ += ", buff=" + xbt::string_printf("%p", dst_buff_); + textual_ += ")"; + return textual_; +} +CommSendTransition::CommSendTransition(aid_t issuer, int times_considered, char* buffer) + : Transition(issuer, times_considered) +{ + std::stringstream stream(buffer); + stream >> mbox_ >> src_buff_ >> size_; +} +std::string CommSendTransition::to_string(bool verbose = false) +{ + textual_ = xbt::string_printf("iSend(sender=%ld mbox=%u", aid_, mbox_); + if (verbose) + textual_ += ", buff=" + xbt::string_printf("%p", src_buff_) + ", size=" + std::to_string(size_); + textual_ += ")"; + return textual_; +} - return res; +Transition* recv_transition(aid_t issuer, int times_considered, kernel::actor::SimcallObserver::Simcall simcall, + char* buffer) +{ + switch (simcall) { + case kernel::actor::SimcallObserver::Simcall::COMM_WAIT: + return new CommWaitTransition(issuer, times_considered, buffer); + case kernel::actor::SimcallObserver::Simcall::IRECV: + return new CommRecvTransition(issuer, times_considered, buffer); + case kernel::actor::SimcallObserver::Simcall::ISEND: + return new CommSendTransition(issuer, times_considered, buffer); + case kernel::actor::SimcallObserver::Simcall::UNKNOWN: + return new Transition(issuer, times_considered); + default: + xbt_die("recv_transition of type %s unimplemented", kernel::actor::SimcallObserver::to_c_str(simcall)); + } } } // namespace mc diff --git a/src/mc/Transition.hpp b/src/mc/Transition.hpp index 3cd9c4c0f4..88929bc749 100644 --- a/src/mc/Transition.hpp +++ b/src/mc/Transition.hpp @@ -8,6 +8,7 @@ #define SIMGRID_MC_TRANSITION_HPP #include "simgrid/forward.h" // aid_t +#include "src/kernel/actor/SimcallObserver.hpp" #include "src/mc/remote/RemotePtr.hpp" #include @@ -24,8 +25,13 @@ namespace mc { */ class Transition { /* Textual representation of the transition, to display backtraces */ - std::string textual_ = ""; static unsigned long executed_transitions_; + static unsigned long replayed_transitions_; + + friend State; // FIXME remove this once we have a proper class to handle the statistics + +protected: + std::string textual_ = ""; public: aid_t aid_ = 0; @@ -40,18 +46,63 @@ public: */ int times_considered_ = 0; + Transition() = default; + Transition(aid_t issuer, int times_considered) : aid_(issuer), times_considered_(times_considered) {} + void init(aid_t aid, int times_considered); - std::string to_string() const; - const char* to_cstring() const; + virtual std::string to_string(bool verbose = false); + const char* to_cstring(bool verbose = false); /* Moves the application toward a path that was already explored, but don't change the current transition */ - RemotePtr replay() const; + void replay() const; + + virtual bool depends(Transition* other) { return true; } /* Returns the total amount of transitions executed so far (for statistics) */ static unsigned long get_executed_transitions() { return executed_transitions_; } + /* Returns the total amount of transitions replayed so far while backtracing (for statistics) */ + static unsigned long get_replayed_transitions() { return replayed_transitions_; } +}; + +class CommWaitTransition : public Transition { + double timeout_; + uintptr_t comm_; + aid_t sender_; + aid_t receiver_; + unsigned mbox_; + unsigned char* src_buff_; + unsigned char* dst_buff_; + size_t size_; + +public: + CommWaitTransition(aid_t issuer, int times_considered, char* buffer); + std::string to_string(bool verbose) override; }; +class CommRecvTransition : public Transition { + unsigned mbox_; + void* dst_buff_; + +public: + CommRecvTransition(aid_t issuer, int times_considered, char* buffer); + std::string to_string(bool verbose) override; +}; + +class CommSendTransition : public Transition { + unsigned mbox_; + void* src_buff_; + size_t size_; + +public: + CommSendTransition(aid_t issuer, int times_considered, char* buffer); + std::string to_string(bool verbose) override; +}; + +/** Make a new transition from serialized description */ +Transition* recv_transition(aid_t issuer, int times_considered, kernel::actor::SimcallObserver::Simcall simcall, + char* buffer); + } // namespace mc } // namespace simgrid diff --git a/src/mc/api.cpp b/src/mc/api.cpp index ea947943b0..6556ab7584 100644 --- a/src/mc/api.cpp +++ b/src/mc/api.cpp @@ -67,14 +67,6 @@ simgrid::mc::ActorInformation* Api::actor_info_cast(smx_actor_t actor) const return process_info; } -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 { if (mc_model_checker == nullptr) diff --git a/src/mc/api.hpp b/src/mc/api.hpp index f0a2d95486..cd5551d6fa 100644 --- a/src/mc/api.hpp +++ b/src/mc/api.hpp @@ -102,8 +102,6 @@ public: void dump_record_path() const; // SIMCALL APIs - bool requests_are_dependent(RemotePtr obs1, - RemotePtr obs2) const; std::string request_get_dot_output(aid_t aid, 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; diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp index 72192fafd6..17ffc5842c 100644 --- a/src/mc/checker/SafetyChecker.cpp +++ b/src/mc/checker/SafetyChecker.cpp @@ -124,7 +124,7 @@ void SafetyChecker::run() } /* Actually answer the request: let execute the selected request (MCed does one step) */ - auto remote_observer = state->execute_next(next); + state->set_transition(state->execute_next(next)); // If there are processes to interleave and the maximum depth has not been // reached then perform one step of the exploration algorithm. @@ -137,7 +137,6 @@ void SafetyChecker::run() /* Create the new expanded state (copy the state of MCed into our MCer data) */ auto next_state = std::make_unique(); - next_state->remote_observer_ = remote_observer; if (_sg_mc_termination) this->check_non_termination(next_state.get()); @@ -196,7 +195,7 @@ void SafetyChecker::backtrack() XBT_DEBUG("Simcall >>%s<< and >>%s<< with same issuer %ld", state->get_transition()->to_cstring(), prev_state->get_transition()->to_cstring(), issuer_id); break; - } else if (api::get().requests_are_dependent(prev_state->remote_observer_, state->remote_observer_)) { + } else if (prev_state->get_transition()->depends(state->get_transition())) { if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) { XBT_DEBUG("Dependent Transitions:"); XBT_DEBUG(" %s (state=%ld)", prev_state->get_transition()->to_cstring(), prev_state->num_); diff --git a/src/mc/mc_record.cpp b/src/mc/mc_record.cpp index c56f726389..ec97313473 100644 --- a/src/mc/mc_record.cpp +++ b/src/mc/mc_record.cpp @@ -58,8 +58,10 @@ RecordTrace parseRecordTrace(const char* data) const char* current = data; while (*current) { - simgrid::mc::Transition item; - int count = sscanf(current, "%ld/%d", &item.aid_, &item.times_considered_); + long aid; + int times_considered; + int count = sscanf(current, "%ld/%d", &aid, ×_considered); + simgrid::mc::Transition item(aid, times_considered); if(count != 2 && count != 1) throw std::invalid_argument("Could not parse record path"); diff --git a/src/mc/mc_state.cpp b/src/mc/mc_state.cpp index f0fbc1ce53..9871c79be6 100644 --- a/src/mc/mc_state.cpp +++ b/src/mc/mc_state.cpp @@ -24,6 +24,7 @@ State::State() : num_(++expended_states_) { const unsigned long maxpid = api::get().get_maxpid(); actor_states_.resize(maxpid); + transition_.reset(new Transition()); /* Stateful model checking */ if ((_sg_mc_checkpoint > 0 && (num_ % _sg_mc_checkpoint == 0)) || _sg_mc_termination) { auto snapshot_ptr = api::get().take_snapshot(num_); @@ -42,7 +43,7 @@ std::size_t State::count_todo() const Transition* State::get_transition() const { - return const_cast(&this->transition_); + return transition_.get(); } int State::next_transition() const @@ -61,7 +62,7 @@ int State::next_transition() const } return -1; } -RemotePtr State::execute_next(int next) +Transition* State::execute_next(int next) { std::vector& actors = mc_model_checker->get_remote_process().actors(); @@ -80,12 +81,17 @@ RemotePtr State::execute_next(int next) actor_state->set_done(); } - transition_.init(aid, times_considered); + transition_->init(aid, times_considered); executed_req_ = actor->simcall_; - XBT_DEBUG("Let's run actor %ld, going for transition %s", aid, transition_.to_cstring()); + XBT_DEBUG("Let's run actor %ld, going for transition %s", aid, transition_->to_cstring()); - return transition_.replay(); + Transition::executed_transitions_++; + + Transition* res = mc_model_checker->handle_simcall(*transition_, true); + mc_model_checker->wait_for_requests(); + + return res; } void State::copy_incomplete_comm_pattern() diff --git a/src/mc/mc_state.hpp b/src/mc/mc_state.hpp index 858f00bfe1..739a40252a 100644 --- a/src/mc/mc_state.hpp +++ b/src/mc/mc_state.hpp @@ -18,7 +18,7 @@ class XBT_PRIVATE State { static long expended_states_; /* Count total amount of states, for stats */ /* Outgoing transition: what was the last transition that we took to leave this state? Useful for replay */ - Transition transition_; + std::unique_ptr transition_; public: explicit State(); @@ -32,9 +32,6 @@ 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_; - /** Snapshot of system state (if needed) */ std::shared_ptr system_state_; @@ -47,11 +44,12 @@ public: int next_transition() const; /* Explore a new path */ - RemotePtr execute_next(int next); + Transition* execute_next(int next); std::size_t count_todo() const; void mark_todo(aid_t actor) { this->actor_states_[actor].mark_todo(); } Transition* get_transition() const; + void set_transition(Transition* t) { transition_.reset(t); } /* Returns the total amount of states created so far (for statistics) */ static long get_expanded_states() { return expended_states_; } diff --git a/src/mc/remote/AppSide.cpp b/src/mc/remote/AppSide.cpp index 40fc447919..57bd6a22be 100644 --- a/src/mc/remote/AppSide.cpp +++ b/src/mc/remote/AppSide.cpp @@ -104,8 +104,13 @@ void AppSide::handle_simcall_execute(const s_mc_message_simcall_execute_t* messa 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); + s_mc_message_simcall_execute_answer_t answer; + memset(&answer, 0, sizeof(answer)); + answer.type = MessageType::SIMCALL_EXECUTE_ANSWER; + if (observer != nullptr) + observer->serialize(answer.simcall, answer.buffer); + XBT_DEBUG("send SIMCALL_EXECUTE_ANSWER(%s) ~> %s '%s'", actor->get_cname(), + simgrid::kernel::actor::SimcallObserver::to_c_str(answer.simcall), answer.buffer); xbt_assert(channel_.send(answer) == 0, "Could not send response"); // The client may send some messages to the server while processing the transition @@ -167,26 +172,6 @@ void AppSide::handle_messages() const break; } - case MessageType::SIMCALL_TO_STRING: { - assert_msg_size("SIMCALL_TO_STRING", s_mc_message_simcall_to_string_t); - auto msg_simcall = (s_mc_message_simcall_to_string_t*)message_buffer.data(); - const kernel::actor::ActorImpl* actor = kernel::actor::ActorImpl::by_pid(msg_simcall->aid); - xbt_assert(actor != nullptr, "Invalid pid %ld", msg_simcall->aid); - xbt_assert(actor->simcall_.observer_, "The transition of %s has no observer", actor->get_cname()); - std::string value = ""; - if (actor->simcall_.observer_ != nullptr) - value = actor->simcall_.observer_->to_string(msg_simcall->time_considered); - else - value = "[(" + std::to_string(actor->get_pid()) + ")" + actor->get_host()->get_cname() + " (" + - actor->get_cname() + ")] " + SIMIX_simcall_name(actor->simcall_) + "(unknown?)"; - - // Send result: - s_mc_message_simcall_to_string_answer_t answer{MessageType::SIMCALL_TO_STRING_ANSWER, {0}}; - value.copy(answer.value, (sizeof answer.value) - 1); // last byte was set to '\0' by initialization above - 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(); @@ -199,33 +184,12 @@ void AppSide::handle_messages() const value = "UNIMPLEMENTED"; // Send result: - s_mc_message_simcall_to_string_answer_t answer{MessageType::SIMCALL_TO_STRING_ANSWER, {0}}; + s_mc_message_simcall_to_string_answer_t answer{MessageType::SIMCALL_DOT_LABEL_ANSWER, {0}}; value.copy(answer.value, (sizeof answer.value) - 1); // last byte was set to '\0' by initialization above xbt_assert(channel_.send(answer) == 0, "Could not send response"); 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::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()); diff --git a/src/mc/remote/mc_protocol.h b/src/mc/remote/mc_protocol.h index 112cddf107..e6a798a850 100644 --- a/src/mc/remote/mc_protocol.h +++ b/src/mc/remote/mc_protocol.h @@ -16,6 +16,8 @@ #ifdef __cplusplus +#include "src/kernel/actor/SimcallObserver.hpp" + #include "mc/datatypes.h" #include "simgrid/forward.h" // aid_t #include @@ -30,9 +32,8 @@ 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_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); + SIMCALL_EXECUTE_ANSWER, SIMCALL_IS_VISIBLE, SIMCALL_IS_VISIBLE_ANSWER, SIMCALL_DOT_LABEL, + SIMCALL_DOT_LABEL_ANSWER, ASSERTION_FAILED, ACTOR_ENABLED, ACTOR_ENABLED_REPLY, FINALIZE); } // namespace mc } // namespace simgrid @@ -102,7 +103,8 @@ struct s_mc_message_simcall_execute_t { }; struct s_mc_message_simcall_execute_answer_t { simgrid::mc::MessageType type; - simgrid::kernel::actor::SimcallObserver* observer; + simgrid::kernel::actor::SimcallObserver::Simcall simcall; + char buffer[2048]; }; struct s_mc_message_restore_t { @@ -125,25 +127,15 @@ struct s_mc_message_simcall_is_visible_answer_t { // MessageType::SIMCALL_IS_VIS bool value; }; -struct s_mc_message_simcall_to_string_t { // MessageType::SIMCALL_TO_STRING or MessageType::SIMCALL_DOT_LABEL +struct s_mc_message_simcall_to_string_t { // MessageType::SIMCALL_DOT_LABEL simgrid::mc::MessageType type; aid_t aid; int time_considered; }; -struct s_mc_message_simcall_to_string_answer_t { // MessageType::SIMCALL_TO_STRING_ANSWER +struct s_mc_message_simcall_to_string_answer_t { // MessageType::SIMCALL_DOT_LABEL_ANSWER simgrid::mc::MessageType type; 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