From 9ae8726744b95dd29d8a68ddc3010781ef09a502 Mon Sep 17 00:00:00 2001 From: Arnaud Giersch Date: Wed, 18 Nov 2020 21:23:15 +0100 Subject: [PATCH] Enum class for MC call types, and MC comm pattern differences. --- .../CommunicationDeterminismChecker.cpp | 87 ++++++++++--------- .../CommunicationDeterminismChecker.hpp | 2 +- src/mc/mc_comm_pattern.cpp | 37 ++++---- src/mc/mc_comm_pattern.hpp | 58 +++++++------ 4 files changed, 93 insertions(+), 91 deletions(-) diff --git a/src/mc/checker/CommunicationDeterminismChecker.cpp b/src/mc/checker/CommunicationDeterminismChecker.cpp index d94b12ad28..e90478fc3e 100644 --- a/src/mc/checker/CommunicationDeterminismChecker.cpp +++ b/src/mc/checker/CommunicationDeterminismChecker.cpp @@ -29,27 +29,28 @@ std::vector> incomplete_communic /********** Static functions ***********/ -static e_mc_comm_pattern_difference_t compare_comm_pattern(const simgrid::mc::PatternCommunication* comm1, - const simgrid::mc::PatternCommunication* comm2) +static simgrid::mc::CommPatternDifference compare_comm_pattern(const simgrid::mc::PatternCommunication* comm1, + const simgrid::mc::PatternCommunication* comm2) { + using simgrid::mc::CommPatternDifference; if(comm1->type != comm2->type) - return TYPE_DIFF; + return CommPatternDifference::TYPE; if (comm1->rdv != comm2->rdv) - return RDV_DIFF; + return CommPatternDifference::RDV; if (comm1->src_proc != comm2->src_proc) - return SRC_PROC_DIFF; + return CommPatternDifference::SRC_PROC; if (comm1->dst_proc != comm2->dst_proc) - return DST_PROC_DIFF; + return CommPatternDifference::DST_PROC; if (comm1->tag != comm2->tag) - return TAG_DIFF; + return CommPatternDifference::TAG; if (comm1->data.size() != comm2->data.size()) - return DATA_SIZE_DIFF; + return CommPatternDifference::DATA_SIZE; if (comm1->data != comm2->data) - return DATA_DIFF; - return NONE_DIFF; + return CommPatternDifference::DATA; + return CommPatternDifference::NONE; } -static char* print_determinism_result(e_mc_comm_pattern_difference_t diff, int process, +static char* print_determinism_result(simgrid::mc::CommPatternDifference diff, int process, const simgrid::mc::PatternCommunication* comm, unsigned int cursor) { char* type; @@ -60,31 +61,32 @@ static char* print_determinism_result(e_mc_comm_pattern_difference_t diff, int p else type = bprintf("The recv communications pattern of the process %d is different!", process - 1); + using simgrid::mc::CommPatternDifference; switch(diff) { - case TYPE_DIFF: - res = bprintf("%s Different type for communication #%u", type, cursor); - break; - case RDV_DIFF: - res = bprintf("%s Different rdv for communication #%u", type, cursor); - break; - case TAG_DIFF: - res = bprintf("%s Different tag for communication #%u", type, cursor); - break; - case SRC_PROC_DIFF: - res = bprintf("%s Different source for communication #%u", type, cursor); - break; - case DST_PROC_DIFF: - res = bprintf("%s Different destination for communication #%u", type, cursor); - break; - case DATA_SIZE_DIFF: - res = bprintf("%s Different data size for communication #%u", type, cursor); - break; - case DATA_DIFF: - res = bprintf("%s Different data for communication #%u", type, cursor); - break; - default: - res = nullptr; - break; + case CommPatternDifference::TYPE: + res = bprintf("%s Different type for communication #%u", type, cursor); + break; + case CommPatternDifference::RDV: + res = bprintf("%s Different rdv for communication #%u", type, cursor); + break; + case CommPatternDifference::TAG: + res = bprintf("%s Different tag for communication #%u", type, cursor); + break; + case CommPatternDifference::SRC_PROC: + res = bprintf("%s Different source for communication #%u", type, cursor); + break; + case CommPatternDifference::DST_PROC: + res = bprintf("%s Different destination for communication #%u", type, cursor); + break; + case CommPatternDifference::DATA_SIZE: + res = bprintf("%s Different data size for communication #%u", type, cursor); + break; + case CommPatternDifference::DATA: + res = bprintf("%s Different data for communication #%u", type, cursor); + break; + default: + res = nullptr; + break; } return res; @@ -123,9 +125,9 @@ void CommunicationDeterminismChecker::deterministic_comm_pattern(int process, co { if (not backtracking) { PatternCommunicationList& list = initial_communications_pattern[process]; - e_mc_comm_pattern_difference_t diff = compare_comm_pattern(list.list[list.index_comm].get(), comm); + CommPatternDifference diff = compare_comm_pattern(list.list[list.index_comm].get(), comm); - if (diff != NONE_DIFF) { + if (diff != CommPatternDifference::NONE) { if (comm->type == PatternCommunicationType::send) { this->send_deterministic = false; if (this->send_diff != nullptr) @@ -169,8 +171,7 @@ void CommunicationDeterminismChecker::deterministic_comm_pattern(int process, co /********** Non Static functions ***********/ -void CommunicationDeterminismChecker::get_comm_pattern(smx_simcall_t request, e_mc_call_type_t call_type, - int backtracking) +void CommunicationDeterminismChecker::get_comm_pattern(smx_simcall_t request, CallType call_type, int backtracking) { const smx_actor_t issuer = MC_smx_simcall_get_issuer(request); const mc::PatternCommunicationList& initial_pattern = initial_communications_pattern[issuer->get_pid()]; @@ -179,7 +180,7 @@ void CommunicationDeterminismChecker::get_comm_pattern(smx_simcall_t request, e_ auto pattern = std::make_unique(); pattern->index = initial_pattern.index_comm + incomplete_pattern.size(); - if (call_type == MC_CALL_TYPE_SEND) { + if (call_type == CallType::SEND) { /* Create comm pattern */ pattern->type = PatternCommunicationType::send; pattern->comm_addr = static_cast(simcall_comm_isend__getraw__result(request)); @@ -220,7 +221,7 @@ void CommunicationDeterminismChecker::get_comm_pattern(smx_simcall_t request, e_ return; } #endif - } else if (call_type == MC_CALL_TYPE_RECV) { + } else if (call_type == CallType::RECV) { pattern->type = PatternCommunicationType::receive; pattern->comm_addr = static_cast(simcall_comm_irecv__getraw__result(request)); @@ -394,7 +395,7 @@ void CommunicationDeterminismChecker::restoreState() smx_simcall_t req = &issuer->simcall_; /* TODO : handle test and testany simcalls */ - e_mc_call_type_t call = MC_get_call_type(req); + CallType call = MC_get_call_type(req); mc_model_checker->handle_simcall(state->transition_); MC_handle_comm_pattern(call, req, req_num, 1); mc_model_checker->wait_for_requests(); @@ -438,7 +439,7 @@ void CommunicationDeterminismChecker::real_run() mc_model_checker->executed_transitions++; /* TODO : handle test and testany simcalls */ - e_mc_call_type_t call = MC_CALL_TYPE_NONE; + CallType call = CallType::NONE; if (_sg_mc_comms_determinism || _sg_mc_send_determinism) call = MC_get_call_type(req); diff --git a/src/mc/checker/CommunicationDeterminismChecker.hpp b/src/mc/checker/CommunicationDeterminismChecker.hpp index 01daeee88a..3d3a91029c 100644 --- a/src/mc/checker/CommunicationDeterminismChecker.hpp +++ b/src/mc/checker/CommunicationDeterminismChecker.hpp @@ -33,7 +33,7 @@ private: public: // These are used by functions which should be moved in CommunicationDeterminismChecker: - void get_comm_pattern(smx_simcall_t request, e_mc_call_type_t call_type, int backtracking); + void get_comm_pattern(smx_simcall_t request, CallType call_type, int backtracking); void complete_comm_pattern(RemotePtr comm_addr, unsigned int issuer, int backtracking); private: diff --git a/src/mc/mc_comm_pattern.cpp b/src/mc/mc_comm_pattern.cpp index d2fb5e6b36..3f066a7f96 100644 --- a/src/mc/mc_comm_pattern.cpp +++ b/src/mc/mc_comm_pattern.cpp @@ -47,33 +47,32 @@ void MC_state_copy_index_communications_pattern(simgrid::mc::State* state) state->communication_indices_.push_back(list_process_comm.index_comm); } -void MC_handle_comm_pattern(e_mc_call_type_t call_type, smx_simcall_t req, int value, int backtracking) +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 MC_CALL_TYPE_NONE: - break; - case MC_CALL_TYPE_SEND: - case MC_CALL_TYPE_RECV: - checker->get_comm_pattern(req, call_type, backtracking); - break; - case MC_CALL_TYPE_WAIT: - case MC_CALL_TYPE_WAITANY: - { - simgrid::mc::RemotePtr comm_addr{nullptr}; - if (call_type == MC_CALL_TYPE_WAIT) - comm_addr = remote(simcall_comm_wait__getraw__comm(req)); + 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)); + 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; + } break; default: xbt_die("Unexpected call type %i", (int)call_type); } diff --git a/src/mc/mc_comm_pattern.hpp b/src/mc/mc_comm_pattern.hpp index 68a42e545d..83803216bb 100644 --- a/src/mc/mc_comm_pattern.hpp +++ b/src/mc/mc_comm_pattern.hpp @@ -14,52 +14,54 @@ namespace simgrid { namespace mc { +enum class CallType { + NONE, + SEND, + RECV, + WAIT, + WAITANY, +}; + +enum class CommPatternDifference { + NONE, + TYPE, + RDV, + TAG, + SRC_PROC, + DST_PROC, + DATA_SIZE, + DATA, +}; + struct PatternCommunicationList { unsigned int index_comm = 0; std::vector> list; }; -} -} +} // namespace mc +} // namespace simgrid extern XBT_PRIVATE std::vector initial_communications_pattern; extern XBT_PRIVATE std::vector> incomplete_communications_pattern; -enum e_mc_call_type_t { - MC_CALL_TYPE_NONE, - MC_CALL_TYPE_SEND, - MC_CALL_TYPE_RECV, - MC_CALL_TYPE_WAIT, - MC_CALL_TYPE_WAITANY, -}; - -enum e_mc_comm_pattern_difference_t { - NONE_DIFF, - TYPE_DIFF, - RDV_DIFF, - TAG_DIFF, - SRC_PROC_DIFF, - DST_PROC_DIFF, - DATA_SIZE_DIFF, - DATA_DIFF, -}; - -static inline e_mc_call_type_t MC_get_call_type(const s_smx_simcall* req) +static inline simgrid::mc::CallType MC_get_call_type(const s_smx_simcall* req) { + using simgrid::mc::CallType; switch (req->call_) { case SIMCALL_COMM_ISEND: - return MC_CALL_TYPE_SEND; + return CallType::SEND; case SIMCALL_COMM_IRECV: - return MC_CALL_TYPE_RECV; + return CallType::RECV; case SIMCALL_COMM_WAIT: - return MC_CALL_TYPE_WAIT; + return CallType::WAIT; case SIMCALL_COMM_WAITANY: - return MC_CALL_TYPE_WAITANY; + return CallType::WAITANY; default: - return MC_CALL_TYPE_NONE; + return CallType::NONE; } } -XBT_PRIVATE void MC_handle_comm_pattern(e_mc_call_type_t call_type, smx_simcall_t request, int value, int backtracking); +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); -- 2.20.1