From 03b61d41e9281c5d7a68ebc72c326d33f1f3bc1a Mon Sep 17 00:00:00 2001 From: Maxwell Pirtle Date: Wed, 10 May 2023 14:34:02 +0200 Subject: [PATCH] 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. --- src/mc/explo/odpor/WakeupTree.cpp | 69 +++++++++++++++++++++++++++++-- src/mc/explo/odpor/WakeupTree.hpp | 19 +++++++-- 2 files changed, 80 insertions(+), 8 deletions(-) diff --git a/src/mc/explo/odpor/WakeupTree.cpp b/src/mc/explo/odpor/WakeupTree.cpp index 0365208c42..e5f983f0de 100644 --- 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 +#include +#include namespace simgrid::mc::odpor { -WakeupTree::WakeupTree() : root(nullptr) {} +WakeupTree::WakeupTree() : WakeupTree(std::unique_ptr(new WakeupTreeNode({}))) {} +WakeupTree::WakeupTree(std::unique_ptr 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> 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(new WakeupTreeNode(u)); - auto* node_handle = node.get(); - this->nodes_[node.get()] = std::move(node); + auto node = std::unique_ptr(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 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 56b3988c15..e0fc5a6212 100644 --- 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& get_ordered_children() const { return children_; } - bool is_leaf() const { return children_.empty(); } + bool is_single_process() const { return children_.size() == static_cast(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> nodes_; + /** + * @brief Transfers the lifetime of node `node` to the tree + */ + void insert_node(std::unique_ptr node); + /** * @brief Creates a new, disconnected node in this tree */ @@ -68,7 +78,8 @@ private: public: WakeupTree(); - ~WakeupTree() = default; + explicit WakeupTree(std::unique_ptr 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 -- 2.20.1