Logo AND Algorithmique Numérique Distribuée

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