X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/a123c47d727be0441ca0702d10a3ef63437deca7..f456852dd160e1f60f58e2a3ef37a0e688993fe0:/src/mc/explo/udpor/Configuration.cpp diff --git a/src/mc/explo/udpor/Configuration.cpp b/src/mc/explo/udpor/Configuration.cpp index 084854de7f..8cc96f2581 100644 --- a/src/mc/explo/udpor/Configuration.cpp +++ b/src/mc/explo/udpor/Configuration.cpp @@ -4,15 +4,205 @@ * under the terms of the license (GNU LGPL) which comes with this package. */ #include "src/mc/explo/udpor/Configuration.hpp" +#include "src/mc/explo/udpor/History.hpp" +#include "src/mc/explo/udpor/UnfoldingEvent.hpp" +#include "xbt/asserts.h" + +#include +#include +#include namespace simgrid::mc::udpor { +Configuration::Configuration(std::initializer_list events) : Configuration(EventSet(std::move(events))) +{ +} + +Configuration::Configuration(const EventSet& events) : events_(events) +{ + if (!events_.is_valid_configuration()) { + throw std::invalid_argument("The events do not form a valid configuration"); + } +} + void Configuration::add_event(UnfoldingEvent* e) { + if (e == nullptr) { + throw std::invalid_argument("Expected a nonnull `UnfoldingEvent*` but received NULL instead"); + } + + if (this->events_.contains(e)) { + return; + } + this->events_.insert(e); this->newest_event = e; - // TODO: Re-compute the maxmimal events + // Preserves the property that the configuration is valid + History history(e); + if (!this->events_.contains(history)) { + throw std::invalid_argument("The newly added event has dependencies " + "which are missing from this configuration"); + } +} + +std::vector Configuration::get_topologically_sorted_events() const +{ + if (events_.empty()) { + return std::vector(); + } + + std::stack event_stack; + std::vector topological_ordering; + EventSet unknown_events = events_, temporarily_marked_events, permanently_marked_events; + + while (not unknown_events.empty()) { + EventSet discovered_events; + event_stack.push(*unknown_events.begin()); + + while (not event_stack.empty()) { + UnfoldingEvent* evt = event_stack.top(); + discovered_events.insert(evt); + + if (not temporarily_marked_events.contains(evt)) { + // If this event hasn't yet been marked, do + // so now so that if we see it again in a child we can + // detect a cycle and if we see it again here + // we can detect that the node is re-processed + temporarily_marked_events.insert(evt); + + EventSet immediate_causes = evt->get_immediate_causes(); + if (!immediate_causes.empty() && immediate_causes.is_subset_of(temporarily_marked_events)) { + throw std::invalid_argument("Attempted to perform a topological sort on a configuration " + "whose contents contain a cycle. The configuration (and the graph " + "connecting all of the events) is an invalid event structure"); + } + immediate_causes.subtract(discovered_events); + immediate_causes.subtract(permanently_marked_events); + const EventSet undiscovered_causes = std::move(immediate_causes); + + for (const auto cause : undiscovered_causes) { + event_stack.push(cause); + } + } else { + // Mark this event as: + // 1. discovered across all DFSs performed + // 2. permanently marked + // 3. part of the topological search + unknown_events.remove(evt); + temporarily_marked_events.remove(evt); + permanently_marked_events.insert(evt); + + // In moving this event to the end of the list, + // we are saying this events "happens before" other + // events that are added later. + topological_ordering.push_back(evt); + + // Only now do we remove the event, i.e. once + // we've processed the same event again + event_stack.pop(); + } + } + } + return topological_ordering; +} + +std::vector Configuration::get_topologically_sorted_events_of_reverse_graph() const +{ + // The method exploits the property that + // a topological sorting S^R of the reverse graph G^R + // of some graph G is simply the reverse of any + // topological sorting S of G. + auto topological_events = get_topologically_sorted_events(); + std::reverse(topological_events.begin(), topological_events.end()); + return topological_events; +} + +std::unique_ptr +Configuration::make_compatibility_graph_filtered_on(std::function pred) const +{ + auto G = std::make_unique(); + + struct UnfoldingEventSearchData { + int immediate_children_count = 0; + CompatibilityGraphNode* potential_placement = nullptr; + std::unordered_set conflicts = std::unordered_set(); + }; + std::unordered_map search_data; + + for (auto* e : get_topologically_sorted_events_of_reverse_graph()) { + + // 1. Figure out where to place `e` in `G` + + // Determine which nodes in the graph are in conflict + // with this event. These nodes would have been added by child + // events while iterating over the topological ordering of the reverse graph + + const auto e_search_data_loc = search_data.find(e); + const bool e_has_no_search_data = e_search_data_loc == search_data.end(); + const auto e_search_data = e_has_no_search_data ? UnfoldingEventSearchData() : std::move(e_search_data_loc->second); + + const auto& e_conflicts = e_search_data.conflicts; + const auto& e_potential_placement = e_search_data.potential_placement; + const auto e_child_count = e_search_data.immediate_children_count; + + CompatibilityGraphNode* e_placement = nullptr; + + // The justification is as follows: + // + // e_has_no_search_data: + // If nobody told us about a placement, we must either be a leaf event + // OR be the cause of an event that itself has more than one cause. + // + // child_count >= 2: + // If there are two or more events that this event causes, + // then we certainly must be part of a different compatibility + // graph node since + const bool new_placement_required = e_has_no_search_data || e_child_count >= 2; + + if (new_placement_required) { + auto new_graph_node = std::make_unique(e_conflicts, EventSet({e})); + e_placement = new_graph_node.get(); + G->insert(std::move(new_graph_node)); + } else { + xbt_assert(e_child_count == 1, "An event was informed by an immediate child of placement in " + "the same compatibility graph node, yet the child did not inform " + "the parent about its precense"); + // A child event told us this node can be in the + // same compatibility node in the graph G. Add ourselves now + e_placement = e_potential_placement; + e_placement->add_event(e); + } + + // 2. Update the children of `e` + + const EventSet& e_immediate_causes = e->get_immediate_causes(); + if (e_immediate_causes.size() == 1) { + // If there is only a single ancestor, then it MAY BE in + // the same "chain" of events as us. Note that the ancestor must + // also have only a single child (see the note on `new_placement_required`) + UnfoldingEvent* only_ancestor = *e_immediate_causes.begin(); + search_data[only_ancestor].potential_placement = e_placement; + } + + // Our ancestors conflict with everyone `e` does else PLUS `e` itself + auto parent_conflicts = std::move(e_conflicts); + parent_conflicts.insert(e_placement); + for (auto* cause : e_immediate_causes) { + search_data[cause].immediate_children_count += 1; + + for (auto parent_conflict : parent_conflicts) { + search_data[cause].conflicts.insert(parent_conflict); + } + } + + // This event will only ever be seen once in the + // topological ordering. Hence, its resources do not + // need to be kept around + search_data.erase(e); + } + + return G; } } // namespace simgrid::mc::udpor