src/mc/Session.cpp

   1 /* Copyright (c) 2015-2018. The SimGrid Team.
   2  * All rights reserved.                                                     */
   3
   4 /* This program is free software; you can redistribute it and/or modify it
   5  * under the terms of the license (GNU LGPL) which comes with this package. */
   6
   7 #include <csignal>
   8 #include <fcntl.h>
   9
  10 #include <functional>
  11
  12 #include "xbt/log.h"
  13 #include "xbt/system_error.hpp"
  14 #include <mc/mc.h>
  15 #include <simgrid/modelchecker.h>
  16 #include <simgrid/sg_config.hpp>
  17
  18 #include "src/mc/Session.hpp"
  19 #include "src/mc/checker/Checker.hpp"
  20 #include "src/mc/mc_private.hpp"
  21 #include "src/mc/mc_state.hpp"
  22
  23 #include "src/smpi/include/private.hpp"
  24
  25 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_Session, mc, "Model-checker session");
  26 extern std::string _sg_mc_dot_output_file;
  27
  28 namespace simgrid {
  29 namespace mc {
  30
  31 static void setup_child_environment(int socket)
  32 {
  33 #ifdef __linux__
  34   // Make sure we do not outlive our parent:
  35   sigset_t mask;
  36   sigemptyset (&mask);
  37   if (sigprocmask(SIG_SETMASK, &mask, nullptr) < 0)
  38     throw simgrid::xbt::errno_error("Could not unblock signals");
  39   if (prctl(PR_SET_PDEATHSIG, SIGHUP) != 0)
  40     throw simgrid::xbt::errno_error("Could not PR_SET_PDEATHSIG");
  41 #endif
  42
  43   int res;
  44
  45   // Remove CLOEXEC in order to pass the socket to the exec-ed program:
  46   int fdflags = fcntl(socket, F_GETFD, 0);
  47   if (fdflags == -1 || fcntl(socket, F_SETFD, fdflags & ~FD_CLOEXEC) == -1)
  48     throw simgrid::xbt::errno_error("Could not remove CLOEXEC for socket");
  49
  50   // Set environment:
  51   setenv(MC_ENV_VARIABLE, "1", 1);
  52
  53   // Disable lazy relocation in the model-checked process.
  54   // We don't want the model-checked process to modify its .got.plt during
  55   // snapshot.
  56   setenv("LC_BIND_NOW", "1", 1);
  57
  58   char buffer[64];
  59   res = std::snprintf(buffer, sizeof(buffer), "%i", socket);
  60   if ((size_t) res >= sizeof(buffer) || res == -1)
  61     std::abort();
  62   setenv(MC_ENV_SOCKET_FD, buffer, 1);
  63 }
  64
  65 /** Execute some code in a forked process */
  66 template<class F>
  67 static inline
  68 pid_t do_fork(F code)
  69 {
  70   pid_t pid = fork();
  71   if (pid < 0)
  72     throw simgrid::xbt::errno_error("Could not fork model-checked process");
  73   if (pid != 0)
  74     return pid;
  75
  76   // Child-process:
  77   try {
  78     code();
  79     _exit(EXIT_SUCCESS);
  80   }
  81   catch(...) {
  82     // The callback should catch exceptions:
  83     std::terminate();
  84   }
  85 }
  86
  87 Session::Session(pid_t pid, int socket)
  88 {
  89   std::unique_ptr<simgrid::mc::RemoteClient> process(new simgrid::mc::RemoteClient(pid, socket));
  90   // TODO, automatic detection of the config from the process
  91   process->privatized(smpi_privatize_global_variables != SMPI_PRIVATIZE_NONE);
  92   modelChecker_ = std::unique_ptr<ModelChecker>(
  93     new simgrid::mc::ModelChecker(std::move(process)));
  94   xbt_assert(mc_model_checker == nullptr);
  95   mc_model_checker = modelChecker_.get();
  96   mc_model_checker->start();
  97 }
  98
  99 Session::~Session()
 100 {
 101   this->close();
 102 }
 103
 104 void Session::initialize()
 105 {
 106   xbt_assert(initialSnapshot_ == nullptr);
 107   mc_model_checker->wait_for_requests();
 108   initialSnapshot_ = simgrid::mc::take_snapshot(0);
 109 }
 110
 111 void Session::execute(Transition const& transition)
 112 {
 113   modelChecker_->handle_simcall(transition);
 114   modelChecker_->wait_for_requests();
 115 }
 116
 117 void Session::restoreInitialState()
 118 {
 119   simgrid::mc::restore_snapshot(this->initialSnapshot_);
 120 }
 121
 122 void Session::logState()
 123 {
 124   mc_model_checker->getChecker()->logState();
 125
 126   if (not _sg_mc_dot_output_file.empty()) {
 127     fprintf(dot_output, "}\n");
 128     fclose(dot_output);
 129   }
 130   if (getenv("SIMGRID_MC_SYSTEM_STATISTICS")){
 131     int ret=system("free");
 132     if(ret!=0)XBT_WARN("system call did not return 0, but %d",ret);
 133   }
 134 }
 135
 136 // static
 137 Session* Session::fork(std::function<void()> code)
 138 {
 139   // Create a AF_LOCAL socketpair used for exchanging messages
 140   // between the model-checker process (ourselves) and the model-checked
 141   // process:
 142   int res;
 143   int sockets[2];
 144   res = socketpair(AF_LOCAL, SOCK_SEQPACKET | SOCK_CLOEXEC, 0, sockets);
 145   if (res == -1)
 146     throw simgrid::xbt::errno_error("Could not create socketpair");
 147
 148   pid_t pid = do_fork([sockets, &code] {
 149     ::close(sockets[1]);
 150     setup_child_environment(sockets[0]);
 151     code();
 152     xbt_die("The model-checked process failed to exec()");
 153   });
 154
 155   // Parent (model-checker):
 156   ::close(sockets[0]);
 157
 158   return new Session(pid, sockets[1]);
 159 }
 160
 161 // static
 162 Session* Session::spawnv(const char *path, char *const argv[])
 163 {
 164   return Session::fork([path, argv] {
 165     execv(path, argv);
 166   });
 167 }
 168
 169 // static
 170 Session* Session::spawnvp(const char *file, char *const argv[])
 171 {
 172   return Session::fork([file, argv] {
 173     execvp(file, argv);
 174   });
 175 }
 176
 177 void Session::close()
 178 {
 179   initialSnapshot_ = nullptr;
 180   if (modelChecker_) {
 181     modelChecker_->shutdown();
 182     modelChecker_ = nullptr;
 183     mc_model_checker = nullptr;
 184   }
 185 }
 186
 187 simgrid::mc::Session* session;
 188
 189 }
 190 }