src/mc/explo/udpor/Configuration.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_UDPOR_CONFIGURATION_HPP
   7 #define SIMGRID_MC_UDPOR_CONFIGURATION_HPP
   8
   9 #include "src/mc/explo/udpor/EventSet.hpp"
  10 #include "src/mc/explo/udpor/udpor_forward.hpp"
  11
  12 #include <optional>
  13 #include <string>
  14 #include <unordered_map>
  15
  16 namespace simgrid::mc::udpor {
  17
  18 class Configuration {
  19 public:
  20   Configuration()                                = default;
  21   Configuration(const Configuration&)            = default;
  22   Configuration& operator=(Configuration const&) = default;
  23   Configuration(Configuration&&)                 = default;
  24
  25   explicit Configuration(const UnfoldingEvent* event);
  26   explicit Configuration(const EventSet& events);
  27   explicit Configuration(const History& history);
  28   explicit Configuration(std::initializer_list<const UnfoldingEvent*> events);
  29
  30   auto begin() const { return this->events_.begin(); }
  31   auto end() const { return this->events_.end(); }
  32   auto cbegin() const { return this->events_.cbegin(); }
  33   auto cend() const { return this->events_.cend(); }
  34
  35   bool contains(const UnfoldingEvent* e) const { return this->events_.contains(e); }
  36   bool contains(const EventSet& events) const { return events.is_subset_of(this->events_); }
  37   const EventSet& get_events() const { return this->events_; }
  38   const UnfoldingEvent* get_latest_event() const { return this->newest_event; }
  39   std::string to_string() const { return this->events_.to_string(); }
  40
  41   /**
  42    * @brief Insert a new event into the configuration
  43    *
  44    * When the newly added event is inserted into the configuration,
  45    * an assertion is made to ensure that the configuration remains
  46    * valid, i.e. that the newly added event's dependencies are contained
  47    * within the configuration.
  48    *
  49    * @param e the event to add to the configuration. If the event is
  50    * already a part of the configuration, calling this method has no
  51    * effect.
  52    *
  53    * @throws an invalid argument exception is raised should the event
  54    * be missing one of its dependencies
  55    *
  56    * @note: UDPOR technically enforces the invariant that all newly-added events
  57    * will ensure that the configuration is valid. We perform extra checks to ensure
  58    * that UDPOR is implemented as expected. There is a performance penalty that
  59    * should be noted: checking for maximality requires ensuring that all events in the
  60    * configuration have their dependencies containes within the configuration, which
  61    * essentially means performing a BFS/DFS over the configuration using a History object.
  62    * However, since the slowest part of UDPOR involves enumerating all
  63    * subsets of maximal events and computing k-partial alternatives (the
  64    * latter definitively an NP-hard problem when optimal), Amdahl's law suggests
  65    * we shouldn't focus so much on this (let alone the additional benefit of the
  66    * assertions)
  67    */
  68   void add_event(const UnfoldingEvent* e);
  69
  70   /**
  71    * @brief Whether or not the given event can be added to
  72    * this configuration while preserving that the configuration
  73    * is causally closed and conflict-free
  74    *
  75    * A configuration `C` is compatible with an event iff
  76    * the event can be added to `C` while preserving that
  77    * the configuration is causally closed and conflict-free.
  78    *
  79    * The method effectively answers the following question:
  80    *
  81    * "Is `C + {e}` a valid configuration?"
  82    */
  83   bool is_compatible_with(const UnfoldingEvent* e) const;
  84
  85   /**
  86    * @brief Whether or not the events in the given history can be added to
  87    * this configuration while keeping the set of events causally closed
  88    * and conflict-free
  89    *
  90    * A configuration `C` is compatible with a history iff all
  91    * events of the history can be added to `C` while preserving
  92    * that the configuration is causally closed and conflict-free.
  93    *
  94    * The method effectively answers the following question:
  95    *
  96    * "Is `C + (U_i [e_i])` a valid configuration?"
  97    */
  98   bool is_compatible_with(const History& history) const;
  99
 100   std::optional<Configuration> compute_alternative_to(const EventSet& D, const Unfolding& U) const;
 101   std::optional<Configuration> compute_k_partial_alternative_to(const EventSet& D, const Unfolding& U, size_t k) const;
 102
 103   /**
 104    * @brief Orders the events of the configuration such that
 105    * "more recent" events (i.e. those that are farther down in
 106    * the event structure's dependency chain) come after those
 107    * that appeared "farther in the past"
 108    *
 109    * @returns a vector `V` with the following property:
 110    *
 111    * 1. Let i(e) := C -> I map events to their indices in `V`.
 112    * For every pair of events e, e' in C, if e < e' then i(e) < i(e')
 113    *
 114    * Intuitively, events that are closer to the "bottom" of the event
 115    * structure appear farther along in the list than those that appear
 116    * closer to the "top"
 117    */
 118   std::vector<const UnfoldingEvent*> get_topologically_sorted_events() const;
 119
 120   /**
 121    * @brief Orders the events of the configuration such that
 122    * "more recent" events (i.e. those that are farther down in
 123    * the event structure's dependency chain) come before those
 124    * that appear "farther in the past"
 125    *
 126    * @note The events of the event structure are arranged such that
 127    * e < e' implies a directed edge from e to e'. However, it is
 128    * also useful to be able to traverse the *reverse* graph (for
 129    * example when computing the compatibility graph of a configuration),
 130    * hence the distinction between "reversed" and the method
 131    * "Configuration::get_topologically_sorted_events()"
 132    *
 133    * @returns a vector `V` with the following property:
 134    *
 135    * 1. Let i(e) := C -> I map events to their indices in `V`.
 136    * For every pair of events e, e' in C, if e < e' then i(e) > i(e')
 137    *
 138    * Intuitively, events that are closer to the "top" of the event
 139    * structure appear farther along in the list than those that appear
 140    * closer to the "bottom"
 141    */
 142   std::vector<const UnfoldingEvent*> get_topologically_sorted_events_of_reverse_graph() const;
 143
 144   /**
 145    * @brief Computes the smallest set of events whose collective histories
 146    * capture all events of this configuration
 147    *
 148    * @invariant The set of all events in the collective histories
 149    * of the events returned by this method is equal to the set of events
 150    * in this configuration
 151    *
 152    * @returns the smallest set of events whose events generates
 153    * this configuration (denoted `config(E)`)
 154    */
 155   EventSet get_minimally_reproducible_events() const;
 156
 157   /**
 158    * @brief Determines the event in the configuration whose associated
 159    * transition is the latest of the given actor
 160    *
 161    * @invariant: At most one event in the configuration will correspond
 162    * to `preEvt(C, a)` for any action `a`. This can be argued by contradiction.
 163    *
 164    * If there were more than one event (`e` and `e'`) in any configuration whose
 165    * associated transitions `a` were run by the same actor at the same step, then they
 166    * could not be causally related (`<`) since `a` could not be enabled in
 167    * both subconfigurations C' and C'' containing the hypothetical events
 168    * `e` and `e` + `e'`. Since they would not be contained in each other's histories,
 169    * they would be in conflict, which cannot happen between any pair of events
 170    * in a configuration. Thus `e` and `e'` cannot exist simultaneously
 171    */
 172   std::optional<const UnfoldingEvent*> get_latest_event_of(aid_t) const;
 173   /**
 174    * @brief Determines the most recent transition of the given actor
 175    * in this configuration, or `pre(a)` as denoted in the thesis of
 176    * The Anh Pham
 177    *
 178    * Conceptually, the execution of an interleaving of the transitions
 179    * (i.e. a topological ordering) of a configuration yields a unique
 180    * state `state(C)`. Since actions taken by the same actor are always
 181    * dependent with one another, any such interleaving always yields a
 182    * unique
 183    *
 184    * @returns the most recent transition of the given actor
 185    * in this configuration, or `std::nullopt` if there are no transitions
 186    * in this configuration run by the given actor
 187    */
 188   std::optional<const Transition*> get_latest_action_of(aid_t aid) const;
 189   std::optional<const UnfoldingEvent*> pre_event(aid_t aid) const { return get_latest_event_of(aid); }
 190
 191 private:
 192   /**
 193    * @brief The most recent event added to the configuration
 194    */
 195   const UnfoldingEvent* newest_event = nullptr;
 196
 197   /**
 198    * @brief The events which make up this configuration
 199    *
 200    * @invariant For each event `e` in `events_`, the set of
 201    * dependencies of `e` is also contained in `events_`
 202    *
 203    * @invariant For each pair of events `e` and `e'` in
 204    * `events_`, `e` and `e'` are not in conflict
 205    */
 206   EventSet events_;
 207
 208   /**
 209    * @brief Maps actors to the latest events which
 210    * are executed by the actor
 211    *
 212    * @invariant: The events that are contained in the map
 213    * are also contained in the set `events_`
 214    */
 215   std::unordered_map<aid_t, const UnfoldingEvent*> latest_event_mapping;
 216 };
 217
 218 } // namespace simgrid::mc::udpor
 219 #endif