Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
[mc] Merge Server class into ModelChecker
[simgrid.git] / src / mc / ModelChecker.cpp
1 /* Copyright (c) 2008-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 <cassert>
8
9 #include <poll.h>
10 #include <sys/types.h>
11 #include <sys/wait.h>
12 #include <sys/socket.h>
13 #include <sys/signalfd.h>
14 #include <sys/ptrace.h>
15
16 #include <memory>
17 #include <system_error>
18
19 #include <xbt/log.h>
20 #include <xbt/automaton.h>
21 #include <xbt/automaton.hpp>
22
23 #include "simgrid/sg_config.h"
24
25 #include "ModelChecker.hpp"
26 #include "PageStore.hpp"
27 #include "ModelChecker.hpp"
28 #include "mc_protocol.h"
29 #include "mc_private.h"
30 #include "mc_ignore.h"
31 #include "mcer_ignore.h"
32 #include "mc_exit.h"
33 #include "src/mc/mc_liveness.h"
34
35 extern "C" {
36
37 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_ModelChecker, mc, "ModelChecker");
38
39 }
40
41 ::simgrid::mc::ModelChecker* mc_model_checker = nullptr;
42
43 using simgrid::mc::remote;
44
45 // Hardcoded index for now:
46 #define SOCKET_FD_INDEX 0
47 #define SIGNAL_FD_INDEX 1
48
49 namespace simgrid {
50 namespace mc {
51
52 ModelChecker::ModelChecker(pid_t pid, int socket) :
53   pid_(pid), socket_(socket),
54   hostnames_(xbt_dict_new()),
55   page_store_(500),
56   parent_snapshot_(nullptr)
57 {
58 }
59
60 ModelChecker::~ModelChecker()
61 {
62   xbt_dict_free(&this->hostnames_);
63 }
64
65 const char* ModelChecker::get_host_name(const char* hostname)
66 {
67   // Lookup the host name in the dictionary (or create it):
68   xbt_dictelm_t elt = xbt_dict_get_elm_or_null(this->hostnames_, hostname);
69   if (!elt) {
70     xbt_dict_set(this->hostnames_, hostname, nullptr, nullptr);
71     elt = xbt_dict_get_elm_or_null(this->hostnames_, hostname);
72     assert(elt);
73   }
74   return elt->key;
75 }
76
77 void ModelChecker::start()
78 {
79   // Block SIGCHLD (this will be handled with accept/signalfd):
80   sigset_t set;
81   sigemptyset(&set);
82   sigaddset(&set, SIGCHLD);
83   if (sigprocmask(SIG_BLOCK, &set, nullptr) == -1)
84     throw std::system_error(errno, std::system_category());
85
86   sigset_t full_set;
87   sigfillset(&full_set);
88
89   // Prepare data for poll:
90
91   struct pollfd* socket_pollfd = &fds_[SOCKET_FD_INDEX];
92   socket_pollfd->fd = socket_;
93   socket_pollfd->events = POLLIN;
94   socket_pollfd->revents = 0;
95
96   int signal_fd = signalfd(-1, &set, 0);
97   if (signal_fd == -1)
98     throw std::system_error(errno, std::system_category());
99
100   struct pollfd* signalfd_pollfd = &fds_[SIGNAL_FD_INDEX];
101   signalfd_pollfd->fd = signal_fd;
102   signalfd_pollfd->events = POLLIN;
103   signalfd_pollfd->revents = 0;
104
105   XBT_DEBUG("Waiting for the model-checked process");
106   int status;
107
108   // The model-checked process SIGSTOP itself to signal it's ready:
109   pid_t res = waitpid(pid_, &status, __WALL);
110   if (res < 0 || !WIFSTOPPED(status) || WSTOPSIG(status) != SIGSTOP)
111     xbt_die("Could not wait model-checked process");
112
113   assert(process_ == nullptr);
114   process_ = std::unique_ptr<Process>(new Process(pid_, socket_));
115   // TODO, avoid direct dependency on sg_cfg
116   process_->privatized(sg_cfg_get_boolean("smpi/privatize_global_variables"));
117
118   mc_comp_times = xbt_new0(s_mc_comparison_times_t, 1);
119
120   /* Initialize statistics */
121   mc_stats = xbt_new0(s_mc_stats_t, 1);
122   mc_stats->state_size = 1;
123
124   if ((_sg_mc_dot_output_file != nullptr) && (_sg_mc_dot_output_file[0] != '\0'))
125     MC_init_dot_output();
126
127   /* Init parmap */
128   //parmap = xbt_parmap_mc_new(xbt_os_get_numcores(), XBT_PARMAP_DEFAULT);
129
130   setup_ignore();
131
132   ptrace(PTRACE_SETOPTIONS, pid_, nullptr, PTRACE_O_TRACEEXIT);
133   ptrace(PTRACE_CONT, pid_, 0, 0);
134 }
135
136 void ModelChecker::setup_ignore()
137 {
138   /* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */
139   MC_ignore_local_variable("e", "*");
140   MC_ignore_local_variable("__ex_cleanup", "*");
141   MC_ignore_local_variable("__ex_mctx_en", "*");
142   MC_ignore_local_variable("__ex_mctx_me", "*");
143   MC_ignore_local_variable("__xbt_ex_ctx_ptr", "*");
144   MC_ignore_local_variable("_log_ev", "*");
145   MC_ignore_local_variable("_throw_ctx", "*");
146   MC_ignore_local_variable("ctx", "*");
147
148   MC_ignore_local_variable("self", "simcall_BODY_mc_snapshot");
149   MC_ignore_local_variable("next_cont"
150     "ext", "smx_ctx_sysv_suspend_serial");
151   MC_ignore_local_variable("i", "smx_ctx_sysv_suspend_serial");
152
153   /* Ignore local variable about time used for tracing */
154   MC_ignore_local_variable("start_time", "*");
155
156   /* Static variable used for tracing */
157   MCer_ignore_global_variable("counter");
158
159   /* SIMIX */
160   MCer_ignore_global_variable("smx_total_comms");
161 }
162
163 void ModelChecker::shutdown()
164 {
165   XBT_DEBUG("Shuting down model-checker");
166
167   simgrid::mc::Process* process = &this->process();
168   if (process->running()) {
169     XBT_DEBUG("Killing process");
170     kill(process->pid(), SIGTERM);
171     process->terminate();
172   }
173 }
174
175 void ModelChecker::resume(simgrid::mc::Process& process)
176 {
177   int res = process.send_message(MC_MESSAGE_CONTINUE);
178   if (res)
179     throw std::system_error(res, std::system_category());
180   process.cache_flags = (mc_process_cache_flags_t) 0;
181 }
182
183 static
184 void throw_socket_error(int fd)
185 {
186   int error = 0;
187   socklen_t errlen = sizeof(error);
188   if (getsockopt(fd, SOL_SOCKET, SO_ERROR, (void *)&error, &errlen) == -1)
189     error = errno;
190   throw std::system_error(error, std::system_category());
191 }
192
193 bool ModelChecker::handle_message(char* buffer, ssize_t size)
194 {
195   s_mc_message_t base_message;
196   if (size < (ssize_t) sizeof(base_message))
197     xbt_die("Broken message");
198   memcpy(&base_message, buffer, sizeof(base_message));
199
200   switch(base_message.type) {
201
202   case MC_MESSAGE_IGNORE_HEAP:
203     {
204       s_mc_ignore_heap_message_t message;
205       if (size != sizeof(message))
206         xbt_die("Broken messsage");
207       memcpy(&message, buffer, sizeof(message));
208       mc_heap_ignore_region_t region = xbt_new(s_mc_heap_ignore_region_t, 1);
209       *region = message.region;
210       MC_heap_region_ignore_insert(region);
211       break;
212     }
213
214   case MC_MESSAGE_UNIGNORE_HEAP:
215     {
216       s_mc_ignore_memory_message_t message;
217       if (size != sizeof(message))
218         xbt_die("Broken messsage");
219       memcpy(&message, buffer, sizeof(message));
220       MC_heap_region_ignore_remove(
221         (void *)(std::uintptr_t) message.addr, message.size);
222       break;
223     }
224
225   case MC_MESSAGE_IGNORE_MEMORY:
226     {
227       s_mc_ignore_memory_message_t message;
228       if (size != sizeof(message))
229         xbt_die("Broken messsage");
230       memcpy(&message, buffer, sizeof(message));
231       this->process().ignore_region(message.addr, message.size);
232       break;
233     }
234
235   case MC_MESSAGE_STACK_REGION:
236     {
237       s_mc_stack_region_message_t message;
238       if (size != sizeof(message))
239         xbt_die("Broken messsage");
240       memcpy(&message, buffer, sizeof(message));
241       stack_region_t stack_region = xbt_new(s_stack_region_t, 1);
242       *stack_region = message.stack_region;
243       MC_stack_area_add(stack_region);
244     }
245     break;
246
247   case MC_MESSAGE_REGISTER_SYMBOL:
248     {
249       s_mc_register_symbol_message_t message;
250       if (size != sizeof(message))
251         xbt_die("Broken message");
252       memcpy(&message, buffer, sizeof(message));
253       if (message.callback)
254         xbt_die("Support for client-side function proposition is not implemented.");
255       XBT_DEBUG("Received symbol: %s", message.name);
256
257       if (_mc_property_automaton == nullptr)
258         _mc_property_automaton = xbt_automaton_new();
259
260       simgrid::mc::Process* process = &this->process();
261       simgrid::mc::remote_ptr<int> address
262         = simgrid::mc::remote((int*) message.data);
263       simgrid::xbt::add_proposition(_mc_property_automaton,
264         message.name,
265         [process, address]() { return process->read(address); }
266         );
267
268       break;
269     }
270
271   case MC_MESSAGE_WAITING:
272     return false;
273
274   case MC_MESSAGE_ASSERTION_FAILED:
275     MC_report_assertion_error();
276     ::exit(SIMGRID_MC_EXIT_SAFETY);
277     break;
278
279   default:
280     xbt_die("Unexpected message from model-checked application");
281
282   }
283   return true;
284 }
285
286 bool ModelChecker::handle_events()
287 {
288   char buffer[MC_MESSAGE_LENGTH];
289   struct pollfd* socket_pollfd = &fds_[SOCKET_FD_INDEX];
290   struct pollfd* signalfd_pollfd = &fds_[SIGNAL_FD_INDEX];
291
292   while(poll(fds_, 2, -1) == -1) {
293     switch(errno) {
294     case EINTR:
295       continue;
296     default:
297       throw std::system_error(errno, std::system_category());
298     }
299   }
300
301   if (socket_pollfd->revents) {
302     if (socket_pollfd->revents & POLLIN) {
303       ssize_t size = MC_receive_message(socket_pollfd->fd, buffer, sizeof(buffer), MSG_DONTWAIT);
304       if (size == -1 && errno != EAGAIN)
305         throw std::system_error(errno, std::system_category());
306       return handle_message(buffer, size);
307     }
308     if (socket_pollfd->revents & POLLERR) {
309       throw_socket_error(socket_pollfd->fd);
310     }
311     if (socket_pollfd->revents & POLLHUP)
312       xbt_die("Socket hang up?");
313   }
314
315   if (signalfd_pollfd->revents) {
316     if (signalfd_pollfd->revents & POLLIN) {
317       this->handle_signals();
318       return true;
319     }
320     if (signalfd_pollfd->revents & POLLERR) {
321       throw_socket_error(signalfd_pollfd->fd);
322     }
323     if (signalfd_pollfd->revents & POLLHUP)
324       xbt_die("Signalfd hang up?");
325   }
326
327   return true;
328 }
329
330 void ModelChecker::loop()
331 {
332   while (this->process().running())
333     this->handle_events();
334 }
335
336 void ModelChecker::handle_signals()
337 {
338   struct signalfd_siginfo info;
339   struct pollfd* signalfd_pollfd = &fds_[SIGNAL_FD_INDEX];
340   while (1) {
341     ssize_t size = read(signalfd_pollfd->fd, &info, sizeof(info));
342     if (size == -1) {
343       if (errno == EINTR)
344         continue;
345       else
346         throw std::system_error(errno, std::system_category());
347     } else if (size != sizeof(info))
348         return throw std::runtime_error(
349           "Bad communication with model-checked application");
350     else
351       break;
352   }
353   this->on_signal(&info);
354 }
355
356 void ModelChecker::handle_waitpid()
357 {
358   XBT_DEBUG("Check for wait event");
359   int status;
360   pid_t pid;
361   while ((pid = waitpid(-1, &status, WNOHANG)) != 0) {
362     if (pid == -1) {
363       if (errno == ECHILD) {
364         // No more children:
365         if (this->process().running())
366           xbt_die("Inconsistent state");
367         else
368           break;
369       } else {
370         XBT_ERROR("Could not wait for pid");
371         throw std::system_error(errno, std::system_category());
372       }
373     }
374
375     if (pid == this->process().pid()) {
376
377       // From PTRACE_O_TRACEEXIT:
378       if (status>>8 == (SIGTRAP | (PTRACE_EVENT_EXIT<<8))) {
379         if (ptrace(PTRACE_GETEVENTMSG, pid_, 0, &status) == -1)
380           xbt_die("Could not get exit status");
381         if (WIFSIGNALED(status)) {
382           MC_report_crash(status);
383           ::exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
384         }
385       }
386
387       // We don't care about signals, just reinject them:
388       if (WIFSTOPPED(status)) {
389         XBT_DEBUG("Stopped with signal %i", (int) WSTOPSIG(status));
390         if (ptrace(PTRACE_CONT, pid_, 0, WSTOPSIG(status)) == -1)
391           xbt_die("Could not PTRACE_CONT");
392       }
393
394       else if (WIFEXITED(status) || WIFSIGNALED(status)) {
395         XBT_DEBUG("Child process is over");
396         this->process().terminate();
397       }
398     }
399   }
400 }
401
402 void ModelChecker::on_signal(const struct signalfd_siginfo* info)
403 {
404   switch(info->ssi_signo) {
405   case SIGCHLD:
406     this->handle_waitpid();
407     break;
408   default:
409     break;
410   }
411 }
412
413 void ModelChecker::wait_client(simgrid::mc::Process& process)
414 {
415   this->resume(process);
416   while (this->process().running()) {
417     if (!this->handle_events())
418       return;
419   }
420 }
421
422 void ModelChecker::simcall_handle(simgrid::mc::Process& process, unsigned long pid, int value)
423 {
424   s_mc_simcall_handle_message m;
425   memset(&m, 0, sizeof(m));
426   m.type  = MC_MESSAGE_SIMCALL_HANDLE;
427   m.pid   = pid;
428   m.value = value;
429   process.send_message(m);
430   process.cache_flags = (mc_process_cache_flags_t) 0;
431   while (process.running()) {
432     if (!this->handle_events())
433       return;
434   }
435 }
436
437 }
438 }