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