src/mc/api/RemoteApp.cpp

   1 /* Copyright (c) 2015-2023. The SimGrid Team. All rights reserved.          */
   2
   3 /* This program is free software; you can redistribute it and/or modify it
   4  * under the terms of the license (GNU LGPL) which comes with this package. */
   5
   6 #include "src/mc/api/RemoteApp.hpp"
   7 #include "src/mc/explo/Exploration.hpp"
   8 #include "src/mc/mc_config.hpp"
   9 #include "xbt/asserts.h"
  10 #include "src/mc/api/State.hpp"
  11 #include "src/mc/mc_config.hpp"
  12 #include "src/mc/mc_exit.hpp"
  13 #include "src/mc/mc_private.hpp"
  14 #include "xbt/log.h"
  15 #include "xbt/system_error.hpp"
  16 #include <signal.h>
  17
  18 #include <algorithm>
  19 #include <array>
  20 #include <memory>
  21 #include <numeric>
  22 #include <string>
  23
  24 #include <sys/ptrace.h>
  25 #include <sys/wait.h>
  26
  27 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_Session, mc, "Model-checker session");
  28 XBT_LOG_EXTERNAL_CATEGORY(mc_global);
  29
  30 namespace simgrid::mc {
  31
  32 RemoteApp::RemoteApp(const std::vector<char*>& args)
  33 {
  34
  35   checker_side_ = std::make_unique<simgrid::mc::CheckerSide>(args);
  36
  37   /* Take the initial snapshot */
  38   initial_snapshot_ = std::make_shared<simgrid::mc::Snapshot>(0, page_store_, checker_side_->get_remote_memory());
  39 }
  40
  41 RemoteApp::~RemoteApp()
  42 {
  43   initial_snapshot_ = nullptr;
  44   shutdown();
  45 }
  46
  47 void RemoteApp::restore_initial_state() const
  48 {
  49   this->initial_snapshot_->restore(checker_side_->get_remote_memory());
  50 }
  51
  52 unsigned long RemoteApp::get_maxpid() const
  53 {
  54   // note: we could maybe cache it and count the actor creation on checker side too.
  55   // But counting correctly accross state checkpoint/restore would be annoying.
  56
  57   checker_side_->get_channel().send(MessageType::ACTORS_MAXPID);
  58   s_mc_message_int_t answer;
  59   ssize_t answer_size = checker_side_->get_channel().receive(answer);
  60   xbt_assert(answer_size != -1, "Could not receive message");
  61   xbt_assert(answer_size == sizeof answer, "Broken message (size=%zd; expected %zu)", answer_size, sizeof answer);
  62   xbt_assert(answer.type == MessageType::ACTORS_MAXPID_REPLY,
  63              "Received unexpected message %s (%i); expected MessageType::ACTORS_MAXPID_REPLY (%i)",
  64              to_c_str(answer.type), (int)answer.type, (int)MessageType::ACTORS_MAXPID_REPLY);
  65
  66   return answer.value;
  67 }
  68
  69 void RemoteApp::get_actors_status(std::map<aid_t, ActorState>& whereto) const
  70 {
  71   // The messaging happens as follows:
  72   //
  73   // CheckerSide                  AppSide
  74   // send ACTORS_STATUS ---->
  75   //                    <----- send ACTORS_STATUS_REPLY
  76   //                    <----- send `N` `s_mc_message_actors_status_one_t` structs
  77   //                    <----- send `M` `s_mc_message_simcall_probe_one_t` structs
  78   checker_side_->get_channel().send(MessageType::ACTORS_STATUS);
  79
  80   s_mc_message_actors_status_answer_t answer;
  81   ssize_t answer_size = checker_side_->get_channel().receive(answer);
  82   xbt_assert(answer_size != -1, "Could not receive message");
  83   xbt_assert(answer_size == sizeof answer, "Broken message (size=%zd; expected %zu)", answer_size, sizeof answer);
  84   xbt_assert(answer.type == MessageType::ACTORS_STATUS_REPLY,
  85              "Received unexpected message %s (%i); expected MessageType::ACTORS_STATUS_REPLY (%i)",
  86              to_c_str(answer.type), (int)answer.type, (int)MessageType::ACTORS_STATUS_REPLY);
  87
  88   // Message sanity checks
  89   xbt_assert(answer.count >= 0, "Received an ACTOR_STATUS_REPLY message with an actor count of '%d' < 0", answer.count);
  90   xbt_assert(answer.transition_count >= 0, "Received an ACTOR_STATUS_REPLY message with transition_count '%d' < 0",
  91              answer.transition_count);
  92   xbt_assert(answer.transition_count == 0 || answer.count >= 0,
  93              "Received an ACTOR_STATUS_REPLY message with no actor data "
  94              "but with transition data nonetheless");
  95
  96   std::vector<s_mc_message_actors_status_one_t> status(answer.count);
  97   if (answer.count > 0) {
  98     size_t size      = status.size() * sizeof(s_mc_message_actors_status_one_t);
  99     ssize_t received = checker_side_->get_channel().receive(status.data(), size);
 100     xbt_assert(static_cast<size_t>(received) == size);
 101   }
 102
 103   // Ensures that each actor sends precisely `answer.transition_count` transitions. While technically
 104   // this doesn't catch the edge case where actor A sends 3 instead of 2 and actor B sends 2 instead
 105   // of 3 transitions, that is ignored here since that invariant needs to be enforced on the AppSide
 106   const auto expected_transitions = std::accumulate(
 107       status.begin(), status.end(), 0, [](int total, const auto& actor) { return total + actor.n_transitions; });
 108   xbt_assert(expected_transitions == answer.transition_count,
 109              "Expected to receive %d transition(s) but was only notified of %d by the app side", expected_transitions,
 110              answer.transition_count);
 111
 112   std::vector<s_mc_message_simcall_probe_one_t> probes(answer.transition_count);
 113   if (answer.transition_count > 0) {
 114     for (auto& probe : probes) {
 115       ssize_t received = checker_side_->get_channel().receive(probe);
 116       xbt_assert(received >= 0, "Could not receive response to ACTORS_PROBE message (%s)", strerror(errno));
 117       xbt_assert(static_cast<size_t>(received) == sizeof probe,
 118                  "Could not receive response to ACTORS_PROBE message (%zd bytes received != %zu bytes expected",
 119                  received, sizeof probe);
 120     }
 121   }
 122
 123   whereto.clear();
 124   std::move_iterator probes_iter(probes.begin());
 125
 126   for (const auto& actor : status) {
 127     xbt_assert(actor.n_transitions == 0 || actor.n_transitions == actor.max_considered,
 128                "If any transitions are serialized for an actor, it must match the "
 129                "total number of transitions that can be considered for the actor "
 130                "(currently %d), but only %d transition(s) was/were said to be encoded",
 131                actor.max_considered, actor.n_transitions);
 132
 133     std::vector<std::shared_ptr<Transition>> actor_transitions;
 134     for (int times_considered = 0; times_considered < actor.n_transitions; times_considered++, probes_iter++) {
 135       std::stringstream stream((*probes_iter).buffer.data());
 136       actor_transitions.emplace_back(deserialize_transition(actor.aid, times_considered, stream));
 137     }
 138
 139     XBT_DEBUG("Received %zu transitions for actor %ld", actor_transitions.size(), actor.aid);
 140     whereto.try_emplace(actor.aid, actor.aid, actor.enabled, actor.max_considered, std::move(actor_transitions));
 141   }
 142 }
 143
 144 void RemoteApp::check_deadlock() const
 145 {
 146   xbt_assert(checker_side_->get_channel().send(MessageType::DEADLOCK_CHECK) == 0, "Could not check deadlock state");
 147   s_mc_message_int_t message;
 148   ssize_t received = checker_side_->get_channel().receive(message);
 149   xbt_assert(received != -1, "Could not receive message");
 150   xbt_assert(received == sizeof message, "Broken message (size=%zd; expected %zu)", received, sizeof message);
 151   xbt_assert(message.type == MessageType::DEADLOCK_CHECK_REPLY,
 152              "Received unexpected message %s (%i); expected MessageType::DEADLOCK_CHECK_REPLY (%i)",
 153              to_c_str(message.type), (int)message.type, (int)MessageType::DEADLOCK_CHECK_REPLY);
 154
 155   if (message.value != 0) {
 156     auto* explo = Exploration::get_instance();
 157     XBT_CINFO(mc_global, "Counter-example execution trace:");
 158     for (auto const& frame : explo->get_textual_trace())
 159       XBT_CINFO(mc_global, "  %s", frame.c_str());
 160     XBT_INFO("You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with "
 161              "--cfg=model-check/replay:'%s'",
 162              explo->get_record_trace().to_string().c_str());
 163     explo->log_state();
 164     throw DeadlockError();
 165   }
 166 }
 167
 168 void RemoteApp::wait_for_requests()
 169 {
 170   checker_side_->wait_for_requests();
 171 }
 172
 173 void RemoteApp::shutdown()
 174 {
 175   XBT_DEBUG("Shutting down model-checker");
 176
 177   if (checker_side_->running()) {
 178     XBT_DEBUG("Killing process");
 179     finalize_app(true);
 180     kill(checker_side_->get_pid(), SIGKILL);
 181     checker_side_->terminate();
 182   }
 183 }
 184
 185 Transition* RemoteApp::handle_simcall(aid_t aid, int times_considered, bool new_transition)
 186 {
 187   s_mc_message_simcall_execute_t m = {};
 188   m.type                           = MessageType::SIMCALL_EXECUTE;
 189   m.aid_                           = aid;
 190   m.times_considered_              = times_considered;
 191   checker_side_->get_channel().send(m);
 192
 193   get_remote_process_memory().clear_cache();
 194   if (checker_side_->running())
 195     checker_side_->dispatch_events(); // The app may send messages while processing the transition
 196
 197   s_mc_message_simcall_execute_answer_t answer;
 198   ssize_t s = checker_side_->get_channel().receive(answer);
 199   xbt_assert(s != -1, "Could not receive message");
 200   xbt_assert(s == sizeof answer, "Broken message (size=%zd; expected %zu)", s, sizeof answer);
 201   xbt_assert(answer.type == MessageType::SIMCALL_EXECUTE_ANSWER,
 202              "Received unexpected message %s (%i); expected MessageType::SIMCALL_EXECUTE_ANSWER (%i)",
 203              to_c_str(answer.type), (int)answer.type, (int)MessageType::SIMCALL_EXECUTE_ANSWER);
 204
 205   if (new_transition) {
 206     std::stringstream stream(answer.buffer.data());
 207     return deserialize_transition(aid, times_considered, stream);
 208   } else
 209     return nullptr;
 210 }
 211
 212 void RemoteApp::finalize_app(bool terminate_asap)
 213 {
 214   s_mc_message_int_t m = {};
 215   m.type               = MessageType::FINALIZE;
 216   m.value              = terminate_asap;
 217   xbt_assert(checker_side_->get_channel().send(m) == 0, "Could not ask the app to finalize on need");
 218
 219   s_mc_message_t answer;
 220   ssize_t s = checker_side_->get_channel().receive(answer);
 221   xbt_assert(s != -1, "Could not receive answer to FINALIZE");
 222   xbt_assert(s == sizeof answer, "Broken message (size=%zd; expected %zu)", s, sizeof answer);
 223   xbt_assert(answer.type == MessageType::FINALIZE_REPLY,
 224              "Received unexpected message %s (%i); expected MessageType::FINALIZE_REPLY (%i)", to_c_str(answer.type),
 225              (int)answer.type, (int)MessageType::FINALIZE_REPLY);
 226 }
 227
 228 } // namespace simgrid::mc