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 }