src/mc/Session.cpp

   1 /* Copyright (c) 2015-2016. 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 <fcntl.h>
   8 #include <signal.h>
   9
  10 #include <functional>
  11
  12 #include <xbt/log.h>
  13 #include <xbt/system_error.hpp>
  14 #include <simgrid/sg_config.h>
  15 #include <simgrid/modelchecker.h>
  16 #include <mc/mc.h>
  17
  18 #include "src/mc/Session.hpp"
  19 #include "src/mc/mc_state.h"
  20 #include "src/mc/mc_private.h"
  21
  22 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_Session, mc, "Model-checker session");
  23
  24 namespace simgrid {
  25 namespace mc {
  26
  27 static void setup_child_environment(int socket)
  28 {
  29 #ifdef __linux__
  30   // Make sure we do not outlive our parent:
  31   sigset_t mask;
  32   sigemptyset (&mask);
  33   if (sigprocmask(SIG_SETMASK, &mask, nullptr) < 0)
  34     throw simgrid::xbt::errno_error(errno, "Could not unblock signals");
  35   if (prctl(PR_SET_PDEATHSIG, SIGHUP) != 0)
  36     throw simgrid::xbt::errno_error(errno, "Could not PR_SET_PDEATHSIG");
  37 #endif
  38
  39   int res;
  40
  41   // Remove CLOEXEC in order to pass the socket to the exec-ed program:
  42   int fdflags = fcntl(socket, F_GETFD, 0);
  43   if (fdflags == -1 || fcntl(socket, F_SETFD, fdflags & ~FD_CLOEXEC) == -1)
  44     throw simgrid::xbt::errno_error(errno, "Could not remove CLOEXEC for socket");
  45
  46   // Set environment:
  47   setenv(MC_ENV_VARIABLE, "1", 1);
  48
  49   // Disable lazy relocation in the model-checked process.
  50   // We don't want the model-checked process to modify its .got.plt during
  51   // snapshot.
  52   setenv("LC_BIND_NOW", "1", 1);
  53
  54   char buffer[64];
  55   res = std::snprintf(buffer, sizeof(buffer), "%i", socket);
  56   if ((size_t) res >= sizeof(buffer) || res == -1)
  57     std::abort();
  58   setenv(MC_ENV_SOCKET_FD, buffer, 1);
  59 }
  60
  61 /** Execute some code in a forked process */
  62 template<class F>
  63 static inline
  64 pid_t do_fork(F code)
  65 {
  66   pid_t pid = fork();
  67   if (pid < 0)
  68     throw simgrid::xbt::errno_error(errno, "Could not fork model-checked process");
  69   if (pid != 0)
  70     return pid;
  71
  72   // Child-process:
  73   try {
  74     code();
  75     _exit(EXIT_SUCCESS);
  76   }
  77   catch(...) {
  78     // The callback should catch exceptions:
  79     std::terminate();
  80   }
  81 }
  82
  83 Session::Session(pid_t pid, int socket)
  84 {
  85   std::unique_ptr<simgrid::mc::Process> process(new simgrid::mc::Process(pid, socket));
  86   // TODO, automatic detection of the config from the process
  87   process->privatized(
  88     xbt_cfg_get_boolean("smpi/privatize_global_variables"));
  89   modelChecker_ = std::unique_ptr<ModelChecker>(
  90     new simgrid::mc::ModelChecker(std::move(process)));
  91   xbt_assert(mc_model_checker == nullptr);
  92   mc_model_checker = modelChecker_.get();
  93   mc_model_checker->start();
  94 }
  95
  96 Session::~Session()
  97 {
  98   this->close();
  99 }
 100
 101 void Session::execute(Transition const& transition)
 102 {
 103   modelChecker_->handle_simcall(transition);
 104   modelChecker_->wait_for_requests();
 105 }
 106
 107 void Session::logState()
 108 {
 109   if(_sg_mc_comms_determinism) {
 110     if (!simgrid::mc::initial_global_state->recv_deterministic &&
 111         simgrid::mc::initial_global_state->send_deterministic){
 112       XBT_INFO("******************************************************");
 113       XBT_INFO("**** Only-send-deterministic communication pattern ****");
 114       XBT_INFO("******************************************************");
 115       XBT_INFO("%s", simgrid::mc::initial_global_state->recv_diff);
 116     }else if(!simgrid::mc::initial_global_state->send_deterministic &&
 117         simgrid::mc::initial_global_state->recv_deterministic) {
 118       XBT_INFO("******************************************************");
 119       XBT_INFO("**** Only-recv-deterministic communication pattern ****");
 120       XBT_INFO("******************************************************");
 121       XBT_INFO("%s", simgrid::mc::initial_global_state->send_diff);
 122     }
 123   }
 124
 125   if (mc_stats->expanded_pairs == 0) {
 126     XBT_INFO("Expanded states = %lu", mc_stats->expanded_states);
 127     XBT_INFO("Visited states = %lu", mc_stats->visited_states);
 128   } else {
 129     XBT_INFO("Expanded pairs = %lu", mc_stats->expanded_pairs);
 130     XBT_INFO("Visited pairs = %lu", mc_stats->visited_pairs);
 131   }
 132   XBT_INFO("Executed transitions = %lu", mc_stats->executed_transitions);
 133   if ((_sg_mc_dot_output_file != nullptr) && (_sg_mc_dot_output_file[0] != '\0')) {
 134     fprintf(dot_output, "}\n");
 135     fclose(dot_output);
 136   }
 137   if (simgrid::mc::initial_global_state != nullptr
 138       && (_sg_mc_comms_determinism || _sg_mc_send_determinism)) {
 139     XBT_INFO("Send-deterministic : %s",
 140       !simgrid::mc::initial_global_state->send_deterministic ? "No" : "Yes");
 141     if (_sg_mc_comms_determinism)
 142       XBT_INFO("Recv-deterministic : %s",
 143         !simgrid::mc::initial_global_state->recv_deterministic ? "No" : "Yes");
 144   }
 145   if (getenv("SIMGRID_MC_SYSTEM_STATISTICS")){
 146     int ret=system("free");
 147     if(ret!=0)XBT_WARN("system call did not return 0, but %d",ret);
 148   }
 149 }
 150
 151 // static
 152 Session* Session::fork(std::function<void(void)> code)
 153 {
 154   // Create a AF_LOCAL socketpair used for exchanging messages
 155   // bewteen the model-checker process (ourselves) and the model-checked
 156   // process:
 157   int res;
 158   int sockets[2];
 159   res = socketpair(AF_LOCAL, SOCK_DGRAM | SOCK_CLOEXEC, 0, sockets);
 160   if (res == -1)
 161     throw simgrid::xbt::errno_error(errno, "Could not create socketpair");
 162
 163   pid_t pid = do_fork([&] {
 164     ::close(sockets[1]);
 165     setup_child_environment(sockets[0]);
 166     code();
 167     xbt_die("The model-checked process failed to exec()");
 168   });
 169
 170   // Parent (model-checker):
 171   ::close(sockets[0]);
 172
 173   return new Session(pid, sockets[1]);
 174 }
 175
 176 // static
 177 Session* Session::spawnv(const char *path, char *const argv[])
 178 {
 179   return Session::fork([&] {
 180     execv(path, argv);
 181   });
 182 }
 183
 184 // static
 185 Session* Session::spawnvp(const char *path, char *const argv[])
 186 {
 187   return Session::fork([&] {
 188     execvp(path, argv);
 189   });
 190 }
 191
 192 void Session::close()
 193 {
 194   if (modelChecker_) {
 195     modelChecker_->shutdown();
 196     modelChecker_ = nullptr;
 197     mc_model_checker = nullptr;
 198   }
 199 }
 200
 201 simgrid::mc::Session* session;
 202
 203 }
 204 }