X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/96d605fde63f72480bf570f7bc7609e2954cb2d7..788fd4a0324f3ef5aa40f37eb6e4c8c5accd1164:/src/mc/explo/CommunicationDeterminismChecker.cpp diff --git a/src/mc/explo/CommunicationDeterminismChecker.cpp b/src/mc/explo/CommunicationDeterminismChecker.cpp index 3212daacbc..a1a51ce080 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,6 +11,7 @@ #include "src/mc/mc_private.hpp" #include "src/mc/transition/TransitionAny.hpp" #include "src/mc/transition/TransitionComm.hpp" +#include "xbt/string.hpp" #include @@ -60,9 +61,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; @@ -74,12 +80,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); @@ -94,17 +100,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); } }; @@ -129,13 +135,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 : @@ -202,8 +208,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(); - Api::get().mc_exit(SIMGRID_MC_EXIT_NON_DETERMINISM); + exploration_.log_state(); + exploration_.system_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 *****"); @@ -212,8 +218,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(); - Api::get().mc_exit(SIMGRID_MC_EXIT_NON_DETERMINISM); + exploration_.log_state(); + exploration_.system_exit(SIMGRID_MC_EXIT_NON_DETERMINISM); } } } @@ -228,7 +234,7 @@ 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) { + if (transition->type_ == Transition::Type::COMM_ASYNC_SEND) { auto* send = static_cast(transition); pattern->type = PatternCommunicationType::send; @@ -237,7 +243,7 @@ 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) { + } else if (transition->type_ == Transition::Type::COMM_ASYNC_RECV) { auto* recv = static_cast(transition); pattern->type = PatternCommunicationType::receive; @@ -285,8 +291,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,26 +320,32 @@ 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, 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, true); + 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++) { @@ -342,10 +354,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("*******************************************************"); @@ -366,7 +380,7 @@ Exploration* create_communication_determinism_checker(RemoteApp* remote_app) delete extension; }); - return new DFSExplorer(remote_app); + return base; } } // namespace simgrid::mc