1 /* Copyright (c) 2008-2023. The SimGrid Team. All rights reserved. */
3 /* This program is free software; you can redistribute it and/or modify it
4 * under the terms of the license (GNU LGPL) which comes with this package. */
6 #include "src/mc/explo/odpor/WakeupTree.hpp"
7 #include "src/mc/explo/odpor/Execution.hpp"
8 #include "xbt/asserts.h"
14 namespace simgrid::mc::odpor {
16 WakeupTree::WakeupTree() : WakeupTree(std::unique_ptr<WakeupTreeNode>(new WakeupTreeNode({}))) {}
17 WakeupTree::WakeupTree(std::unique_ptr<WakeupTreeNode> root) : root_(root.get())
19 this->insert_node(std::move(root));
22 WakeupTree WakeupTree::new_subtree_rooted_at(WakeupTreeNode* root)
24 if (not root->is_single_process()) {
25 throw std::invalid_argument("Selecting subtrees is only defined for single-process nodes");
28 const aid_t p = (*(root->get_sequence().begin()))->aid_;
30 // Perform a BFS search to perform a deep copy of the portion
31 // of the tree underneath and including `root`. Note that `root`
32 // is contained within the context of a *different* wakeup tree;
33 // hence, we have to be careful to update each node's children
35 auto subtree = WakeupTree();
36 WakeupTreeNode* root_equivalent = subtree.make_node(root->get_sequence());
38 std::list<std::pair<WakeupTreeNode*, WakeupTreeNode*>> frontier{std::make_pair(root, root_equivalent)};
39 while (not frontier.empty()) {
40 auto [node_in_other_tree, subtree_equivalent] = frontier.front();
43 // For each child of the node corresponding to that in `subtree`,
44 // make clones of each of its children and add them to `frontier`
45 // to that their children are added, and so on. Note that the subtree
46 // **explicitly** removes the first process from each child
47 for (WakeupTreeNode* child_in_other_tree : node_in_other_tree->get_ordered_children()) {
48 auto p_w = child_in_other_tree->get_sequence();
49 const auto p_again = p_w.front()->aid_;
51 // INVARIANT: A nodes of a wakeup tree form a prefix-closed set;
52 // this means that any child node `c` of a node `n` must contain
53 // `n.get_sequence()` as a prefix of `c.get_sequence()`
54 xbt_assert(p_again == p,
55 "Invariant Violation: The wakeup tree from which a subtree with actor "
56 "`%ld` is being taken is not prefix free! The child node starts with "
57 "`%ld` while the parent is `%ld`! This indicates that there "
58 "is a bug in the insertion logic for the wakeup tree",
62 WakeupTreeNode* child_equivalent = subtree.make_node(p_w);
63 subtree_equivalent->add_child(child_equivalent);
64 frontier.push_back(std::make_pair(child_in_other_tree, child_equivalent));
70 void WakeupTree::remove_subtree_rooted_at(WakeupTreeNode* root)
72 if (not contains(root)) {
73 throw std::invalid_argument("Attempting to remove a subtree pivoted from a node "
74 "that is not contained in this wakeup tree");
77 std::list<WakeupTreeNode*> subtree_contents;
78 std::list<WakeupTreeNode*> frontier{root};
79 while (not frontier.empty()) {
80 auto node = frontier.front();
82 for (const auto& child : node->get_ordered_children()) {
83 frontier.push_back(child);
84 subtree_contents.push_back(child);
88 // After having found each node with BFS, now we can
89 // remove them. This prevents the "joys" iteration during mutation
90 for (WakeupTreeNode* node_to_remove : subtree_contents) {
91 this->remove_node(node_to_remove);
95 bool WakeupTree::contains(WakeupTreeNode* node) const
97 return std::find_if(this->nodes_.begin(), this->nodes_.end(), [=](const auto& pair) { return pair.first == node; }) !=
101 WakeupTreeNode* WakeupTree::make_node(const PartialExecution& u)
103 auto node = std::unique_ptr<WakeupTreeNode>(new WakeupTreeNode(u));
104 auto* node_handle = node.get();
105 this->nodes_[node_handle] = std::move(node);
109 void WakeupTree::insert_node(std::unique_ptr<WakeupTreeNode> node)
111 auto* node_handle = node.get();
112 this->nodes_[node_handle] = std::move(node);
115 void WakeupTree::remove_node(WakeupTreeNode* node)
117 this->nodes_.erase(node);
120 void WakeupTree::insert(const Execution& E, const PartialExecution& w)
122 // See section 6.2 of Abdulla. et al.'s 2017 ODPOR paper for details
124 // Find the first node `v` in the tree such that
125 // `v ~_[E] w` and `v` is not a leaf node
126 for (WakeupTreeNode* node : *this) {
127 if (const auto shortest_sequence = E.get_shortest_odpor_sq_subset_insertion(node->get_sequence(), w);
128 shortest_sequence.has_value()) {
129 // Insert the sequence as a child of `node`, but only
130 // if the node is not already a leaf
131 if (not node->is_leaf() or node == this->root_) {
132 WakeupTreeNode* new_node = this->make_node(shortest_sequence.value());
133 node->add_child(new_node);
135 // Since we're following the post-order traversal of the tree,
136 // the first such node we see is the smallest w.r.t "<"
142 } // namespace simgrid::mc::odpor