Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
afe4ba08a0eab1d486ed1ee60c3cf8cd1f408532
[simgrid.git] / src / mc / simgrid_mc.cpp
1 /* Copyright (c) 2015. 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 <exception>
8
9 #include <cstdlib>
10 #include <cstdio>
11 #include <cstring>
12
13 #include <signal.h>
14 #include <poll.h>
15
16 #include <unistd.h>
17
18 #include <sys/types.h>
19 #include <sys/socket.h>
20 #include <sys/wait.h>
21
22 #ifdef __linux__
23 #include <sys/prctl.h>
24 #endif
25
26 #include <xbt/log.h>
27
28 #include "simgrid/sg_config.h"
29 #include "xbt_modinter.h"
30
31 #include "mc_base.h"
32 #include "mc_private.h"
33 #include "mc_protocol.h"
34 #include "mc_server.h"
35 #include "mc_safety.h"
36 #include "mc_comm_pattern.h"
37 #include "mc_liveness.h"
38
39 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_main, mc, "Entry point for simgrid-mc");
40
41 static int do_child(int socket, char** argv)
42 {
43   XBT_DEBUG("Inside the child process PID=%i", (int) getpid());
44
45 #ifdef __linux__
46   // Make sure we do not outlive our parent:
47   if (prctl(PR_SET_PDEATHSIG, SIGHUP) != 0) {
48     std::perror("simgrid-mc");
49     return MC_SERVER_ERROR;
50   }
51 #endif
52
53   int res;
54
55   // Remove CLOEXEC in order to pass the socket to the exec-ed program:
56   int fdflags = fcntl(socket, F_GETFD, 0);
57   if (fdflags == -1) {
58     std::perror("simgrid-mc");
59     return MC_SERVER_ERROR;
60   }
61   if (fcntl(socket, F_SETFD, fdflags & ~FD_CLOEXEC) == -1) {
62     std::perror("simgrid-mc");
63     return MC_SERVER_ERROR;
64   }
65
66   XBT_DEBUG("CLOEXEC removed on socket %i", socket);
67
68   // Set environment:
69   setenv(MC_ENV_VARIABLE, "1", 1);
70
71   char buffer[64];
72   res = std::snprintf(buffer, sizeof(buffer), "%i", socket);
73   if ((size_t) res >= sizeof(buffer) || res == -1)
74     return MC_SERVER_ERROR;
75   setenv(MC_ENV_SOCKET_FD, buffer, 1);
76
77   execvp(argv[1], argv+1);
78   std::perror("simgrid-mc");
79   return MC_SERVER_ERROR;
80 }
81
82 static int do_parent(int socket, pid_t child)
83 {
84   XBT_DEBUG("Inside the parent process");
85   if (mc_server)
86     xbt_die("MC server already present");
87   try {
88     mc_mode = MC_MODE_SERVER;
89     mc_server = new s_mc_server(child, socket);
90     mc_server->start();
91     MC_init_model_checker(child, socket);
92     if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
93       MC_modelcheck_comm_determinism();
94     else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0')
95       MC_modelcheck_safety();
96     else
97       MC_modelcheck_liveness();
98     mc_server->shutdown();
99     mc_server->exit();
100   }
101   catch(std::exception& e) {
102     XBT_ERROR("Exception: %s", e.what());
103   }
104   exit(MC_SERVER_ERROR);
105 }
106
107 static char** argvdup(int argc, char** argv)
108 {
109   char** argv_copy = xbt_new(char*, argc+1);
110   std::memcpy(argv_copy, argv, sizeof(char*) * argc);
111   argv_copy[argc] = NULL;
112   return argv_copy;
113 }
114
115 int main(int argc, char** argv)
116 {
117   // We need to keep the original parameters in order to pass them to the
118   // model-checked process:
119   int argc_copy = argc;
120   char** argv_copy = argvdup(argc, argv);
121   xbt_log_init(&argc_copy, argv_copy);
122   sg_config_init(&argc_copy, argv_copy);
123
124   if (argc < 2)
125     xbt_die("Missing arguments.\n");
126
127   bool server_mode = true;
128   char* env = std::getenv("SIMGRID_MC_MODE");
129   if (env) {
130     if (std::strcmp(env, "server") == 0)
131       server_mode = true;
132     else if (std::strcmp(env, "standalone") == 0)
133       server_mode = false;
134     else
135       xbt_die("Unrecognised value for SIMGRID_MC_MODE (server/standalone)");
136   }
137
138   if (!server_mode) {
139     setenv(MC_ENV_VARIABLE, "1", 1);
140     execvp(argv[1], argv+1);
141
142     std::perror("simgrid-mc");
143     return 127;
144   }
145
146   // Create a AF_LOCAL socketpair:
147   int res;
148
149   int sockets[2];
150   res = socketpair(AF_LOCAL, SOCK_DGRAM | SOCK_CLOEXEC, 0, sockets);
151   if (res == -1) {
152     perror("simgrid-mc");
153     return MC_SERVER_ERROR;
154   }
155
156   XBT_DEBUG("Created socketpair");
157
158   pid_t pid = fork();
159   if (pid < 0) {
160     perror("simgrid-mc");
161     return MC_SERVER_ERROR;
162   } else if (pid == 0) {
163     close(sockets[1]);
164     return do_child(sockets[0], argv);
165   } else {
166     close(sockets[0]);
167     return do_parent(sockets[1], pid);
168   }
169
170   return 0;
171 }