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>
18 #include "ModelChecker.hpp"
19 #include "mc_protocol.h"
20 #include "mc_server.h"
21 #include "mc_private.h"
22 #include "mc_ignore.h"
23 #include "mcer_ignore.h"
26 using simgrid::mc::remote;
30 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_server, mc, "MC server logic");
32 // HArdcoded index for now:
33 #define SOCKET_FD_INDEX 0
34 #define SIGNAL_FD_INDEX 1
36 mc_server_t mc_server;
38 struct mc_symbol_pointer_callback
40 simgrid::mc::Process* process;
44 static int mc_symbol_pointer_callback_evaluate(void* p)
46 struct mc_symbol_pointer_callback* callback = (struct mc_symbol_pointer_callback*) p;
48 callback->process->read_bytes(&value, sizeof(value), remote(callback->value));
52 s_mc_server::s_mc_server(pid_t pid, int socket)
55 this->socket = socket;
58 void s_mc_server::start()
60 /* Wait for the target process to initialize and exchange a HELLO messages
61 * before trying to look at its memory map.
63 int res = MC_protocol_hello(socket);
65 throw std::system_error(res, std::system_category());
67 // Block SIGCHLD (this will be handled with accept/signalfd):
70 sigaddset(&set, SIGCHLD);
71 if (sigprocmask(SIG_BLOCK, &set, NULL) == -1)
72 throw std::system_error(errno, std::system_category());
75 sigfillset(&full_set);
77 // Prepare data for poll:
79 struct pollfd* socket_pollfd = &fds[SOCKET_FD_INDEX];
80 socket_pollfd->fd = socket;
81 socket_pollfd->events = POLLIN;
82 socket_pollfd->revents = 0;
84 int signal_fd = signalfd(-1, &set, 0);
86 throw std::system_error(errno, std::system_category());
88 struct pollfd* signalfd_pollfd = &fds[SIGNAL_FD_INDEX];
89 signalfd_pollfd->fd = signal_fd;
90 signalfd_pollfd->events = POLLIN;
91 signalfd_pollfd->revents = 0;
94 void s_mc_server::shutdown()
96 XBT_DEBUG("Shuting down model-checker");
98 simgrid::mc::Process* process = &mc_model_checker->process();
99 int status = process->status();
100 if (process->running()) {
101 XBT_DEBUG("Killing process");
102 kill(process->pid(), SIGTERM);
103 if (waitpid(process->pid(), &status, 0) == -1)
104 throw std::system_error(errno, std::system_category());
105 // TODO, handle the case when the process does not want to die with a timeout
106 process->terminate(status);
110 void s_mc_server::exit()
113 int status = mc_model_checker->process().status();
114 if (WIFEXITED(status))
115 ::exit(WEXITSTATUS(status));
116 else if (WIFSIGNALED(status)) {
117 // Try to uplicate the signal of the model-checked process.
118 // This is a temporary hack so we don't try too hard.
119 kill(mc_model_checker->process().pid(), WTERMSIG(status));
122 xbt_die("Unexpected status from model-checked process");
126 void s_mc_server::resume(simgrid::mc::Process* process)
128 int res = process->send_message(MC_MESSAGE_CONTINUE);
130 throw std::system_error(res, std::system_category());
131 process->cache_flags = (mc_process_cache_flags_t) 0;
135 void throw_socket_error(int fd)
138 socklen_t errlen = sizeof(error);
139 if (getsockopt(fd, SOL_SOCKET, SO_ERROR, (void *)&error, &errlen) == -1)
141 throw std::system_error(error, std::system_category());
144 bool s_mc_server::handle_events()
146 char buffer[MC_MESSAGE_LENGTH];
147 struct pollfd* socket_pollfd = &fds[SOCKET_FD_INDEX];
148 struct pollfd* signalfd_pollfd = &fds[SIGNAL_FD_INDEX];
150 while(poll(fds, 2, -1) == -1) {
155 throw std::system_error(errno, std::system_category());
159 if (socket_pollfd->revents) {
160 if (socket_pollfd->revents & POLLIN) {
162 ssize_t size = MC_receive_message(socket_pollfd->fd, buffer, sizeof(buffer), MSG_DONTWAIT);
163 if (size == -1 && errno != EAGAIN)
164 throw std::system_error(errno, std::system_category());
166 s_mc_message_t base_message;
167 if (size < (ssize_t) sizeof(base_message))
168 xbt_die("Broken message");
169 memcpy(&base_message, buffer, sizeof(base_message));
171 switch(base_message.type) {
173 case MC_MESSAGE_IGNORE_HEAP:
175 s_mc_ignore_heap_message_t message;
176 if (size != sizeof(message))
177 xbt_die("Broken messsage");
178 memcpy(&message, buffer, sizeof(message));
179 mc_heap_ignore_region_t region = xbt_new(s_mc_heap_ignore_region_t, 1);
180 *region = message.region;
181 MC_heap_region_ignore_insert(region);
185 case MC_MESSAGE_UNIGNORE_HEAP:
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_heap_region_ignore_remove(
192 (void *)(std::uintptr_t) message.addr, message.size);
196 case MC_MESSAGE_IGNORE_MEMORY:
198 s_mc_ignore_memory_message_t message;
199 if (size != sizeof(message))
200 xbt_die("Broken messsage");
201 memcpy(&message, buffer, sizeof(message));
202 mc_model_checker->process().ignore_region(
203 message.addr, message.size);
207 case MC_MESSAGE_STACK_REGION:
209 s_mc_stack_region_message_t message;
210 if (size != sizeof(message))
211 xbt_die("Broken messsage");
212 memcpy(&message, buffer, sizeof(message));
213 stack_region_t stack_region = xbt_new(s_stack_region_t, 1);
214 *stack_region = message.stack_region;
215 MC_stack_area_add(stack_region);
219 case MC_MESSAGE_REGISTER_SYMBOL:
221 s_mc_register_symbol_message_t message;
222 if (size != sizeof(message))
223 xbt_die("Broken message");
224 memcpy(&message, buffer, sizeof(message));
225 if (message.callback)
226 xbt_die("Support for callbacks/functions symbols not implemented in client/server mode.");
227 XBT_DEBUG("Received symbol: %s", message.name);
229 struct mc_symbol_pointer_callback* callback = xbt_new(struct mc_symbol_pointer_callback, 1);
230 callback->process = &mc_model_checker->process();
231 callback->value = message.data;
233 MC_automaton_new_propositional_symbol_callback(message.name,
234 mc_symbol_pointer_callback_evaluate, callback, free);
238 case MC_MESSAGE_WAITING:
241 case MC_MESSAGE_ASSERTION_FAILED:
242 MC_report_assertion_error();
243 ::exit(SIMGRID_EXIT_SAFETY);
247 xbt_die("Unexpected message from model-checked application");
252 if (socket_pollfd->revents & POLLERR) {
253 throw_socket_error(socket_pollfd->fd);
255 if (socket_pollfd->revents & POLLHUP)
256 xbt_die("Socket hang up?");
259 if (signalfd_pollfd->revents) {
260 if (signalfd_pollfd->revents & POLLIN) {
261 this->handle_signals();
264 if (signalfd_pollfd->revents & POLLERR) {
265 throw_socket_error(signalfd_pollfd->fd);
267 if (signalfd_pollfd->revents & POLLHUP)
268 xbt_die("Signalfd hang up?");
274 void s_mc_server::loop()
276 while (mc_model_checker->process().running())
277 this->handle_events();
280 void s_mc_server::handle_signals()
282 struct signalfd_siginfo info;
283 struct pollfd* signalfd_pollfd = &fds[SIGNAL_FD_INDEX];
285 ssize_t size = read(signalfd_pollfd->fd, &info, sizeof(info));
290 throw std::system_error(errno, std::system_category());
291 } else if (size != sizeof(info))
292 return throw std::runtime_error(
293 "Bad communication with model-checked application");
297 this->on_signal(&info);
300 void s_mc_server::handle_waitpid()
302 XBT_DEBUG("Check for wait event");
305 while ((pid = waitpid(-1, &status, WNOHANG)) != 0) {
307 if (errno == ECHILD) {
309 if (mc_model_checker->process().running())
310 xbt_die("Inconsistent state");
314 XBT_ERROR("Could not wait for pid");
315 throw std::system_error(errno, std::system_category());
319 if (pid == mc_model_checker->process().pid()) {
320 if (WIFEXITED(status) || WIFSIGNALED(status)) {
321 XBT_DEBUG("Child process is over");
322 mc_model_checker->process().terminate(status);
328 void s_mc_server::on_signal(const struct signalfd_siginfo* info)
330 switch(info->ssi_signo) {
332 this->handle_waitpid();
339 void MC_server_wait_client(simgrid::mc::Process* process)
341 mc_server->resume(process);
342 while (mc_model_checker->process().running()) {
343 if (!mc_server->handle_events())
348 void MC_server_simcall_handle(simgrid::mc::Process* process, unsigned long pid, int value)
350 s_mc_simcall_handle_message m;
351 memset(&m, 0, sizeof(m));
352 m.type = MC_MESSAGE_SIMCALL_HANDLE;
355 mc_model_checker->process().send_message(m);
356 process->cache_flags = (mc_process_cache_flags_t) 0;
357 while (mc_model_checker->process().running()) {
358 if (!mc_server->handle_events())
363 void MC_server_loop(mc_server_t server)