From: Maxwell Pirtle Date: Thu, 11 May 2023 10:38:46 +0000 (+0200) Subject: Add tree pruning/subtree methods to State X-Git-Tag: v3.34~68^2~36 X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/d76deff32a7106e3c08371778d54f02f72e491bd Add tree pruning/subtree methods to State ODPOR requires that we can remove a subtree from a wakeup tree as we continue the exploration. Further, we must also be able to create a subtree from a given wakeup tree. The functionality for those methods has already been added; this commit instead introduces the management of wakeup trees specifically in the context of ODPOR exploration. --- diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp index da94f4cd9f..7606d26ead 100644 --- a/src/mc/api/State.cpp +++ b/src/mc/api/State.cpp @@ -130,7 +130,7 @@ aid_t State::next_odpor_transition() const xbt_assert(wakeup_tree_node->get_sequence().size() == 1, "We claimed that the selected branch " "contained only a single process, yet more " "than one process was actually contained in it :("); - return wakeup_tree_node->get_sequence().front()->aid_; + return wakeup_tree_node->get_first_actor(); } return -1; } @@ -201,4 +201,34 @@ void State::seed_wakeup_tree_if_needed(const odpor::Execution& prior) } } +void State::sprout_tree_from_parent_state() +{ + xbt_assert(parent_state_ != nullptr, "Attempting to construct a wakeup tree for the root state " + "(or what appears to be, rather for state without a parent defined)"); + const auto p = parent_state_->get_transition_out()->aid_; + const auto branch = std::find_if(wakeup_tree_.begin(), wakeup_tree_.end(), [=](const odpor::WakeupTreeNode* node) { + return node->is_single_process() && node->get_first_actor() == p; + }); + xbt_assert(branch != wakeup_tree_.end(), + "Attempted to create a subtree from the wakeup tree of the parent " + "state using actor `%ld`, but no such subtree could be found. " + "This implies that the wakeup tree management is broken, " + "and more specifically that subtree formation is not working " + "as intended; for if this state was generated by the parent " + "having taken an action by actor `%ld`, this implies that " + "ODPOR found `%ld` as a candidate branch prior", + p, p, p); + this->wakeup_tree_ = odpor::WakeupTree::make_subtree_rooted_at(*branch); +} + +void State::remove_subtree_starting_with(aid_t p) +{ + const auto branch = std::find_if(wakeup_tree_.begin(), wakeup_tree_.end(), [=](const odpor::WakeupTreeNode* node) { + return node->is_single_process() && node->get_first_actor() == p; + }); + xbt_assert(branch != wakeup_tree_.end(), "Attempted to remove a subtree of this state's " + "wakeup tree that does not exist"); + this->wakeup_tree_.remove_subtree_rooted_at(*branch); +} + } // namespace simgrid::mc diff --git a/src/mc/api/State.hpp b/src/mc/api/State.hpp index a991219bc2..c1aace8d0b 100644 --- a/src/mc/api/State.hpp +++ b/src/mc/api/State.hpp @@ -136,6 +136,19 @@ public: */ void seed_wakeup_tree_if_needed(const odpor::Execution& prior); + /** + * @brief Initializes the wakeup_tree_ instance by taking the subtree rooted at the + * single-process node `N` running actor `p := "actor taken by parent to form this state"` + * of the *parent's* wakeup tree + */ + void sprout_tree_from_parent_state(); + + /** + * @brief Removes the subtree rooted at the single-process node + * `N` running actor `p` of this state's wakeup tree + */ + void remove_subtree_starting_with(aid_t p); + /* Returns the total amount of states created so far (for statistics) */ static long get_expanded_states() { return expended_states_; } }; diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp index 5a3ebaad78..a4f5bc3303 100644 --- a/src/mc/explo/DFSExplorer.cpp +++ b/src/mc/explo/DFSExplorer.cpp @@ -221,7 +221,20 @@ void DFSExplorer::run() * done after next_state creation */ XBT_DEBUG("Marking Transition >>%s<< of process %ld done and adding it to the sleep set", state->get_transition_out()->to_string().c_str(), state->get_transition_out()->aid_); - state->add_sleep_set(state->get_transition_out()); // Actors are marked done when they are considerd in ActorState + state->add_sleep_set(state->get_transition_out()); // Actors are marked done when they are considered in ActorState + + if (reduction_mode_ == ReductionMode::odpor) { + // With ODPOR, after taking a step forward, we must: + // 1. remove the subtree whose root is a single-process + // node of actor `next` (viz. the action we took) from + // the wakeup tree of `state` + // + // 2. assign a copy of that subtree to the next state + // + // The latter evidently must be done BEFORE the former + next_state->sprout_tree_from_parent_state(); + state->remove_subtree_starting_with(next); + } /* DPOR persistent set procedure: * for each new transition considered, check if it depends on any other previous transition executed before it diff --git a/src/mc/explo/odpor/WakeupTree.cpp b/src/mc/explo/odpor/WakeupTree.cpp index 4b0bb65be3..9335c69b7f 100644 --- a/src/mc/explo/odpor/WakeupTree.cpp +++ b/src/mc/explo/odpor/WakeupTree.cpp @@ -13,13 +13,23 @@ namespace simgrid::mc::odpor { +aid_t WakeupTreeNode::get_first_actor() const +{ + if (seq_.empty()) { + throw std::invalid_argument("Attempted to extract the first actor from " + "a node in a wakeup tree representing the " + "empty execution (likely the root node)"); + } + return get_sequence().front()->aid_; +} + 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) +WakeupTree WakeupTree::make_subtree_rooted_at(WakeupTreeNode* root) { if (not root->is_single_process()) { throw std::invalid_argument("Selecting subtrees is only defined for single-process nodes"); diff --git a/src/mc/explo/odpor/WakeupTree.hpp b/src/mc/explo/odpor/WakeupTree.hpp index 32938f6e56..553667caeb 100644 --- a/src/mc/explo/odpor/WakeupTree.hpp +++ b/src/mc/explo/odpor/WakeupTree.hpp @@ -44,6 +44,7 @@ public: const std::list& get_ordered_children() const { return children_; } bool is_leaf() const { return children_.empty(); } bool is_single_process() const { return seq_.size() == static_cast(1); } + aid_t get_first_actor() const; /** Insert a node `node` as a new child of this node */ void add_child(WakeupTreeNode* node) { this->children_.push_back(node); } @@ -51,8 +52,7 @@ public: class WakeupTree { private: - /** @brief The root node of the tree */ - WakeupTreeNode* const root_; + WakeupTreeNode* root_; /** * @brief All of the nodes that are currently are a part of the tree @@ -86,7 +86,7 @@ public: auto end() const { return WakeupTreeIterator(); } void remove_subtree_rooted_at(WakeupTreeNode* root); - static WakeupTree new_subtree_rooted_at(WakeupTreeNode* root); + static WakeupTree make_subtree_rooted_at(WakeupTreeNode* root); /** * @brief Whether or not this tree is considered empty