src/mc/Session.cpp

   1 /* Copyright (c) 2015-2020. 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/Session.hpp"
   7 #include "src/mc/checker/Checker.hpp"
   8 #include "src/mc/mc_config.hpp"
   9 #include "src/internal_config.h" // HAVE_SMPI
  10 #if HAVE_SMPI
  11 #include "smpi/smpi.h"
  12 #endif
  13 #include "src/mc/mc_private.hpp"
  14 #include "src/mc/mc_state.hpp"
  15 #include "xbt/log.h"
  16 #include "xbt/system_error.hpp"
  17
  18 #include <array>
  19 #include <memory>
  20 #include <string>
  21
  22 #include <fcntl.h>
  23 #ifdef __linux__
  24 #include <sys/prctl.h>
  25 #endif
  26
  27 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_Session, mc, "Model-checker session");
  28
  29 namespace simgrid {
  30 namespace mc {
  31
  32 template <class Code> void run_child_process(int socket, Code code)
  33 {
  34   /* On startup, simix_global_init() calls simgrid::mc::Client::initialize(), which checks whether the MC_ENV_SOCKET_FD
  35    * env variable is set. If so, MC mode is assumed, and the client is setup from its side
  36    */
  37
  38 #ifdef __linux__
  39   // Make sure we do not outlive our parent
  40   sigset_t mask;
  41   sigemptyset (&mask);
  42   xbt_assert(sigprocmask(SIG_SETMASK, &mask, nullptr) >= 0, "Could not unblock signals");
  43   xbt_assert(prctl(PR_SET_PDEATHSIG, SIGHUP) == 0, "Could not PR_SET_PDEATHSIG");
  44 #endif
  45
  46   // Remove CLOEXEC to pass the socket to the application
  47   int fdflags = fcntl(socket, F_GETFD, 0);
  48   xbt_assert(fdflags != -1 && fcntl(socket, F_SETFD, fdflags & ~FD_CLOEXEC) != -1,
  49              "Could not remove CLOEXEC for socket");
  50
  51   // Disable lazy relocation in the model-checked process to prevent the application from
  52   // modifying its .got.plt during snapshot.
  53   setenv("LC_BIND_NOW", "1", 1);
  54
  55   setenv(MC_ENV_SOCKET_FD, std::to_string(socket).c_str(), 1);
  56
  57   code();
  58 }
  59
  60 Session::Session(const std::function<void()>& code)
  61 {
  62 #if HAVE_SMPI
  63   smpi_init_options();//only performed once
  64   xbt_assert(smpi_cfg_privatization() != SmpiPrivStrategies::MMAP,
  65              "Please use the dlopen privatization schema when model-checking SMPI code");
  66 #endif
  67
  68   // Create an AF_LOCAL socketpair used for exchanging messages
  69   // between the model-checker process (ourselves) and the model-checked
  70   // process:
  71   int sockets[2];
  72   int res = socketpair(AF_LOCAL, SOCK_SEQPACKET | SOCK_CLOEXEC, 0, sockets);
  73   xbt_assert(res != -1, "Could not create socketpair");
  74
  75   pid_t pid = fork();
  76   xbt_assert(pid >= 0, "Could not fork model-checked process");
  77
  78   if (pid == 0) { // Child
  79     ::close(sockets[1]);
  80     run_child_process(sockets[0], code);
  81     DIE_IMPOSSIBLE;
  82   }
  83
  84   // Parent (model-checker):
  85   ::close(sockets[0]);
  86
  87   xbt_assert(mc_model_checker == nullptr, "Did you manage to start the MC twice in this process?");
  88
  89   auto process = std::make_unique<simgrid::mc::RemoteSimulation>(pid);
  90   model_checker_ = std::make_unique<simgrid::mc::ModelChecker>(std::move(process), sockets[1]);
  91
  92   mc_model_checker = model_checker_.get();
  93   model_checker_->start();
  94 }
  95
  96 Session::~Session()
  97 {
  98   this->close();
  99 }
 100
 101 /** Take the initial snapshot of the application, that must be stopped. */
 102 void Session::initialize()
 103 {
 104   xbt_assert(initial_snapshot_ == nullptr);
 105   model_checker_->wait_for_requests();
 106   initial_snapshot_ = std::make_shared<simgrid::mc::Snapshot>(0);
 107 }
 108
 109 void Session::execute(Transition const& transition) const
 110 {
 111   model_checker_->handle_simcall(transition);
 112   model_checker_->wait_for_requests();
 113 }
 114
 115 void Session::restore_initial_state() const
 116 {
 117   this->initial_snapshot_->restore(&model_checker_->get_remote_simulation());
 118 }
 119
 120 void Session::log_state() const
 121 {
 122   model_checker_->getChecker()->log_state();
 123
 124   if (not _sg_mc_dot_output_file.get().empty()) {
 125     fprintf(dot_output, "}\n");
 126     fclose(dot_output);
 127   }
 128   if (getenv("SIMGRID_MC_SYSTEM_STATISTICS")){
 129     int ret=system("free");
 130     if (ret != 0)
 131       XBT_WARN("Call to system(free) did not return 0, but %d", ret);
 132   }
 133 }
 134
 135 void Session::close()
 136 {
 137   initial_snapshot_ = nullptr;
 138   if (model_checker_) {
 139     model_checker_->shutdown();
 140     model_checker_   = nullptr;
 141     mc_model_checker = nullptr;
 142   }
 143 }
 144
 145 bool Session::actor_is_enabled(aid_t pid) const
 146 {
 147   s_mc_message_actor_enabled_t msg{simgrid::mc::MessageType::ACTOR_ENABLED, pid};
 148   model_checker_->channel().send(msg);
 149   std::array<char, MC_MESSAGE_LENGTH> buff;
 150   ssize_t received = model_checker_->channel().receive(buff.data(), buff.size(), true);
 151   xbt_assert(received == sizeof(s_mc_message_int_t), "Unexpected size in answer to ACTOR_ENABLED");
 152   return ((s_mc_message_int_t*)buff.data())->value;
 153 }
 154
 155 simgrid::mc::Session* session;
 156
 157 }
 158 }