Logo AND Algorithmique Numérique Distribuée

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