Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
f0f149f61347caacd00f1c85fc473bb68bfaf54f
[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 #include <xbt/system_error.hpp>
23
24 #include "simgrid/sg_config.h"
25
26 #include "src/mc/ModelChecker.hpp"
27 #include "src/mc/PageStore.hpp"
28 #include "src/mc/ModelChecker.hpp"
29 #include "src/mc/mc_protocol.h"
30 #include "src/mc/mc_private.h"
31 #include "src/mc/mc_ignore.h"
32 #include "src/mc/mc_exit.h"
33 #include "src/mc/mc_record.h"
34 #include "src/mc/Transition.hpp"
35 #include "src/mc/Checker.hpp"
36
37 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_ModelChecker, mc, "ModelChecker");
38
39 ::simgrid::mc::ModelChecker* mc_model_checker = nullptr;
40
41 using simgrid::mc::remote;
42
43 #ifdef __linux__
44 # define WAITPID_CHECKED_FLAGS __WALL
45 #else
46 # define WAITPID_CHECKED_FLAGS 0
47 #endif
48
49 // Hardcoded index for now:
50 #define SOCKET_FD_INDEX 0
51 #define SIGNAL_FD_INDEX 1
52
53 namespace simgrid {
54 namespace mc {
55
56 ModelChecker::ModelChecker(std::unique_ptr<Process> process) :
57   page_store_(500),
58   process_(std::move(process)),
59   parent_snapshot_(nullptr)
60 {
61
62 }
63
64 ModelChecker::~ModelChecker() {}
65
66 void ModelChecker::start()
67 {
68   const pid_t pid = process_->pid();
69
70   // Block SIGCHLD (this will be handled with accept/signalfd):
71   sigset_t set;
72   sigemptyset(&set);
73   sigaddset(&set, SIGCHLD);
74   if (sigprocmask(SIG_BLOCK, &set, nullptr) == -1)
75     throw simgrid::xbt::errno_error();
76
77   sigset_t full_set;
78   sigfillset(&full_set);
79
80   // Prepare data for poll:
81
82   struct pollfd* socket_pollfd = &fds_[SOCKET_FD_INDEX];
83   socket_pollfd->fd = process_->getChannel().getSocket();
84   socket_pollfd->events = POLLIN;
85   socket_pollfd->revents = 0;
86
87   int signal_fd = signalfd(-1, &set, 0);
88   if (signal_fd == -1)
89     throw simgrid::xbt::errno_error();
90
91   struct pollfd* signalfd_pollfd = &fds_[SIGNAL_FD_INDEX];
92   signalfd_pollfd->fd = signal_fd;
93   signalfd_pollfd->events = POLLIN;
94   signalfd_pollfd->revents = 0;
95
96   XBT_DEBUG("Waiting for the model-checked process");
97   int status;
98
99   // The model-checked process SIGSTOP itself to signal it's ready:
100   pid_t res = waitpid(pid, &status, WAITPID_CHECKED_FLAGS);
101   if (res < 0 || !WIFSTOPPED(status) || WSTOPSIG(status) != SIGSTOP)
102     xbt_die("Could not wait model-checked process");
103
104   process_->init();
105
106   if ((_sg_mc_dot_output_file != nullptr) && (_sg_mc_dot_output_file[0] != '\0'))
107     MC_init_dot_output();
108
109   setup_ignore();
110
111 #ifdef __linux__
112   ptrace(PTRACE_SETOPTIONS, pid, nullptr, PTRACE_O_TRACEEXIT);
113   ptrace(PTRACE_CONT, pid, 0, 0);
114 #elif defined BSD
115   ptrace(PT_CONTINUE, pid, (caddr_t)1, 0);
116 #else
117 # error "no ptrace equivalent coded for this platform"
118 #endif
119 }
120
121 static const std::pair<const char*, const char*> ignored_local_variables[] = {
122   std::pair<const char*, const char*>{  "e", "*" },
123   std::pair<const char*, const char*>{ "__ex_cleanup", "*" },
124   std::pair<const char*, const char*>{ "__ex_mctx_en", "*" },
125   std::pair<const char*, const char*>{ "__ex_mctx_me", "*" },
126   std::pair<const char*, const char*>{ "__xbt_ex_ctx_ptr", "*" },
127   std::pair<const char*, const char*>{ "_log_ev", "*" },
128   std::pair<const char*, const char*>{ "_throw_ctx", "*" },
129   std::pair<const char*, const char*>{ "ctx", "*" },
130
131   std::pair<const char*, const char*>{ "self", "simcall_BODY_mc_snapshot" },
132   std::pair<const char*, const char*>{ "next_context", "smx_ctx_sysv_suspend_serial" },
133   std::pair<const char*, const char*>{ "i", "smx_ctx_sysv_suspend_serial" },
134
135   /* Ignore local variable about time used for tracing */
136   std::pair<const char*, const char*>{ "start_time", "*" },
137 };
138
139 void ModelChecker::setup_ignore()
140 {
141   Process& process = this->process();
142   for (std::pair<const char*, const char*> const& var :
143       ignored_local_variables)
144     process.ignore_local_variable(var.first, var.second);
145
146   /* Static variable used for tracing */
147   process.ignore_global_variable("counter");
148 }
149
150 void ModelChecker::shutdown()
151 {
152   XBT_DEBUG("Shuting down model-checker");
153
154   simgrid::mc::Process* process = &this->process();
155   if (process->running()) {
156     XBT_DEBUG("Killing process");
157     kill(process->pid(), SIGTERM);
158     process->terminate();
159   }
160 }
161
162 void ModelChecker::resume(simgrid::mc::Process& process)
163 {
164   int res = process.getChannel().send(MC_MESSAGE_CONTINUE);
165   if (res)
166     throw simgrid::xbt::errno_error();
167   process.clear_cache();
168 }
169
170 static
171 void throw_socket_error(int fd)
172 {
173   int error = 0;
174   socklen_t errlen = sizeof(error);
175   if (getsockopt(fd, SOL_SOCKET, SO_ERROR, (void *)&error, &errlen) == -1)
176     error = errno;
177   throw simgrid::xbt::errno_error();
178 }
179
180 static void MC_report_crash(int status)
181 {
182   XBT_INFO("**************************");
183   XBT_INFO("** CRASH IN THE PROGRAM **");
184   XBT_INFO("**************************");
185   if (WIFSIGNALED(status))
186     XBT_INFO("From signal: %s", strsignal(WTERMSIG(status)));
187   else if (WIFEXITED(status))
188     XBT_INFO("From exit: %i", WEXITSTATUS(status));
189   if (WCOREDUMP(status))
190     XBT_INFO("A core dump was generated by the system.");
191   else
192     XBT_INFO("No core dump was generated by the system.");
193   XBT_INFO("Counter-example execution trace:");
194   simgrid::mc::dumpRecordPath();
195   for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
196     XBT_INFO("%s", s.c_str());
197   simgrid::mc::session->logState();
198   XBT_INFO("Stack trace:");
199   mc_model_checker->process().dumpStack();
200 }
201
202 static void MC_report_assertion_error(void)
203 {
204   XBT_INFO("**************************");
205   XBT_INFO("*** PROPERTY NOT VALID ***");
206   XBT_INFO("**************************");
207   XBT_INFO("Counter-example execution trace:");
208   simgrid::mc::dumpRecordPath();
209   for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
210     XBT_INFO("%s", s.c_str());
211   simgrid::mc::session->logState();
212 }
213
214 bool ModelChecker::handle_message(char* buffer, ssize_t size)
215 {
216   s_mc_message_t base_message;
217   if (size < (ssize_t) sizeof(base_message))
218     xbt_die("Broken message");
219   memcpy(&base_message, buffer, sizeof(base_message));
220
221   switch(base_message.type) {
222
223   case MC_MESSAGE_IGNORE_HEAP:
224     {
225       s_mc_ignore_heap_message_t message;
226       if (size != sizeof(message))
227         xbt_die("Broken messsage");
228       memcpy(&message, buffer, sizeof(message));
229
230       IgnoredHeapRegion region;
231       region.block = message.block;
232       region.fragment = message.fragment;
233       region.address = message.address;
234       region.size = message.size;
235       process().ignore_heap(region);
236       break;
237     }
238
239   case MC_MESSAGE_UNIGNORE_HEAP:
240     {
241       s_mc_ignore_memory_message_t message;
242       if (size != sizeof(message))
243         xbt_die("Broken messsage");
244       memcpy(&message, buffer, sizeof(message));
245       process().unignore_heap(
246         (void *)(std::uintptr_t) message.addr, message.size);
247       break;
248     }
249
250   case MC_MESSAGE_IGNORE_MEMORY:
251     {
252       s_mc_ignore_memory_message_t message;
253       if (size != sizeof(message))
254         xbt_die("Broken messsage");
255       memcpy(&message, buffer, sizeof(message));
256       this->process().ignore_region(message.addr, message.size);
257       break;
258     }
259
260   case MC_MESSAGE_STACK_REGION:
261     {
262       s_mc_stack_region_message_t message;
263       if (size != sizeof(message))
264         xbt_die("Broken messsage");
265       memcpy(&message, buffer, sizeof(message));
266       this->process().stack_areas().push_back(message.stack_region);
267     }
268     break;
269
270   case MC_MESSAGE_REGISTER_SYMBOL:
271     {
272       s_mc_register_symbol_message_t message;
273       if (size != sizeof(message))
274         xbt_die("Broken message");
275       memcpy(&message, buffer, sizeof(message));
276       if (message.callback)
277         xbt_die("Support for client-side function proposition is not implemented.");
278       XBT_DEBUG("Received symbol: %s", message.name);
279
280       if (simgrid::mc::property_automaton == nullptr)
281         simgrid::mc::property_automaton = xbt_automaton_new();
282
283       simgrid::mc::Process* process = &this->process();
284       simgrid::mc::RemotePtr<int> address
285         = simgrid::mc::remote((int*) message.data);
286       simgrid::xbt::add_proposition(simgrid::mc::property_automaton,
287         message.name,
288         [process, address]() { return process->read(address); }
289         );
290
291       break;
292     }
293
294   case MC_MESSAGE_WAITING:
295     return false;
296
297   case MC_MESSAGE_ASSERTION_FAILED:
298     MC_report_assertion_error();
299     this->exit(SIMGRID_MC_EXIT_SAFETY);
300     break;
301
302   default:
303     xbt_die("Unexpected message from model-checked application");
304
305   }
306   return true;
307 }
308
309 /** Terminate the model-checker application */
310 void ModelChecker::exit(int status)
311 {
312   // TODO, terminate the model checker politely instead of exiting rudely
313   if (process().running())
314     kill(process().pid(), SIGKILL);
315   ::exit(status);
316 }
317
318 bool ModelChecker::handle_events()
319 {
320   char buffer[MC_MESSAGE_LENGTH];
321   struct pollfd* socket_pollfd = &fds_[SOCKET_FD_INDEX];
322   struct pollfd* signalfd_pollfd = &fds_[SIGNAL_FD_INDEX];
323
324   while(poll(fds_, 2, -1) == -1) {
325     switch(errno) {
326     case EINTR:
327       continue;
328     default:
329       throw simgrid::xbt::errno_error();
330     }
331   }
332
333   if (socket_pollfd->revents) {
334     if (socket_pollfd->revents & POLLIN) {
335       ssize_t size = process_->getChannel().receive(buffer, sizeof(buffer), false);
336       if (size == -1 && errno != EAGAIN)
337         throw simgrid::xbt::errno_error();
338       return handle_message(buffer, size);
339     }
340     if (socket_pollfd->revents & POLLERR)
341       throw_socket_error(socket_pollfd->fd);
342     if (socket_pollfd->revents & POLLHUP)
343       xbt_die("Socket hang up?");
344   }
345
346   if (signalfd_pollfd->revents) {
347     if (signalfd_pollfd->revents & POLLIN) {
348       this->handle_signals();
349       return true;
350     }
351     if (signalfd_pollfd->revents & POLLERR)
352       throw_socket_error(signalfd_pollfd->fd);
353     if (signalfd_pollfd->revents & POLLHUP)
354       xbt_die("Signalfd hang up?");
355   }
356
357   return true;
358 }
359
360 void ModelChecker::loop()
361 {
362   while (this->process().running())
363     this->handle_events();
364 }
365
366 void ModelChecker::handle_signals()
367 {
368   struct signalfd_siginfo info;
369   struct pollfd* signalfd_pollfd = &fds_[SIGNAL_FD_INDEX];
370   while (1) {
371     ssize_t size = read(signalfd_pollfd->fd, &info, sizeof(info));
372     if (size == -1) {
373       if (errno == EINTR)
374         continue;
375       else
376         throw simgrid::xbt::errno_error();
377     } else if (size != sizeof(info))
378         return throw std::runtime_error(
379           "Bad communication with model-checked application");
380     else
381       break;
382   }
383   this->on_signal(&info);
384 }
385
386 void ModelChecker::handle_waitpid()
387 {
388   XBT_DEBUG("Check for wait event");
389   int status;
390   pid_t pid;
391   while ((pid = waitpid(-1, &status, WNOHANG)) != 0) {
392     if (pid == -1) {
393       if (errno == ECHILD) {
394         // No more children:
395         if (this->process().running())
396           xbt_die("Inconsistent state");
397         else
398           break;
399       } else {
400         XBT_ERROR("Could not wait for pid");
401         throw simgrid::xbt::errno_error();
402       }
403     }
404
405     if (pid == this->process().pid()) {
406
407       // From PTRACE_O_TRACEEXIT:
408 #ifdef __linux__
409       if (status>>8 == (SIGTRAP | (PTRACE_EVENT_EXIT<<8))) {
410         if (ptrace(PTRACE_GETEVENTMSG, this->process().pid(), 0, &status) == -1)
411           xbt_die("Could not get exit status");
412         if (WIFSIGNALED(status)) {
413           MC_report_crash(status);
414           mc_model_checker->exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
415         }
416       }
417 #endif
418
419       // We don't care about signals, just reinject them:
420       if (WIFSTOPPED(status)) {
421         XBT_DEBUG("Stopped with signal %i", (int) WSTOPSIG(status));
422         errno = 0;
423 #ifdef __linux__
424         ptrace(PTRACE_CONT, this->process().pid(), 0, WSTOPSIG(status));
425 #elif defined BSD
426         ptrace(PT_CONTINUE, this->process().pid(), (caddr_t)1, WSTOPSIG(status));
427 #endif
428         if (errno != 0)
429           xbt_die("Could not PTRACE_CONT");
430       }
431
432       else if (WIFEXITED(status) || WIFSIGNALED(status)) {
433         XBT_DEBUG("Child process is over");
434         this->process().terminate();
435       }
436     }
437   }
438 }
439
440 void ModelChecker::on_signal(const struct signalfd_siginfo* info)
441 {
442   switch(info->ssi_signo) {
443   case SIGCHLD:
444     this->handle_waitpid();
445     break;
446   default:
447     break;
448   }
449 }
450
451 void ModelChecker::wait_client(simgrid::mc::Process& process)
452 {
453   this->resume(process);
454   while (this->process().running())
455     if (!this->handle_events())
456       return;
457 }
458
459 void ModelChecker::handle_simcall(Transition const& transition)
460 {
461   s_mc_simcall_handle_message m;
462   memset(&m, 0, sizeof(m));
463   m.type  = MC_MESSAGE_SIMCALL_HANDLE;
464   m.pid   = transition.pid;
465   m.value = transition.argument;
466   this->process_->getChannel().send(m);
467   this->process_->clear_cache();
468   while (this->process_->running())
469     if (!this->handle_events())
470       return;
471 }
472
473 bool ModelChecker::checkDeadlock()
474 {
475   int res;
476   if ((res = this->process().getChannel().send(MC_MESSAGE_DEADLOCK_CHECK)))
477     xbt_die("Could not check deadlock state");
478   s_mc_int_message_t message;
479   ssize_t s = mc_model_checker->process().getChannel().receive(message);
480   if (s == -1)
481     xbt_die("Could not receive message");
482   if (s != sizeof(message) || message.type != MC_MESSAGE_DEADLOCK_CHECK_REPLY)
483     xbt_die("Received unexpected message %s (%i, size=%i) "
484       "expected MC_MESSAGE_DEADLOCK_CHECK_REPLY (%i, size=%i)",
485       MC_message_type_name(message.type), (int) message.type, (int) s,
486       (int) MC_MESSAGE_DEADLOCK_CHECK_REPLY, (int) sizeof(message)
487       );
488   return message.value != 0;
489 }
490
491 }
492 }