src/mc/explo/udpor/Configuration.cpp

   1 /* Copyright (c) 2008-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 #include "src/mc/explo/udpor/Configuration.hpp"
   7 #include "src/mc/explo/udpor/History.hpp"
   8 #include "src/mc/explo/udpor/UnfoldingEvent.hpp"
   9 #include "src/mc/explo/udpor/maximal_subsets_iterator.hpp"
  10 #include "xbt/asserts.h"
  11
  12 #include <algorithm>
  13 #include <stack>
  14 #include <stdexcept>
  15
  16 namespace simgrid::mc::udpor {
  17
  18 Configuration::Configuration(std::initializer_list<const UnfoldingEvent*> events)
  19     : Configuration(EventSet(std::move(events)))
  20 {
  21 }
  22
  23 Configuration::Configuration(const EventSet& events) : events_(events)
  24 {
  25   if (!events_.is_valid_configuration()) {
  26     throw std::invalid_argument("The events do not form a valid configuration");
  27   }
  28 }
  29
  30 void Configuration::add_event(const UnfoldingEvent* e)
  31 {
  32   if (e == nullptr) {
  33     throw std::invalid_argument("Expected a nonnull `UnfoldingEvent*` but received NULL instead");
  34   }
  35
  36   if (this->events_.contains(e)) {
  37     return;
  38   }
  39
  40   this->events_.insert(e);
  41   this->newest_event = e;
  42
  43   // Preserves the property that the configuration is valid
  44   History history(e);
  45   if (!this->events_.contains(history)) {
  46     throw std::invalid_argument("The newly added event has dependencies "
  47                                 "which are missing from this configuration");
  48   }
  49 }
  50
  51 std::vector<const UnfoldingEvent*> Configuration::get_topologically_sorted_events() const
  52 {
  53   if (events_.empty()) {
  54     return std::vector<const UnfoldingEvent*>();
  55   }
  56
  57   std::stack<const UnfoldingEvent*> event_stack;
  58   std::vector<const UnfoldingEvent*> topological_ordering;
  59   EventSet unknown_events = events_;
  60   EventSet temporarily_marked_events;
  61   EventSet permanently_marked_events;
  62
  63   while (not unknown_events.empty()) {
  64     EventSet discovered_events;
  65     event_stack.push(*unknown_events.begin());
  66
  67     while (not event_stack.empty()) {
  68       const UnfoldingEvent* evt = event_stack.top();
  69       discovered_events.insert(evt);
  70
  71       if (not temporarily_marked_events.contains(evt)) {
  72         // If this event hasn't yet been marked, do
  73         // so now so that if we see it again in a child we can
  74         // detect a cycle and if we see it again here
  75         // we can detect that the node is re-processed
  76         temporarily_marked_events.insert(evt);
  77
  78         EventSet immediate_causes = evt->get_immediate_causes();
  79         if (!immediate_causes.empty() && immediate_causes.is_subset_of(temporarily_marked_events)) {
  80           throw std::invalid_argument("Attempted to perform a topological sort on a configuration "
  81                                       "whose contents contain a cycle. The configuration (and the graph "
  82                                       "connecting all of the events) is an invalid event structure");
  83         }
  84         immediate_causes.subtract(discovered_events);
  85         immediate_causes.subtract(permanently_marked_events);
  86         const EventSet undiscovered_causes = std::move(immediate_causes);
  87
  88         for (const auto cause : undiscovered_causes) {
  89           event_stack.push(cause);
  90         }
  91       } else {
  92         unknown_events.remove(evt);
  93         temporarily_marked_events.remove(evt);
  94         permanently_marked_events.insert(evt);
  95
  96         // In moving this event to the end of the list,
  97         // we are saying this events "happens before" other
  98         // events that are added later.
  99         topological_ordering.push_back(evt);
 100
 101         // Only now do we remove the event, i.e. once
 102         // we've processed the same event twice
 103         event_stack.pop();
 104       }
 105     }
 106   }
 107   return topological_ordering;
 108 }
 109
 110 std::vector<const UnfoldingEvent*> Configuration::get_topologically_sorted_events_of_reverse_graph() const
 111 {
 112   // The implementation exploits the property that
 113   // a topological sorting S^R of the reverse graph G^R
 114   // of some graph G is simply the reverse of any
 115   // topological sorting S of G.
 116   auto topological_events = get_topologically_sorted_events();
 117   std::reverse(topological_events.begin(), topological_events.end());
 118   return topological_events;
 119 }
 120
 121 EventSet Configuration::get_minimally_reproducible_events() const
 122 {
 123   // The implementation exploits the following observations:
 124   //
 125   // To select the smallest reproducible set of events, we want
 126   // to pick events that "knock out" a lot of others. Furthermore,
 127   // we need to ensure that the events furthest down in the
 128   // causality graph are also selected. If you combine these ideas,
 129   // you're basically left with traversing the set of maximal
 130   // subsets of C! And we have an iterator for that already!
 131   //
 132   // The next observation is that the moment we don't increase in size
 133   // the current maximal set (or decrease the number of events),
 134   // we know that the prior set `S` covered the entire history of C and
 135   // was maximal. Subsequent sets will miss events earlier in the
 136   // topological ordering that appear in `S`
 137   EventSet minimally_reproducible_events = EventSet();
 138
 139   for (const auto& maximal_set : maximal_subsets_iterator_wrapper(*this)) {
 140     if (maximal_set.size() > minimally_reproducible_events.size()) {
 141       minimally_reproducible_events = maximal_set;
 142     } else {
 143       // The moment we see the iterator generate a set of size
 144       // that is not monotonically increasing, we can stop:
 145       // the set prior was the minimally-reproducible one
 146       return minimally_reproducible_events;
 147     }
 148   }
 149   return minimally_reproducible_events;
 150 }
 151
 152 } // namespace simgrid::mc::udpor