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/api/State.hpp"
  11 #include "src/mc/explo/Exploration.hpp"
  12 #include "src/mc/explo/udpor/Configuration.hpp"
  13 #include "src/mc/explo/udpor/EventSet.hpp"
  14 #include "src/mc/explo/udpor/Unfolding.hpp"
  15 #include "src/mc/explo/udpor/UnfoldingEvent.hpp"
  16 #include "src/mc/mc_record.hpp"
  17
  18 #include <functional>
  19 #include <list>
  20 #include <optional>
  21
  22 namespace simgrid::mc::udpor {
  23
  24 /**
  25  * @brief Performs exploration of a concurrent system via the
  26  * UDPOR algorithm
  27  *
  28  * The `UdporChecker` implementation is based primarily off three papers,
  29  * herein referred to as [1], [2], and [3] respectively, as well as the
  30  * current implementation of `tiny_simgrid`:
  31  *
  32  * 1. "Unfolding-based Partial Order Reduction" by Rodriguez et al.
  33  * 2. "Quasi-Optimal Partial Order Reduction" by Nguyen et al.
  34  * 3. The Anh Pham's Thesis "Exploration efficace de l'espace ..."
  35  */
  36 class XBT_PRIVATE UdporChecker : public Exploration {
  37 public:
  38   explicit UdporChecker(const std::vector<char*>& args);
  39
  40   void run() override;
  41   RecordTrace get_record_trace() override;
  42   std::unique_ptr<State> get_current_state() { return std::make_unique<State>(get_remote_app()); }
  43
  44 private:
  45   Unfolding unfolding = Unfolding();
  46
  47   // The current sequence of states that the checker has
  48   // visited in order to reach the current configuration
  49   std::list<std::unique_ptr<State>> state_stack;
  50
  51   /**
  52    * @brief Explores the unfolding of the concurrent system
  53    * represented by the ModelChecker instance "mcmodel_checker"
  54    *
  55    * This function performs the actual search following the
  56    * UDPOR algorithm according to [1].
  57    *
  58    * @param C the current configuration from which UDPOR will be used
  59    * to explore expansions of the concurrent system being modeled
  60    * @param D the set of events that should not be considered by UDPOR
  61    * while performing its searches, in order to avoid sleep-set blocked
  62    * executions. See [1] for more details
  63    * @param A the set of events to "guide" UDPOR in the correct direction
  64    * when it returns back to a node in the unfolding and must decide among
  65    * events to select from `ex(C)`. See [1] for more details
  66    *
  67    * TODO: Add the optimization where we can check if e == e_prior
  68    * to prevent repeated work when computing ex(C)
  69    */
  70   void explore(const Configuration& C, EventSet D, EventSet A, EventSet prev_exC);
  71
  72   /**
  73    * @brief Identifies the next event from the unfolding of the concurrent system
  74    * that should next be explored as an extension of a configuration with
  75    * enabled events `enC`
  76    *
  77    * @param A The set of events `A` maintained by the UDPOR algorithm to help
  78    * determine how events should be selected. See the original paper [1] for more details
  79    *
  80    * @param enC The set `enC` of enabled events from the extension set `exC` used
  81    * by the UDPOR algorithm to select new events to search. See the original
  82    * paper [1] for more details
  83    */
  84   UnfoldingEvent* select_next_unfolding_event(const EventSet& A, const EventSet& enC);
  85
  86   /**
  87    * @brief Computes the sets `ex(C)` and `en(C)` of the given configuration
  88    * `C` as an incremental computation from the the previous computation of `ex(C)`
  89    *
  90    * A central component to UDPOR is the computation of the set `ex(C)`. The
  91    * extension set `ex(C)` of a configuration `C` is defined as the set of events
  92    * outside of `C` whose full dependency chain is contained in `C` (see [1]
  93    * for more details).
  94    *
  95    * In general, computing `ex(C)` is very expensive. In paper [3], The Anh Pham
  96    * shows a method of incremental computation of the set `ex(C)` under the
  97    * conclusions afforded under the computation model in consideration, of which
  98    * SimGrid is apart, which allow for `ex(C)` to be computed much more efficiently.
  99    * Intuitively, the idea is to take advantage of the fact that you can avoid a lot
 100    * of repeated computation by exploiting the aforementioned properties (in [3]) in
 101    * what is akin to a dynamic programming optimization. See [3] for more details
 102    *
 103    * @param C the configuration based on which the two sets `ex(C)` and `en(C)` are
 104    * computed
 105    * @param stateC the state of the program after having executed C (viz. `state(C)`)
 106    * @param prev_exC the previous value of `ex(C)`, viz. that which was computed for
 107    * the configuration `C' := C - {e}`
 108    * @returns the extension set `ex(C)` of `C`
 109    */
 110   EventSet compute_exC(const Configuration& C, const State& stateC, const EventSet& prev_exC);
 111   EventSet compute_enC(const Configuration& C, const EventSet& exC) const;
 112
 113   /**
 114    *
 115    */
 116   void move_to_stateCe(State* stateC, UnfoldingEvent* e);
 117
 118   /**
 119    * @brief Creates a new snapshot of the state of the application
 120    * as it currently looks
 121    */
 122   std::unique_ptr<State> record_current_state();
 123
 124   /**
 125    * @brief Move the application side into the state at the top of the
 126    * state stack provided
 127    *
 128    * As UDPOR performs its search, it moves the application-side along with
 129    * it so that the application is always providing the checker with
 130    * the correct information about what each actor is running (and whether
 131    * those actors are enabled) at the state reached by the configuration it
 132    * decides to search.
 133    *
 134    * When UDPOR decides to "backtrack" (e.g. after reaching a configuration
 135    * whose en(C) is empty), before it attempts to continue the search by taking
 136    * a different path from a configuration it visited in the past, it must ensure
 137    * that the application-side has moved back into `state(C)`.
 138    *
 139    * The search may have moved the application arbitrarily deep into its execution,
 140    * and the search may backtrack arbitrarily closer to the beginning of the execution.
 141    * The UDPOR implementation in SimGrid ensures that the stack is updated appropriately,
 142    * but the process must still be regenerated.
 143    */
 144   void restore_program_state_with_current_stack();
 145
 146   /**
 147    * @brief Perform the functionality of the `Remove(e, C, D)` function in [1]
 148    */
 149   void clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D);
 150 };
 151 } // namespace simgrid::mc::udpor
 152
 153 #endif