Add logic for subtree extraction from wakeup trees

Extracting a subtree from a wakeup tree is required
for ODPOR to continue its search and to pass information
down to the other paths that ODPOR decides to visit.
Extracting a copy of a subtree is difficult as it
requires a deep copy of the tree, making sure
that references to any nodes in the tree that is copied
are copied appropriately. One additional subtlety is that
the subtree can only be taken with respect to single-process
branches and, further, that that process is removed from
each descendant of the node that contains the single process.

diff --git a/src/mc/explo/odpor/WakeupTree.cpp b/src/mc/explo/odpor/WakeupTree.cpp
index 0365208..e5f983f 100644 (file)
--- a/src/mc/explo/odpor/WakeupTree.cpp
+++ b/src/mc/explo/odpor/WakeupTree.cpp
@@ -5,21 +5,82 @@
 
 #include "src/mc/explo/odpor/WakeupTree.hpp"
 #include "src/mc/explo/odpor/Execution.hpp"
+#include "xbt/asserts.h"
 
 #include <algorithm>
+#include <exception>
+#include <queue>
 
 namespace simgrid::mc::odpor {
 
-WakeupTree::WakeupTree() : root(nullptr) {}
+WakeupTree::WakeupTree() : WakeupTree(std::unique_ptr<WakeupTreeNode>(new WakeupTreeNode({}))) {}
+WakeupTree::WakeupTree(std::unique_ptr<WakeupTreeNode> root) : root_(root.get())
+{
+  this->insert_node(std::move(root));
+}
+
+WakeupTree WakeupTree::new_subtree_rooted_at(WakeupTreeNode* root)
+{
+  if (not root->is_single_process()) {
+    throw std::invalid_argument("Selecting subtrees is only defined for single-process nodes");
+  }
+
+  const aid_t p = (*(root->get_sequence().begin()))->aid_;
+
+  // Perform a BFS search to perform a deep copy of the portion
+  // of the tree underneath and including `root`. Note that `root`
+  // is contained within the context of a *different* wakeup tree;
+  // hence, we have to be careful to update each node's children
+  // appropriately
+  auto subtree                    = WakeupTree();
+  WakeupTreeNode* root_equivalent = subtree.make_node(root->get_sequence());
+
+  std::list<std::pair<WakeupTreeNode*, WakeupTreeNode*>> frontier{std::make_pair(root, root_equivalent)};
+  while (not frontier.empty()) {
+    auto [node_in_other_tree, subtree_equivalent] = frontier.front();
+    frontier.pop_front();
+
+    // For each child of the node corresponding to that in `subtree`,
+    // make clones of each of its children and add them to `frontier`
+    // to that their children are added, and so on. Note that the subtree
+    // **explicitly** removes the first process from each child
+    for (WakeupTreeNode* child_in_other_tree : node_in_other_tree->get_ordered_children()) {
+      auto p_w           = child_in_other_tree->get_sequence();
+      const auto p_again = p_w.front()->aid_;
+
+      // INVARIANT: A nodes of a wakeup tree form a prefix-closed set;
+      // this means that any child node `c` of a node `n` must contain
+      // `n.get_sequence()` as a prefix of `c.get_sequence()`
+      xbt_assert(p_again == p,
+                 "Invariant Violation: The wakeup tree from which a subtree with actor "
+                 "`%ld` is being taken is not prefix free! The child node starts with "
+                 "`%ld` while the parent is `%ld`! This indicates that there "
+                 "is a bug in the insertion logic for the wakeup tree",
+                 p, p_again, p);
+      p_w.pop_front();
+
+      WakeupTreeNode* child_equivalent = subtree.make_node(p_w);
+      subtree_equivalent->add_child(child_equivalent);
+      frontier.push_back(std::make_pair(child_in_other_tree, child_equivalent));
+    }
+  }
+  return subtree;
+}
 
 WakeupTreeNode* WakeupTree::make_node(const PartialExecution& u)
 {
-  auto node                = std::unique_ptr<WakeupTreeNode>(new WakeupTreeNode(u));
-  auto* node_handle        = node.get();
-  this->nodes_[node.get()] = std::move(node);
+  auto node                 = std::unique_ptr<WakeupTreeNode>(new WakeupTreeNode(u));
+  auto* node_handle         = node.get();
+  this->nodes_[node_handle] = std::move(node);
   return node_handle;
 }
 
+void WakeupTree::insert_node(std::unique_ptr<WakeupTreeNode> node)
+{
+  auto* node_handle         = node.get();
+  this->nodes_[node_handle] = std::move(node);
+}
+
 void WakeupTree::insert(const Execution& E, const PartialExecution& w)
 {
   // See section 6.2 of Abdulla. et al.'s 2017 ODPOR paper for details

diff --git a/src/mc/explo/odpor/WakeupTree.hpp b/src/mc/explo/odpor/WakeupTree.hpp
index 56b3988..e0fc5a6 100644 (file)
--- a/src/mc/explo/odpor/WakeupTree.hpp
+++ b/src/mc/explo/odpor/WakeupTree.hpp
@@ -29,6 +29,11 @@ private:
   friend WakeupTree;
 
 public:
+  WakeupTreeNode(const WakeupTreeNode&)            = delete;
+  WakeupTreeNode(WakeupTreeNode&&)                 = default;
+  WakeupTreeNode& operator=(const WakeupTreeNode&) = delete;
+  WakeupTreeNode& operator=(WakeupTreeNode&&)      = default;
+
   const auto begin() const { return this->children_.begin(); }
   const auto end() const { return this->children_.end(); }
   const auto rbegin() const { return this->children_.rbegin(); }
@@ -36,8 +41,8 @@ public:
 
   const PartialExecution& get_sequence() const { return seq_; }
   const std::list<WakeupTreeNode*>& get_ordered_children() const { return children_; }
-
   bool is_leaf() const { return children_.empty(); }
+  bool is_single_process() const { return children_.size() == static_cast<size_t>(1); }
 
   /** Insert a node `node` as a new child of this node */
   void add_child(WakeupTreeNode* node) { this->children_.push_back(node); }
@@ -46,7 +51,7 @@ public:
 class WakeupTree {
 private:
   /** @brief The root node of the tree */
-  const WakeupTreeNode* const root;
+  WakeupTreeNode* const root_;
 
   /**
    * @brief All of the nodes that are currently are a part of the tree
@@ -58,6 +63,11 @@ private:
    */
   std::unordered_map<WakeupTreeNode*, std::unique_ptr<WakeupTreeNode>> nodes_;
 
+  /**
+   * @brief Transfers the lifetime of node `node` to the tree
+   */
+  void insert_node(std::unique_ptr<WakeupTreeNode> node);
+
   /**
    * @brief Creates a new, disconnected node in this tree
    */
@@ -68,7 +78,8 @@ private:
 
 public:
   WakeupTree();
-  ~WakeupTree() = default;
+  explicit WakeupTree(std::unique_ptr<WakeupTreeNode> root);
+  static WakeupTree new_subtree_rooted_at(WakeupTreeNode* root);
 
   auto begin() const { return WakeupTreeIterator(*this); }
   auto end() const { return WakeupTreeIterator(); }
@@ -78,7 +89,7 @@ public:
    * such that that this tree is a wakeup tree relative to the
    * given execution
    */
-  void insert(const Execution&, const PartialExecution& seq);
+  void insert(const Execution& E, const PartialExecution& seq);
 };
 
 } // namespace simgrid::mc::odpor