From: Ehsan Azimi Date: Mon, 30 Nov 2020 16:34:23 +0000 (+0100) Subject: handle_comm_pattern() defined in CommunicationDeterminismChecker class, X-Git-Tag: v3.26~72^2^2~11 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/e6dcda80c72f6c1c092cf257c308812fe4442599 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() --- 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