From e8b892d82b85cf919ae6afe05617ea74e4e0cfbf Mon Sep 17 00:00:00 2001 From: Martin Quinson Date: Fri, 11 Feb 2022 16:54:52 +0100 Subject: [PATCH] Fix builds with/without MC and with/without clang (hopefully) --- MANIFEST.in | 2 + src/kernel/actor/SimcallObserver.hpp | 3 +- src/mc/ModelChecker.cpp | 1 + src/mc/Transition.cpp | 178 ++----------------------- src/mc/Transition.hpp | 50 +------ src/mc/TransitionComm.cpp | 187 +++++++++++++++++++++++++++ src/mc/TransitionComm.hpp | 66 ++++++++++ src/mc/mc_record.cpp | 2 +- tools/cmake/DefinePackages.cmake | 4 +- 9 files changed, 272 insertions(+), 221 deletions(-) create mode 100644 src/mc/TransitionComm.cpp create mode 100644 src/mc/TransitionComm.hpp diff --git a/MANIFEST.in b/MANIFEST.in index 4b721fce06..3c9f6948c5 100644 --- a/MANIFEST.in +++ b/MANIFEST.in @@ -2337,6 +2337,8 @@ include src/mc/Session.cpp include src/mc/Session.hpp include src/mc/Transition.cpp include src/mc/Transition.hpp +include src/mc/TransitionComm.cpp +include src/mc/TransitionComm.hpp include src/mc/VisitedState.cpp include src/mc/VisitedState.hpp include src/mc/api.cpp diff --git a/src/kernel/actor/SimcallObserver.hpp b/src/kernel/actor/SimcallObserver.hpp index 29642013de..c3ae91bd8b 100644 --- a/src/kernel/actor/SimcallObserver.hpp +++ b/src/kernel/actor/SimcallObserver.hpp @@ -22,7 +22,6 @@ class SimcallObserver { 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. @@ -213,7 +212,7 @@ public: { } SimcallObserver* clone() override { return new ActivityWaitSimcall(get_issuer(), activity_, timeout_); } - void serialize(Simcall& type, char* buffer); + void serialize(Simcall& type, char* buffer) override; bool is_visible() const override { return true; } bool is_enabled() const override; std::string dot_label(int times_considered) const override; diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp index b2a8f146c4..a753c9d3fa 100644 --- a/src/mc/ModelChecker.cpp +++ b/src/mc/ModelChecker.cpp @@ -6,6 +6,7 @@ #include "src/mc/ModelChecker.hpp" #include "src/mc/Session.hpp" #include "src/mc/Transition.hpp" +#include "src/mc/TransitionComm.hpp" #include "src/mc/checker/Checker.hpp" #include "src/mc/mc_config.hpp" #include "src/mc/mc_exit.hpp" diff --git a/src/mc/Transition.cpp b/src/mc/Transition.cpp index 28779c347d..134452e310 100644 --- a/src/mc/Transition.cpp +++ b/src/mc/Transition.cpp @@ -4,11 +4,12 @@ * under the terms of the license (GNU LGPL) which comes with this package. */ #include "src/mc/Transition.hpp" -#include "src/mc/ModelChecker.hpp" -#include "src/mc/Session.hpp" -#include "src/mc/mc_state.hpp" -#include "src/mc/remote/RemoteProcess.hpp" +#include "src/mc/TransitionComm.hpp" #include "xbt/asserts.h" +#include +#if SIMGRID_HAVE_MC +#include "src/mc/ModelChecker.hpp" +#endif #include @@ -19,16 +20,15 @@ namespace mc { unsigned long Transition::executed_transitions_ = 0; unsigned long Transition::replayed_transitions_ = 0; +Transition::~Transition() { +} // Make sure that we have a vtable for Transition by putting this virtual function out of the header + 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(bool verbose) { - xbt_assert(mc_model_checker != nullptr, "Must be called from MCer"); - to_string(); return textual_.c_str(); } @@ -41,170 +41,10 @@ void Transition::replay() const { replayed_transitions_++; +#if SIMGRID_HAVE_MC 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_; - 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) -{ - textual_ = 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_); - } - textual_ += ")"; - return textual_; -} -bool CommWaitTransition::depends(const Transition* other) const -{ - if (aid_ == other->aid_) - return false; - - if (auto* send = dynamic_cast(other)) - return send->depends(this); - - if (auto* recv = dynamic_cast(other)) - return recv->depends(this); - - /* Timeouts in wait transitions are not considered by the independence theorem, thus assumed dependent */ - if (const auto* wait = dynamic_cast(other)) { - if (timeout_ || wait->timeout_) - return true; - - if (src_buff_ == wait->src_buff_ && dst_buff_ == wait->dst_buff_) - return false; - if (src_buff_ != nullptr && dst_buff_ != nullptr && wait->src_buff_ != nullptr && wait->dst_buff_ != nullptr && - dst_buff_ != wait->src_buff_ && dst_buff_ != wait->dst_buff_ && dst_buff_ != src_buff_) - return false; - } - - return true; -} - -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("%ld: iRecv(mbox=%u", aid_, mbox_); - if (verbose) - textual_ += ", buff=" + xbt::string_printf("%p", dst_buff_); - textual_ += ")"; - return textual_; -} -bool CommRecvTransition::depends(const Transition* other) const -{ - if (aid_ == other->aid_) - return false; - - if (const auto* other_irecv = dynamic_cast(other)) - return mbox_ == other_irecv->mbox_; - - if (auto* isend = dynamic_cast(other)) - return isend->depends(this); - - if (auto* wait = dynamic_cast(other)) { - if (wait->timeout_) - return true; - - if (mbox_ != wait->mbox_) - return false; - - if ((aid_ != wait->sender_) && (aid_ != wait->receiver_)) - return false; - - if (wait->dst_buff_ != dst_buff_) - return false; - } - - /* FIXME: the following rule assumes that the result of the isend/irecv call is not stored in a buffer used in the - * test call. */ -#if 0 - if (dynamic_cast(other)) - return false; #endif - - return true; -} - -CommSendTransition::CommSendTransition(aid_t issuer, int times_considered, char* buffer) - : Transition(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) -{ - textual_ = 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_; -} -bool CommSendTransition::depends(const Transition* other) const -{ - if (aid_ == other->aid_) - return false; - - if (const auto* other_isend = dynamic_cast(other)) - return mbox_ == other_isend->mbox_; - - // FIXME: Not in the former dependency check because of the ordering but seems logical to add it - if (dynamic_cast(other) != nullptr) - return false; - - if (const auto* wait = dynamic_cast(other)) { - if (wait->timeout_) - return true; - - if (mbox_ != wait->mbox_) - return false; - - if ((aid_ != wait->sender_) && (aid_ != wait->receiver_)) - return false; - - if (wait->src_buff_ != src_buff_) - return false; - } - - /* FIXME: the following rule assumes that the result of the isend/irecv call is not stored in a buffer used in the - * test call. */ -#if 0 - if (dynamic_cast(other)) - return false; -#endif - - return true; -} - -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 3ec28b26f1..856da0a2d9 100644 --- a/src/mc/Transition.hpp +++ b/src/mc/Transition.hpp @@ -8,8 +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 namespace simgrid { @@ -47,6 +46,7 @@ public: int times_considered_ = 0; Transition() = default; + virtual ~Transition(); Transition(aid_t issuer, int times_considered) : aid_(issuer), times_considered_(times_considered) {} void init(aid_t aid, int times_considered); @@ -65,52 +65,6 @@ public: static unsigned long get_replayed_transitions() { return replayed_transitions_; } }; -class CommSendTransition; -class CommRecvTransition; - -class CommWaitTransition : public Transition { - bool timeout_; - void* comm_; - aid_t sender_; - aid_t receiver_; - unsigned mbox_; - void* src_buff_; - void* dst_buff_; - size_t size_; - friend CommSendTransition; - friend CommRecvTransition; - -public: - CommWaitTransition(aid_t issuer, int times_considered, char* buffer); - std::string to_string(bool verbose) override; - bool depends(const Transition* other) const 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; - bool depends(const Transition* other) const 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; - 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); - } // namespace mc } // namespace simgrid diff --git a/src/mc/TransitionComm.cpp b/src/mc/TransitionComm.cpp new file mode 100644 index 0000000000..e40f6ccb71 --- /dev/null +++ b/src/mc/TransitionComm.cpp @@ -0,0 +1,187 @@ +/* Copyright (c) 2015-2022. The SimGrid Team. All rights reserved. */ + +/* This program is free software; you can redistribute it and/or modify it + * under the terms of the license (GNU LGPL) which comes with this package. */ + +#include "src/mc/TransitionComm.hpp" +#include "src/mc/Transition.hpp" +#include "xbt/asserts.h" +#include +#if SIMGRID_HAVE_MC +#include "src/mc/ModelChecker.hpp" +#include "src/mc/Session.hpp" +#include "src/mc/mc_state.hpp" +#endif + +#include + +XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_trans_comm, mc_transition, + "Logging specific to MC transitions about communications"); + +namespace simgrid { +namespace mc { + +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_; + 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) +{ + textual_ = 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_); + } + textual_ += ")"; + return textual_; +} +bool CommWaitTransition::depends(const Transition* other) const +{ + if (aid_ == other->aid_) + return false; + + if (auto* send = dynamic_cast(other)) + return send->depends(this); + + if (auto* recv = dynamic_cast(other)) + return recv->depends(this); + + /* Timeouts in wait transitions are not considered by the independence theorem, thus assumed dependent */ + if (const auto* wait = dynamic_cast(other)) { + if (timeout_ || wait->timeout_) + return true; + + if (src_buff_ == wait->src_buff_ && dst_buff_ == wait->dst_buff_) + return false; + if (src_buff_ != nullptr && dst_buff_ != nullptr && wait->src_buff_ != nullptr && wait->dst_buff_ != nullptr && + dst_buff_ != wait->src_buff_ && dst_buff_ != wait->dst_buff_ && dst_buff_ != src_buff_) + return false; + } + + return true; +} + +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("%ld: iRecv(mbox=%u", aid_, mbox_); + if (verbose) + textual_ += ", buff=" + xbt::string_printf("%p", dst_buff_); + textual_ += ")"; + return textual_; +} +bool CommRecvTransition::depends(const Transition* other) const +{ + if (aid_ == other->aid_) + return false; + + if (const auto* other_irecv = dynamic_cast(other)) + return mbox_ == other_irecv->mbox_; + + if (auto* isend = dynamic_cast(other)) + return isend->depends(this); + + if (auto* wait = dynamic_cast(other)) { + if (wait->timeout_) + return true; + + if (mbox_ != wait->mbox_) + return false; + + if ((aid_ != wait->sender_) && (aid_ != wait->receiver_)) + return false; + + if (wait->dst_buff_ != dst_buff_) + return false; + } + + /* FIXME: the following rule assumes that the result of the isend/irecv call is not stored in a buffer used in the + * test call. */ +#if 0 + if (dynamic_cast(other)) + return false; +#endif + + return true; +} + +CommSendTransition::CommSendTransition(aid_t issuer, int times_considered, char* buffer) + : Transition(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) +{ + textual_ = 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_; +} +bool CommSendTransition::depends(const Transition* other) const +{ + if (aid_ == other->aid_) + return false; + + if (const auto* other_isend = dynamic_cast(other)) + return mbox_ == other_isend->mbox_; + + // FIXME: Not in the former dependency check because of the ordering but seems logical to add it + if (dynamic_cast(other) != nullptr) + return false; + + if (const auto* wait = dynamic_cast(other)) { + if (wait->timeout_) + return true; + + if (mbox_ != wait->mbox_) + return false; + + if ((aid_ != wait->sender_) && (aid_ != wait->receiver_)) + return false; + + if (wait->src_buff_ != src_buff_) + return false; + } + + /* FIXME: the following rule assumes that the result of the isend/irecv call is not stored in a buffer used in the + * test call. */ +#if 0 + if (dynamic_cast(other)) + return false; +#endif + + return true; +} + +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 +} // namespace simgrid diff --git a/src/mc/TransitionComm.hpp b/src/mc/TransitionComm.hpp new file mode 100644 index 0000000000..8c6f57c6c6 --- /dev/null +++ b/src/mc/TransitionComm.hpp @@ -0,0 +1,66 @@ +/* Copyright (c) 2015-2022. The SimGrid Team. + * All rights reserved. */ + +/* This program is free software; you can redistribute it and/or modify it + * under the terms of the license (GNU LGPL) which comes with this package. */ + +#ifndef SIMGRID_MC_TRANSITION_COMM_HPP +#define SIMGRID_MC_TRANSITION_COMM_HPP + +#include "simgrid/forward.h" // aid_t +#include "src/kernel/actor/SimcallObserver.hpp" +#include + +namespace simgrid { +namespace mc { + +class CommSendTransition; +class CommRecvTransition; + +class CommWaitTransition : public Transition { + bool timeout_; + void* comm_; + aid_t sender_; + aid_t receiver_; + unsigned mbox_; + void* src_buff_; + void* dst_buff_; + size_t size_; + friend CommSendTransition; + friend CommRecvTransition; + +public: + CommWaitTransition(aid_t issuer, int times_considered, char* buffer); + std::string to_string(bool verbose) override; + bool depends(const Transition* other) const 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; + bool depends(const Transition* other) const 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; + 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); + +} // namespace mc +} // namespace simgrid + +#endif diff --git a/src/mc/mc_record.cpp b/src/mc/mc_record.cpp index ec97313473..02522b06cc 100644 --- a/src/mc/mc_record.cpp +++ b/src/mc/mc_record.cpp @@ -87,7 +87,7 @@ std::string traceToString(simgrid::mc::RecordTrace const& trace) if (i != trace.begin()) stream << ';'; stream << i->aid_; - if (i->times_considered_) + if (i->times_considered_ > 0) stream << '/' << i->times_considered_; } return stream.str(); diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake index db341ce05d..b4de54e65a 100644 --- a/tools/cmake/DefinePackages.cmake +++ b/tools/cmake/DefinePackages.cmake @@ -552,6 +552,7 @@ set(MC_SRC_BASE src/mc/mc_config.cpp src/mc/mc_config.hpp src/mc/mc_global.cpp + src/mc/Transition.cpp ) set(MC_SRC @@ -628,8 +629,9 @@ set(MC_SRC src/mc/mc_client_api.cpp src/mc/mc_smx.cpp src/mc/mc_exit.hpp - src/mc/Transition.cpp src/mc/Transition.hpp + src/mc/TransitionComm.cpp + src/mc/TransitionComm.hpp src/mc/udpor_global.cpp src/mc/udpor_global.hpp ) -- 2.20.1