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 <functional>
  18 #include <optional>
  19
  20 namespace simgrid::mc::udpor {
  21
  22 /**
  23  * @brief Performs exploration of a concurrent system via the
  24  * UDPOR algorithm
  25  *
  26  * The `UdporChecker` implementation is based primarily off three papers,
  27  * herein referred to as [1], [2], and [3] respectively, as well as the
  28  * current implementation of `tiny_simgrid`:
  29  *
  30  * 1. "Unfolding-based Partial Order Reduction" by Rodriguez et al.
  31  * 2. "Quasi-Optimal Partial Order Reduction" by Nguyen et al.
  32  * 3. The Anh Pham's Thesis "Exploration efficace de l'espace ..."
  33  */
  34 class XBT_PRIVATE UdporChecker : public Exploration {
  35 public:
  36   explicit UdporChecker(const std::vector<char*>& args);
  37
  38   void run() override;
  39   RecordTrace get_record_trace() override;
  40   std::vector<std::string> get_textual_trace() override;
  41
  42   inline std::unique_ptr<State> get_current_state() { return std::make_unique<State>(get_remote_app()); }
  43
  44 private:
  45   Unfolding unfolding = Unfolding();
  46
  47   /**
  48    * @brief A collection of specialized functions which can incrementally
  49    * compute the extension of a configuration based on the action taken
  50    */
  51   using ExtensionFunction = std::function<EventSet(const Configuration&, const std::shared_ptr<Transition>)>;
  52   std::unordered_map<Transition::Type, ExtensionFunction> incremental_extension_functions =
  53       std::unordered_map<Transition::Type, ExtensionFunction>();
  54
  55   /**
  56    * @brief Explores the unfolding of the concurrent system
  57    * represented by the ModelChecker instance "mcmodel_checker"
  58    *
  59    * This function performs the actual search following the
  60    * UDPOR algorithm according to [1].
  61    *
  62    * @param C the current configuration from which UDPOR will be used
  63    * to explore expansions of the concurrent system being modeled
  64    * @param D the set of events that should not be considered by UDPOR
  65    * while performing its searches, in order to avoid sleep-set blocked
  66    * executions. See [1] for more details
  67    * @param A the set of events to "guide" UDPOR in the correct direction
  68    * when it returns back to a node in the unfolding and must decide among
  69    * events to select from `ex(C)`. See [1] for more details
  70    * @param stateC the state of the program after having executed `C`,
  71    * viz. `state(C)`  using the notation of [1]
  72    *
  73    * TODO: Add the optimization where we can check if e == e_prior
  74    * to prevent repeated work when computing ex(C)
  75    */
  76   void explore(const Configuration& C, EventSet D, EventSet A, std::unique_ptr<State> stateC, EventSet prev_exC);
  77
  78   /**
  79    * @brief Identifies the next event from the unfolding of the concurrent system
  80    * that should next be explored as an extension of a configuration with
  81    * enabled events `enC`
  82    *
  83    * @param A The set of events `A` maintained by the UDPOR algorithm to help
  84    * determine how events should be selected. See the original paper [1] for more details
  85    *
  86    * @param enC The set `enC` of enabled events from the extension set `exC` used
  87    * by the UDPOR algorithm to select new events to search. See the original
  88    * paper [1] for more details
  89    */
  90   const UnfoldingEvent* select_next_unfolding_event(const EventSet& A, const EventSet& enC);
  91
  92   /**
  93    * @brief Computes the sets `ex(C)` and `en(C)` of the given configuration
  94    * `C` as an incremental computation from the the previous computation of `ex(C)`
  95    *
  96    * A central component to UDPOR is the computation of the set `ex(C)`. The
  97    * extension set `ex(C)` of a configuration `C` is defined as the set of events
  98    * outside of `C` whose full dependency chain is contained in `C` (see [1]
  99    * for more details).
 100    *
 101    * In general, computing `ex(C)` is very expensive. In paper [3], The Anh Pham
 102    * shows a method of incremental computation of the set `ex(C)` under the
 103    * conclusions afforded under the computation model in consideration, of which
 104    * SimGrid is apart, which allow for `ex(C)` to be computed much more efficiently.
 105    * Intuitively, the idea is to take advantage of the fact that you can avoid a lot
 106    * of repeated computation by exploiting the aforementioned properties (in [3]) in
 107    * what is akin to a dynamic programming optimization. See [3] for more details
 108    *
 109    * @param C the configuration based on which the two sets `ex(C)` and `en(C)` are
 110    * computed
 111    * @param stateC the state of the program after having executed C (viz. `state(C)`)
 112    * @param prev_exC the previous value of `ex(C)`, viz. that which was computed for
 113    * the configuration `C' := C - {e}`
 114    * @returns the extension set `ex(C)` of `C`
 115    */
 116   EventSet compute_exC(const Configuration& C, const State& stateC, const EventSet& prev_exC);
 117
 118   /**
 119    * @brief Computes a portion of the extension set of a configuration given
 120    * some action `action` by directly enumerating all maximal subsets of C
 121    * (i.e. without specializations based on the action)
 122    */
 123   EventSet compute_exC_by_enumeration(const Configuration& C, const std::shared_ptr<Transition> action);
 124
 125   EventSet compute_enC(const Configuration& C, const EventSet& exC) const;
 126
 127   /**
 128    *
 129    */
 130   void move_to_stateCe(State& stateC, const UnfoldingEvent& e);
 131
 132   /**
 133    * @brief Creates a new snapshot of the state of the progam undergoing
 134    * model checking
 135    *
 136    * @returns the handle used to uniquely identify this state later in the
 137    * exploration of the unfolding. You provide this handle to an event in the
 138    * unfolding to regenerate past states
 139    */
 140   std::unique_ptr<State> record_current_state();
 141
 142   /**
 143    *
 144    */
 145   void restore_program_state_to(const State& stateC);
 146
 147   /**
 148    *
 149    */
 150   void clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D);
 151 };
 152 } // namespace simgrid::mc::udpor
 153
 154 #endif