From e6dcda80c72f6c1c092cf257c308812fe4442599 Mon Sep 17 00:00:00 2001 From: Ehsan Azimi Date: Mon, 30 Nov 2020 17:34:23 +0100 Subject: [PATCH] handle_comm_pattern() defined in CommunicationDeterminismChecker class, mc_api::get_comm_wait_raw_addr() and mc_api::get_comm_waitany_raw_addr() are used in handle_comm_pattern() --- .../CommunicationDeterminismChecker.cpp | 29 ++++++++++++++-- .../CommunicationDeterminismChecker.hpp | 1 + src/mc/mc_comm_pattern.cpp | 33 +------------------ src/mc/mc_comm_pattern.hpp | 3 -- 4 files changed, 29 insertions(+), 37 deletions(-) diff --git a/src/mc/checker/CommunicationDeterminismChecker.cpp b/src/mc/checker/CommunicationDeterminismChecker.cpp index 42e0f62613..4b56822d56 100644 --- a/src/mc/checker/CommunicationDeterminismChecker.cpp +++ b/src/mc/checker/CommunicationDeterminismChecker.cpp @@ -372,7 +372,7 @@ void CommunicationDeterminismChecker::restoreState() /* TODO : handle test and testany simcalls */ CallType call = MC_get_call_type(req); mcapi::get().handle_simcall(state->transition_); - MC_handle_comm_pattern(call, req, req_num, 1); + handle_comm_pattern(call, req, req_num, 1); mcapi::get().mc_wait_for_requests(); /* Update statistics */ @@ -381,6 +381,31 @@ void CommunicationDeterminismChecker::restoreState() } } +void CommunicationDeterminismChecker::handle_comm_pattern(simgrid::mc::CallType call_type, smx_simcall_t req, int value, int backtracking) +{ + using simgrid::mc::CallType; + switch(call_type) { + case CallType::NONE: + break; + case CallType::SEND: + case CallType::RECV: + get_comm_pattern(req, call_type, backtracking); + break; + case CallType::WAIT: + case CallType::WAITANY: { + simgrid::mc::RemotePtr comm_addr{nullptr}; + if (call_type == CallType::WAIT) + comm_addr = mcapi::get().get_comm_wait_raw_addr(req); + else + comm_addr = mcapi::get().get_comm_waitany_raw_addr(req, value); + auto simcall_issuer = mcapi::get().simcall_get_issuer(req); + complete_comm_pattern(comm_addr, simcall_issuer->get_pid(), backtracking); + } break; + default: + xbt_die("Unexpected call type %i", (int)call_type); + } +} + void CommunicationDeterminismChecker::real_run() { std::unique_ptr visited_state = nullptr; @@ -422,7 +447,7 @@ void CommunicationDeterminismChecker::real_run() mcapi::get().handle_simcall(cur_state->transition_); /* After this call req is no longer useful */ - MC_handle_comm_pattern(call, req, req_num, 0); + handle_comm_pattern(call, req, req_num, 0); /* Wait for requests (schedules processes) */ mcapi::get().mc_wait_for_requests(); diff --git a/src/mc/checker/CommunicationDeterminismChecker.hpp b/src/mc/checker/CommunicationDeterminismChecker.hpp index 3d3a91029c..c8ca066264 100644 --- a/src/mc/checker/CommunicationDeterminismChecker.hpp +++ b/src/mc/checker/CommunicationDeterminismChecker.hpp @@ -30,6 +30,7 @@ private: void log_state() override; void deterministic_comm_pattern(int process, const PatternCommunication* comm, int backtracking); void restoreState(); + void handle_comm_pattern(simgrid::mc::CallType call_type, smx_simcall_t req, int value, int backtracking); public: // These are used by functions which should be moved in CommunicationDeterminismChecker: diff --git a/src/mc/mc_comm_pattern.cpp b/src/mc/mc_comm_pattern.cpp index 7dd9704a95..e3ead2ce10 100644 --- a/src/mc/mc_comm_pattern.cpp +++ b/src/mc/mc_comm_pattern.cpp @@ -27,35 +27,4 @@ void MC_restore_communications_pattern(simgrid::mc::State* state) for (unsigned i = 0; i < MC_smx_get_maxpid(); i++) MC_patterns_copy(incomplete_communications_pattern[i], state->incomplete_comm_pattern_[i]); -} - -void MC_handle_comm_pattern(simgrid::mc::CallType call_type, smx_simcall_t req, int value, int backtracking) -{ - // HACK, do not rely on the Checker implementation outside of it - auto* checker = static_cast(mc_model_checker->getChecker()); - - using simgrid::mc::CallType; - switch(call_type) { - case CallType::NONE: - break; - case CallType::SEND: - case CallType::RECV: - checker->get_comm_pattern(req, call_type, backtracking); - break; - case CallType::WAIT: - case CallType::WAITANY: { - simgrid::mc::RemotePtr comm_addr{nullptr}; - if (call_type == CallType::WAIT) - comm_addr = remote(simcall_comm_wait__getraw__comm(req)); - - else { - simgrid::kernel::activity::ActivityImpl* addr; - addr = mc_model_checker->get_remote_simulation().read(remote(simcall_comm_waitany__getraw__comms(req) + value)); - comm_addr = remote(static_cast(addr)); - } - checker->complete_comm_pattern(comm_addr, MC_smx_simcall_get_issuer(req)->get_pid(), backtracking); - } break; - default: - xbt_die("Unexpected call type %i", (int)call_type); - } -} +} \ No newline at end of file diff --git a/src/mc/mc_comm_pattern.hpp b/src/mc/mc_comm_pattern.hpp index a408136ee7..ca221ea58d 100644 --- a/src/mc/mc_comm_pattern.hpp +++ b/src/mc/mc_comm_pattern.hpp @@ -61,9 +61,6 @@ static inline simgrid::mc::CallType MC_get_call_type(const s_smx_simcall* req) } } -XBT_PRIVATE void MC_handle_comm_pattern(simgrid::mc::CallType call_type, smx_simcall_t request, int value, - int backtracking); - XBT_PRIVATE void MC_restore_communications_pattern(simgrid::mc::State* state); #endif -- 2.20.1