X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/97e2219ed6c0e511f6165460cec79afadf42f589..497aee08bf8b36b4981083b79d8473991db1ccde:/src/mc/explo/CommunicationDeterminismChecker.cpp diff --git a/src/mc/explo/CommunicationDeterminismChecker.cpp b/src/mc/explo/CommunicationDeterminismChecker.cpp index 6e1bcbadca..ad0677a8e0 100644 --- a/src/mc/explo/CommunicationDeterminismChecker.cpp +++ b/src/mc/explo/CommunicationDeterminismChecker.cpp @@ -16,8 +16,7 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_comm_determinism, mc, "Logging specific to MC communication determinism detection"); -namespace simgrid { -namespace mc { +namespace simgrid::mc { enum class CallType { NONE, SEND, RECV, WAIT, WAITANY }; enum class CommPatternDifference { NONE, TYPE, MBOX, TAG, SRC_PROC, DST_PROC, DATA_SIZE }; @@ -61,9 +60,14 @@ struct PatternCommunicationList { /********** Checker extension **********/ -struct CommDetExtension { +class CommDetExtension { + Exploration& exploration_; + +public: static simgrid::xbt::Extension EXTENSION_ID; + explicit CommDetExtension(Exploration& explo) : exploration_(explo) {} + std::vector initial_communications_pattern; std::vector> incomplete_communications_pattern; @@ -75,12 +79,12 @@ struct CommDetExtension { void exploration_start() { - const unsigned long maxpid = Api::get().get_maxpid(); + const unsigned long maxpid = exploration_.get_remote_app().get_maxpid(); initial_communications_pattern.resize(maxpid); incomplete_communications_pattern.resize(maxpid); } - void restore_communications_pattern(const simgrid::mc::State* state); + void restore_communications_pattern(const simgrid::mc::State* state, RemoteApp const& remote_app); void enforce_deterministic_pattern(aid_t process, const PatternCommunication* comm); void get_comm_pattern(const Transition* transition); void complete_comm_pattern(const CommWaitTransition* transition); @@ -95,17 +99,17 @@ public: std::vector communication_indices_; static simgrid::xbt::Extension EXTENSION_ID; - explicit StateCommDet(CommDetExtension* checker) + explicit StateCommDet(CommDetExtension& checker, RemoteApp const& remote_app) { - const unsigned long maxpid = Api::get().get_maxpid(); + const unsigned long maxpid = remote_app.get_maxpid(); for (unsigned long i = 0; i < maxpid; i++) { std::vector res; - for (auto const& comm : checker->incomplete_communications_pattern[i]) + for (auto const& comm : checker.incomplete_communications_pattern[i]) res.push_back(comm->dup()); incomplete_comm_pattern_.push_back(std::move(res)); } - for (auto const& list_process_comm : checker->initial_communications_pattern) + for (auto const& list_process_comm : checker.initial_communications_pattern) this->communication_indices_.push_back(list_process_comm.index_comm); } }; @@ -130,13 +134,13 @@ static simgrid::mc::CommPatternDifference compare_comm_pattern(const simgrid::mc return CommPatternDifference::NONE; } -void CommDetExtension::restore_communications_pattern(const simgrid::mc::State* state) +void CommDetExtension::restore_communications_pattern(const simgrid::mc::State* state, RemoteApp const& remote_app) { for (size_t i = 0; i < initial_communications_pattern.size(); i++) initial_communications_pattern[i].index_comm = state->extension()->communication_indices_[i]; - const unsigned long maxpid = Api::get().get_maxpid(); + const unsigned long maxpid = remote_app.get_maxpid(); for (unsigned long i = 0; i < maxpid; i++) { incomplete_communications_pattern[i].clear(); for (simgrid::mc::PatternCommunication const& comm : @@ -203,8 +207,8 @@ void CommDetExtension::enforce_deterministic_pattern(aid_t actor, const PatternC XBT_INFO("***** Non-send-deterministic communications pattern *****"); XBT_INFO("*********************************************************"); XBT_INFO("%s", send_diff.c_str()); - Api::get().get_session().log_state(); - Api::get().mc_exit(SIMGRID_MC_EXIT_NON_DETERMINISM); + exploration_.log_state(); + mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM); } else if (_sg_mc_comms_determinism && (not send_deterministic && not recv_deterministic)) { XBT_INFO("****************************************************"); XBT_INFO("***** Non-deterministic communications pattern *****"); @@ -213,8 +217,8 @@ void CommDetExtension::enforce_deterministic_pattern(aid_t actor, const PatternC XBT_INFO("%s", send_diff.c_str()); if (not recv_diff.empty()) XBT_INFO("%s", recv_diff.c_str()); - Api::get().get_session().log_state(); - Api::get().mc_exit(SIMGRID_MC_EXIT_NON_DETERMINISM); + exploration_.log_state(); + mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM); } } } @@ -287,8 +291,6 @@ void CommDetExtension::handle_comm_pattern(const Transition* transition) switch (transition->type_) { case Transition::Type::COMM_SEND: - get_comm_pattern(transition); - break; case Transition::Type::COMM_RECV: get_comm_pattern(transition); break; @@ -317,26 +319,32 @@ void CommDetExtension::handle_comm_pattern(const Transition* transition) } */ -Exploration* create_communication_determinism_checker(Session* session) +Exploration* create_communication_determinism_checker(const std::vector& args, bool with_dpor) { CommDetExtension::EXTENSION_ID = simgrid::mc::Exploration::extension_create(); StateCommDet::EXTENSION_ID = simgrid::mc::State::extension_create(); XBT_DEBUG("********* Start communication determinism verification *********"); - auto extension = new CommDetExtension(); + auto base = new DFSExplorer(args, with_dpor); + auto extension = new CommDetExtension(*base); - DFSExplorer::on_exploration_start([extension]() { + DFSExplorer::on_exploration_start([extension](RemoteApp const&) { XBT_INFO("Check communication determinism"); extension->exploration_start(); }); - DFSExplorer::on_backtracking([extension]() { extension->initial_communications_pattern_done = true; }); - DFSExplorer::on_state_creation([extension](State* state) { state->extension_set(new StateCommDet(extension)); }); + DFSExplorer::on_backtracking( + [extension](RemoteApp const&) { extension->initial_communications_pattern_done = true; }); + DFSExplorer::on_state_creation([extension](State* state, RemoteApp const& remote_app) { + state->extension_set(new StateCommDet(*extension, remote_app)); + }); - DFSExplorer::on_restore_system_state([extension](State* state) { extension->restore_communications_pattern(state); }); + DFSExplorer::on_restore_system_state([extension](State* state, RemoteApp const& remote_app) { + extension->restore_communications_pattern(state, remote_app); + }); - DFSExplorer::on_restore_initial_state([extension]() { - const unsigned long maxpid = Api::get().get_maxpid(); + DFSExplorer::on_restore_initial_state([extension](RemoteApp const& remote_app) { + const unsigned long maxpid = remote_app.get_maxpid(); assert(maxpid == extension->incomplete_communications_pattern.size()); assert(maxpid == extension->initial_communications_pattern.size()); for (unsigned long j = 0; j < maxpid; j++) { @@ -345,10 +353,12 @@ Exploration* create_communication_determinism_checker(Session* session) } }); - DFSExplorer::on_transition_replay([extension](Transition* t) { extension->handle_comm_pattern(t); }); - DFSExplorer::on_transition_execute([extension](Transition* t) { extension->handle_comm_pattern(t); }); + DFSExplorer::on_transition_replay( + [extension](Transition* t, RemoteApp const&) { extension->handle_comm_pattern(t); }); + DFSExplorer::on_transition_execute( + [extension](Transition* t, RemoteApp const&) { extension->handle_comm_pattern(t); }); - DFSExplorer::on_log_state([extension]() { + DFSExplorer::on_log_state([extension](RemoteApp const&) { if (_sg_mc_comms_determinism) { if (extension->send_deterministic && not extension->recv_deterministic) { XBT_INFO("*******************************************************"); @@ -369,8 +379,7 @@ Exploration* create_communication_determinism_checker(Session* session) delete extension; }); - return new DFSExplorer(session); + return base; } -} // namespace mc -} // namespace simgrid +} // namespace simgrid::mc