X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/6d521fad4dc4a469b023850e9449a5ec8d29b356..7e625e5e848a284b522d69ec28cb111f1f88515b:/src/mc/explo/CommunicationDeterminismChecker.cpp diff --git a/src/mc/explo/CommunicationDeterminismChecker.cpp b/src/mc/explo/CommunicationDeterminismChecker.cpp index 1099126bf0..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,8 +11,10 @@ #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"); @@ -60,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; @@ -72,14 +79,14 @@ struct CommDetExtension { std::string send_diff; std::string recv_diff; - void exploration_start(RemoteApp& remote_app) + void exploration_start() { - const unsigned long maxpid = remote_app.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, RemoteApp& remote_app); + 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); @@ -94,7 +101,7 @@ public: std::vector communication_indices_; static simgrid::xbt::Extension EXTENSION_ID; - explicit StateCommDet(CommDetExtension& checker, RemoteApp& remote_app) + explicit StateCommDet(CommDetExtension const& checker, RemoteApp const& remote_app) { const unsigned long maxpid = remote_app.get_maxpid(); for (unsigned long i = 0; i < maxpid; i++) { @@ -129,7 +136,7 @@ static simgrid::mc::CommPatternDifference compare_comm_pattern(const simgrid::mc return CommPatternDifference::NONE; } -void CommDetExtension::restore_communications_pattern(const simgrid::mc::State* state, RemoteApp& remote_app) +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 = @@ -202,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_remote_app().log_state(); - mc_model_checker->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 *****"); @@ -212,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_remote_app().log_state(); - mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM); + exploration_.log_state(); + throw McError(ExitStatus::NON_DETERMINISM); } } } @@ -228,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(); @@ -237,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(); @@ -285,8 +292,8 @@ void CommDetExtension::handle_comm_pattern(const Transition* transition) return; switch (transition->type_) { - case Transition::Type::COMM_SEND: - 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: @@ -314,27 +321,31 @@ void CommDetExtension::handle_comm_pattern(const Transition* transition) } */ -Exploration* create_communication_determinism_checker(RemoteApp& remote_app) +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, &remote_app]() { + DFSExplorer::on_exploration_start([extension](RemoteApp const&) { XBT_INFO("Check communication determinism"); - extension->exploration_start(remote_app); + extension->exploration_start(); + }); + 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_backtracking([extension]() { extension->initial_communications_pattern_done = true; }); - DFSExplorer::on_state_creation( - [extension, &remote_app](State* state) { state->extension_set(new StateCommDet(*extension, remote_app)); }); - DFSExplorer::on_restore_system_state( - [extension, &remote_app](State* state) { extension->restore_communications_pattern(state, remote_app); }); + 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, &remote_app]() { + 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()); @@ -344,10 +355,12 @@ Exploration* create_communication_determinism_checker(RemoteApp& remote_app) } }); - 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("*******************************************************"); @@ -368,7 +381,7 @@ Exploration* create_communication_determinism_checker(RemoteApp& remote_app) delete extension; }); - return new DFSExplorer(remote_app); + return base; } } // namespace simgrid::mc