Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
[mc] Simplification, remove profiling code
[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   /* Initialize statistics */
119   mc_stats = xbt_new0(s_mc_stats_t, 1);
120   mc_stats->state_size = 1;
121
122   if ((_sg_mc_dot_output_file != nullptr) && (_sg_mc_dot_output_file[0] != '\0'))
123     MC_init_dot_output();
124
125   /* Init parmap */
126   //parmap = xbt_parmap_mc_new(xbt_os_get_numcores(), XBT_PARMAP_DEFAULT);
127
128   setup_ignore();
129
130   ptrace(PTRACE_SETOPTIONS, pid_, nullptr, PTRACE_O_TRACEEXIT);
131   ptrace(PTRACE_CONT, pid_, 0, 0);
132 }
133
134 void ModelChecker::setup_ignore()
135 {
136   /* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */
137   MC_ignore_local_variable("e", "*");
138   MC_ignore_local_variable("__ex_cleanup", "*");
139   MC_ignore_local_variable("__ex_mctx_en", "*");
140   MC_ignore_local_variable("__ex_mctx_me", "*");
141   MC_ignore_local_variable("__xbt_ex_ctx_ptr", "*");
142   MC_ignore_local_variable("_log_ev", "*");
143   MC_ignore_local_variable("_throw_ctx", "*");
144   MC_ignore_local_variable("ctx", "*");
145
146   MC_ignore_local_variable("self", "simcall_BODY_mc_snapshot");
147   MC_ignore_local_variable("next_cont"
148     "ext", "smx_ctx_sysv_suspend_serial");
149   MC_ignore_local_variable("i", "smx_ctx_sysv_suspend_serial");
150
151   /* Ignore local variable about time used for tracing */
152   MC_ignore_local_variable("start_time", "*");
153
154   /* Static variable used for tracing */
155   MCer_ignore_global_variable("counter");
156
157   /* SIMIX */
158   MCer_ignore_global_variable("smx_total_comms");
159 }
160
161 void ModelChecker::shutdown()
162 {
163   XBT_DEBUG("Shuting down model-checker");
164
165   simgrid::mc::Process* process = &this->process();
166   if (process->running()) {
167     XBT_DEBUG("Killing process");
168     kill(process->pid(), SIGTERM);
169     process->terminate();
170   }
171 }
172
173 void ModelChecker::resume(simgrid::mc::Process& process)
174 {
175   int res = process.send_message(MC_MESSAGE_CONTINUE);
176   if (res)
177     throw std::system_error(res, std::system_category());
178   process.cache_flags = (mc_process_cache_flags_t) 0;
179 }
180
181 static
182 void throw_socket_error(int fd)
183 {
184   int error = 0;
185   socklen_t errlen = sizeof(error);
186   if (getsockopt(fd, SOL_SOCKET, SO_ERROR, (void *)&error, &errlen) == -1)
187     error = errno;
188   throw std::system_error(error, std::system_category());
189 }
190
191 bool ModelChecker::handle_message(char* buffer, ssize_t size)
192 {
193   s_mc_message_t base_message;
194   if (size < (ssize_t) sizeof(base_message))
195     xbt_die("Broken message");
196   memcpy(&base_message, buffer, sizeof(base_message));
197
198   switch(base_message.type) {
199
200   case MC_MESSAGE_IGNORE_HEAP:
201     {
202       s_mc_ignore_heap_message_t message;
203       if (size != sizeof(message))
204         xbt_die("Broken messsage");
205       memcpy(&message, buffer, sizeof(message));
206       mc_heap_ignore_region_t region = xbt_new(s_mc_heap_ignore_region_t, 1);
207       *region = message.region;
208       MC_heap_region_ignore_insert(region);
209       break;
210     }
211
212   case MC_MESSAGE_UNIGNORE_HEAP:
213     {
214       s_mc_ignore_memory_message_t message;
215       if (size != sizeof(message))
216         xbt_die("Broken messsage");
217       memcpy(&message, buffer, sizeof(message));
218       MC_heap_region_ignore_remove(
219         (void *)(std::uintptr_t) message.addr, message.size);
220       break;
221     }
222
223   case MC_MESSAGE_IGNORE_MEMORY:
224     {
225       s_mc_ignore_memory_message_t message;
226       if (size != sizeof(message))
227         xbt_die("Broken messsage");
228       memcpy(&message, buffer, sizeof(message));
229       this->process().ignore_region(message.addr, message.size);
230       break;
231     }
232
233   case MC_MESSAGE_STACK_REGION:
234     {
235       s_mc_stack_region_message_t message;
236       if (size != sizeof(message))
237         xbt_die("Broken messsage");
238       memcpy(&message, buffer, sizeof(message));
239       stack_region_t stack_region = xbt_new(s_stack_region_t, 1);
240       *stack_region = message.stack_region;
241       MC_stack_area_add(stack_region);
242     }
243     break;
244
245   case MC_MESSAGE_REGISTER_SYMBOL:
246     {
247       s_mc_register_symbol_message_t message;
248       if (size != sizeof(message))
249         xbt_die("Broken message");
250       memcpy(&message, buffer, sizeof(message));
251       if (message.callback)
252         xbt_die("Support for client-side function proposition is not implemented.");
253       XBT_DEBUG("Received symbol: %s", message.name);
254
255       if (_mc_property_automaton == nullptr)
256         _mc_property_automaton = xbt_automaton_new();
257
258       simgrid::mc::Process* process = &this->process();
259       simgrid::mc::remote_ptr<int> address
260         = simgrid::mc::remote((int*) message.data);
261       simgrid::xbt::add_proposition(_mc_property_automaton,
262         message.name,
263         [process, address]() { return process->read(address); }
264         );
265
266       break;
267     }
268
269   case MC_MESSAGE_WAITING:
270     return false;
271
272   case MC_MESSAGE_ASSERTION_FAILED:
273     MC_report_assertion_error();
274     ::exit(SIMGRID_MC_EXIT_SAFETY);
275     break;
276
277   default:
278     xbt_die("Unexpected message from model-checked application");
279
280   }
281   return true;
282 }
283
284 bool ModelChecker::handle_events()
285 {
286   char buffer[MC_MESSAGE_LENGTH];
287   struct pollfd* socket_pollfd = &fds_[SOCKET_FD_INDEX];
288   struct pollfd* signalfd_pollfd = &fds_[SIGNAL_FD_INDEX];
289
290   while(poll(fds_, 2, -1) == -1) {
291     switch(errno) {
292     case EINTR:
293       continue;
294     default:
295       throw std::system_error(errno, std::system_category());
296     }
297   }
298
299   if (socket_pollfd->revents) {
300     if (socket_pollfd->revents & POLLIN) {
301       ssize_t size = MC_receive_message(socket_pollfd->fd, buffer, sizeof(buffer), MSG_DONTWAIT);
302       if (size == -1 && errno != EAGAIN)
303         throw std::system_error(errno, std::system_category());
304       return handle_message(buffer, size);
305     }
306     if (socket_pollfd->revents & POLLERR) {
307       throw_socket_error(socket_pollfd->fd);
308     }
309     if (socket_pollfd->revents & POLLHUP)
310       xbt_die("Socket hang up?");
311   }
312
313   if (signalfd_pollfd->revents) {
314     if (signalfd_pollfd->revents & POLLIN) {
315       this->handle_signals();
316       return true;
317     }
318     if (signalfd_pollfd->revents & POLLERR) {
319       throw_socket_error(signalfd_pollfd->fd);
320     }
321     if (signalfd_pollfd->revents & POLLHUP)
322       xbt_die("Signalfd hang up?");
323   }
324
325   return true;
326 }
327
328 void ModelChecker::loop()
329 {
330   while (this->process().running())
331     this->handle_events();
332 }
333
334 void ModelChecker::handle_signals()
335 {
336   struct signalfd_siginfo info;
337   struct pollfd* signalfd_pollfd = &fds_[SIGNAL_FD_INDEX];
338   while (1) {
339     ssize_t size = read(signalfd_pollfd->fd, &info, sizeof(info));
340     if (size == -1) {
341       if (errno == EINTR)
342         continue;
343       else
344         throw std::system_error(errno, std::system_category());
345     } else if (size != sizeof(info))
346         return throw std::runtime_error(
347           "Bad communication with model-checked application");
348     else
349       break;
350   }
351   this->on_signal(&info);
352 }
353
354 void ModelChecker::handle_waitpid()
355 {
356   XBT_DEBUG("Check for wait event");
357   int status;
358   pid_t pid;
359   while ((pid = waitpid(-1, &status, WNOHANG)) != 0) {
360     if (pid == -1) {
361       if (errno == ECHILD) {
362         // No more children:
363         if (this->process().running())
364           xbt_die("Inconsistent state");
365         else
366           break;
367       } else {
368         XBT_ERROR("Could not wait for pid");
369         throw std::system_error(errno, std::system_category());
370       }
371     }
372
373     if (pid == this->process().pid()) {
374
375       // From PTRACE_O_TRACEEXIT:
376       if (status>>8 == (SIGTRAP | (PTRACE_EVENT_EXIT<<8))) {
377         if (ptrace(PTRACE_GETEVENTMSG, pid_, 0, &status) == -1)
378           xbt_die("Could not get exit status");
379         if (WIFSIGNALED(status)) {
380           MC_report_crash(status);
381           ::exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
382         }
383       }
384
385       // We don't care about signals, just reinject them:
386       if (WIFSTOPPED(status)) {
387         XBT_DEBUG("Stopped with signal %i", (int) WSTOPSIG(status));
388         if (ptrace(PTRACE_CONT, pid_, 0, WSTOPSIG(status)) == -1)
389           xbt_die("Could not PTRACE_CONT");
390       }
391
392       else if (WIFEXITED(status) || WIFSIGNALED(status)) {
393         XBT_DEBUG("Child process is over");
394         this->process().terminate();
395       }
396     }
397   }
398 }
399
400 void ModelChecker::on_signal(const struct signalfd_siginfo* info)
401 {
402   switch(info->ssi_signo) {
403   case SIGCHLD:
404     this->handle_waitpid();
405     break;
406   default:
407     break;
408   }
409 }
410
411 void ModelChecker::wait_client(simgrid::mc::Process& process)
412 {
413   this->resume(process);
414   while (this->process().running()) {
415     if (!this->handle_events())
416       return;
417   }
418 }
419
420 void ModelChecker::simcall_handle(simgrid::mc::Process& process, unsigned long pid, int value)
421 {
422   s_mc_simcall_handle_message m;
423   memset(&m, 0, sizeof(m));
424   m.type  = MC_MESSAGE_SIMCALL_HANDLE;
425   m.pid   = pid;
426   m.value = value;
427   process.send_message(m);
428   process.cache_flags = (mc_process_cache_flags_t) 0;
429   while (process.running()) {
430     if (!this->handle_events())
431       return;
432   }
433 }
434
435 }
436 }