From e01a8f10de51f1d10f5ee7529c201d132e630904 Mon Sep 17 00:00:00 2001 From: eazimi Date: Mon, 25 Jan 2021 16:08:31 +0100 Subject: [PATCH] simcall_check_dependency() defined and implemented --- src/mc/checker/SafetyChecker.cpp | 2 +- src/mc/mc_api.cpp | 34 +++++++- src/mc/mc_api.hpp | 2 +- src/mc/mc_request.cpp | 130 ------------------------------- src/mc/mc_request.hpp | 2 - 5 files changed, 34 insertions(+), 136 deletions(-) diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp index 4f6b149c47..b28094196b 100644 --- a/src/mc/checker/SafetyChecker.cpp +++ b/src/mc/checker/SafetyChecker.cpp @@ -200,7 +200,7 @@ void SafetyChecker::backtrack() const kernel::actor::ActorImpl* issuer = mcapi::get().simcall_get_issuer(req); for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) { State* prev_state = i->get(); - if (mcapi::get().request_depend(req, &prev_state->internal_req_)) { + if (mcapi::get().simcall_check_dependency(req, &prev_state->internal_req_)) { if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) { XBT_DEBUG("Dependent Transitions:"); int value = prev_state->transition_.argument_; diff --git a/src/mc/mc_api.cpp b/src/mc/mc_api.cpp index cb5578c6b2..33cc69249d 100644 --- a/src/mc/mc_api.cpp +++ b/src/mc/mc_api.cpp @@ -566,9 +566,39 @@ smx_simcall_t mc_api::mc_state_choose_request(simgrid::mc::State* state) const return nullptr; } -bool mc_api::request_depend(smx_simcall_t req1, smx_simcall_t req2) const +bool mc_api::simcall_check_dependency(smx_simcall_t const req1, smx_simcall_t const req2) const { - return simgrid::mc::request_depend(req1, req2); + if (req1->issuer_ == req2->issuer_) + return false; + + /* Wait with timeout transitions are not considered by the independence theorem, thus we consider them as dependent with all other transitions */ + if ((req1->call_ == Simcall::COMM_WAIT && simcall_comm_wait__get__timeout(req1) > 0) || + (req2->call_ == Simcall::COMM_WAIT && simcall_comm_wait__get__timeout(req2) > 0)) + return true; + + if (req1->call_ != req2->call_) + return request_depend_asymmetric(req1, req2) && request_depend_asymmetric(req2, req1); + + // Those are internal requests, we do not need indirection because those objects are copies: + const kernel::activity::CommImpl* synchro1 = get_comm(req1); + const kernel::activity::CommImpl* synchro2 = get_comm(req2); + + switch (req1->call_) { + case Simcall::COMM_ISEND: + return simcall_comm_isend__get__mbox(req1) == simcall_comm_isend__get__mbox(req2); + case Simcall::COMM_IRECV: + return simcall_comm_irecv__get__mbox(req1) == simcall_comm_irecv__get__mbox(req2); + case Simcall::COMM_WAIT: + if (synchro1->src_buff_ == synchro2->src_buff_ && synchro1->dst_buff_ == synchro2->dst_buff_) + return false; + if (synchro1->src_buff_ != nullptr && synchro1->dst_buff_ != nullptr && synchro2->src_buff_ != nullptr && + synchro2->dst_buff_ != nullptr && synchro1->dst_buff_ != synchro2->src_buff_ && + synchro1->dst_buff_ != synchro2->dst_buff_ && synchro2->dst_buff_ != synchro1->src_buff_) + return false; + return true; + default: + return true; + } } std::string mc_api::request_to_string(smx_simcall_t req, int value, RequestType request_type) const diff --git a/src/mc/mc_api.hpp b/src/mc/mc_api.hpp index d2e218fc5c..99b51f571e 100644 --- a/src/mc/mc_api.hpp +++ b/src/mc/mc_api.hpp @@ -93,7 +93,6 @@ public: smx_simcall_t mc_state_choose_request(simgrid::mc::State* state) const; // SIMCALL APIs - bool request_depend(smx_simcall_t req1, smx_simcall_t req2) const; std::string request_to_string(smx_simcall_t req, int value, RequestType request_type) const; std::string request_get_dot_output(smx_simcall_t req, int value) const; const char *simcall_get_name(simgrid::simix::Simcall kind) const; @@ -101,6 +100,7 @@ public: long simcall_get_actor_id(s_smx_simcall const* req) const; smx_mailbox_t simcall_get_mbox(smx_simcall_t const req) const; simgrid::kernel::activity::CommImpl* simcall_get_comm(smx_simcall_t const req) const; + bool simcall_check_dependency(smx_simcall_t const req1, smx_simcall_t const req2) const; #if HAVE_SMPI int get_smpi_request_tag(smx_simcall_t const& simcall, simgrid::simix::Simcall type) const; diff --git a/src/mc/mc_request.cpp b/src/mc/mc_request.cpp index 6a1c4a7a11..84219c7bef 100644 --- a/src/mc/mc_request.cpp +++ b/src/mc/mc_request.cpp @@ -17,136 +17,6 @@ using simgrid::simix::Simcall; XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_request, mc, "Logging specific to MC (request)"); -static inline simgrid::kernel::activity::CommImpl* MC_get_comm(smx_simcall_t r) -{ - switch (r->call_) { - case Simcall::COMM_WAIT: - return simcall_comm_wait__getraw__comm(r); - case Simcall::COMM_TEST: - return simcall_comm_test__getraw__comm(r); - default: - return nullptr; - } -} - -static inline -smx_mailbox_t MC_get_mbox(smx_simcall_t r) -{ - switch (r->call_) { - case Simcall::COMM_ISEND: - return simcall_comm_isend__get__mbox(r); - case Simcall::COMM_IRECV: - return simcall_comm_irecv__get__mbox(r); - default: - return nullptr; - } -} - -namespace simgrid { -namespace mc { - -// Does half the job -static inline -bool request_depend_asymmetric(smx_simcall_t r1, smx_simcall_t r2) -{ - if (r1->call_ == Simcall::COMM_ISEND && r2->call_ == Simcall::COMM_IRECV) - return false; - - if (r1->call_ == Simcall::COMM_IRECV && r2->call_ == Simcall::COMM_ISEND) - return false; - - // Those are internal requests, we do not need indirection because those objects are copies: - const kernel::activity::CommImpl* synchro1 = MC_get_comm(r1); - const kernel::activity::CommImpl* synchro2 = MC_get_comm(r2); - - if ((r1->call_ == Simcall::COMM_ISEND || r1->call_ == Simcall::COMM_IRECV) && r2->call_ == Simcall::COMM_WAIT) { - const kernel::activity::MailboxImpl* mbox = MC_get_mbox(r1); - - if (mbox != synchro2->mbox_cpy - && simcall_comm_wait__get__timeout(r2) <= 0) - return false; - - if ((r1->issuer_ != synchro2->src_actor_.get()) && (r1->issuer_ != synchro2->dst_actor_.get()) && - simcall_comm_wait__get__timeout(r2) <= 0) - return false; - - if ((r1->call_ == Simcall::COMM_ISEND) && (synchro2->type_ == kernel::activity::CommImpl::Type::SEND) && - (synchro2->src_buff_ != simcall_comm_isend__get__src_buff(r1)) && simcall_comm_wait__get__timeout(r2) <= 0) - return false; - - if ((r1->call_ == Simcall::COMM_IRECV) && (synchro2->type_ == kernel::activity::CommImpl::Type::RECEIVE) && - (synchro2->dst_buff_ != simcall_comm_irecv__get__dst_buff(r1)) && simcall_comm_wait__get__timeout(r2) <= 0) - 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((r1->call == Simcall::COMM_ISEND || r1->call == Simcall::COMM_IRECV) - && r2->call == Simcall::COMM_TEST) - return false; -#endif - - if (r1->call_ == Simcall::COMM_WAIT && (r2->call_ == Simcall::COMM_WAIT || r2->call_ == Simcall::COMM_TEST) && - (synchro1->src_actor_.get() == nullptr || synchro1->dst_actor_.get() == nullptr)) - return false; - - if (r1->call_ == Simcall::COMM_TEST && - (simcall_comm_test__get__comm(r1) == nullptr || synchro1->src_buff_ == nullptr || synchro1->dst_buff_ == nullptr)) - return false; - - if (r1->call_ == Simcall::COMM_TEST && r2->call_ == Simcall::COMM_WAIT && - synchro1->src_buff_ == synchro2->src_buff_ && synchro1->dst_buff_ == synchro2->dst_buff_) - return false; - - if (r1->call_ == Simcall::COMM_WAIT && r2->call_ == Simcall::COMM_TEST && synchro1->src_buff_ != nullptr && - synchro1->dst_buff_ != nullptr && synchro2->src_buff_ != nullptr && synchro2->dst_buff_ != nullptr && - synchro1->dst_buff_ != synchro2->src_buff_ && synchro1->dst_buff_ != synchro2->dst_buff_ && - synchro2->dst_buff_ != synchro1->src_buff_) - return false; - - return true; -} - -// Those are internal_req -bool request_depend(smx_simcall_t req1, smx_simcall_t req2) -{ - if (req1->issuer_ == req2->issuer_) - return false; - - /* Wait with timeout transitions are not considered by the independence theorem, thus we consider them as dependent with all other transitions */ - if ((req1->call_ == Simcall::COMM_WAIT && simcall_comm_wait__get__timeout(req1) > 0) || - (req2->call_ == Simcall::COMM_WAIT && simcall_comm_wait__get__timeout(req2) > 0)) - return true; - - if (req1->call_ != req2->call_) - return request_depend_asymmetric(req1, req2) && request_depend_asymmetric(req2, req1); - - // Those are internal requests, we do not need indirection because those objects are copies: - const kernel::activity::CommImpl* synchro1 = MC_get_comm(req1); - const kernel::activity::CommImpl* synchro2 = MC_get_comm(req2); - - switch (req1->call_) { - case Simcall::COMM_ISEND: - return simcall_comm_isend__get__mbox(req1) == simcall_comm_isend__get__mbox(req2); - case Simcall::COMM_IRECV: - return simcall_comm_irecv__get__mbox(req1) == simcall_comm_irecv__get__mbox(req2); - case Simcall::COMM_WAIT: - if (synchro1->src_buff_ == synchro2->src_buff_ && synchro1->dst_buff_ == synchro2->dst_buff_) - return false; - if (synchro1->src_buff_ != nullptr && synchro1->dst_buff_ != nullptr && synchro2->src_buff_ != nullptr && - synchro2->dst_buff_ != nullptr && synchro1->dst_buff_ != synchro2->src_buff_ && - synchro1->dst_buff_ != synchro2->dst_buff_ && synchro2->dst_buff_ != synchro1->src_buff_) - return false; - return true; - default: - return true; - } -} - -} // namespace mc -} // namespace simgrid - namespace simgrid { namespace mc { diff --git a/src/mc/mc_request.hpp b/src/mc/mc_request.hpp index 92686b8fc7..ca980d7a18 100644 --- a/src/mc/mc_request.hpp +++ b/src/mc/mc_request.hpp @@ -17,8 +17,6 @@ enum class RequestType { internal, }; -XBT_PRIVATE bool request_depend(smx_simcall_t req1, smx_simcall_t req2); - XBT_PRIVATE bool request_is_enabled_by_idx(smx_simcall_t req, unsigned int idx); } } -- 2.30.2