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 }