1 /* Copyright (c) 2015. 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. */
21 #include <sys/types.h>
22 #include <sys/socket.h>
24 #include <sys/ptrace.h>
27 #include <sys/prctl.h>
31 #include <xbt/sysdep.h>
32 #include <xbt/system_error.hpp>
34 #include "simgrid/sg_config.h"
35 #include "src/xbt_modinter.h"
37 #include "src/mc/mc_base.h"
38 #include "src/mc/mc_private.h"
39 #include "src/mc/mc_protocol.h"
40 #include "src/mc/mc_safety.h"
41 #include "src/mc/mc_comm_pattern.h"
42 #include "src/mc/mc_liveness.h"
43 #include "src/mc/mc_exit.h"
45 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_main, mc, "Entry point for simgrid-mc");
47 /** Execute some code in a forked process */
54 throw simgrid::xbt::errno_error(errno, "Could not fork model-checked process");
61 std::exit(EXIT_SUCCESS);
64 // The callback should catch exceptions:
70 int exec_model_checked(int socket, char** argv)
72 XBT_DEBUG("Inside the child process PID=%i", (int) getpid());
75 // Make sure we do not outlive our parent:
78 if (sigprocmask(SIG_SETMASK, &mask, nullptr) < 0)
79 throw simgrid::xbt::errno_error(errno, "Could not unblock signals");
80 if (prctl(PR_SET_PDEATHSIG, SIGHUP) != 0)
81 throw simgrid::xbt::errno_error(errno, "Could not PR_SET_PDEATHSIG");
86 // Remove CLOEXEC in order to pass the socket to the exec-ed program:
87 int fdflags = fcntl(socket, F_GETFD, 0);
88 if (fdflags == -1 || fcntl(socket, F_SETFD, fdflags & ~FD_CLOEXEC) == -1)
89 throw simgrid::xbt::errno_error(errno, "Could not remove CLOEXEC for socket");
92 setenv(MC_ENV_VARIABLE, "1", 1);
94 // Disable lazy relocation in the model-checked process.
95 // We don't want the model-checked process to modify its .got.plt during
97 setenv("LC_BIND_NOW", "1", 1);
100 res = std::snprintf(buffer, sizeof(buffer), "%i", socket);
101 if ((size_t) res >= sizeof(buffer) || res == -1)
103 setenv(MC_ENV_SOCKET_FD, buffer, 1);
105 execvp(argv[1], argv+1);
107 XBT_ERROR("Could not run the model-checked program");
108 // This is the value used by system() and popen() in this case:
113 std::pair<pid_t, int> create_model_checked(char** argv)
115 // Create a AF_LOCAL socketpair used for exchanging messages
116 // bewteen the model-checker process (ourselves) and the model-checked
120 res = socketpair(AF_LOCAL, SOCK_DGRAM | SOCK_CLOEXEC, 0, sockets);
122 throw simgrid::xbt::errno_error(errno, "Could not create socketpair");
124 pid_t pid = do_fork([&] {
126 int res = exec_model_checked(sockets[0], argv);
127 XBT_DEBUG("Error in the child process creation");
131 // Parent (model-checker):
133 return std::make_pair(pid, sockets[1]);
137 char** argvdup(int argc, char** argv)
139 char** argv_copy = xbt_new(char*, argc+1);
140 std::memcpy(argv_copy, argv, sizeof(char*) * argc);
141 argv_copy[argc] = nullptr;
145 int main(int argc, char** argv)
149 xbt_die("Missing arguments.\n");
151 _sg_do_model_check = 1;
153 // The initialisation function can touch argv.
154 // We need to keep the original parameters in order to pass them to the
155 // model-checked process so we make a copy of them:
156 int argc_copy = argc;
157 char** argv_copy = argvdup(argc, argv);
158 xbt_log_init(&argc_copy, argv_copy);
159 sg_config_init(&argc_copy, argv_copy);
162 pid_t model_checked_pid;
163 std::tie(model_checked_pid, sock) = create_model_checked(argv);
164 XBT_DEBUG("Inside the parent process");
165 if (mc_model_checker)
166 xbt_die("MC server already present");
168 mc_mode = MC_MODE_SERVER;
169 std::unique_ptr<simgrid::mc::Process> process(new simgrid::mc::Process(model_checked_pid, sock));
170 process->privatized(sg_cfg_get_boolean("smpi/privatize_global_variables"));
171 mc_model_checker = new simgrid::mc::ModelChecker(std::move(process));
172 mc_model_checker->start();
174 if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
175 res = MC_modelcheck_comm_determinism();
176 else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0')
177 res = simgrid::mc::modelcheck_safety();
179 res = simgrid::mc::modelcheck_liveness();
180 mc_model_checker->shutdown();
183 catch(std::exception& e) {
184 XBT_ERROR("Exception: %s", e.what());
185 return SIMGRID_MC_EXIT_ERROR;
188 XBT_ERROR("Unknown exception");
189 return SIMGRID_MC_EXIT_ERROR;