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>
17 #include <xbt/automaton.h>
18 #include <xbt/automaton.hpp>
20 #include "ModelChecker.hpp"
21 #include "mc_protocol.h"
22 #include "mc_server.h"
23 #include "mc_private.h"
24 #include "mc_ignore.h"
25 #include "mcer_ignore.h"
27 #include "mc/mc_liveness.h"
29 using simgrid::mc::remote;
33 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_server, mc, "MC server logic");
35 // HArdcoded index for now:
36 #define SOCKET_FD_INDEX 0
37 #define SIGNAL_FD_INDEX 1
39 mc_server_t mc_server;
41 s_mc_server::s_mc_server(pid_t pid, int socket)
44 this->socket = socket;
47 void s_mc_server::start()
49 /* Wait for the target process to initialize and exchange a HELLO messages
50 * before trying to look at its memory map.
52 int res = MC_protocol_hello(socket);
54 throw std::system_error(res, std::system_category());
56 // Block SIGCHLD (this will be handled with accept/signalfd):
59 sigaddset(&set, SIGCHLD);
60 if (sigprocmask(SIG_BLOCK, &set, NULL) == -1)
61 throw std::system_error(errno, std::system_category());
64 sigfillset(&full_set);
66 // Prepare data for poll:
68 struct pollfd* socket_pollfd = &fds[SOCKET_FD_INDEX];
69 socket_pollfd->fd = socket;
70 socket_pollfd->events = POLLIN;
71 socket_pollfd->revents = 0;
73 int signal_fd = signalfd(-1, &set, 0);
75 throw std::system_error(errno, std::system_category());
77 struct pollfd* signalfd_pollfd = &fds[SIGNAL_FD_INDEX];
78 signalfd_pollfd->fd = signal_fd;
79 signalfd_pollfd->events = POLLIN;
80 signalfd_pollfd->revents = 0;
83 void s_mc_server::shutdown()
85 XBT_DEBUG("Shuting down model-checker");
87 simgrid::mc::Process* process = &mc_model_checker->process();
88 int status = process->status();
89 if (process->running()) {
90 XBT_DEBUG("Killing process");
91 kill(process->pid(), SIGTERM);
92 if (waitpid(process->pid(), &status, 0) == -1)
93 throw std::system_error(errno, std::system_category());
94 // TODO, handle the case when the process does not want to die with a timeout
95 process->terminate(status);
99 void s_mc_server::exit()
102 int status = mc_model_checker->process().status();
103 if (WIFEXITED(status))
104 ::exit(WEXITSTATUS(status));
105 else if (WIFSIGNALED(status)) {
106 // Try to uplicate the signal of the model-checked process.
107 // This is a temporary hack so we don't try too hard.
108 kill(mc_model_checker->process().pid(), WTERMSIG(status));
111 xbt_die("Unexpected status from model-checked process");
115 void s_mc_server::resume(simgrid::mc::Process* process)
117 int res = process->send_message(MC_MESSAGE_CONTINUE);
119 throw std::system_error(res, std::system_category());
120 process->cache_flags = (mc_process_cache_flags_t) 0;
124 void throw_socket_error(int fd)
127 socklen_t errlen = sizeof(error);
128 if (getsockopt(fd, SOL_SOCKET, SO_ERROR, (void *)&error, &errlen) == -1)
130 throw std::system_error(error, std::system_category());
133 bool s_mc_server::handle_events()
135 char buffer[MC_MESSAGE_LENGTH];
136 struct pollfd* socket_pollfd = &fds[SOCKET_FD_INDEX];
137 struct pollfd* signalfd_pollfd = &fds[SIGNAL_FD_INDEX];
139 while(poll(fds, 2, -1) == -1) {
144 throw std::system_error(errno, std::system_category());
148 if (socket_pollfd->revents) {
149 if (socket_pollfd->revents & POLLIN) {
151 ssize_t size = MC_receive_message(socket_pollfd->fd, buffer, sizeof(buffer), MSG_DONTWAIT);
152 if (size == -1 && errno != EAGAIN)
153 throw std::system_error(errno, std::system_category());
155 s_mc_message_t base_message;
156 if (size < (ssize_t) sizeof(base_message))
157 xbt_die("Broken message");
158 memcpy(&base_message, buffer, sizeof(base_message));
160 switch(base_message.type) {
162 case MC_MESSAGE_IGNORE_HEAP:
164 s_mc_ignore_heap_message_t message;
165 if (size != sizeof(message))
166 xbt_die("Broken messsage");
167 memcpy(&message, buffer, sizeof(message));
168 mc_heap_ignore_region_t region = xbt_new(s_mc_heap_ignore_region_t, 1);
169 *region = message.region;
170 MC_heap_region_ignore_insert(region);
174 case MC_MESSAGE_UNIGNORE_HEAP:
176 s_mc_ignore_memory_message_t message;
177 if (size != sizeof(message))
178 xbt_die("Broken messsage");
179 memcpy(&message, buffer, sizeof(message));
180 MC_heap_region_ignore_remove(
181 (void *)(std::uintptr_t) message.addr, message.size);
185 case MC_MESSAGE_IGNORE_MEMORY:
187 s_mc_ignore_memory_message_t message;
188 if (size != sizeof(message))
189 xbt_die("Broken messsage");
190 memcpy(&message, buffer, sizeof(message));
191 mc_model_checker->process().ignore_region(
192 message.addr, message.size);
196 case MC_MESSAGE_STACK_REGION:
198 s_mc_stack_region_message_t message;
199 if (size != sizeof(message))
200 xbt_die("Broken messsage");
201 memcpy(&message, buffer, sizeof(message));
202 stack_region_t stack_region = xbt_new(s_stack_region_t, 1);
203 *stack_region = message.stack_region;
204 MC_stack_area_add(stack_region);
208 case MC_MESSAGE_REGISTER_SYMBOL:
210 s_mc_register_symbol_message_t message;
211 if (size != sizeof(message))
212 xbt_die("Broken message");
213 memcpy(&message, buffer, sizeof(message));
214 if (message.callback)
215 xbt_die("Support for client-side function proposition is not implemented.");
216 XBT_DEBUG("Received symbol: %s", message.name);
218 if (_mc_property_automaton == NULL)
219 _mc_property_automaton = xbt_automaton_new();
221 simgrid::mc::Process* process = &mc_model_checker->process();
222 simgrid::mc::remote_ptr<int> address
223 = simgrid::mc::remote((int*) message.data);
224 simgrid::xbt::add_proposition(_mc_property_automaton,
226 [process, address]() { return process->read(address); }
232 case MC_MESSAGE_WAITING:
235 case MC_MESSAGE_ASSERTION_FAILED:
236 MC_report_assertion_error();
237 ::exit(SIMGRID_EXIT_SAFETY);
241 xbt_die("Unexpected message from model-checked application");
246 if (socket_pollfd->revents & POLLERR) {
247 throw_socket_error(socket_pollfd->fd);
249 if (socket_pollfd->revents & POLLHUP)
250 xbt_die("Socket hang up?");
253 if (signalfd_pollfd->revents) {
254 if (signalfd_pollfd->revents & POLLIN) {
255 this->handle_signals();
258 if (signalfd_pollfd->revents & POLLERR) {
259 throw_socket_error(signalfd_pollfd->fd);
261 if (signalfd_pollfd->revents & POLLHUP)
262 xbt_die("Signalfd hang up?");
268 void s_mc_server::loop()
270 while (mc_model_checker->process().running())
271 this->handle_events();
274 void s_mc_server::handle_signals()
276 struct signalfd_siginfo info;
277 struct pollfd* signalfd_pollfd = &fds[SIGNAL_FD_INDEX];
279 ssize_t size = read(signalfd_pollfd->fd, &info, sizeof(info));
284 throw std::system_error(errno, std::system_category());
285 } else if (size != sizeof(info))
286 return throw std::runtime_error(
287 "Bad communication with model-checked application");
291 this->on_signal(&info);
294 void s_mc_server::handle_waitpid()
296 XBT_DEBUG("Check for wait event");
299 while ((pid = waitpid(-1, &status, WNOHANG)) != 0) {
301 if (errno == ECHILD) {
303 if (mc_model_checker->process().running())
304 xbt_die("Inconsistent state");
308 XBT_ERROR("Could not wait for pid");
309 throw std::system_error(errno, std::system_category());
313 if (pid == mc_model_checker->process().pid()) {
314 if (WIFEXITED(status) || WIFSIGNALED(status)) {
315 XBT_DEBUG("Child process is over");
316 mc_model_checker->process().terminate(status);
322 void s_mc_server::on_signal(const struct signalfd_siginfo* info)
324 switch(info->ssi_signo) {
326 this->handle_waitpid();
333 void MC_server_wait_client(simgrid::mc::Process* process)
335 mc_server->resume(process);
336 while (mc_model_checker->process().running()) {
337 if (!mc_server->handle_events())
342 void MC_server_simcall_handle(simgrid::mc::Process* process, unsigned long pid, int value)
344 s_mc_simcall_handle_message m;
345 memset(&m, 0, sizeof(m));
346 m.type = MC_MESSAGE_SIMCALL_HANDLE;
349 mc_model_checker->process().send_message(m);
350 process->cache_flags = (mc_process_cache_flags_t) 0;
351 while (mc_model_checker->process().running()) {
352 if (!mc_server->handle_events())
357 void MC_server_loop(mc_server_t server)