src/mc/explo/DFSExplorer.hpp

   1 /* Copyright (c) 2008-2023. 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_SAFETY_CHECKER_HPP
   7 #define SIMGRID_MC_SAFETY_CHECKER_HPP
   8
   9 #include "src/mc/api/ClockVector.hpp"
  10 #include "src/mc/api/State.hpp"
  11 #include "src/mc/explo/Exploration.hpp"
  12 #include "src/mc/explo/odpor/Execution.hpp"
  13 #include "src/mc/mc_config.hpp"
  14
  15 #if SIMGRID_HAVE_STATEFUL_MC
  16 #include "src/mc/VisitedState.hpp"
  17 #endif
  18
  19 #include <deque>
  20 #include <list>
  21 #include <memory>
  22 #include <set>
  23 #include <string>
  24 #include <unordered_map>
  25 #include <vector>
  26
  27 namespace simgrid::mc {
  28
  29 using stack_t = std::deque<std::shared_ptr<State>>;
  30
  31 class XBT_PRIVATE DFSExplorer : public Exploration {
  32 private:
  33   ReductionMode reduction_mode_;
  34   unsigned long backtrack_count_      = 0; // for statistics
  35   unsigned long visited_states_count_ = 0; // for statistics
  36
  37   static xbt::signal<void(RemoteApp&)> on_exploration_start_signal;
  38   static xbt::signal<void(RemoteApp&)> on_backtracking_signal;
  39
  40   static xbt::signal<void(State*, RemoteApp&)> on_state_creation_signal;
  41
  42   static xbt::signal<void(State*, RemoteApp&)> on_restore_system_state_signal;
  43   static xbt::signal<void(RemoteApp&)> on_restore_initial_state_signal;
  44   static xbt::signal<void(Transition*, RemoteApp&)> on_transition_replay_signal;
  45   static xbt::signal<void(Transition*, RemoteApp&)> on_transition_execute_signal;
  46
  47   static xbt::signal<void(RemoteApp&)> on_log_state_signal;
  48
  49 public:
  50   explicit DFSExplorer(const std::vector<char*>& args, ReductionMode mode, bool need_memory_info = false);
  51   void run() override;
  52   RecordTrace get_record_trace() override;
  53   void log_state() override;
  54
  55   /** Called once when the exploration starts */
  56   static void on_exploration_start(std::function<void(RemoteApp& remote_app)> const& f)
  57   {
  58     on_exploration_start_signal.connect(f);
  59   }
  60   /** Called each time that the exploration backtracks from a exploration end */
  61   static void on_backtracking(std::function<void(RemoteApp& remote_app)> const& f)
  62   {
  63     on_backtracking_signal.connect(f);
  64   }
  65   /** Called each time that a new state is create */
  66   static void on_state_creation(std::function<void(State*, RemoteApp& remote_app)> const& f)
  67   {
  68     on_state_creation_signal.connect(f);
  69   }
  70   /** Called when rollbacking directly onto a previously checkpointed state */
  71   static void on_restore_system_state(std::function<void(State*, RemoteApp& remote_app)> const& f)
  72   {
  73     on_restore_system_state_signal.connect(f);
  74   }
  75   /** Called when the state to which we backtrack was not checkpointed state, forcing us to restore the initial state
  76    * before replaying some transitions */
  77   static void on_restore_initial_state(std::function<void(RemoteApp& remote_app)> const& f)
  78   {
  79     on_restore_initial_state_signal.connect(f);
  80   }
  81   /** Called when replaying a transition that was previously executed, to reach a backtracked state */
  82   static void on_transition_replay(std::function<void(Transition*, RemoteApp& remote_app)> const& f)
  83   {
  84     on_transition_replay_signal.connect(f);
  85   }
  86   /** Called when executing a new transition */
  87   static void on_transition_execute(std::function<void(Transition*, RemoteApp& remote_app)> const& f)
  88   {
  89     on_transition_execute_signal.connect(f);
  90   }
  91   /** Called when displaying the statistics at the end of the exploration */
  92   static void on_log_state(std::function<void(RemoteApp&)> const& f) { on_log_state_signal.connect(f); }
  93
  94 private:
  95   void check_non_termination(const State* current_state);
  96   void backtrack();
  97
  98   /** Stack representing the position in the exploration graph */
  99   stack_t stack_;
 100
 101   /**
 102    * Provides additional metadata about the position in the exploration graph
 103    * which is used by SDPOR and ODPOR
 104    */
 105   odpor::Execution execution_seq_;
 106
 107   /** Per-actor clock vectors used to compute the "happens-before" relation */
 108   std::unordered_map<aid_t, ClockVector> per_actor_clocks_;
 109
 110 #if SIMGRID_HAVE_STATEFUL_MC
 111   VisitedStates visited_states_;
 112   std::unique_ptr<VisitedState> visited_state_;
 113 #else
 114   void* visited_state_ = nullptr; /* The code uses it to detect whether we are doing stateful MC */
 115 #endif
 116
 117   /** Opened states are states that still contains todo actors.
 118    *  When backtracking, we pick a state from it*/
 119   std::vector<std::shared_ptr<State>> opened_states_;
 120   std::shared_ptr<State> best_opened_state();
 121
 122   /** If we're running ODPOR, picks the corresponding state in the stack
 123    * (opened_states_ are ignored)
 124    */
 125   std::shared_ptr<State> next_odpor_state();
 126
 127   /** Change current stack_ value to correspond to the one we would have
 128    *  had if we executed transition to get to state. This is required when
 129    *  backtracking, and achieved thanks to the fact states save their parent.*/
 130   void restore_stack(std::shared_ptr<State> state);
 131
 132   RecordTrace get_record_trace_of_stack(stack_t stack);
 133 };
 134
 135 } // namespace simgrid::mc
 136
 137 #endif