src/mc/ModelChecker.hpp

   1 /* Copyright (c) 2007-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 #ifndef SIMGRID_MC_MODEL_CHECKER_HPP
   8 #define SIMGRID_MC_MODEL_CHECKER_HPP
   9
  10 #include <sys/types.h>
  11
  12 #include <poll.h>
  13
  14 #include <memory>
  15 #include <set>
  16 #include <string>
  17
  18 #include <simgrid_config.h>
  19 #include <xbt/base.h>
  20 #include <sys/types.h>
  21
  22 #include "src/mc/mc_forward.hpp"
  23 #include "src/mc/Process.hpp"
  24 #include "src/mc/PageStore.hpp"
  25 #include "src/mc/mc_protocol.h"
  26 #include "src/mc/Transition.hpp"
  27
  28 namespace simgrid {
  29 namespace mc {
  30
  31 /** State of the model-checker (global variables for the model checker)
  32  */
  33 class ModelChecker {
  34   struct pollfd fds_[2];
  35   /** String pool for host names */
  36   // TODO, use std::set with heterogeneous comparison lookup (C++14)?
  37   std::set<std::string> hostnames_;
  38   // This is the parent snapshot of the current state:
  39   PageStore page_store_;
  40   std::unique_ptr<Process> process_;
  41   Checker* checker_ = nullptr;
  42 public:
  43   std::shared_ptr<simgrid::mc::Snapshot> parent_snapshot_;
  44
  45 public:
  46   ModelChecker(ModelChecker const&) = delete;
  47   ModelChecker& operator=(ModelChecker const&) = delete;
  48   ModelChecker(std::unique_ptr<Process> process);
  49   ~ModelChecker();
  50
  51   Process& process()
  52   {
  53     return *process_;
  54   }
  55   PageStore& page_store()
  56   {
  57     return page_store_;
  58   }
  59
  60   std::string const& get_host_name(const char* hostname)
  61   {
  62     return *this->hostnames_.insert(hostname).first;
  63   }
  64   std::string const& get_host_name(std::string const& hostname)
  65   {
  66     return *this->hostnames_.insert(hostname).first;
  67   }
  68
  69   void start();
  70   void shutdown();
  71   void resume(simgrid::mc::Process& process);
  72   void loop();
  73   bool handle_events();
  74   void wait_client(simgrid::mc::Process& process);
  75   void handle_simcall(Transition const& transition);
  76   void wait_for_requests()
  77   {
  78     mc_model_checker->wait_client(mc_model_checker->process());
  79   }
  80   void exit(int status);
  81
  82   bool checkDeadlock();
  83
  84   Checker* getChecker() const { return checker_; }
  85   void setChecker(Checker* checker) { checker_ = checker; }
  86
  87 private:
  88   void setup_ignore();
  89   bool handle_message(char* buffer, ssize_t size);
  90   void handle_signals();
  91   void handle_waitpid();
  92   void on_signal(const struct signalfd_siginfo* info);
  93
  94 public:
  95   unsigned long visited_states = 0;
  96   unsigned long executed_transitions = 0;
  97 };
  98
  99 }
 100 }
 101
 102 #endif