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 "mc_model_checker.h"
19 #include "mc_protocol.h"
20 #include "mc_server.h"
21 #include "mc_private.h"
23 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_server, mc, "MC server logic");
25 // HArdcoded index for now:
26 #define SOCKET_FD_INDEX 0
27 #define SIGNAL_FD_INDEX 1
29 mc_server_t mc_server;
31 int MC_server_init(pid_t pid, int socket)
34 xbt_die("MC server already present");
35 mc_mode = MC_MODE_SERVER;
36 mc_server = new s_mc_server(pid, socket);
41 void MC_server_run(void)
44 mc_server->resume(&mc_model_checker->process);
46 mc_server->shutdown();
49 catch(std::exception& e) {
51 exit(MC_SERVER_ERROR);
55 s_mc_server::s_mc_server(pid_t pid, int socket)
58 this->socket = socket;
61 void s_mc_server::start()
63 /* Wait for the target process to initialize and exchange a HELLO messages
64 * before trying to look at its memory map.
66 XBT_DEBUG("Greeting the MC client");
67 int res = MC_protocol_hello(socket);
69 throw std::system_error(res, std::system_category());
70 XBT_DEBUG("Greeted the MC client");
72 MC_init_pid(pid, socket);
74 // Block SIGCHLD (this will be handled with accept/signalfd):
77 sigaddset(&set, SIGCHLD);
78 if (sigprocmask(SIG_BLOCK, &set, NULL) == -1)
79 throw std::system_error(errno, std::system_category());
82 sigfillset(&full_set);
84 // Prepare data for poll:
86 struct pollfd* socket_pollfd = &fds[SOCKET_FD_INDEX];
87 socket_pollfd->fd = socket;
88 socket_pollfd->events = POLLIN;
89 socket_pollfd->revents = 0;
91 int signal_fd = signalfd(-1, &set, 0);
93 throw std::system_error(errno, std::system_category());
95 struct pollfd* signalfd_pollfd = &fds[SIGNAL_FD_INDEX];
96 signalfd_pollfd->fd = signal_fd;
97 signalfd_pollfd->events = POLLIN;
98 signalfd_pollfd->revents = 0;
101 void s_mc_server::shutdown()
103 XBT_DEBUG("Shuting down model-checker");
105 mc_process_t process = &mc_model_checker->process;
106 int status = process->status;
107 if (process->running) {
108 XBT_DEBUG("Killing process");
109 kill(process->pid, SIGTERM);
110 if (waitpid(process->pid, &status, 0) == -1)
111 throw std::system_error(errno, std::system_category());
112 // TODO, handle the case when the process does not want to die with a timeout
113 process->status = status;
117 void s_mc_server::exit()
120 int status = mc_model_checker->process.status;
121 if (WIFEXITED(status))
122 ::exit(WEXITSTATUS(status));
123 else if (WIFSIGNALED(status)) {
124 // Try to uplicate the signal of the model-checked process.
125 // This is a temporary hack so we don't try too hard.
126 kill(mc_model_checker->process.pid, WTERMSIG(status));
129 xbt_die("Unexpected status from model-checked process");
133 void s_mc_server::resume(mc_process_t process)
135 int socket = process->socket;
136 int res = MC_protocol_send_simple_message(socket, MC_MESSAGE_CONTINUE);
138 throw std::system_error(res, std::system_category());
142 void throw_socket_error(int fd)
145 socklen_t errlen = sizeof(error);
146 if (getsockopt(fd, SOL_SOCKET, SO_ERROR, (void *)&error, &errlen) == -1)
148 throw std::system_error(error, std::system_category());
151 void s_mc_server::handle_events()
153 s_mc_message_t message;
154 struct pollfd* socket_pollfd = &fds[SOCKET_FD_INDEX];
155 struct pollfd* signalfd_pollfd = &fds[SIGNAL_FD_INDEX];
157 while(poll(fds, 2, -1) == -1) {
162 throw std::system_error(errno, std::system_category());
166 if (socket_pollfd->revents) {
167 if (socket_pollfd->revents & POLLIN) {
168 ssize_t size = recv(socket_pollfd->fd, &message, sizeof(message), MSG_DONTWAIT);
169 if (size == -1 && errno != EAGAIN)
170 throw std::system_error(errno, std::system_category());
171 else switch(message.type) {
173 xbt_die("Unexpected message from model-checked application");
177 if (socket_pollfd->revents & POLLERR) {
178 throw_socket_error(socket_pollfd->fd);
180 if (socket_pollfd->revents & POLLHUP)
181 xbt_die("Socket hang up?");
184 if (signalfd_pollfd->revents) {
185 if (signalfd_pollfd->revents & POLLIN) {
186 this->handle_signals();
189 if (signalfd_pollfd->revents & POLLERR) {
190 throw_socket_error(signalfd_pollfd->fd);
192 if (signalfd_pollfd->revents & POLLHUP)
193 xbt_die("Signalfd hang up?");
197 void s_mc_server::loop()
199 while (mc_model_checker->process.running)
200 this->handle_events();
203 void s_mc_server::handle_signals()
205 struct signalfd_siginfo info;
206 struct pollfd* signalfd_pollfd = &fds[SIGNAL_FD_INDEX];
208 ssize_t size = read(signalfd_pollfd->fd, &info, sizeof(info));
213 throw std::system_error(errno, std::system_category());
214 } else if (size != sizeof(info))
215 return throw std::runtime_error(
216 "Bad communication with model-checked application");
220 this->on_signal(&info);
223 void s_mc_server::handle_waitpid()
225 XBT_DEBUG("Check for wait event");
228 while ((pid = waitpid(-1, &status, WNOHANG)) != 0) {
230 if (errno == ECHILD) {
232 if (mc_model_checker->process.running)
233 xbt_die("Inconsistent state");
237 XBT_ERROR("Could not wait for pid: %s", strerror(errno));
238 throw std::system_error(errno, std::system_category());
242 if (pid == mc_model_checker->process.pid) {
243 if (WIFEXITED(status) || WIFSIGNALED(status)) {
244 XBT_DEBUG("Child process is over");
245 mc_model_checker->process.status = status;
246 mc_model_checker->process.running = false;
252 void s_mc_server::on_signal(const struct signalfd_siginfo* info)
254 switch(info->ssi_signo) {
256 this->handle_waitpid();