src/mc/explo/UdporChecker.hpp

   1 /* Copyright (c) 2007-2023. 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_UDPOR_CHECKER_HPP
   8 #define SIMGRID_MC_UDPOR_CHECKER_HPP
   9
  10 #include "src/mc/explo/Exploration.hpp"
  11 #include "src/mc/explo/udpor/Configuration.hpp"
  12 #include "src/mc/explo/udpor/EventSet.hpp"
  13 #include "src/mc/explo/udpor/Unfolding.hpp"
  14 #include "src/mc/explo/udpor/UnfoldingEvent.hpp"
  15 #include "src/mc/mc_record.hpp"
  16
  17 #include <optional>
  18
  19 namespace simgrid::mc::udpor {
  20
  21 /**
  22  * @brief Performs exploration of a concurrent system via the
  23  * UDPOR algorithm
  24  *
  25  * The `UdporChecker` implementation is based primarily off three papers,
  26  * herein referred to as [1], [2], and [3] respectively, as well as the
  27  * current implementation of `tiny_simgrid`:
  28  *
  29  * 1. "Unfolding-based Partial Order Reduction" by Rodriguez et al.
  30  * 2. Quasi-Optimal Partial Order Reduction by Nguyen et al.
  31  * 3. The Anh Pham's Thesis "Exploration efficace de l'espace ..."
  32  */
  33 class XBT_PRIVATE UdporChecker : public Exploration {
  34 public:
  35   explicit UdporChecker(const std::vector<char*>& args);
  36
  37   void run() override;
  38   RecordTrace get_record_trace() override;
  39   std::vector<std::string> get_textual_trace() override;
  40
  41   inline std::unique_ptr<State> get_current_state() { return std::make_unique<State>(get_remote_app()); }
  42
  43 private:
  44   /**
  45    * The total number of events created whilst exploring the unfolding
  46    */
  47   /* FIXME: private fields are not used
  48     uint32_t nb_events = 0;
  49     uint32_t nb_traces = 0;
  50   */
  51
  52   /**
  53    * @brief The "relevant" portions of the unfolding that must be kept around to ensure that
  54    * UDPOR properly searches the state space
  55    *
  56    * The set `U` is a global variable which is maintained by UDPOR
  57    * to keep track of "just enough" information about the unfolding
  58    * to compute *alternatives* (see the paper for more details).
  59    *
  60    * @invariant: When a new event is created by UDPOR, it is inserted into
  61    * this set. All new events that are created by UDPOR have causes that
  62    * also exist in U and are valid for the duration of the search.
  63    *
  64    * If an event is discarded instead of moved from set `U` to set `G`,
  65    * the event and its contents will be discarded.
  66    */
  67   EventSet U;
  68
  69   /**
  70    * @brief The "irrelevant" portions of the unfolding that do not need to be kept
  71    * around to ensure that UDPOR functions correctly
  72    *
  73    * The set `G` is another global variable maintained by the UDPOR algorithm which
  74    * is used to keep track of all events which used to be important to UDPOR
  75    */
  76   EventSet G;
  77
  78   /**
  79    * @brief UDPOR's current "view" of the program it is exploring
  80    */
  81   Unfolding unfolding = Unfolding();
  82
  83 private:
  84   /**
  85    * @brief Explores the unfolding of the concurrent system
  86    * represented by the ModelChecker instance "mcmodel_checker"
  87    *
  88    * This function performs the actual search following the
  89    * UDPOR algorithm according to [1].
  90    *
  91    * @param C the current configuration from which UDPOR will be used
  92    * to explore expansions of the concurrent system being modeled
  93    * @param D the set of events that should not be considered by UDPOR
  94    * while performing its searches, in order to avoid sleep-set blocked
  95    * executions. See [1] for more details
  96    * @param A the set of events to "guide" UDPOR in the correct direction
  97    * when it returns back to a node in the unfolding and must decide among
  98    * events to select from `ex(C)`. See [1] for more details
  99    * @param stateC the state of the program after having executed `C`,
 100    * viz. `state(C)`  using the notation of [1]
 101    *
 102    * TODO: Add the optimization where we can check if e == e_prior
 103    * to prevent repeated work when computing ex(C)
 104    */
 105   void explore(Configuration C, EventSet D, EventSet A, std::unique_ptr<State> stateC, EventSet prev_exC);
 106
 107   /**
 108    * @brief Identifies the next event from the unfolding of the concurrent system
 109    * that should next be explored as an extension of a configuration with
 110    * enabled events `enC`
 111    *
 112    * @param A The set of events `A` maintained by the UDPOR algorithm to help
 113    * determine how events should be selected. See the original paper [1] for more details
 114    *
 115    * @param enC The set `enC` of enabled events from the extension set `exC` used
 116    * by the UDPOR algorithm to select new events to search. See the original
 117    * paper [1] for more details
 118    */
 119   UnfoldingEvent* select_next_unfolding_event(const EventSet& A, const EventSet& enC);
 120
 121   /**
 122    * @brief Computes the sets `ex(C)` and `en(C)` of the given configuration
 123    * `C` as an incremental computation from the the previous computation of `ex(C)`
 124    *
 125    * A central component to UDPOR is the computation of the set `ex(C)`. The
 126    * extension set `ex(C)` of a configuration `C` is defined as the set of events
 127    * outside of `C` whose full dependency chain is contained in `C` (see [1]
 128    * for more details).
 129    *
 130    * In general, computing `ex(C)` is very expensive. In paper [3], The Anh Pham
 131    * shows a method of incremental computation of the set `ex(C)` under the
 132    * conclusions afforded under the computation model in consideration, of which
 133    * SimGrid is apart, which allow for `ex(C)` to be computed much more efficiently.
 134    * Intuitively, the idea is to take advantage of the fact that you can avoid a lot
 135    * of repeated computation by exploiting the aforementioned properties (in [3]) in
 136    * what is effectively a dynamic programming optimization. See [3] for more details
 137    *
 138    * @param C the configuration based on which the two sets `ex(C)` and `en(C)` are
 139    * computed
 140    * @param prev_exC the previous value of `ex(C)`, viz. that which was computed for
 141    * the configuration `C' := C - {e}`
 142    * @returns a tuple containing the pair of sets `ex(C)` and `en(C)` respectively
 143    */
 144   std::tuple<EventSet, EventSet> compute_extension(const Configuration& C, const EventSet& prev_exC) const;
 145
 146   /**
 147    *
 148    */
 149   EventSet compute_partial_alternative(const EventSet& D, const Configuration& C, const unsigned k) const;
 150
 151   /**
 152    *
 153    */
 154   void move_to_stateCe(State& stateC, const UnfoldingEvent& e);
 155
 156   /**
 157    * @brief Creates a new snapshot of the state of the progam undergoing
 158    * model checking
 159    *
 160    * @returns the handle used to uniquely identify this state later in the
 161    * exploration of the unfolding. You provide this handle to an event in the
 162    * unfolding to regenerate past states
 163    */
 164   std::unique_ptr<State> record_current_state();
 165
 166   /**
 167    *
 168    */
 169   void restore_program_state_to(const State& stateC);
 170
 171   /**
 172    *
 173    */
 174   void clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D);
 175 };
 176 } // namespace simgrid::mc::udpor
 177
 178 #endif