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. */
8 #include <system_error>
11 #include <sys/types.h>
13 #include <sys/socket.h>
14 #include <sys/signalfd.h>
15 #include <sys/ptrace.h>
18 #include <xbt/automaton.h>
19 #include <xbt/automaton.hpp>
21 #include "ModelChecker.hpp"
22 #include "mc_protocol.h"
23 #include "mc_server.h"
24 #include "mc_private.h"
25 #include "mc_ignore.h"
26 #include "mcer_ignore.h"
28 #include "src/mc/mc_liveness.h"
30 using simgrid::mc::remote;
34 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_server, mc, "MC server logic");
36 // HArdcoded index for now:
37 #define SOCKET_FD_INDEX 0
38 #define SIGNAL_FD_INDEX 1
40 mc_server_t mc_server;
42 s_mc_server::s_mc_server(pid_t pid_, int socket_)
43 : pid(pid_), socket(socket_) {}
45 void s_mc_server::start()
47 // Block SIGCHLD (this will be handled with accept/signalfd):
50 sigaddset(&set, SIGCHLD);
51 if (sigprocmask(SIG_BLOCK, &set, NULL) == -1)
52 throw std::system_error(errno, std::system_category());
55 sigfillset(&full_set);
57 // Prepare data for poll:
59 struct pollfd* socket_pollfd = &fds[SOCKET_FD_INDEX];
60 socket_pollfd->fd = socket;
61 socket_pollfd->events = POLLIN;
62 socket_pollfd->revents = 0;
64 int signal_fd = signalfd(-1, &set, 0);
66 throw std::system_error(errno, std::system_category());
68 struct pollfd* signalfd_pollfd = &fds[SIGNAL_FD_INDEX];
69 signalfd_pollfd->fd = signal_fd;
70 signalfd_pollfd->events = POLLIN;
71 signalfd_pollfd->revents = 0;
73 XBT_DEBUG("Waiting for the model-checked process");
76 // The model-checked process SIGSTOP itself to signal it's ready:
77 pid_t res = waitpid(pid, &status, __WALL);
78 if (res < 0 || !WIFSTOPPED(status) || WSTOPSIG(status) != SIGSTOP)
79 xbt_die("Could not wait model-checked process");
81 // The model-checked process is ready, we can read its memory layout:
82 MC_init_model_checker(pid, socket);
84 ptrace(PTRACE_CONT, pid, 0, 0);
87 void s_mc_server::shutdown()
89 XBT_DEBUG("Shuting down model-checker");
91 simgrid::mc::Process* process = &mc_model_checker->process();
92 int status = process->status();
93 if (process->running()) {
94 XBT_DEBUG("Killing process");
95 kill(process->pid(), SIGTERM);
96 if (waitpid(process->pid(), &status, 0) == -1)
97 throw std::system_error(errno, std::system_category());
98 // TODO, handle the case when the process does not want to die with a timeout
99 process->terminate(status);
103 void s_mc_server::exit()
106 int status = mc_model_checker->process().status();
107 if (WIFEXITED(status))
108 ::exit(WEXITSTATUS(status));
109 else if (WIFSIGNALED(status)) {
110 // Try to uplicate the signal of the model-checked process.
111 // This is a temporary hack so we don't try too hard.
112 kill(mc_model_checker->process().pid(), WTERMSIG(status));
115 xbt_die("Unexpected status from model-checked process");
119 void s_mc_server::resume(simgrid::mc::Process* process)
121 int res = process->send_message(MC_MESSAGE_CONTINUE);
123 throw std::system_error(res, std::system_category());
124 process->cache_flags = (mc_process_cache_flags_t) 0;
128 void throw_socket_error(int fd)
131 socklen_t errlen = sizeof(error);
132 if (getsockopt(fd, SOL_SOCKET, SO_ERROR, (void *)&error, &errlen) == -1)
134 throw std::system_error(error, std::system_category());
137 bool s_mc_server::handle_events()
139 char buffer[MC_MESSAGE_LENGTH];
140 struct pollfd* socket_pollfd = &fds[SOCKET_FD_INDEX];
141 struct pollfd* signalfd_pollfd = &fds[SIGNAL_FD_INDEX];
143 while(poll(fds, 2, -1) == -1) {
148 throw std::system_error(errno, std::system_category());
152 if (socket_pollfd->revents) {
153 if (socket_pollfd->revents & POLLIN) {
155 ssize_t size = MC_receive_message(socket_pollfd->fd, buffer, sizeof(buffer), MSG_DONTWAIT);
156 if (size == -1 && errno != EAGAIN)
157 throw std::system_error(errno, std::system_category());
159 s_mc_message_t base_message;
160 if (size < (ssize_t) sizeof(base_message))
161 xbt_die("Broken message");
162 memcpy(&base_message, buffer, sizeof(base_message));
164 switch(base_message.type) {
166 case MC_MESSAGE_IGNORE_HEAP:
168 s_mc_ignore_heap_message_t message;
169 if (size != sizeof(message))
170 xbt_die("Broken messsage");
171 memcpy(&message, buffer, sizeof(message));
172 mc_heap_ignore_region_t region = xbt_new(s_mc_heap_ignore_region_t, 1);
173 *region = message.region;
174 MC_heap_region_ignore_insert(region);
178 case MC_MESSAGE_UNIGNORE_HEAP:
180 s_mc_ignore_memory_message_t message;
181 if (size != sizeof(message))
182 xbt_die("Broken messsage");
183 memcpy(&message, buffer, sizeof(message));
184 MC_heap_region_ignore_remove(
185 (void *)(std::uintptr_t) message.addr, message.size);
189 case MC_MESSAGE_IGNORE_MEMORY:
191 s_mc_ignore_memory_message_t message;
192 if (size != sizeof(message))
193 xbt_die("Broken messsage");
194 memcpy(&message, buffer, sizeof(message));
195 mc_model_checker->process().ignore_region(
196 message.addr, message.size);
200 case MC_MESSAGE_STACK_REGION:
202 s_mc_stack_region_message_t message;
203 if (size != sizeof(message))
204 xbt_die("Broken messsage");
205 memcpy(&message, buffer, sizeof(message));
206 stack_region_t stack_region = xbt_new(s_stack_region_t, 1);
207 *stack_region = message.stack_region;
208 MC_stack_area_add(stack_region);
212 case MC_MESSAGE_REGISTER_SYMBOL:
214 s_mc_register_symbol_message_t message;
215 if (size != sizeof(message))
216 xbt_die("Broken message");
217 memcpy(&message, buffer, sizeof(message));
218 if (message.callback)
219 xbt_die("Support for client-side function proposition is not implemented.");
220 XBT_DEBUG("Received symbol: %s", message.name);
222 if (_mc_property_automaton == NULL)
223 _mc_property_automaton = xbt_automaton_new();
225 simgrid::mc::Process* process = &mc_model_checker->process();
226 simgrid::mc::remote_ptr<int> address
227 = simgrid::mc::remote((int*) message.data);
228 simgrid::xbt::add_proposition(_mc_property_automaton,
230 [process, address]() { return process->read(address); }
236 case MC_MESSAGE_WAITING:
239 case MC_MESSAGE_ASSERTION_FAILED:
240 MC_report_assertion_error();
241 ::exit(SIMGRID_EXIT_SAFETY);
245 xbt_die("Unexpected message from model-checked application");
250 if (socket_pollfd->revents & POLLERR) {
251 throw_socket_error(socket_pollfd->fd);
253 if (socket_pollfd->revents & POLLHUP)
254 xbt_die("Socket hang up?");
257 if (signalfd_pollfd->revents) {
258 if (signalfd_pollfd->revents & POLLIN) {
259 this->handle_signals();
262 if (signalfd_pollfd->revents & POLLERR) {
263 throw_socket_error(signalfd_pollfd->fd);
265 if (signalfd_pollfd->revents & POLLHUP)
266 xbt_die("Signalfd hang up?");
272 void s_mc_server::loop()
274 while (mc_model_checker->process().running())
275 this->handle_events();
278 void s_mc_server::handle_signals()
280 struct signalfd_siginfo info;
281 struct pollfd* signalfd_pollfd = &fds[SIGNAL_FD_INDEX];
283 ssize_t size = read(signalfd_pollfd->fd, &info, sizeof(info));
288 throw std::system_error(errno, std::system_category());
289 } else if (size != sizeof(info))
290 return throw std::runtime_error(
291 "Bad communication with model-checked application");
295 this->on_signal(&info);
298 void s_mc_server::handle_waitpid()
300 XBT_DEBUG("Check for wait event");
303 while ((pid = waitpid(-1, &status, WNOHANG)) != 0) {
305 if (errno == ECHILD) {
307 if (mc_model_checker->process().running())
308 xbt_die("Inconsistent state");
312 XBT_ERROR("Could not wait for pid");
313 throw std::system_error(errno, std::system_category());
317 if (pid == mc_model_checker->process().pid()) {
318 if (WIFEXITED(status) || WIFSIGNALED(status)) {
319 XBT_DEBUG("Child process is over");
320 mc_model_checker->process().terminate(status);
326 void s_mc_server::on_signal(const struct signalfd_siginfo* info)
328 switch(info->ssi_signo) {
330 this->handle_waitpid();
337 void MC_server_wait_client(simgrid::mc::Process* process)
339 mc_server->resume(process);
340 while (mc_model_checker->process().running()) {
341 if (!mc_server->handle_events())
346 void MC_server_simcall_handle(simgrid::mc::Process* process, unsigned long pid, int value)
348 s_mc_simcall_handle_message m;
349 memset(&m, 0, sizeof(m));
350 m.type = MC_MESSAGE_SIMCALL_HANDLE;
353 mc_model_checker->process().send_message(m);
354 process->cache_flags = (mc_process_cache_flags_t) 0;
355 while (mc_model_checker->process().running()) {
356 if (!mc_server->handle_events())
361 void MC_server_loop(mc_server_t server)