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/mc_record.hpp"
  12 #include "src/mc/udpor_global.hpp"
  13
  14 #include <optional>
  15
  16 namespace simgrid::mc::udpor {
  17
  18 /**
  19  * @brief Performs exploration of a concurrent system via the
  20  * UDPOR algorithm
  21  *
  22  * The `UdporChecker` implementation is based primarily off three papers,
  23  * herein referred to as [1], [2], and [3] respectively, as well as the
  24  * current implementation of `tiny_simgrid`:
  25  *
  26  * 1. "Unfolding-based Partial Order Reduction" by Rodriguez et al.
  27  * 2. Quasi-Optimal Partial Order Reduction by Nguyen et al.
  28  * 3. The Anh Pham's Thesis "Exploration efficace de l'espace ..."
  29  */
  30 class XBT_PRIVATE UdporChecker : public Exploration {
  31 public:
  32   explicit UdporChecker(const std::vector<char*>& args);
  33
  34   void run() override;
  35   RecordTrace get_record_trace() override;
  36   std::vector<std::string> get_textual_trace() override;
  37
  38   inline std::unique_ptr<State> get_current_state() { return std::make_unique<State>(get_remote_app()); }
  39
  40 private:
  41   /**
  42    * The total number of events created whilst exploring the unfolding
  43    */
  44   uint32_t nb_events = 0;
  45   uint32_t nb_traces = 0;
  46
  47   /**
  48    * @brief The "relevant" portions of the unfolding that must be kept around to ensure that
  49    * UDPOR properly searches the state space
  50    *
  51    * The set `U` is a global variable which is maintained by UDPOR
  52    * to keep track of "just enough" information about the unfolding
  53    * to compute *alternatives* (see the paper for more details).
  54    *
  55    * @invariant: When a new event is created by UDPOR, it is inserted into
  56    * this set. All new events that are created by UDPOR have causes that
  57    * also exist in U and are valid for the duration of the search.
  58    *
  59    * If an event is discarded instead of moved from set `U` to set `G`,
  60    * the event and its contents will be discarded.
  61    */
  62   EventSet U;
  63
  64   /**
  65    * @brief The "irrelevant" portions of the unfolding that do not need to be kept
  66    * around to ensure that UDPOR functions correctly
  67    *
  68    * The set `G` is another global variable maintained by the UDPOR algorithm which
  69    * is used to keep track of all events which used to be important to UDPOR
  70    */
  71   EventSet G;
  72
  73   /**
  74    * Maintains the mapping between handles referenced by events in
  75    * the current state of the unfolding
  76    */
  77   StateManager state_manager_;
  78
  79 private:
  80   /**
  81    * @brief Explores the unfolding of the concurrent system
  82    * represented by the ModelChecker instance "mcmodel_checker"
  83    *
  84    * This function performs the actual search following the
  85    * UDPOR algorithm according to [1].
  86    */
  87   void explore(Configuration C, EventSet D, EventSet A, std::list<EventSet> max_evt_history, UnfoldingEvent* cur_event,
  88                EventSet prev_exC);
  89
  90   /**
  91    * @brief Computes the sets `ex(C)` and `en(C)` of the given configuration
  92    * `C` as an incremental computation from the the previous computation of `ex(C)`
  93    *
  94    * A central component to UDPOR is the computation of the set `ex(C)`. The
  95    * extension set `ex(C)` of a configuration `C` is defined as the set of events
  96    * outside of `C` whose full dependency chain is contained in `C` (see [1]
  97    * for more details).
  98    *
  99    * In general, computing `ex(C)` is very expensive. In paper [3], The Anh Pham
 100    * shows a method of incremental computation of the set `ex(C)` under the
 101    * conclusions afforded under the computation model in consideration, of which
 102    * SimGrid is apart, which allow for `ex(C)` to be computed much more efficiently.
 103    * Intuitively, the idea is to take advantage of the fact that you can avoid a lot
 104    * of repeated computation by exploiting the aforementioned properties (in [3]) in
 105    * what is effectively a dynamic programming optimization. See [3] for more details
 106    *
 107    * @param C the configuration based on which the two sets `ex(C)` and `en(C)` are
 108    * computed
 109    * @param cur_event the event where UDPOR currently "rests", viz. the event UDPOR
 110    * is now currently considering
 111    * @param prev_exC the previous value of `ex(C)`, viz. that which was computed for
 112    * the configuration `C' := C - {cur_event}`
 113    * @returns a tuple containing the pair of sets `ex(C)` and `en(C)` respectively
 114    */
 115   std::tuple<EventSet, EventSet> compute_extension(const Configuration& C, const std::list<EventSet>& max_evt_history,
 116                                                    const UnfoldingEvent& cur_event, const EventSet& prev_exC) const;
 117
 118   /**
 119    *
 120    */
 121   void observe_unfolding_event(const UnfoldingEvent& event);
 122   State& get_state_referenced_by(const UnfoldingEvent& event);
 123   StateHandle record_newly_visited_state();
 124
 125   /**
 126    * @brief Identifies the next event from the unfolding of the concurrent system
 127    * that should next be explored as an extension of a configuration with
 128    * enabled events `enC`
 129    *
 130    * @param A The set of events `A` maintained by the UDPOR algorithm to help
 131    * determine how events should be selected. See the original paper [1] for more details
 132    *
 133    * @param enC The set `enC` of enabled events from the extension set `exC` used
 134    * by the UDPOR algorithm to select new events to search. See the original
 135    * paper [1] for more details
 136    */
 137   UnfoldingEvent* select_next_unfolding_event(const EventSet& A, const EventSet& enC);
 138
 139   /**
 140    *
 141    */
 142   EventSet compute_partial_alternative(const EventSet& D, const Configuration& C, const unsigned k) const;
 143
 144   /**
 145    *
 146    */
 147   void clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D);
 148 };
 149 } // namespace simgrid::mc::udpor
 150
 151 #endif