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 class Event {
  28   std::pair<const Transition*, ClockVector> contents_;
  29
  30 public:
  31   Event()                        = default;
  32   Event(Event&&)                 = default;
  33   Event(const Event&)            = default;
  34   Event& operator=(const Event&) = default;
  35
  36   explicit Event(std::pair<const Transition*, ClockVector> pair) : contents_(std::move(pair)) {}
  37
  38   const Transition* get_transition() const { return std::get<0>(contents_); }
  39   const ClockVector& get_clock_vector() const { return std::get<1>(contents_); }
  40 };
  41
  42 /**
  43  * @brief An ordered sequence of transitions which describe
  44  * the evolution of a process undergoing model checking
  45  *
  46  * An execution conceptually is just a string of actors
  47  * ids (e.g. "1.2.3.1.2.2.1.1"), where the `i`th occurrence
  48  * of actor id `j` corresponds to the `i`th action executed
  49  * by the actor with id `j` (viz. the `i`th step of actor `j`).
  50  * Executions can stand alone on their own or can extend
  51  * the execution of other sequences
  52  *
  53  * Executions are conceived based on the following papers:
  54  * 1. "Source Sets: A Foundation for Optimal Dynamic Partial Order Reduction"
  55  * by Abdulla et al.
  56  *
  57  * In addition to representing an actual steps taken,
  58  * an execution keeps track of the "happens-before"
  59  * relation among the transitions in the execution
  60  * by following the procedure outlined in the
  61  * original DPOR paper with clock vectors
  62  *
  63  * @note: For more nuanced happens-before relations, clock
  64  * vectors may not always suffice. Clock vectors work
  65  * well with transition-based dependencies like that used in
  66  * SimGrid; but to have a more refined independence relation,
  67  * an event-based dependency approach is needed. See the section 2
  68  * in the ODPOR paper [1] concerning event-based dependencies and
  69  * how the happens-before relation can be refined in a
  70  * computation model much like that of SimGrid. In fact, the same issue
  71  * arrises with UDPOR with context-sensitive dependencies:
  72  * the two concepts are analogous if not identical
  73  */
  74 class Execution {
  75 private:
  76   /**
  77    * @brief The actual steps that are taken by the process
  78    * during exploration, relative to the
  79    */
  80   std::vector<Event> contents_;
  81
  82   Execution(std::vector<Event>&& contents) : contents_(std::move(contents)) {}
  83
  84 public:
  85   using Handle      = decltype(contents_)::const_iterator;
  86   using EventHandle = uint32_t;
  87
  88   Execution()                            = default;
  89   Execution(const Execution&)            = default;
  90   Execution& operator=(Execution const&) = default;
  91   Execution(Execution&&)                 = default;
  92   Execution(ExecutionSequence&& seq);
  93   Execution(const ExecutionSequence& seq);
  94
  95   size_t size() const { return this->contents_.size(); }
  96   bool empty() const { return this->contents_.empty(); }
  97
  98   std::optional<aid_t> get_first_ssdpor_initial_from(EventHandle e, std::unordered_set<aid_t> disqualified) const;
  99   std::unordered_set<aid_t> get_ssdpor_initials_from(EventHandle e, std::unordered_set<aid_t> disqualified) const;
 100
 101   // std::unordered_set<aid_t> get_initials_after(const Hypothetical& w) const;
 102   // std::unordered_set<aid_t> get_weak_initials_after(const Hypothetical& w) const;
 103
 104   // std::unordered_set<aid_t> get_initials_after(const Hypothetical& w) const;
 105   // std::unordered_set<aid_t> get_weak_initials_after(const Hypothetical& w) const;
 106
 107   // bool is_initial(aid_t p, const Hypothetical& w) const;
 108   // bool is_weak_initial(aid_t p, const Hypothetical& w) const;
 109
 110   const Event& get_event_with_handle(EventHandle handle) const { return contents_[handle]; }
 111   aid_t get_actor_with_handle(EventHandle handle) const { return get_event_with_handle(handle).get_transition()->aid_; }
 112
 113   /**
 114    * @brief Returns a set of IDs of events which are in
 115    * "immediate conflict" (according to the definition given
 116    * in the ODPOR paper) with one another
 117    */
 118   std::unordered_set<EventHandle> get_racing_events_of(EventHandle) const;
 119
 120   /**
 121    * @brief Returns a handle to the newest event of the execution,
 122    * if such an event exists
 123    */
 124   std::optional<EventHandle> get_latest_event_handle() const
 125   {
 126     return contents_.empty() ? std::nullopt : std::optional<EventHandle>{static_cast<EventHandle>(size() - 1)};
 127   }
 128
 129   Execution get_prefix_up_to(EventHandle) const;
 130
 131   /**
 132    * @brief Whether the event represented by `e1`
 133    * "happens-before" the event represented by
 134    * `e2` in the context of this execution
 135    *
 136    * In the terminology of the ODPOR paper,
 137    * this function computes
 138    *
 139    * `e1 --->_E e2`
 140    *
 141    * where `E` is this execution
 142    *
 143    * @note: The happens-before relation computed by this
 144    * execution is "coarse" in the sense that context-sensitive
 145    * independence is not exploited. To include such context-sensitive
 146    * dependencies requires a new method of keeping track of
 147    * the happens-before procedure, which is nontrivial...
 148    */
 149   bool happens_before(EventHandle e1, EventHandle e2) const;
 150
 151   /**
 152    * @brief Removes the last event of the execution,
 153    * if such an event exists
 154    *
 155    * @note: When you remove events from an execution, any views
 156    * of the execution referring to those removed events
 157    * become invalidated
 158    */
 159   void pop_latest();
 160
 161   /**
 162    * @brief Extends the execution by one more step
 163    *
 164    * Intutively, pushing a transition `t` onto execution `E`
 165    * is equivalent to making the execution become (using the
 166    * notation of [1]) `E.proc(t)` where `proc(t)` is the
 167    * actor which executed transition `t`.
 168    */
 169   void push_transition(const Transition*);
 170 };
 171
 172 } // namespace simgrid::mc::odpor
 173 #endif