From 71f071bb10968ac0d3c4ed606a7225d9447d9034 Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Thu, 14 Apr 2016 11:52:15 +0200 Subject: [PATCH] [mc] Move mc_global stuff into CommunicationDeterminismChecker Get rid of initial_global_state. --- src/mc/CommunicationDeterminismChecker.cpp | 104 ++++++++++----------- src/mc/CommunicationDeterminismChecker.hpp | 11 +++ src/mc/mc_comm_pattern.cpp | 9 +- src/mc/mc_comm_pattern.h | 2 - src/mc/mc_global.cpp | 1 - src/mc/mc_snapshot.h | 8 -- src/mc/mc_state.h | 2 - 7 files changed, 68 insertions(+), 69 deletions(-) diff --git a/src/mc/CommunicationDeterminismChecker.cpp b/src/mc/CommunicationDeterminismChecker.cpp index c6f1270ba2..2a32b59502 100644 --- a/src/mc/CommunicationDeterminismChecker.cpp +++ b/src/mc/CommunicationDeterminismChecker.cpp @@ -116,7 +116,10 @@ static void update_comm_pattern(simgrid::mc::PatternCommunication* comm_pattern, } } -static void deterministic_comm_pattern(int process, simgrid::mc::PatternCommunication* comm, int backtracking) { +namespace simgrid { +namespace mc { + +void CommunicationDeterminismChecker::deterministic_comm_pattern(int process, simgrid::mc::PatternCommunication* comm, int backtracking) { simgrid::mc::PatternCommunicationList* list = xbt_dynar_get_as(initial_communications_pattern, process, simgrid::mc::PatternCommunicationList*); @@ -127,37 +130,36 @@ static void deterministic_comm_pattern(int process, simgrid::mc::PatternCommunic if (diff != NONE_DIFF) { if (comm->type == SIMIX_COMM_SEND){ - simgrid::mc::initial_global_state->send_deterministic = 0; - if(simgrid::mc::initial_global_state->send_diff != nullptr) - xbt_free(simgrid::mc::initial_global_state->send_diff); - simgrid::mc::initial_global_state->send_diff = print_determinism_result(diff, process, comm, list->index_comm + 1); + this->send_deterministic = 0; + if (this->send_diff != nullptr) + xbt_free(this->send_diff); + this->send_diff = print_determinism_result(diff, process, comm, list->index_comm + 1); }else{ - simgrid::mc::initial_global_state->recv_deterministic = 0; - if(simgrid::mc::initial_global_state->recv_diff != nullptr) - xbt_free(simgrid::mc::initial_global_state->recv_diff); - simgrid::mc::initial_global_state->recv_diff = print_determinism_result(diff, process, comm, list->index_comm + 1); + this->recv_deterministic = 0; + if (this->recv_diff != nullptr) + xbt_free(this->recv_diff); + this->recv_diff = print_determinism_result(diff, process, comm, list->index_comm + 1); } - if(_sg_mc_send_determinism && !simgrid::mc::initial_global_state->send_deterministic){ + if(_sg_mc_send_determinism && !this->send_deterministic){ XBT_INFO("*********************************************************"); XBT_INFO("***** Non-send-deterministic communications pattern *****"); XBT_INFO("*********************************************************"); - XBT_INFO("%s", simgrid::mc::initial_global_state->send_diff); - xbt_free(simgrid::mc::initial_global_state->send_diff); - simgrid::mc::initial_global_state->send_diff = nullptr; + XBT_INFO("%s", this->send_diff); + xbt_free(this->send_diff); + this->send_diff = nullptr; simgrid::mc::session->logState(); mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM); }else if(_sg_mc_comms_determinism - && (!simgrid::mc::initial_global_state->send_deterministic - && !simgrid::mc::initial_global_state->recv_deterministic)) { + && (!this->send_deterministic && !this->recv_deterministic)) { XBT_INFO("****************************************************"); XBT_INFO("***** Non-deterministic communications pattern *****"); XBT_INFO("****************************************************"); - XBT_INFO("%s", simgrid::mc::initial_global_state->send_diff); - XBT_INFO("%s", simgrid::mc::initial_global_state->recv_diff); - xbt_free(simgrid::mc::initial_global_state->send_diff); - simgrid::mc::initial_global_state->send_diff = nullptr; - xbt_free(simgrid::mc::initial_global_state->recv_diff); - simgrid::mc::initial_global_state->recv_diff = nullptr; + XBT_INFO("%s", this->send_diff); + XBT_INFO("%s", this->recv_diff); + xbt_free(this->send_diff); + this->send_diff = nullptr; + xbt_free(this->recv_diff); + this->recv_diff = nullptr; simgrid::mc::session->logState(); mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM); } @@ -167,7 +169,7 @@ static void deterministic_comm_pattern(int process, simgrid::mc::PatternCommunic /********** Non Static functions ***********/ -void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking) +void CommunicationDeterminismChecker::get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking) { const smx_process_t issuer = MC_smx_simcall_get_issuer(request); simgrid::mc::PatternCommunicationList* initial_pattern = xbt_dynar_get_as( @@ -208,7 +210,7 @@ void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type remote(synchro.comm.src_buff)); } if(mpi_request.detached){ - if (!simgrid::mc::initial_global_state->initial_communications_pattern_done) { + if (!this->initial_communications_pattern_done) { /* Store comm pattern */ simgrid::mc::PatternCommunicationList* list = xbt_dynar_get_as( initial_communications_pattern, pattern->src_proc, @@ -216,7 +218,7 @@ void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type list->list.push_back(std::move(pattern)); } else { /* Evaluate comm determinism */ - deterministic_comm_pattern(pattern->src_proc, pattern.get(), backtracking); + this->deterministic_comm_pattern(pattern->src_proc, pattern.get(), backtracking); xbt_dynar_get_as( initial_communications_pattern, pattern->src_proc, simgrid::mc::PatternCommunicationList* )->index_comm++; @@ -253,7 +255,9 @@ void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type xbt_dynar_push(dynar, &pattern2); } -void MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigned int issuer, int backtracking) { + +void CommunicationDeterminismChecker::complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigned int issuer, int backtracking) +{ simgrid::mc::PatternCommunication* current_comm_pattern; unsigned int cursor = 0; std::unique_ptr comm_pattern; @@ -279,22 +283,16 @@ void MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigne simgrid::mc::PatternCommunicationList* pattern = xbt_dynar_get_as( initial_communications_pattern, issuer, simgrid::mc::PatternCommunicationList*); - if (!simgrid::mc::initial_global_state->initial_communications_pattern_done) + if (!this->initial_communications_pattern_done) /* Store comm pattern */ pattern->list.push_back(std::move(comm_pattern)); else { /* Evaluate comm determinism */ - deterministic_comm_pattern(issuer, comm_pattern.get(), backtracking); + this->deterministic_comm_pattern(issuer, comm_pattern.get(), backtracking); pattern->index_comm++; } } - -/************************ Main algorithm ************************/ - -namespace simgrid { -namespace mc { - CommunicationDeterminismChecker::CommunicationDeterminismChecker(Session& session) : Checker(session) { @@ -330,29 +328,29 @@ void CommunicationDeterminismChecker::logState() // override { Checker::logState(); if (_sg_mc_comms_determinism && - !simgrid::mc::initial_global_state->recv_deterministic && - simgrid::mc::initial_global_state->send_deterministic) { + !this->recv_deterministic && + this->send_deterministic) { XBT_INFO("******************************************************"); XBT_INFO("**** Only-send-deterministic communication pattern ****"); XBT_INFO("******************************************************"); - XBT_INFO("%s", simgrid::mc::initial_global_state->recv_diff); + XBT_INFO("%s", this->recv_diff); } else if(_sg_mc_comms_determinism && - !simgrid::mc::initial_global_state->send_deterministic && - simgrid::mc::initial_global_state->recv_deterministic) { + !this->send_deterministic && + this->recv_deterministic) { XBT_INFO("******************************************************"); XBT_INFO("**** Only-recv-deterministic communication pattern ****"); XBT_INFO("******************************************************"); - XBT_INFO("%s", simgrid::mc::initial_global_state->send_diff); + XBT_INFO("%s", this->send_diff); } XBT_INFO("Expanded states = %lu", expandedStatesCount_); XBT_INFO("Visited states = %lu", mc_model_checker->visited_states); XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions); - if (simgrid::mc::initial_global_state != nullptr) + if (this != nullptr) XBT_INFO("Send-deterministic : %s", - !simgrid::mc::initial_global_state->send_deterministic ? "No" : "Yes"); - if (simgrid::mc::initial_global_state != nullptr && _sg_mc_comms_determinism) + !this->send_deterministic ? "No" : "Yes"); + if (this != nullptr && _sg_mc_comms_determinism) XBT_INFO("Recv-deterministic : %s", - !simgrid::mc::initial_global_state->recv_deterministic ? "No" : "Yes"); + !this->recv_deterministic ? "No" : "Yes"); } void CommunicationDeterminismChecker::prepare() @@ -445,7 +443,7 @@ int CommunicationDeterminismChecker::main(void) mc_model_checker->handle_simcall(state->transition); /* After this call req is no longer useful */ - if(!initial_global_state->initial_communications_pattern_done) + if (!this->initial_communications_pattern_done) MC_handle_comm_pattern(call, req, req_num, initial_communications_pattern, 0); else MC_handle_comm_pattern(call, req, req_num, nullptr, 0); @@ -462,7 +460,7 @@ int CommunicationDeterminismChecker::main(void) These communications are incomplete and they cannot be analyzed and compared with the initial pattern. */ bool compare_snapshots = all_communications_are_finished() - && initial_global_state->initial_communications_pattern_done; + && this->initial_communications_pattern_done; if (_sg_mc_visited == 0 || (visited_state = visitedStates_.addVisitedState( @@ -493,8 +491,8 @@ int CommunicationDeterminismChecker::main(void) XBT_DEBUG("There are no more processes to interleave. (depth %zi)", stack_.size()); - if (!initial_global_state->initial_communications_pattern_done) - initial_global_state->initial_communications_pattern_done = 1; + if (!this->initial_communications_pattern_done) + this->initial_communications_pattern_done = 1; /* Trash the current state, no longer needed */ XBT_DEBUG("Delete state %d at depth %zi", @@ -544,15 +542,13 @@ int CommunicationDeterminismChecker::run() this->prepare(); - initial_global_state = std::unique_ptr(new s_mc_global_t()); - initial_global_state->initial_communications_pattern_done = 0; - initial_global_state->recv_deterministic = 1; - initial_global_state->send_deterministic = 1; - initial_global_state->recv_diff = nullptr; - initial_global_state->send_diff = nullptr; + this->initial_communications_pattern_done = 0; + this->recv_deterministic = 1; + this->send_deterministic = 1; + this->recv_diff = nullptr; + this->send_diff = nullptr; int res = this->main(); - initial_global_state = nullptr; return res; } diff --git a/src/mc/CommunicationDeterminismChecker.hpp b/src/mc/CommunicationDeterminismChecker.hpp index 781c2ba143..b19fb12e4a 100644 --- a/src/mc/CommunicationDeterminismChecker.hpp +++ b/src/mc/CommunicationDeterminismChecker.hpp @@ -30,11 +30,22 @@ private: void prepare(); int main(); void logState() override; + void deterministic_comm_pattern(int process, simgrid::mc::PatternCommunication* comm, int backtracking); +public: + // These are used by functions which should be moved in CommunicationDeterminismChecker: + void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking); + void complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigned int issuer, int backtracking); private: /** Stack representing the position in the exploration graph */ std::list> stack_; simgrid::mc::VisitedStates visitedStates_; unsigned long expandedStatesCount_ = 0; + + int initial_communications_pattern_done = 0; + int recv_deterministic = 0; + int send_deterministic = 0; + char *send_diff = nullptr; + char *recv_diff = nullptr; }; #endif diff --git a/src/mc/mc_comm_pattern.cpp b/src/mc/mc_comm_pattern.cpp index 8d064c96c5..1241a60e31 100644 --- a/src/mc/mc_comm_pattern.cpp +++ b/src/mc/mc_comm_pattern.cpp @@ -13,6 +13,8 @@ #include "src/mc/mc_comm_pattern.h" #include "src/mc/mc_smx.h" #include "src/mc/mc_xbt.hpp" +#include "src/mc/Checker.hpp" +#include "src/mc/CommunicationDeterminismChecker.hpp" using simgrid::mc::remote; @@ -71,13 +73,16 @@ void MC_handle_comm_pattern( e_mc_call_type_t call_type, smx_simcall_t req, int value, xbt_dynar_t pattern, int backtracking) { + // HACK, do not rely on the Checker implementation outside of it + simgrid::mc::CommunicationDeterminismChecker* checker = + (simgrid::mc::CommunicationDeterminismChecker*) mc_model_checker->getChecker(); switch(call_type) { case MC_CALL_TYPE_NONE: break; case MC_CALL_TYPE_SEND: case MC_CALL_TYPE_RECV: - MC_get_comm_pattern(pattern, req, call_type, backtracking); + checker->get_comm_pattern(pattern, req, call_type, backtracking); break; case MC_CALL_TYPE_WAIT: case MC_CALL_TYPE_WAITANY: @@ -89,7 +94,7 @@ void MC_handle_comm_pattern( // comm_addr = REMOTE(xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value, smx_synchro_t)): simgrid::mc::read_element(mc_model_checker->process(), &comm_addr, remote(simcall_comm_waitany__get__comms(req)), value, sizeof(comm_addr)); - MC_complete_comm_pattern(pattern, comm_addr, + checker->complete_comm_pattern(pattern, comm_addr, MC_smx_simcall_get_issuer(req)->pid, backtracking); } break; diff --git a/src/mc/mc_comm_pattern.h b/src/mc/mc_comm_pattern.h index c84643cb27..2b128bf71c 100644 --- a/src/mc/mc_comm_pattern.h +++ b/src/mc/mc_comm_pattern.h @@ -80,9 +80,7 @@ static inline e_mc_call_type_t MC_get_call_type(smx_simcall_t req) } } -XBT_PRIVATE void MC_get_comm_pattern(xbt_dynar_t communications_pattern, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking); XBT_PRIVATE void MC_handle_comm_pattern(e_mc_call_type_t call_type, smx_simcall_t request, int value, xbt_dynar_t current_pattern, int backtracking); -XBT_PRIVATE void MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigned int issuer, int backtracking); XBT_PRIVATE void MC_restore_communications_pattern(simgrid::mc::State* state); diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp index c1b88d16f1..059a4878d9 100644 --- a/src/mc/mc_global.cpp +++ b/src/mc/mc_global.cpp @@ -69,7 +69,6 @@ char mc_replay_mode = false; namespace simgrid { namespace mc { -std::unique_ptr initial_global_state = nullptr; xbt_automaton_t property_automaton = nullptr; } diff --git a/src/mc/mc_snapshot.h b/src/mc/mc_snapshot.h index 7befa377df..c799698414 100644 --- a/src/mc/mc_snapshot.h +++ b/src/mc/mc_snapshot.h @@ -128,14 +128,6 @@ typedef struct XBT_PRIVATE s_mc_snapshot_stack { int process_index; } s_mc_snapshot_stack_t, *mc_snapshot_stack_t; -typedef struct s_mc_global_t { - int initial_communications_pattern_done = 0; - int recv_deterministic = 0; - int send_deterministic = 0; - char *send_diff = nullptr; - char *recv_diff = nullptr; -}s_mc_global_t, *mc_global_t; - namespace simgrid { namespace mc { diff --git a/src/mc/mc_state.h b/src/mc/mc_state.h index 599b0cb785..2feff61fa7 100644 --- a/src/mc/mc_state.h +++ b/src/mc/mc_state.h @@ -22,8 +22,6 @@ namespace simgrid { namespace mc { -extern XBT_PRIVATE std::unique_ptr initial_global_state; - struct PatternCommunication { int num = 0; smx_synchro_t comm_addr; -- 2.20.1