Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
mc: move some files related to ELF, DWARF or unwind reading into their own directory
[simgrid.git] / src / mc / ModelChecker.hpp
1 /* Copyright (c) 2007-2019. The SimGrid Team. All rights reserved.          */
2
3 /* This program is free software; you can redistribute it and/or modify it
4  * under the terms of the license (GNU LGPL) which comes with this package. */
5
6 #ifndef SIMGRID_MC_MODEL_CHECKER_HPP
7 #define SIMGRID_MC_MODEL_CHECKER_HPP
8
9 #include <sys/types.h>
10
11 #include <memory>
12 #include <set>
13 #include <string>
14
15 #include <event2/event.h>
16
17 #include <sys/types.h>
18
19 #include "src/mc/mc_forward.hpp"
20 #include "src/mc/remote/mc_protocol.h"
21 #include "src/mc/sosp/PageStore.hpp"
22
23 namespace simgrid {
24 namespace mc {
25
26 /** State of the model-checker (global variables for the model checker)
27  */
28 class ModelChecker {
29   struct event_base *base_;
30   struct event* socket_event_;
31   struct event* signal_event_;
32   /** String pool for host names */
33   // TODO, use std::set with heterogeneous comparison lookup (C++14)?
34   std::set<std::string> hostnames_;
35   // This is the parent snapshot of the current state:
36   PageStore page_store_;
37   std::unique_ptr<RemoteClient> process_;
38   Checker* checker_ = nullptr;
39 public:
40   std::shared_ptr<simgrid::mc::Snapshot> parent_snapshot_;
41
42   ModelChecker(ModelChecker const&) = delete;
43   ModelChecker& operator=(ModelChecker const&) = delete;
44   explicit ModelChecker(std::unique_ptr<RemoteClient> process);
45   ~ModelChecker();
46
47   RemoteClient& process() { return *process_; }
48   PageStore& page_store()
49   {
50     return page_store_;
51   }
52
53   std::string const& get_host_name(const char* hostname)
54   {
55     return *this->hostnames_.insert(hostname).first;
56   }
57   std::string const& get_host_name(std::string const& hostname)
58   {
59     return *this->hostnames_.insert(hostname).first;
60   }
61
62   void start();
63   void shutdown();
64   void resume(simgrid::mc::RemoteClient& process);
65   void loop();
66   void handle_events(int fd, short events);
67   void wait_for_requests();
68   void handle_simcall(Transition const& transition);
69   XBT_ATTRIB_NORETURN void exit(int status);
70
71   bool checkDeadlock();
72
73   Checker* getChecker() const { return checker_; }
74   void setChecker(Checker* checker) { checker_ = checker; }
75
76 private:
77   void setup_ignore();
78   bool handle_message(char* buffer, ssize_t size);
79   void handle_waitpid();
80   void on_signal(int signo);
81
82 public:
83   unsigned long visited_states = 0;
84   unsigned long executed_transitions = 0;
85 };
86
87 }
88 }
89
90 #endif