Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Add predicate filtering to compatibility graph comp
authorMaxwell Pirtle <maxwellpirtle@gmail.com>
Fri, 24 Feb 2023 14:40:39 +0000 (15:40 +0100)
committerMaxwell Pirtle <maxwellpirtle@gmail.com>
Mon, 27 Feb 2023 08:24:17 +0000 (09:24 +0100)
Computing the compatibility graph should attempt to
disqualify as many events as possible from the configuration
to minimize the size of the resulting compatibility graph.
This is _esepcially_ important because we will enumerate
all cliques of the graph and subsequently all possible
events contains within each node. This means that removing
even one or two nodes could reduce the time spent in
enumeration dramatically.

For now, the UdporChecker can only prune based on
dependency. Perhaps, though, there are more clever
ways to prune based on whether `a` is enabled e.g.
in knowing some properties about the event structure.
This will be investigated later, but is a secondary
concern to getting an implementation of the algorithm
up-and-running.

src/mc/explo/UdporChecker.cpp
src/mc/explo/udpor/CompatibilityGraph.hpp
src/mc/explo/udpor/CompatibilityGraphNode.hpp
src/mc/explo/udpor/Configuration.cpp
src/mc/explo/udpor/Configuration.hpp

index 3d97acd..c5d596d 100644 (file)
@@ -165,7 +165,7 @@ EventSet UdporChecker::compute_extension_by_enumeration(const Configuration& C,
 
   // 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<CompatibilityGraph> G = C.make_compatibility_graph_filtered_on([=](UnfoldingEvent* e) {
+  const std::unique_ptr<CompatibilityGraph> G = C.make_compatibility_graph_filtered_on([=](const UnfoldingEvent* e) {
     const auto e_transition = e->get_transition();
     return action.depends(e_transition);
   });
index 275e7f8..a49056c 100644 (file)
@@ -52,6 +52,9 @@ public:
   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<CompatibilityGraphNode> e);
 
index 49e6611..1f2d18f 100644 (file)
@@ -33,6 +33,7 @@ public:
 
   void add_event(UnfoldingEvent* e) { this->events_.insert(e); }
   const EventSet& get_events() const { return this->events_; }
+  const std::unordered_set<CompatibilityGraphNode*>& get_conflicts() const { return this->conflicts; }
 };
 
 } // namespace simgrid::mc::udpor
index 8cc96f2..ac99056 100644 (file)
@@ -119,7 +119,7 @@ std::vector<UnfoldingEvent*> Configuration::get_topologically_sorted_events_of_r
 }
 
 std::unique_ptr<CompatibilityGraph>
-Configuration::make_compatibility_graph_filtered_on(std::function<bool(UnfoldingEvent*)> pred) const
+Configuration::make_compatibility_graph_filtered_on(std::function<bool(const UnfoldingEvent*)> pred) const
 {
   auto G = std::make_unique<CompatibilityGraph>();
 
@@ -146,48 +146,76 @@ Configuration::make_compatibility_graph_filtered_on(std::function<bool(Unfolding
     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;
 
-    // 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<CompatibilityGraphNode>(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);
+    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<CompatibilityGraphNode>(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) {
-      // 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;
+      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);
-    parent_conflicts.insert(e_placement);
+    if (e_should_appear) {
+      parent_conflicts.insert(e_placement);
+    }
     for (auto* cause : e_immediate_causes) {
       search_data[cause].immediate_children_count += 1;
 
index ead739e..b2c469e 100644 (file)
@@ -114,7 +114,7 @@ public:
    * of events of C that satisfy the predicate `pred`
    */
   std::unique_ptr<CompatibilityGraph>
-  make_compatibility_graph_filtered_on(std::function<bool(UnfoldingEvent*)> pred) const;
+  make_compatibility_graph_filtered_on(std::function<bool(const UnfoldingEvent*)> pred) const;
 
 private:
   /**