X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/261e680f278e36ba4efbc0755fb08d00ff3cad83..e80fc92c523fadeda71f4f7c2f0ca6a5a7dea7a7:/src/mc/explo/CommunicationDeterminismChecker.cpp diff --git a/src/mc/explo/CommunicationDeterminismChecker.cpp b/src/mc/explo/CommunicationDeterminismChecker.cpp index 24b2227962..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"); @@ -84,7 +86,7 @@ public: 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); @@ -99,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++) { @@ -134,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 = @@ -207,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()); - exploration_.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 *****"); @@ -217,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()); - exploration_.get_remote_app().log_state(); - mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM); + exploration_.log_state(); + throw McError(ExitStatus::NON_DETERMINISM); } } } @@ -233,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(); @@ -242,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(); @@ -290,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: @@ -319,28 +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 base = new DFSExplorer(remote_app); - auto extension = new CommDetExtension(*base); + 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, &remote_app](State* state) { state->extension_set(new StateCommDet(*extension, remote_app)); }); + 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, &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()); @@ -350,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("*******************************************************");