1 /* Copyright (c) 2015-2016. The SimGrid Team.
2 * All rights reserved. */
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. */
12 #include <xbt/system_error.hpp>
13 #include <simgrid/sg_config.h>
14 #include <simgrid/modelchecker.h>
16 #include "src/mc/Session.hpp"
18 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_Session, mc, "Model-checker session");
23 static void setup_child_environment(int socket)
26 // Make sure we do not outlive our parent:
29 if (sigprocmask(SIG_SETMASK, &mask, nullptr) < 0)
30 throw simgrid::xbt::errno_error(errno, "Could not unblock signals");
31 if (prctl(PR_SET_PDEATHSIG, SIGHUP) != 0)
32 throw simgrid::xbt::errno_error(errno, "Could not PR_SET_PDEATHSIG");
37 // Remove CLOEXEC in order to pass the socket to the exec-ed program:
38 int fdflags = fcntl(socket, F_GETFD, 0);
39 if (fdflags == -1 || fcntl(socket, F_SETFD, fdflags & ~FD_CLOEXEC) == -1)
40 throw simgrid::xbt::errno_error(errno, "Could not remove CLOEXEC for socket");
43 setenv(MC_ENV_VARIABLE, "1", 1);
45 // Disable lazy relocation in the model-checked process.
46 // We don't want the model-checked process to modify its .got.plt during
48 setenv("LC_BIND_NOW", "1", 1);
51 res = std::snprintf(buffer, sizeof(buffer), "%i", socket);
52 if ((size_t) res >= sizeof(buffer) || res == -1)
54 setenv(MC_ENV_SOCKET_FD, buffer, 1);
57 /** Execute some code in a forked process */
64 throw simgrid::xbt::errno_error(errno, "Could not fork model-checked process");
74 // The callback should catch exceptions:
79 Session::Session(pid_t pid, int socket)
81 std::unique_ptr<simgrid::mc::Process> process(new simgrid::mc::Process(pid, socket));
82 // TODO, automatic detection of the config from the process
84 sg_cfg_get_boolean("smpi/privatize_global_variables"));
85 modelChecker_ = std::unique_ptr<ModelChecker>(
86 new simgrid::mc::ModelChecker(std::move(process)));
87 xbt_assert(mc_model_checker == nullptr);
88 mc_model_checker = modelChecker_.get();
89 mc_model_checker->start();
98 Session* Session::fork(std::function<void(void)> code)
100 // Create a AF_LOCAL socketpair used for exchanging messages
101 // bewteen the model-checker process (ourselves) and the model-checked
105 res = socketpair(AF_LOCAL, SOCK_DGRAM | SOCK_CLOEXEC, 0, sockets);
107 throw simgrid::xbt::errno_error(errno, "Could not create socketpair");
109 pid_t pid = do_fork([&] {
111 setup_child_environment(sockets[0]);
113 xbt_die("The model-checked process failed to exec()");
116 // Parent (model-checker):
119 return new Session(pid, sockets[1]);
123 Session* Session::spawnv(const char *path, char *const argv[])
125 return Session::fork([&] {
131 Session* Session::spawnvp(const char *path, char *const argv[])
133 return Session::fork([&] {
138 void Session::close()
141 modelChecker_->shutdown();
142 modelChecker_ = nullptr;
143 mc_model_checker = nullptr;
147 simgrid::mc::Session* session;