-pid_t do_fork(F f)
-{
- pid_t pid = fork();
- if (pid < 0)
- throw simgrid::xbt::errno_error(errno, "Could not fork model-checked process");
- if (pid != 0)
- return pid;
-
- // Child-process:
- try {
- f();
- std::exit(EXIT_SUCCESS);
- }
- catch(...) {
- // The callback should catch exceptions:
- abort();
- }
-}
-
-static
-int exec_model_checked(int socket, char** argv)
-{
- XBT_DEBUG("Inside the child process PID=%i", (int) getpid());
-
-#ifdef __linux__
- // Make sure we do not outlive our parent:
- sigset_t mask;
- sigemptyset (&mask);
- if (sigprocmask(SIG_SETMASK, &mask, nullptr) < 0)
- throw simgrid::xbt::errno_error(errno, "Could not unblock signals");
- if (prctl(PR_SET_PDEATHSIG, SIGHUP) != 0)
- throw simgrid::xbt::errno_error(errno, "Could not PR_SET_PDEATHSIG");
-#endif
-
- int res;
-
- // Remove CLOEXEC in order to pass the socket to the exec-ed program:
- int fdflags = fcntl(socket, F_GETFD, 0);
- if (fdflags == -1 || fcntl(socket, F_SETFD, fdflags & ~FD_CLOEXEC) == -1)
- throw simgrid::xbt::errno_error(errno, "Could not remove CLOEXEC for socket");
-
- // Set environment:
- setenv(MC_ENV_VARIABLE, "1", 1);
-
- // Disable lazy relocation in the model-checked process.
- // We don't want the model-checked process to modify its .got.plt during
- // snapshot.
- setenv("LC_BIND_NOW", "1", 1);
-
- char buffer[64];
- res = std::snprintf(buffer, sizeof(buffer), "%i", socket);
- if ((size_t) res >= sizeof(buffer) || res == -1)
- std::abort();
- setenv(MC_ENV_SOCKET_FD, buffer, 1);
-
- execvp(argv[1], argv+1);
-
- XBT_ERROR("Could not run the model-checked program");
- // This is the value used by system() and popen() in this case:
- return 127;
-}
-
-static
-std::pair<pid_t, int> create_model_checked(char** argv)
-{
- // Create a AF_LOCAL socketpair used for exchanging messages
- // bewteen the model-checker process (ourselves) and the model-checked
- // process:
- int res;
- int sockets[2];
- res = socketpair(AF_LOCAL, SOCK_DGRAM | SOCK_CLOEXEC, 0, sockets);
- if (res == -1)
- throw simgrid::xbt::errno_error(errno, "Could not create socketpair");
-
- pid_t pid = do_fork([&] {
- close(sockets[1]);
- int res = exec_model_checked(sockets[0], argv);
- XBT_DEBUG("Error in the child process creation");
- exit(res);
- });
-
- // Parent (model-checker):
- close(sockets[0]);
- return std::make_pair(pid, sockets[1]);
-}
-
-static