src/mc/explo/odpor/Execution.hpp

   1 /* Copyright (c) 2007-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_ODPOR_EXECUTION_HPP
   7 #define SIMGRID_MC_ODPOR_EXECUTION_HPP
   8
   9 #include "src/mc/api/ClockVector.hpp"
  10 #include "src/mc/explo/odpor/odpor_forward.hpp"
  11 #include "src/mc/mc_forward.hpp"
  12 #include "src/mc/mc_record.hpp"
  13 #include "src/mc/transition/Transition.hpp"
  14
  15 #include <list>
  16 #include <optional>
  17 #include <unordered_set>
  18 #include <vector>
  19
  20 namespace simgrid::mc::odpor {
  21
  22 /**
  23  * @brief The occurrence of a transition in an execution
  24  *
  25  * An execution is set of *events*, where each element represents
  26  * the occurrence or execution of the `i`th step of a particular
  27  * actor `j`
  28  */
  29 class Event {
  30   std::pair<std::shared_ptr<Transition>, ClockVector> contents_;
  31
  32 public:
  33   Event()                        = default;
  34   Event(Event&&)                 = default;
  35   Event(const Event&)            = default;
  36   Event& operator=(const Event&) = default;
  37   explicit Event(std::pair<std::shared_ptr<Transition>, ClockVector> pair) : contents_(std::move(pair)) {}
  38
  39   std::shared_ptr<Transition> get_transition() const { return std::get<0>(contents_); }
  40   const ClockVector& get_clock_vector() const { return std::get<1>(contents_); }
  41 };
  42
  43 /**
  44  * @brief An ordered sequence of transitions which describe
  45  * the evolution of a process undergoing model checking
  46  *
  47  * An execution conceptually is just a string of actors
  48  * ids (e.g. "1.2.3.1.2.2.1.1"), where the `i`th occurrence
  49  * of actor id `j` corresponds to the `i`th action executed
  50  * by the actor with id `j` (viz. the `i`th step of actor `j`).
  51  * Executions can stand alone on their own or can extend
  52  * the execution of other sequences
  53  *
  54  * Executions are conceived based on the following papers:
  55  * 1. "Source Sets: A Foundation for Optimal Dynamic Partial Order Reduction"
  56  * by Abdulla et al.
  57  *
  58  * In addition to representing an actual steps taken,
  59  * an execution keeps track of the "happens-before"
  60  * relation among the transitions in the execution
  61  * by following the procedure outlined in section 4 of the
  62  * original DPOR paper with clock vectors.
  63  * As new transitions are added to the execution, clock vectors are
  64  * computed as appropriate and associated with the corresponding position
  65  * in the execution. This allows us to determine “happens-before” in
  66  * constant-time between points in the execution (called events
  67  * [which is unfortunately the same name used in UDPOR for a slightly
  68  * different concept]), albeit for an up-front cost of traversing the
  69  * execution stack. The happens-before relation is important in many
  70  * places in SDPOR and ODPOR.
  71  *
  72  * @note: For more nuanced happens-before relations, clock
  73  * vectors may not always suffice. Clock vectors work
  74  * well with transition-based dependencies like that used in
  75  * SimGrid; but to have a more refined independence relation,
  76  * an event-based dependency approach is needed. See the section 2
  77  * in the ODPOR paper [1] concerning event-based dependencies and
  78  * how the happens-before relation can be refined in a
  79  * computation model much like that of SimGrid. In fact, the same issue
  80  * arrises with UDPOR with context-sensitive dependencies:
  81  * the two concepts are analogous if not identical
  82  */
  83 class Execution {
  84 private:
  85   std::vector<Event> contents_;
  86   Execution(std::vector<Event>&& contents) : contents_(std::move(contents)) {}
  87
  88 public:
  89   using Handle      = decltype(contents_)::const_iterator;
  90   using EventHandle = uint32_t;
  91
  92   Execution()                            = default;
  93   Execution(const Execution&)            = default;
  94   Execution& operator=(Execution const&) = default;
  95   Execution(Execution&&)                 = default;
  96
  97   size_t size() const { return this->contents_.size(); }
  98   bool empty() const { return this->contents_.empty(); }
  99   auto begin() const { return this->contents_.begin(); }
 100   auto end() const { return this->contents_.end(); }
 101
 102   /**
 103    * @brief Computes the "core" portion the SDPOR algorithm,
 104    * viz. the intersection of the backtracking set and the
 105    * set of initials with respect to the *last* event added
 106    * to the execution
 107    *
 108    * The "core" portion of the SDPOR algorithm is found on
 109    * lines 6-9 of the pseudocode:
 110    *
 111    * 6 | let E' := pre(E, e)
 112    * 7 | let v :=  notdep(e, E).p
 113    * 8 | if I_[E'](v) ∩ backtrack(E') = empty then
 114    * 9 |    --> add some q in I_[E'](v) to backtrack(E')
 115    *
 116    * This method computes all of the lines simultaneously,
 117    * returning some actor `q` if it passes line 8 and exists.
 118    * The event `e` and the set `backtrack(E')` are the provided
 119    * arguments to the method.
 120    *
 121    * @param e the event with respect to which to determine
 122    * whether a backtrack point needs to be added for the
 123    * prefix corresponding to the execution prior to `e`
 124    *
 125    * @param backtrack_set The set of actors which should
 126    * not be considered for selection as an SDPOR initial.
 127    * While this set need not necessarily correspond to the
 128    * backtrack set `backtrack(E')`, doing so provides what
 129    * is expected for SDPOR
 130    *
 131    * See the SDPOR algorithm pseudocode in [1] for more
 132    * details for the context of the function.
 133    *
 134    * @invariant: This method assumes that events `e` and
 135    * `e' := get_latest_event_handle()` are in a *reversible* race
 136    * as is explicitly the case in SDPOR
 137    *
 138    * @returns an actor not contained in `disqualified` which
 139    * can serve as an initial to reverse the race between `e`
 140    * and `e'`
 141    */
 142   std::optional<aid_t> get_first_sdpor_initial_from(EventHandle e, std::unordered_set<aid_t> backtrack_set) const;
 143
 144   /**
 145    * @brief For a given sequence of actors `v` and a sequence of transitions `w`,
 146    * computes the sequence, if any, that should be inserted as a child a wakeup tree for
 147    * this execution
 148    */
 149   std::optional<PartialExecution> get_shortest_odpor_sq_subset_insertion(const PartialExecution& v,
 150                                                                          const PartialExecution& w) const;
 151
 152   /**
 153    * @brief For a given reversible race
 154    *
 155    * @invariant: This method assumes that events `e` and
 156    * `e_prime` are in a *reversible* race as is the case
 157    * in ODPOR
 158    */
 159   std::optional<PartialExecution> get_odpor_extension_from(EventHandle e, EventHandle e_prime,
 160                                                            const State& state_at_e) const;
 161
 162   bool is_initial_after_execution(const PartialExecution& w, aid_t p) const;
 163   bool is_independent_with_execution(const PartialExecution& w, std::shared_ptr<Transition> next_E_p) const;
 164
 165   /**
 166    * @brief Determines the event associated with
 167    * the given handle `handle`
 168    */
 169   const Event& get_event_with_handle(EventHandle handle) const { return contents_[handle]; }
 170
 171   /**
 172    * @brief Determines the actor associated with
 173    * the given event handle `handle`
 174    */
 175   aid_t get_actor_with_handle(EventHandle handle) const { return get_event_with_handle(handle).get_transition()->aid_; }
 176
 177   /**
 178    * @brief Returns a handle to the newest event of the execution,
 179    * if such an event exists
 180    */
 181   std::optional<EventHandle> get_latest_event_handle() const
 182   {
 183     return contents_.empty() ? std::nullopt : std::optional<EventHandle>{static_cast<EventHandle>(size() - 1)};
 184   }
 185
 186   /**
 187    * @brief Returns a set of events which are in
 188    * "immediate conflict" (according to the definition given
 189    * in the ODPOR paper) with the given event
 190    *
 191    * Two events `e` and `e'` in an execution `E` are said to
 192    * race iff
 193    *
 194    * 1. `proc(e) != proc(e')`; that is, the events correspond to
 195    * the execution of different actors
 196    * 2. `e -->_E e'` and there is no `e''` in `E` such that
 197    *  `e -->_E e''` and `e'' -->_E e'`; that is, the two events
 198    * "happen-before" one another in `E` and no other event in
 199    * `E` "happens-between" `e` and `e'`
 200    *
 201    * @param handle the event with respect to which races are
 202    * computed
 203    * @returns a set of event handles from which race with `handle`
 204    */
 205   std::unordered_set<EventHandle> get_racing_events_of(EventHandle handle) const;
 206
 207   /**
 208    * @brief Computes `pre(e, E)` as described in ODPOR [1]
 209    *
 210    * The execution `pre(e, E)` for an event `e` in an
 211    * execution `E` is the contiguous prefix of events
 212    * `E' <= E` up to by excluding the event `e` itself.
 213    * The prefix intuitively represents the "history" of
 214    * causes that permitted event `e` to exist (roughly
 215    * speaking)
 216    */
 217   Execution get_prefix_before(EventHandle) const;
 218
 219   /**
 220    * @brief Whether the event represented by `e1`
 221    * "happens-before" the event represented by
 222    * `e2` in the context of this execution
 223    *
 224    * In the terminology of the ODPOR paper,
 225    * this function computes
 226    *
 227    * `e1 --->_E e2`
 228    *
 229    * where `E` is this execution
 230    *
 231    * @note: The happens-before relation computed by this
 232    * execution is "coarse" in the sense that context-sensitive
 233    * independence is not exploited. To include such context-sensitive
 234    * dependencies requires a new method of keeping track of
 235    * the happens-before procedure, which is nontrivial...
 236    */
 237   bool happens_before(EventHandle e1, EventHandle e2) const;
 238
 239   /**
 240    * @brief Extends the execution by one more step
 241    *
 242    * Intutively, pushing a transition `t` onto execution `E`
 243    * is equivalent to making the execution become (using the
 244    * notation of [1]) `E.proc(t)` where `proc(t)` is the
 245    * actor which executed transition `t`.
 246    */
 247   void push_transition(std::shared_ptr<Transition>);
 248 };
 249
 250 } // namespace simgrid::mc::odpor
 251 #endif