X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/0db94857a5dd1d7b1880f9f06dd2993b5d24c5e6..285132b31c7186e9b1d67b2ce96b02d216886a9f:/src/mc/api/RemoteApp.cpp diff --git a/src/mc/api/RemoteApp.cpp b/src/mc/api/RemoteApp.cpp index d7c1037db8..ee1627feda 100644 --- a/src/mc/api/RemoteApp.cpp +++ b/src/mc/api/RemoteApp.cpp @@ -1,4 +1,4 @@ -/* Copyright (c) 2015-2022. The SimGrid Team. All rights reserved. */ +/* Copyright (c) 2015-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. */ @@ -7,6 +7,7 @@ #include "src/internal_config.h" // HAVE_SMPI #include "src/mc/explo/Exploration.hpp" #include "src/mc/mc_config.hpp" +#include "xbt/asserts.h" #if HAVE_SMPI #include "smpi/smpi.h" #include "src/smpi/include/private.hpp" @@ -19,9 +20,11 @@ #include "xbt/log.h" #include "xbt/system_error.hpp" +#include #include #include #include +#include #include #include @@ -41,7 +44,7 @@ static simgrid::config::Flag _sg_mc_setenv{ namespace simgrid::mc { -static void run_child_process(int socket, const std::vector& args) +XBT_ATTRIB_NORETURN static void run_child_process(int socket, const std::vector& args) { /* On startup, simix_global_init() calls simgrid::mc::Client::initialize(), which checks whether the MC_ENV_SOCKET_FD * env variable is set. If so, MC mode is assumed, and the client is setup from its side @@ -87,7 +90,14 @@ static void run_child_process(int socket, const std::vector& args) "Unable to find a binary to exec on the command line. Did you only pass config flags?"); execvp(args[i], args.data() + i); - xbt_die("The model-checked process failed to exec(%s): %s", args[i], strerror(errno)); + XBT_CRITICAL("The model-checked process failed to exec(%s): %s.\n" + " Make sure that your binary exists on disk and is executable.", + args[i], strerror(errno)); + if (strchr(args[i], '=') != nullptr) + XBT_CRITICAL("If you want to pass environment variables to the application, please use --cfg=model-check/setenv:%s", + args[i]); + + xbt_die("Aborting now."); } RemoteApp::RemoteApp(const std::vector& args) @@ -151,10 +161,14 @@ unsigned long RemoteApp::get_maxpid() const void RemoteApp::get_actors_status(std::map& whereto) const { - s_mc_message_t msg; - memset(&msg, 0, sizeof msg); - msg.type = simgrid::mc::MessageType::ACTORS_STATUS; - model_checker_->channel().send(msg); + // The messaging happens as follows: + // + // CheckerSide AppSide + // send ACTORS_STATUS ----> + // <----- send ACTORS_STATUS_REPLY + // <----- send `N` `s_mc_message_actors_status_one_t` structs + // <----- send `M` `s_mc_message_simcall_probe_one_t` structs + model_checker_->channel().send(MessageType::ACTORS_STATUS); s_mc_message_actors_status_answer_t answer; ssize_t received = model_checker_->channel().receive(answer); @@ -165,13 +179,62 @@ void RemoteApp::get_actors_status(std::map& whereto) const to_c_str(answer.type), (int)answer.type, (int)received, (int)MessageType::ACTORS_STATUS_REPLY, (int)sizeof(answer)); - s_mc_message_actors_status_one_t status[answer.count]; - received = model_checker_->channel().receive(&status, sizeof(status)); - xbt_assert(static_cast(received) == sizeof(status)); + // Message sanity checks + xbt_assert(answer.count >= 0, "Received an ACTOR_STATUS_REPLY message with an actor count of '%d' < 0", answer.count); + xbt_assert(answer.transition_count >= 0, "Received an ACTOR_STATUS_REPLY message with transition_count '%d' < 0", + answer.transition_count); + xbt_assert(answer.transition_count == 0 || answer.count >= 0, + "Received an ACTOR_STATUS_REPLY message with no actor data " + "but with transition data nonetheless"); + + std::vector status(answer.count); + if (answer.count > 0) { + size_t size = status.size() * sizeof(s_mc_message_actors_status_one_t); + ssize_t received = model_checker_->channel().receive(status.data(), size); + xbt_assert(static_cast(received) == size); + } + + // Ensures that each actor sends precisely `answer.transition_count` transitions. While technically + // this doesn't catch the edge case where actor A sends 3 instead of 2 and actor B sends 2 instead + // of 3 transitions, that is ignored here since that invariant needs to be enforced on the AppSide + const auto expected_transitions = std::accumulate( + status.begin(), status.end(), 0, [](int total, const auto& actor) { return total + actor.n_transitions; }); + xbt_assert(expected_transitions == answer.transition_count, + "Expected to receive %d transition(s) but was only notified of %d by the app side", expected_transitions, + answer.transition_count); + + std::vector probes(answer.transition_count); + if (answer.transition_count > 0) { + for (auto& probe : probes) { + size_t size = sizeof(s_mc_message_simcall_probe_one_t); + ssize_t received = model_checker_->channel().receive(&probe, size); + xbt_assert(received >= 0, "Could not receive response to ACTORS_PROBE message (%s)", strerror(errno)); + xbt_assert(static_cast(received) == size, + "Could not receive response to ACTORS_PROBE message (%zd bytes received != %zu bytes expected", + received, size); + } + } whereto.clear(); - for (auto const& actor : status) - whereto.try_emplace(actor.aid, actor.aid, actor.enabled, actor.max_considered); + auto probes_iter = std::move_iterator(probes.begin()); + + for (const auto& actor : status) { + xbt_assert(actor.n_transitions == 0 || actor.n_transitions == actor.max_considered, + "If any transitions are serialized for an actor, it must match the " + "total number of transitions that can be considered for the actor " + "(currently %d), but only %d transition(s) was/were said to be encoded", + actor.max_considered, actor.n_transitions); + + auto actor_transitions = std::vector>(actor.n_transitions); + for (int times_considered = 0; times_considered < actor.n_transitions; times_considered++, probes_iter++) { + std::stringstream stream((*probes_iter).buffer.data()); + auto transition = std::shared_ptr(deserialize_transition(actor.aid, times_considered, stream)); + actor_transitions[times_considered] = std::move(transition); + } + + XBT_DEBUG("Received %d transitions for actor %ld", actor.n_transitions, actor.aid); + whereto.try_emplace(actor.aid, actor.aid, actor.enabled, actor.max_considered, std::move(actor_transitions)); + } } void RemoteApp::check_deadlock() const @@ -187,13 +250,12 @@ void RemoteApp::check_deadlock() const (int)sizeof(message)); if (message.value != 0) { - XBT_CINFO(mc_global, "**************************"); - XBT_CINFO(mc_global, "*** DEADLOCK DETECTED ***"); - XBT_CINFO(mc_global, "**************************"); XBT_CINFO(mc_global, "Counter-example execution trace:"); for (auto const& frame : model_checker_->get_exploration()->get_textual_trace()) XBT_CINFO(mc_global, " %s", frame.c_str()); - XBT_CINFO(mc_global, "Path = %s", model_checker_->get_exploration()->get_record_trace().to_string().c_str()); + XBT_INFO("You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with " + "--cfg=model-check/replay:'%s'", + model_checker_->get_exploration()->get_record_trace().to_string().c_str()); model_checker_->get_exploration()->log_state(); throw DeadlockError(); }