From: Maxwell Pirtle Date: Tue, 28 Feb 2023 14:52:20 +0000 (+0100) Subject: Remove CompatibilityGraph and friends X-Git-Tag: v3.34~422^2~1 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/301109703c933c28285e0223836a570eaeb8875a?ds=sidebyside Remove CompatibilityGraph and friends The CompatibilityGraph and friends that were added in order to compute maximal sets of events needlessly complicated the algorithm. A much better approach was suggested which will be implemented in the next phase. While perhaps a rebase could also have been performed, it would have required quite careful precision. Since the end goal is the same and there are better uses of our time, I simply opted to tag on another commit --- diff --git a/MANIFEST.in b/MANIFEST.in index 3f308514cf..66bc0e6b50 100644 --- a/MANIFEST.in +++ b/MANIFEST.in @@ -2231,10 +2231,6 @@ include src/mc/transition/TransitionRandom.cpp include src/mc/transition/TransitionRandom.hpp include src/mc/transition/TransitionSynchro.cpp include src/mc/transition/TransitionSynchro.hpp -include src/mc/explo/udpor/CompatibilityGraph.hpp -include src/mc/explo/udpor/CompatibilityGraph.cpp -include src/mc/explo/udpor/CompatibilityGraphNode.hpp -include src/mc/explo/udpor/CompatibilityGraphNode.cpp include src/mc/explo/udpor/Configuration.hpp include src/mc/explo/udpor/Configuration.cpp include src/mc/explo/udpor/EventSet.cpp diff --git a/src/mc/explo/UdporChecker.cpp b/src/mc/explo/UdporChecker.cpp index cb6f522fa3..8a298fbc5a 100644 --- a/src/mc/explo/UdporChecker.cpp +++ b/src/mc/explo/UdporChecker.cpp @@ -5,7 +5,6 @@ #include "src/mc/explo/UdporChecker.hpp" #include "src/mc/api/State.hpp" -#include "src/mc/explo/udpor/CompatibilityGraph.hpp" #include #include @@ -162,19 +161,7 @@ EventSet UdporChecker::compute_extension_by_enumeration(const Configuration& C, // where `a` is the `action` given to us. EventSet incremental_exC; - // We only consider those combinations of events for which `action` is dependent with - // the action associated with any given event ("`a` depends on all of K") - const std::unique_ptr G = C.make_compatibility_graph_filtered_on([=](const UnfoldingEvent* e) { - const auto e_transition = e->get_transition(); - return action.depends(e_transition); - }); - - // TODO: Now that the graph has been constructed, enumerate - // all possible k-cliques of the complement of G - - // TODO: For each enumeration, check all possible - // combinations of selecting a single event from - // each set associated with the graph nodes + // Compute the extension set here using the algorithm Martin described... return incremental_exC; } diff --git a/src/mc/explo/udpor/CompatibilityGraph.cpp b/src/mc/explo/udpor/CompatibilityGraph.cpp deleted file mode 100644 index 179ca4e391..0000000000 --- a/src/mc/explo/udpor/CompatibilityGraph.cpp +++ /dev/null @@ -1,39 +0,0 @@ -/* Copyright (c) 2008-2023. The SimGrid Team. All rights reserved. */ - -/* This program is free software; you can redistribute it and/or modify it - * under the terms of the license (GNU LGPL) which comes with this package. */ - -#include "src/mc/explo/udpor/CompatibilityGraph.hpp" - -#include - -namespace simgrid::mc::udpor { - -// TODO: Remove duplication between the CompatibilityGraph -// and the Unfolding: they are practically identical - -void CompatibilityGraph::remove(CompatibilityGraphNode* e) -{ - if (e == nullptr) { - throw std::invalid_argument("Expected a non-null pointer to an event, but received NULL"); - } - this->nodes.erase(e); -} - -void CompatibilityGraph::insert(std::unique_ptr e) -{ - CompatibilityGraphNode* handle = e.get(); - auto loc = this->nodes.find(handle); - if (loc != this->nodes.end()) { - // This is bad: someone wrapped the raw event address twice - // in two different unique ptrs and attempted to - // insert it into the unfolding... - throw std::invalid_argument("Attempted to insert a node owned twice." - "This will result in a double free error and must be fixed."); - } - - // Map the handle to its owner - this->nodes[handle] = std::move(e); -} - -} // namespace simgrid::mc::udpor diff --git a/src/mc/explo/udpor/CompatibilityGraph.hpp b/src/mc/explo/udpor/CompatibilityGraph.hpp deleted file mode 100644 index a49056cddb..0000000000 --- a/src/mc/explo/udpor/CompatibilityGraph.hpp +++ /dev/null @@ -1,66 +0,0 @@ -/* Copyright (c) 2007-2023. The SimGrid Team. All rights reserved. */ - -/* This program is free software; you can redistribute it and/or modify it - * under the terms of the license (GNU LGPL) which comes with this package. */ - -#ifndef SIMGRID_MC_UDPOR_COMPATIBILITY_GRAPH_HPP -#define SIMGRID_MC_UDPOR_COMPATIBILITY_GRAPH_HPP - -#include "src/mc/explo/udpor/CompatibilityGraphNode.hpp" -#include "src/mc/explo/udpor/udpor_forward.hpp" - -#include -#include - -namespace simgrid::mc::udpor { - -/** - * @brief A graph which describes the causal-conflicts between groups of - * events from an unfolding - * - * A compatibility graph conceptually describes how causal "strands" of an - * event structure are related to one another. Each node in the graph - * represents a set of events from which only a single event could be selected - * if creating a new subset of the events of an unfolding which is *causally-free*. - * We say a set of events is *causally free* if and only if that set of events is a - * maximal set of events (i.e., the two conditions are equivalent). We write - * E(_node_) to denote the set of events associated with that node. - * - * The edges of the graph describe which "strands" are in causal conflict with one - * another. That is, if (u, v) is an edge of compatibility graph G, then at - * most one event from the set S(u) ∪ S(v) could be selected in a causally-free - * subset of events of an unfolding. - * - * An important property of a compatibility graph G is that the cliques of - * its complement graph G' (recall that the complement G' of a graph G is the - * graph which has an edge (u,v) whenever G lacks an edge (u,v)) - * determine all possible combinations of events which are maximal events; - * i.e., a clique of size `k` in G' is such that all maximal event sets - * with events chosen from the union of all events mapped to each node in the - * clique can be formed. Thus, the problem of determining sets of maximal - * events of a configuration is equivalent to finding all possible cliques - * of the compatibility graph. While this is an NP-complete problem in - * general, it is still a (potentially major) refinement over checking - * all possible subsets of events of the configuration directly. - */ -class CompatibilityGraph { -private: - std::unordered_map> nodes; - -public: - CompatibilityGraph() = default; - CompatibilityGraph& operator=(CompatibilityGraph&&) = default; - CompatibilityGraph(CompatibilityGraph&&) = default; - - auto begin() const { return this->nodes.begin(); } - auto end() const { return this->nodes.end(); } - - void remove(CompatibilityGraphNode* e); - void insert(std::unique_ptr e); - - size_t size() const { return this->nodes.size(); } - bool empty() const { return this->nodes.empty(); } -}; - -} // namespace simgrid::mc::udpor -#endif \ No newline at end of file diff --git a/src/mc/explo/udpor/CompatibilityGraphNode.cpp b/src/mc/explo/udpor/CompatibilityGraphNode.cpp deleted file mode 100644 index 00f28fcbdf..0000000000 --- a/src/mc/explo/udpor/CompatibilityGraphNode.cpp +++ /dev/null @@ -1,18 +0,0 @@ -/* Copyright (c) 2008-2023. The SimGrid Team. All rights reserved. */ - -/* This program is free software; you can redistribute it and/or modify it - * under the terms of the license (GNU LGPL) which comes with this package. */ - -#include "src/mc/explo/udpor/CompatibilityGraphNode.hpp" - -#include -#include - -namespace simgrid::mc::udpor { - -CompatibilityGraphNode::CompatibilityGraphNode(std::unordered_set conflicts, EventSet events_) - : conflicts(std::move(conflicts)), events_(std::move(events_)) -{ -} - -} // namespace simgrid::mc::udpor diff --git a/src/mc/explo/udpor/CompatibilityGraphNode.hpp b/src/mc/explo/udpor/CompatibilityGraphNode.hpp deleted file mode 100644 index 1f2d18f63a..0000000000 --- a/src/mc/explo/udpor/CompatibilityGraphNode.hpp +++ /dev/null @@ -1,40 +0,0 @@ -/* Copyright (c) 2007-2023. The SimGrid Team. All rights reserved. */ - -/* This program is free software; you can redistribute it and/or modify it - * under the terms of the license (GNU LGPL) which comes with this package. */ - -#ifndef SIMGRID_MC_UDPOR_COMPATIBILITY_GRAPH_NODE_HPP -#define SIMGRID_MC_UDPOR_COMPATIBILITY_GRAPH_NODE_HPP - -#include "src/mc/explo/udpor/EventSet.hpp" -#include "src/mc/explo/udpor/udpor_forward.hpp" - -#include -#include -#include - -namespace simgrid::mc::udpor { - -/** - * @brief A node in a `CompatabilityGraph` which describes which - * combinations of events are in causal-conflict with the events - * associated with the node - */ -class CompatibilityGraphNode { -private: - std::unordered_set conflicts; - EventSet events_; - -public: - CompatibilityGraphNode(const CompatibilityGraphNode&) = default; - CompatibilityGraphNode& operator=(CompatibilityGraphNode const&) = default; - CompatibilityGraphNode(CompatibilityGraphNode&&) = default; - CompatibilityGraphNode(std::unordered_set conflicts, EventSet events_ = EventSet()); - - void add_event(UnfoldingEvent* e) { this->events_.insert(e); } - const EventSet& get_events() const { return this->events_; } - const std::unordered_set& get_conflicts() const { return this->conflicts; } -}; - -} // namespace simgrid::mc::udpor -#endif \ No newline at end of file diff --git a/src/mc/explo/udpor/Configuration.cpp b/src/mc/explo/udpor/Configuration.cpp index 1923345630..a05d3a7a0a 100644 --- a/src/mc/explo/udpor/Configuration.cpp +++ b/src/mc/explo/udpor/Configuration.cpp @@ -120,124 +120,4 @@ std::vector Configuration::get_topologically_sorted_events_of_r 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; - - const bool e_should_appear = pred(e); - CompatibilityGraphNode* e_placement = nullptr; - - if (e_should_appear) { - // The justification is as follows: - // - // e_has_no_search_data: - // The event `e` is a leaf node, so there are no prior - // nodes in `G` to join - // - // child_count >= 2: - // If there are two or more events that this event causes, - // then we certainly must be part of a compatibility - // graph node that conflicts with each of our children - // - // e_potential_placement == nullptr: - // If nobody told us about a placement and yet still have search - // data, this means means that our child `C` had more than one child itself, - // so it we could not have moved into `C`'s _potential_ placement. - const bool new_placement_required = - e_has_no_search_data || e_child_count >= 2 || e_potential_placement == nullptr; - - 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 presence"); - // 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 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`). - // - // If there is more than one child, then each child is in conflict with `e` - // so we don't potentially place it - if (e_immediate_causes.size() == 1) { - UnfoldingEvent* only_ancestor = *e_immediate_causes.begin(); - - // If `e` is included in the graph, forward its placement on to - // the sole child. Otherwise attempt to forward `e`'s _potential_ - // (potential is stressed) placement. We can only forward `e`'s - // potential placement iff `e` has only a single child; for if - // `e` had more children, then our sole ancestor would conflict with - // each one of `e`'s children and thus couldn't be in the same group - // as any of them - if (e_should_appear) { - search_data[only_ancestor].potential_placement = e_placement; - } else { - search_data[only_ancestor].potential_placement = e_child_count == 1 ? e_potential_placement : nullptr; - } - } - - // Our ancestors conflict with everyone `e` does else PLUS `e` itself - // ONLY IF e actually was placed - auto parent_conflicts = std::move(e_conflicts); - if (e_should_appear) { - 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; -} - -std::unique_ptr Configuration::make_compatibility_graph() const -{ - return make_compatibility_graph_filtered_on([=](const UnfoldingEvent*) { return true; }); -} - } // namespace simgrid::mc::udpor diff --git a/src/mc/explo/udpor/Configuration.hpp b/src/mc/explo/udpor/Configuration.hpp index d6c95616f0..8b2c219df6 100644 --- a/src/mc/explo/udpor/Configuration.hpp +++ b/src/mc/explo/udpor/Configuration.hpp @@ -6,7 +6,6 @@ #ifndef SIMGRID_MC_UDPOR_CONFIGURATION_HPP #define SIMGRID_MC_UDPOR_CONFIGURATION_HPP -#include "src/mc/explo/udpor/CompatibilityGraph.hpp" #include "src/mc/explo/udpor/EventSet.hpp" #include "src/mc/explo/udpor/udpor_forward.hpp" @@ -103,27 +102,6 @@ public: */ std::vector get_topologically_sorted_events_of_reverse_graph() const; - /** - * @brief Construct a new compatibility graph from the events of the - * configuration that satisfy the given predicate - * - * @param pred whether or not to even consider the unfolding event in any - * compatibility nodes of the resulting graph - * @returns a new compatibility graph that defines possible maximal subsets - * of events of C that satisfy the predicate `pred` - */ - std::unique_ptr - make_compatibility_graph_filtered_on(std::function pred) const; - - /** - * @brief Construct a new compatibility graph from the events of the - * configuration - * - * @returns a new compatibility graph that defines possible maximal subsets - * of events of C - */ - std::unique_ptr make_compatibility_graph() const; - private: /** * @brief The most recent event added to the configuration diff --git a/src/mc/explo/udpor/udpor_forward.hpp b/src/mc/explo/udpor/udpor_forward.hpp index 8ac003e59d..10082359fb 100644 --- a/src/mc/explo/udpor/udpor_forward.hpp +++ b/src/mc/explo/udpor/udpor_forward.hpp @@ -14,8 +14,6 @@ namespace simgrid::mc::udpor { class EventSet; -class CompatabilityGraph; -class CompatabilityGraphNode; class Configuration; class History; class Unfolding; diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake index 60745e1f52..f8bdb6c8b3 100644 --- a/tools/cmake/DefinePackages.cmake +++ b/tools/cmake/DefinePackages.cmake @@ -527,10 +527,6 @@ set(MC_SRC src/mc/explo/UdporChecker.cpp src/mc/explo/UdporChecker.hpp - src/mc/explo/udpor/CompatibilityGraph.hpp - src/mc/explo/udpor/CompatibilityGraph.cpp - src/mc/explo/udpor/CompatibilityGraphNode.hpp - src/mc/explo/udpor/CompatibilityGraphNode.cpp src/mc/explo/udpor/Configuration.hpp src/mc/explo/udpor/Configuration.cpp src/mc/explo/udpor/EventSet.cpp