X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/103f2224567ba33817757197ad4760172407fa31..fe4080b8dd04acb2074ca72d36e3019acddea455:/src/mc/explo/CommunicationDeterminismChecker.cpp diff --git a/src/mc/explo/CommunicationDeterminismChecker.cpp b/src/mc/explo/CommunicationDeterminismChecker.cpp index 6e1bcbadca..639b28c1f4 100644 --- a/src/mc/explo/CommunicationDeterminismChecker.cpp +++ b/src/mc/explo/CommunicationDeterminismChecker.cpp @@ -1,4 +1,4 @@ -/* Copyright (c) 2008-2022. The SimGrid Team. All rights reserved. */ +/* Copyright (c) 2008-2023. The SimGrid Team. All rights reserved. */ /* This program is free software; you can redistribute it and/or modify it * under the terms of the license (GNU LGPL) which comes with this package. */ @@ -11,13 +11,14 @@ #include "src/mc/mc_private.hpp" #include "src/mc/transition/TransitionAny.hpp" #include "src/mc/transition/TransitionComm.hpp" +#include "xbt/string.hpp" #include +#include 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 +62,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 +81,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 +101,17 @@ public: std::vector communication_indices_; static simgrid::xbt::Extension EXTENSION_ID; - explicit StateCommDet(CommDetExtension* checker) + explicit StateCommDet(CommDetExtension const& 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 +136,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 +209,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(); + throw McError(ExitStatus::NON_DETERMINISM); } else if (_sg_mc_comms_determinism && (not send_deterministic && not recv_deterministic)) { XBT_INFO("****************************************************"); XBT_INFO("***** Non-deterministic communications pattern *****"); @@ -213,8 +219,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(); + throw McError(ExitStatus::NON_DETERMINISM); } } } @@ -229,8 +235,8 @@ void CommDetExtension::get_comm_pattern(const Transition* transition) auto pattern = std::make_unique(); pattern->index = initial_pattern.index_comm + incomplete_pattern.size(); - if (transition->type_ == Transition::Type::COMM_SEND) { - auto* send = static_cast(transition); + if (transition->type_ == Transition::Type::COMM_ASYNC_SEND) { + const auto* send = static_cast(transition); pattern->type = PatternCommunicationType::send; pattern->comm_addr = send->get_comm(); @@ -238,8 +244,8 @@ void CommDetExtension::get_comm_pattern(const Transition* transition) // FIXME: Detached sends should be enforced when the receive is waited - } else if (transition->type_ == Transition::Type::COMM_RECV) { - auto* recv = static_cast(transition); + } else if (transition->type_ == Transition::Type::COMM_ASYNC_RECV) { + const auto* recv = static_cast(transition); pattern->type = PatternCommunicationType::receive; pattern->comm_addr = recv->get_comm(); @@ -286,10 +292,8 @@ void CommDetExtension::handle_comm_pattern(const Transition* transition) return; switch (transition->type_) { - case Transition::Type::COMM_SEND: - get_comm_pattern(transition); - break; - case Transition::Type::COMM_RECV: + case Transition::Type::COMM_ASYNC_SEND: + case Transition::Type::COMM_ASYNC_RECV: get_comm_pattern(transition); break; case Transition::Type::COMM_WAIT: @@ -317,26 +321,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, ReductionMode mode) { 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, mode); + 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 const* 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 +355,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 const* t, RemoteApp const&) { extension->handle_comm_pattern(t); }); + DFSExplorer::on_transition_execute( + [extension](Transition const* 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 +381,7 @@ Exploration* create_communication_determinism_checker(Session* session) delete extension; }); - return new DFSExplorer(session); + return base; } -} // namespace mc -} // namespace simgrid +} // namespace simgrid::mc