From 3b12e64243918b9f086546bb55cadb11c1ec7ef4 Mon Sep 17 00:00:00 2001 From: Martin Quinson Date: Sat, 12 Feb 2022 12:30:10 +0100 Subject: [PATCH] Move dot_label() from Observer to Transition (+ some reorgs) --- src/kernel/actor/SimcallObserver.cpp | 102 ++---------------- src/kernel/actor/SimcallObserver.hpp | 37 ++----- src/mc/ModelChecker.cpp | 24 ----- src/mc/ModelChecker.hpp | 1 - src/mc/api.cpp | 7 +- src/mc/api.hpp | 2 +- src/mc/api/Transition.cpp | 17 +-- src/mc/api/Transition.hpp | 19 ++-- src/mc/api/TransitionComm.cpp | 56 +++++----- src/mc/api/TransitionComm.hpp | 9 +- .../CommunicationDeterminismChecker.cpp | 5 +- src/mc/checker/LivenessChecker.cpp | 13 +-- src/mc/checker/SafetyChecker.cpp | 17 ++- src/mc/mc_record.cpp | 2 +- src/mc/remote/AppSide.cpp | 24 +---- src/mc/remote/mc_protocol.h | 16 +-- 16 files changed, 97 insertions(+), 254 deletions(-) diff --git a/src/kernel/actor/SimcallObserver.cpp b/src/kernel/actor/SimcallObserver.cpp index aa457e4fbb..b816e92d0f 100644 --- a/src/kernel/actor/SimcallObserver.cpp +++ b/src/kernel/actor/SimcallObserver.cpp @@ -28,9 +28,9 @@ bool RandomSimcall::depends(SimcallObserver* other) { return get_issuer() == other->get_issuer(); } -void RandomSimcall::serialize(Simcall& type, std::stringstream& stream) +void RandomSimcall::serialize(mc::Transition::Type& type, std::stringstream& stream) { - type = Simcall::RANDOM; + type = mc::Transition::Type::RANDOM; stream << min_ << ' ' << max_; } @@ -57,25 +57,6 @@ 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) 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 -{ - if (issuer_->get_host()) - return xbt::string_printf("[(%ld)%s] ", issuer_->get_pid(), issuer_->get_host()->get_cname()); - return xbt::string_printf("[(%ld)] ", issuer_->get_pid()); -} - -std::string RandomSimcall::dot_label(int times_considered) const -{ - return SimcallObserver::dot_label(times_considered) + "MC_RANDOM(" + std::to_string(next_value_) + ")"; -} - void RandomSimcall::prepare(int times_considered) { next_value_ = min_ + times_considered; @@ -87,11 +68,6 @@ int RandomSimcall::get_max_consider() const return max_ - min_ + 1; } -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 { @@ -103,21 +79,11 @@ std::string MutexLockSimcall::to_string(int times_considered) const return res; }*/ -std::string MutexLockSimcall::dot_label(int times_considered) const -{ - return SimcallObserver::dot_label(times_considered) + (blocking_ ? "Mutex LOCK" : "Mutex TRYLOCK"); -} - bool MutexLockSimcall::is_enabled() const { return not blocking_ || get_mutex()->get_owner() == nullptr || get_mutex()->get_owner() == get_issuer(); } -std::string ConditionWaitSimcall::dot_label(int times_considered) const -{ - return SimcallObserver::dot_label(times_considered) + "Condition WAIT"; -} - bool ConditionWaitSimcall::is_enabled() const { static bool warned = false; @@ -128,11 +94,6 @@ bool ConditionWaitSimcall::is_enabled() const return true; } -std::string SemAcquireSimcall::dot_label(int times_considered) const -{ - return SimcallObserver::dot_label(times_considered) + "Sem ACQUIRE"; -} - bool SemAcquireSimcall::is_enabled() const { static bool warned = false; @@ -172,17 +133,6 @@ std::string ActivityTestanySimcall::to_string(int times_considered) const return res; }*/ -std::string ActivityTestanySimcall::dot_label(int times_considered) const -{ - std::string res = SimcallObserver::dot_label(times_considered) + "TestAny "; - if (times_considered == -1) { - res += "FALSE"; - } else { - res += xbt::string_printf("TRUE [%d of %zu]", times_considered + 1, activities_.size()); - } - return res; -} - bool ActivityTestSimcall::depends(SimcallObserver* other) { if (get_issuer() == other->get_issuer()) @@ -224,17 +174,17 @@ bool ActivityTestSimcall::depends(SimcallObserver* other) return true; } -void ActivityWaitSimcall::serialize(Simcall& type, std::stringstream& stream) +void ActivityWaitSimcall::serialize(mc::Transition::Type& type, std::stringstream& stream) { if (auto* comm = dynamic_cast(activity_)) { - type = Simcall::COMM_WAIT; + type = mc::Transition::Type::COMM_WAIT; stream << (timeout_ > 0) << ' ' << 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_id(); stream << ' ' << (void*)comm->src_buff_ << ' ' << (void*)comm->dst_buff_ << ' ' << comm->src_buff_size_; } else { - type = Simcall::UNKNOWN; + type = mc::Transition::Type::UNKNOWN; } } @@ -263,18 +213,6 @@ std::string ActivityTestSimcall::to_string(int times_considered) const return res; }*/ -std::string ActivityTestSimcall::dot_label(int times_considered) const -{ - std::string res = SimcallObserver::dot_label(times_considered) + "Test "; - const auto* comm = dynamic_cast(activity_); - if (comm && (comm->src_actor_.get() == nullptr || comm->dst_actor_.get() == nullptr)) { - res += "FALSE"; - } else { - res += "TRUE"; - } - return res; -} - bool ActivityWaitSimcall::is_enabled() const { /* FIXME: check also that src and dst processes are not suspended */ @@ -294,28 +232,6 @@ bool ActivityWaitSimcall::is_enabled() const return (comm->src_actor_ && comm->dst_actor_); } -std::string ActivityWaitSimcall::dot_label(int times_considered) const -{ - std::string res = SimcallObserver::dot_label(times_considered); - res += (times_considered == -1) ? "WaitTimeout " : "Wait "; - - const auto* comm = dynamic_cast(activity_); - if (comm) { - auto src = comm->src_actor_; - auto dst = comm->dst_actor_; - res += " [(" + std::to_string(src ? src->get_pid() : 0) + ")"; - res += "->(" + std::to_string(dst ? dst->get_pid() : 0) + ")]"; - } else - xbt_die("Only Comms are supported here for now"); - return res; -} - -std::string ActivityWaitanySimcall::dot_label(int times_considered) const -{ - return SimcallObserver::dot_label(times_considered) + - xbt::string_printf("WaitAny [%d of %zu]", times_considered + 1, activities_.size()); -} - bool ActivityWaitanySimcall::is_enabled() const { // FIXME: deal with other kind of activities (Exec and I/Os) @@ -345,16 +261,16 @@ void ActivityWaitanySimcall::prepare(int times_considered) next_value_ = times_considered; } -void CommIsendSimcall::serialize(Simcall& type, std::stringstream& stream) +void CommIsendSimcall::serialize(mc::Transition::Type& type, std::stringstream& stream) { - type = Simcall::ISEND; + type = mc::Transition::Type::ISEND; stream << mbox_->get_id() << ' ' << (void*)src_buff_ << ' ' << src_buff_size_; XBT_DEBUG("SendObserver mbox:%u buff:%p size:%zu", mbox_->get_id(), src_buff_, src_buff_size_); } -void CommIrecvSimcall::serialize(Simcall& type, std::stringstream& stream) +void CommIrecvSimcall::serialize(mc::Transition::Type& type, std::stringstream& stream) { - type = Simcall::IRECV; + type = mc::Transition::Type::IRECV; stream << mbox_->get_id() << dst_buff_; } diff --git a/src/kernel/actor/SimcallObserver.hpp b/src/kernel/actor/SimcallObserver.hpp index 002d36fc17..18ce979d3d 100644 --- a/src/kernel/actor/SimcallObserver.hpp +++ b/src/kernel/actor/SimcallObserver.hpp @@ -7,8 +7,8 @@ #define SIMGRID_MC_SIMCALL_OBSERVER_HPP #include "simgrid/forward.h" +#include "src/mc/api/Transition.hpp" #include "xbt/asserts.h" -#include "xbt/utility.hpp" #include @@ -20,8 +20,6 @@ class SimcallObserver { ActorImpl* const issuer_; public: - XBT_DECLARE_ENUM_CLASS(Simcall, UNKNOWN, RANDOM, ISEND, IRECV, COMM_WAIT, COMM_TEST); - explicit SimcallObserver(ActorImpl* issuer) : issuer_(issuer) {} ActorImpl* get_issuer() const { return issuer_; } /** Whether this transition can currently be taken without blocking. @@ -56,12 +54,14 @@ public: virtual bool depends(SimcallObserver* other); /** Serialize to the given string buffer */ - virtual void serialize(Simcall& type, std::stringstream& stream) { type = Simcall::UNKNOWN; } + virtual void serialize(mc::Transition::Type& type, std::stringstream& stream) + { + type = mc::Transition::Type::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 dot_label(int times_considered) const = 0; }; template class ResultingSimcall : public SimcallObserver { @@ -84,10 +84,9 @@ public: { xbt_assert(min < max); } - void serialize(Simcall& type, std::stringstream& stream) override; + void serialize(mc::Transition::Type& type, std::stringstream& stream) override; int get_max_consider() const override; void prepare(int times_considered) override; - std::string dot_label(int times_considered) const override; int get_value() const { return next_value_; } bool depends(SimcallObserver* other) override; }; @@ -103,9 +102,6 @@ public: class MutexUnlockSimcall : public MutexSimcall { using MutexSimcall::MutexSimcall; - -public: - std::string dot_label(int times_considered) const override; }; class MutexLockSimcall : public MutexSimcall { @@ -117,7 +113,6 @@ public: { } bool is_enabled() const override; - std::string dot_label(int times_considered) const override; }; class ConditionWaitSimcall : public ResultingSimcall { @@ -133,7 +128,6 @@ public: } bool is_enabled() const override; bool is_visible() const override { return false; } - std::string dot_label(int times_considered) const override; activity::ConditionVariableImpl* get_cond() const { return cond_; } activity::MutexImpl* get_mutex() const { return mutex_; } double get_timeout() const { return timeout_; } @@ -150,7 +144,6 @@ public: } bool is_enabled() const override; bool is_visible() const override { return false; } - std::string dot_label(int times_considered) const override; activity::SemaphoreImpl* get_sem() const { return sem_; } double get_timeout() const { return timeout_; } }; @@ -165,7 +158,6 @@ public: } bool is_visible() const override { return true; } bool depends(SimcallObserver* other) override; - std::string dot_label(int times_considered) const override; activity::ActivityImpl* get_activity() const { return activity_; } }; @@ -181,7 +173,6 @@ public: bool is_visible() const override { return true; } int get_max_consider() const override; void prepare(int times_considered) 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_; } }; @@ -195,10 +186,9 @@ public: : ResultingSimcall(actor, false), activity_(activity), timeout_(timeout) { } - void serialize(Simcall& type, std::stringstream& stream) override; + void serialize(mc::Transition::Type& type, std::stringstream& stream) override; bool is_visible() const override { return true; } bool is_enabled() 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; } double get_timeout() const { return timeout_; } @@ -218,7 +208,6 @@ public: bool is_visible() const override { return true; } void prepare(int times_considered) override; int get_max_consider() 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_; } int get_value() const { return next_value_; } @@ -256,12 +245,8 @@ public: , copy_data_fun_(copy_data_fun) { } - void serialize(Simcall& type, std::stringstream& stream) override; + void serialize(mc::Transition::Type& type, std::stringstream& stream) override; bool is_visible() const override { return true; } - std::string dot_label(int times_considered) const override - { - return SimcallObserver::dot_label(times_considered) + "iSend"; - } activity::MailboxImpl* get_mailbox() const { return mbox_; } double get_payload_size() const { return payload_size_; } double get_rate() const { return rate_; } @@ -295,12 +280,8 @@ public: , copy_data_fun_(copy_data_fun) { } - void serialize(Simcall& type, std::stringstream& stream) override; + void serialize(mc::Transition::Type& type, std::stringstream& stream) override; bool is_visible() const override { return true; } - std::string dot_label(int times_considered) const override - { - return SimcallObserver::dot_label(times_considered) + "iRecv"; - } activity::MailboxImpl* get_mailbox() const { return mbox_; } double get_rate() const { return rate_; } unsigned char* get_dst_buff() const { return dst_buff_; } diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp index 4d74699b98..fdae4fe19d 100644 --- a/src/mc/ModelChecker.cpp +++ b/src/mc/ModelChecker.cpp @@ -361,30 +361,6 @@ bool ModelChecker::simcall_is_visible(aid_t aid) return answer.value; } -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 = MessageType::SIMCALL_DOT_LABEL; - m.aid = aid; - m.time_considered = times_considered; - checker_side_.get_channel().send(m); - - 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_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_DOT_LABEL_ANSWER, - (int)sizeof(answer)); - - XBT_DEBUG("dot_label(%ld) is returning %s", aid, answer.value); - return answer.value; -} - void ModelChecker::finalize_app(bool terminate_asap) { s_mc_message_int_t m; diff --git a/src/mc/ModelChecker.hpp b/src/mc/ModelChecker.hpp index daee1b954c..ab99ea5eee 100644 --- a/src/mc/ModelChecker.hpp +++ b/src/mc/ModelChecker.hpp @@ -56,7 +56,6 @@ public: /* Interactions with the simcall observer */ bool simcall_is_visible(aid_t aid); - std::string simcall_dot_label(aid_t aid, int times_considered); XBT_ATTRIB_NORETURN void exit(int status); diff --git a/src/mc/api.cpp b/src/mc/api.cpp index c99d687e1c..09764e401c 100644 --- a/src/mc/api.cpp +++ b/src/mc/api.cpp @@ -351,11 +351,10 @@ void Api::mc_exit(int status) const mc_model_checker->exit(status); } -std::string Api::request_get_dot_output(aid_t aid, int value) const +std::string Api::request_get_dot_output(const Transition* t) const { - const char* color = get_color(aid - 1); - return "label = \"" + mc_model_checker->simcall_dot_label(aid, value) + "\", color = " + color + - ", fontcolor = " + color; + const char* color = get_color(t->aid_ - 1); + return "label = \"" + t->dot_label() + "\", color = " + color + ", fontcolor = " + color; } #if HAVE_SMPI diff --git a/src/mc/api.hpp b/src/mc/api.hpp index c7fd769486..9da3c6d5c3 100644 --- a/src/mc/api.hpp +++ b/src/mc/api.hpp @@ -101,7 +101,7 @@ public: XBT_ATTRIB_NORETURN void mc_exit(int status) const; // SIMCALL APIs - std::string request_get_dot_output(aid_t aid, int value) const; + std::string request_get_dot_output(const Transition* t) 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; diff --git a/src/mc/api/Transition.cpp b/src/mc/api/Transition.cpp index 229e546924..0af324b945 100644 --- a/src/mc/api/Transition.cpp +++ b/src/mc/api/Transition.cpp @@ -24,14 +24,13 @@ unsigned long Transition::replayed_transitions_ = 0; // Do not move this to the header, to ensure that we have a vtable for Transition Transition::~Transition() = default; -std::string Transition::to_string(bool) +std::string Transition::to_string(bool) const { - return textual_; + return ""; } -const char* Transition::to_cstring(bool verbose) +std::string Transition::dot_label() const { - to_string(verbose); - return textual_.c_str(); + return xbt::string_printf("[(%ld)] %s", aid_, Transition::to_c_str(type_)); } void Transition::replay() const { @@ -42,17 +41,21 @@ void Transition::replay() const mc_model_checker->wait_for_requests(); #endif } -std::string RandomTransition::to_string(bool verbose) +std::string RandomTransition::to_string(bool verbose) const { return xbt::string_printf("Random([%d;%d] ~> %d)", min_, max_, times_considered_); } RandomTransition::RandomTransition(aid_t issuer, int times_considered, char* buffer) - : Transition(issuer, times_considered) + : Transition(Type::RANDOM, issuer, times_considered) { std::stringstream stream(buffer); stream >> min_ >> max_; } +std::string RandomTransition::dot_label() const +{ + return Transition::dot_label() + to_c_str(type_); +} } // namespace mc } // namespace simgrid diff --git a/src/mc/api/Transition.hpp b/src/mc/api/Transition.hpp index 416241b229..1db0101f6f 100644 --- a/src/mc/api/Transition.hpp +++ b/src/mc/api/Transition.hpp @@ -8,6 +8,7 @@ #define SIMGRID_MC_TRANSITION_HPP #include "simgrid/forward.h" // aid_t +#include "xbt/utility.hpp" // XBT_DECLARE_ENUM_CLASS #include @@ -29,10 +30,10 @@ class Transition { friend State; // FIXME remove this once we have a proper class to handle the statistics -protected: - std::string textual_ = ""; - public: + XBT_DECLARE_ENUM_CLASS(Type, UNKNOWN, RANDOM, ISEND, IRECV, COMM_WAIT, COMM_TEST); + Type type_ = Type::UNKNOWN; + aid_t aid_ = 0; /* Which transition was executed for this simcall @@ -46,11 +47,14 @@ public: int times_considered_ = 0; Transition() = default; + Transition(Type type, aid_t issuer, int times_considered) + : type_(type), aid_(issuer), times_considered_(times_considered) + { + } virtual ~Transition(); - Transition(aid_t issuer, int times_considered) : aid_(issuer), times_considered_(times_considered) {} - virtual std::string to_string(bool verbose = false); - const char* to_cstring(bool verbose = false); + virtual std::string to_string(bool verbose = false) const; + virtual std::string dot_label() const; /* Moves the application toward a path that was already explored, but don't change the current transition */ void replay() const; @@ -68,7 +72,8 @@ class RandomTransition : public Transition { int max_; public: - std::string to_string(bool verbose) override; + std::string to_string(bool verbose) const override; + std::string dot_label() const override; RandomTransition(aid_t issuer, int times_considered, char* buffer); bool depends(const Transition* other) const override { return false; } // Independent with any other transition }; diff --git a/src/mc/api/TransitionComm.cpp b/src/mc/api/TransitionComm.cpp index 6fa6730217..da627c5863 100644 --- a/src/mc/api/TransitionComm.cpp +++ b/src/mc/api/TransitionComm.cpp @@ -21,23 +21,23 @@ namespace simgrid { namespace mc { CommWaitTransition::CommWaitTransition(aid_t issuer, int times_considered, char* buffer) - : Transition(issuer, times_considered) + : Transition(Type::COMM_WAIT, issuer, times_considered) { std::stringstream stream(buffer); stream >> timeout_ >> comm_ >> sender_ >> receiver_ >> mbox_ >> src_buff_ >> dst_buff_ >> size_; XBT_DEBUG("CommWaitTransition %s comm:%p, sender:%ld receiver:%ld mbox:%u sbuff:%p rbuff:%p size:%zu", (timeout_ ? "timeout" : "no-timeout"), comm_, sender_, receiver_, mbox_, src_buff_, dst_buff_, size_); } -std::string CommWaitTransition::to_string(bool verbose) +std::string CommWaitTransition::to_string(bool verbose) const { - textual_ = xbt::string_printf("%ld: WaitComm(from %ld to %ld, mbox=%u, %s", aid_, sender_, receiver_, mbox_, + auto res = xbt::string_printf("%ld: WaitComm(from %ld to %ld, mbox=%u, %s", aid_, sender_, receiver_, mbox_, (timeout_ ? "timeout" : "no 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_); + res += ", src_buff=" + xbt::string_printf("%p", src_buff_) + ", size=" + std::to_string(size_); + res += ", dst_buff=" + xbt::string_printf("%p", dst_buff_); } - textual_ += ")"; - return textual_; + res += ")"; + return res; } bool CommWaitTransition::depends(const Transition* other) const { @@ -69,18 +69,18 @@ bool CommWaitTransition::depends(const Transition* other) const } CommRecvTransition::CommRecvTransition(aid_t issuer, int times_considered, char* buffer) - : Transition(issuer, times_considered) + : Transition(Type::IRECV, issuer, times_considered) { std::stringstream stream(buffer); stream >> mbox_ >> dst_buff_; } -std::string CommRecvTransition::to_string(bool verbose) +std::string CommRecvTransition::to_string(bool verbose) const { - textual_ = xbt::string_printf("%ld: iRecv(mbox=%u", aid_, mbox_); + auto res = xbt::string_printf("%ld: iRecv(mbox=%u", aid_, mbox_); if (verbose) - textual_ += ", buff=" + xbt::string_printf("%p", dst_buff_); - textual_ += ")"; - return textual_; + res += ", buff=" + xbt::string_printf("%p", dst_buff_); + res += ")"; + return res; } bool CommRecvTransition::depends(const Transition* other) const { @@ -118,20 +118,21 @@ bool CommRecvTransition::depends(const Transition* other) const } CommSendTransition::CommSendTransition(aid_t issuer, int times_considered, char* buffer) - : Transition(issuer, times_considered) + : Transition(Type::ISEND, issuer, times_considered) { std::stringstream stream(buffer); stream >> mbox_ >> src_buff_ >> size_; XBT_DEBUG("SendTransition mbox:%u buff:%p size:%zu", mbox_, src_buff_, size_); } -std::string CommSendTransition::to_string(bool verbose = false) +std::string CommSendTransition::to_string(bool verbose = false) const { - textual_ = xbt::string_printf("%ld: iSend(mbox=%u", aid_, mbox_); + auto res = xbt::string_printf("%ld: iSend(mbox=%u", aid_, mbox_); if (verbose) - textual_ += ", buff=" + xbt::string_printf("%p", src_buff_) + ", size=" + std::to_string(size_); - textual_ += ")"; - return textual_; + res += ", buff=" + xbt::string_printf("%p", src_buff_) + ", size=" + std::to_string(size_); + res += ")"; + return res; } + bool CommSendTransition::depends(const Transition* other) const { if (aid_ == other->aid_) @@ -167,24 +168,23 @@ bool CommSendTransition::depends(const Transition* other) const return true; } -Transition* recv_transition(aid_t issuer, int times_considered, kernel::actor::SimcallObserver::Simcall simcall, - char* buffer) +Transition* recv_transition(aid_t issuer, int times_considered, Transition::Type simcall, char* buffer) { switch (simcall) { - case kernel::actor::SimcallObserver::Simcall::COMM_WAIT: + case Transition::Type::COMM_WAIT: return new CommWaitTransition(issuer, times_considered, buffer); - case kernel::actor::SimcallObserver::Simcall::IRECV: + case Transition::Type::IRECV: return new CommRecvTransition(issuer, times_considered, buffer); - case kernel::actor::SimcallObserver::Simcall::ISEND: + case Transition::Type::ISEND: return new CommSendTransition(issuer, times_considered, buffer); - case kernel::actor::SimcallObserver::Simcall::RANDOM: + case Transition::Type::RANDOM: return new RandomTransition(issuer, times_considered, buffer); - case kernel::actor::SimcallObserver::Simcall::UNKNOWN: - return new Transition(issuer, times_considered); + case Transition::Type::UNKNOWN: + return new Transition(Transition::Type::UNKNOWN, issuer, times_considered); default: - xbt_die("recv_transition of type %s unimplemented", kernel::actor::SimcallObserver::to_c_str(simcall)); + xbt_die("recv_transition of type %s unimplemented", Transition::to_c_str(simcall)); } } diff --git a/src/mc/api/TransitionComm.hpp b/src/mc/api/TransitionComm.hpp index e2103facc4..3e83dcaa68 100644 --- a/src/mc/api/TransitionComm.hpp +++ b/src/mc/api/TransitionComm.hpp @@ -32,7 +32,7 @@ class CommWaitTransition : public Transition { public: CommWaitTransition(aid_t issuer, int times_considered, char* buffer); - std::string to_string(bool verbose) override; + std::string to_string(bool verbose) const override; bool depends(const Transition* other) const override; }; @@ -42,7 +42,7 @@ class CommRecvTransition : public Transition { public: CommRecvTransition(aid_t issuer, int times_considered, char* buffer); - std::string to_string(bool verbose) override; + std::string to_string(bool verbose) const override; bool depends(const Transition* other) const override; }; @@ -53,13 +53,12 @@ class CommSendTransition : public Transition { public: CommSendTransition(aid_t issuer, int times_considered, char* buffer); - std::string to_string(bool verbose) override; + std::string to_string(bool verbose) const override; bool depends(const Transition* other) const override; }; /** Make a new transition from serialized description */ -Transition* recv_transition(aid_t issuer, int times_considered, kernel::actor::SimcallObserver::Simcall simcall, - char* buffer); +Transition* recv_transition(aid_t issuer, int times_considered, Transition::Type simcall, char* buffer); } // namespace mc } // namespace simgrid diff --git a/src/mc/checker/CommunicationDeterminismChecker.cpp b/src/mc/checker/CommunicationDeterminismChecker.cpp index 388e9e220c..249d869009 100644 --- a/src/mc/checker/CommunicationDeterminismChecker.cpp +++ b/src/mc/checker/CommunicationDeterminismChecker.cpp @@ -420,15 +420,14 @@ void CommunicationDeterminismChecker::real_run() if (next_transition >= 0 && visited_state == nullptr) { cur_state->execute_next(next_transition); - aid_t aid = cur_state->get_transition()->aid_; int req_num = cur_state->get_transition()->times_considered_; smx_simcall_t req = &cur_state->executed_req_; - XBT_DEBUG("Execute: %s", cur_state->get_transition()->to_cstring()); + XBT_DEBUG("Execute: %s", cur_state->get_transition()->to_string().c_str()); std::string req_str; if (dot_output != nullptr) - req_str = api::get().request_get_dot_output(aid, req_num); + req_str = api::get().request_get_dot_output(cur_state->get_transition()); /* TODO : handle test and testany simcalls */ CallType call = CallType::NONE; diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp index e8f39c176e..41a4c2ffb5 100644 --- a/src/mc/checker/LivenessChecker.cpp +++ b/src/mc/checker/LivenessChecker.cpp @@ -123,7 +123,7 @@ void LivenessChecker::replay() if (pair->exploration_started) { state->get_transition()->replay(); - XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, state->get_transition()->to_cstring(), state.get()); + XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, state->get_transition()->to_string().c_str(), state.get()); } /* Update statistics */ @@ -333,13 +333,8 @@ void LivenessChecker::run() } } - int next = current_pair->graph_state->next_transition(); - - current_pair->graph_state->execute_next(next); - - aid_t aid = current_pair->graph_state->get_transition()->aid_; - int req_num = current_pair->graph_state->get_transition()->times_considered_; - XBT_DEBUG("Execute: %s", current_pair->graph_state->get_transition()->to_cstring()); + current_pair->graph_state->execute_next(current_pair->graph_state->next_transition()); + XBT_DEBUG("Execute: %s", current_pair->graph_state->get_transition()->to_string().c_str()); if (dot_output != nullptr) { if (this->previous_pair_ != 0 && this->previous_pair_ != current_pair->num) { @@ -348,7 +343,7 @@ void LivenessChecker::run() this->previous_request_.clear(); } this->previous_pair_ = current_pair->num; - this->previous_request_ = api::get().request_get_dot_output(aid, req_num); + this->previous_request_ = api::get().request_get_dot_output(current_pair->graph_state->get_transition()); if (current_pair->search_cycle) fprintf(dot_output, "%d [shape=doublecircle];\n", current_pair->num); fflush(dot_output); diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp index 5a8c9380fc..c79f3842f5 100644 --- a/src/mc/checker/SafetyChecker.cpp +++ b/src/mc/checker/SafetyChecker.cpp @@ -128,12 +128,11 @@ void SafetyChecker::run() // If there are processes to interleave and the maximum depth has not been // reached then perform one step of the exploration algorithm. - XBT_DEBUG("Execute: %s", state->get_transition()->to_cstring()); + XBT_DEBUG("Execute: %s", state->get_transition()->to_string().c_str()); std::string req_str; if (dot_output != nullptr) - req_str = - api::get().request_get_dot_output(state->get_transition()->aid_, state->get_transition()->times_considered_); + req_str = api::get().request_get_dot_output(state->get_transition()); /* Create the new expanded state (copy the state of MCed into our MCer data) */ auto next_state = std::make_unique(); @@ -193,13 +192,13 @@ void SafetyChecker::backtrack() for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) { State* prev_state = i->get(); if (state->get_transition()->aid_ == prev_state->get_transition()->aid_) { - XBT_DEBUG("Simcall >>%s<< and >>%s<< with same issuer %ld", state->get_transition()->to_cstring(), - prev_state->get_transition()->to_cstring(), issuer_id); + XBT_DEBUG("Simcall >>%s<< and >>%s<< with same issuer %ld", state->get_transition()->to_string().c_str(), + prev_state->get_transition()->to_string().c_str(), issuer_id); break; } else if (prev_state->get_transition()->depends(state->get_transition())) { XBT_VERB("Dependent Transitions:"); - XBT_VERB(" %s (state=%ld)", prev_state->get_transition()->to_cstring(), prev_state->num_); - XBT_VERB(" %s (state=%ld)", state->get_transition()->to_cstring(), state->num_); + XBT_VERB(" %s (state=%ld)", prev_state->get_transition()->to_string().c_str(), prev_state->num_); + XBT_VERB(" %s (state=%ld)", state->get_transition()->to_string().c_str(), state->num_); if (not prev_state->actor_states_[issuer_id].is_done()) prev_state->mark_todo(issuer_id); @@ -208,8 +207,8 @@ void SafetyChecker::backtrack() break; } else { XBT_VERB("INDEPENDENT Transitions:"); - XBT_VERB(" %s (state=%ld)", prev_state->get_transition()->to_cstring(), prev_state->num_); - XBT_VERB(" %s (state=%ld)", state->get_transition()->to_cstring(), state->num_); + XBT_VERB(" %s (state=%ld)", prev_state->get_transition()->to_string().c_str(), prev_state->num_); + XBT_VERB(" %s (state=%ld)", state->get_transition()->to_string().c_str(), state->num_); } } } diff --git a/src/mc/mc_record.cpp b/src/mc/mc_record.cpp index 2e330d6eb6..c33e7e0201 100644 --- a/src/mc/mc_record.cpp +++ b/src/mc/mc_record.cpp @@ -65,7 +65,7 @@ simgrid::mc::RecordTrace::RecordTrace(const char* data) if(count != 2 && count != 1) throw std::invalid_argument("Could not parse record path"); - push_back(new simgrid::mc::Transition(aid, times_considered)); + push_back(new simgrid::mc::Transition(simgrid::mc::Transition::Type::UNKNOWN, aid, times_considered)); // Find next chunk: const char* end = std::strchr(current, ';'); diff --git a/src/mc/remote/AppSide.cpp b/src/mc/remote/AppSide.cpp index e0026c06af..3517fe193f 100644 --- a/src/mc/remote/AppSide.cpp +++ b/src/mc/remote/AppSide.cpp @@ -110,11 +110,11 @@ void AppSide::handle_simcall_execute(const s_mc_message_simcall_execute_t* messa "The serialized simcall is too large for the buffer. Please fix the code."); strncpy(answer.buffer, stream.str().c_str(), SIMCALL_SERIALIZATION_BUFFER_SIZE); } else { - answer.simcall = kernel::actor::SimcallObserver::Simcall::UNKNOWN; + answer.simcall = mc::Transition::Type::UNKNOWN; } - XBT_DEBUG("send SIMCALL_EXECUTE_ANSWER(%s) ~> %s '%s'", actor->get_cname(), - simgrid::kernel::actor::SimcallObserver::to_c_str(answer.simcall), answer.buffer); + XBT_DEBUG("send SIMCALL_EXECUTE_ANSWER(%s) ~> %s '%s'", actor->get_cname(), mc::Transition::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 @@ -176,24 +176,6 @@ void AppSide::handle_messages() const 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(); - const kernel::actor::ActorImpl* actor = kernel::actor::ActorImpl::by_pid(msg_simcall->aid); - xbt_assert(actor != nullptr, "Invalid pid %ld", msg_simcall->aid); - std::string value = ""; - if (actor->simcall_.observer_ != nullptr) - value = actor->simcall_.observer_->dot_label(msg_simcall->time_considered); - else - value = "UNIMPLEMENTED"; - - // Send result: - 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::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 8def3dabe6..d8915e5aca 100644 --- a/src/mc/remote/mc_protocol.h +++ b/src/mc/remote/mc_protocol.h @@ -32,8 +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_DOT_LABEL, - SIMCALL_DOT_LABEL_ANSWER, ASSERTION_FAILED, ACTOR_ENABLED, ACTOR_ENABLED_REPLY, FINALIZE); + SIMCALL_EXECUTE_ANSWER, SIMCALL_IS_VISIBLE, SIMCALL_IS_VISIBLE_ANSWER, ASSERTION_FAILED, + ACTOR_ENABLED, ACTOR_ENABLED_REPLY, FINALIZE); #define SIMCALL_SERIALIZATION_BUFFER_SIZE 2048 @@ -105,7 +105,7 @@ struct s_mc_message_simcall_execute_t { }; struct s_mc_message_simcall_execute_answer_t { simgrid::mc::MessageType type; - simgrid::kernel::actor::SimcallObserver::Simcall simcall; + simgrid::mc::Transition::Type simcall; char buffer[SIMCALL_SERIALIZATION_BUFFER_SIZE]; }; @@ -129,15 +129,5 @@ 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_DOT_LABEL - simgrid::mc::MessageType type; - aid_t aid; - int time_considered; -}; -struct s_mc_message_simcall_to_string_answer_t { // MessageType::SIMCALL_DOT_LABEL_ANSWER - simgrid::mc::MessageType type; - char value[1024]; -}; - #endif // __cplusplus #endif -- 2.20.1