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 namespace simgrid::mc::udpor {
  13
  14 class Configuration {
  15 public:
  16   Configuration()                                = default;
  17   Configuration(const Configuration&)            = default;
  18   Configuration& operator=(Configuration const&) = default;
  19   Configuration(Configuration&&)                 = default;
  20
  21   explicit Configuration(const EventSet& events);
  22   explicit Configuration(std::initializer_list<const UnfoldingEvent*> events);
  23
  24   auto begin() const { return this->events_.begin(); }
  25   auto end() const { return this->events_.end(); }
  26
  27   bool contains(const UnfoldingEvent* e) const { return this->events_.contains(e); }
  28   const EventSet& get_events() const { return this->events_; }
  29   const UnfoldingEvent* get_latest_event() const { return this->newest_event; }
  30
  31   /**
  32    * @brief Insert a new event into the configuration
  33    *
  34    * When the newly added event is inserted into the configuration,
  35    * an assertion is made to ensure that the configuration remains
  36    * valid, i.e. that the newly added event's dependencies are contained
  37    * within the configuration.
  38    *
  39    * @param e the event to add to the configuration. If the event is
  40    * already a part of the configuration, calling this method has no
  41    * effect.
  42    *
  43    * @throws an invalid argument exception is raised should the event
  44    * be missing one of its dependencies
  45    *
  46    * @note: UDPOR technically enforces the invariant that all newly-added events
  47    * will ensure that the configuration is valid. We perform extra checks to ensure
  48    * that UDPOR is implemented as expected. There is a performance penalty that
  49    * should be noted: checking for maximality requires ensuring that all events in the
  50    * configuration have their dependencies containes within the configuration, which
  51    * essentially means performing a BFS/DFS over the configuration using a History object.
  52    * However, since the slowest part of UDPOR involves enumerating all
  53    * subsets of maximal events and computing k-partial alternatives (the
  54    * latter definitively an NP-hard problem when optimal), Amdahl's law suggests
  55    * we shouldn't focus so much on this (let alone the additional benefit of the
  56    * assertions)
  57    */
  58   void add_event(const UnfoldingEvent* e);
  59
  60   /**
  61    * @brief Orders the events of the configuration such that
  62    * "more recent" events (i.e. those that are farther down in
  63    * the event structure's dependency chain) come after those
  64    * that appeared "farther in the past"
  65    *
  66    * @returns a vector `V` with the following property:
  67    *
  68    * 1. Let i(e) := C -> I map events to their indices in `V`.
  69    * For every pair of events e, e' in C, if e < e' then i(e) < i(e')
  70    *
  71    * Intuitively, events that are closer to the "bottom" of the event
  72    * structure appear farther along in the list than those that appear
  73    * closer to the "top"
  74    */
  75   std::vector<const UnfoldingEvent*> get_topologically_sorted_events() const;
  76
  77   /**
  78    * @brief Orders the events of the configuration such that
  79    * "more recent" events (i.e. those that are farther down in
  80    * the event structure's dependency chain) come before those
  81    * that appear "farther in the past"
  82    *
  83    * @note The events of the event structure are arranged such that
  84    * e < e' implies a directed edge from e to e'. However, it is
  85    * also useful to be able to traverse the *reverse* graph (for
  86    * example when computing the compatibility graph of a configuration),
  87    * hence the distinction between "reversed" and the method
  88    * "Configuration::get_topologically_sorted_events()"
  89    *
  90    * @returns a vector `V` with the following property:
  91    *
  92    * 1. Let i(e) := C -> I map events to their indices in `V`.
  93    * For every pair of events e, e' in C, if e < e' then i(e) > i(e')
  94    *
  95    * Intuitively, events that are closer to the "top" of the event
  96    * structure appear farther along in the list than those that appear
  97    * closer to the "bottom"
  98    */
  99   std::vector<const UnfoldingEvent*> get_topologically_sorted_events_of_reverse_graph() const;
 100
 101   /**
 102    * @brief Computes the smallest set of events whose collective histories
 103    * capture all events of this configuration
 104    *
 105    * @invariant The set of all events in the collective histories
 106    * of the events returned by this method is equal to the set of events
 107    * in this configuration
 108    *
 109    * @returns the smallest set of events whose events generates this configuration
 110    * (denoted `config(E)`)
 111    */
 112   EventSet get_minimally_reproducible_events() const;
 113
 114 private:
 115   /**
 116    * @brief The most recent event added to the configuration
 117    */
 118   const UnfoldingEvent* newest_event = nullptr;
 119
 120   /**
 121    * @brief The events which make up this configuration
 122    *
 123    * @invariant For each event `e` in `events_`, the set of
 124    * dependencies of `e` is also contained in `events_`
 125    */
 126   EventSet events_;
 127 };
 128
 129 } // namespace simgrid::mc::udpor
 130 #endif