From 4164a74926df84d357f66508c72d0dd716de5387 Mon Sep 17 00:00:00 2001 From: Maxwell Pirtle Date: Thu, 11 May 2023 11:04:23 +0200 Subject: [PATCH] Add skeleton for expansion phase of ODPOR --- src/mc/api/ActorState.hpp | 8 +++-- src/mc/api/State.cpp | 30 +++++++++++++++++- src/mc/api/State.hpp | 38 ++++++++++++++++++++--- src/mc/explo/DFSExplorer.cpp | 36 ++++++++++++++++++--- src/mc/explo/odpor/WakeupTree.cpp | 2 +- src/mc/explo/odpor/WakeupTree.hpp | 7 ++--- src/mc/explo/odpor/WakeupTreeIterator.cpp | 7 +++-- src/mc/mc_config.cpp | 3 +- 8 files changed, 109 insertions(+), 22 deletions(-) diff --git a/src/mc/api/ActorState.hpp b/src/mc/api/ActorState.hpp index 315ed8af38..18be326da7 100644 --- a/src/mc/api/ActorState.hpp +++ b/src/mc/api/ActorState.hpp @@ -115,16 +115,18 @@ public: } void mark_done() { this->state_ = InterleavingType::done; } - inline Transition* get_transition(unsigned times_considered) const + std::shared_ptr get_transition() const { return get_transition(get_times_considered()); } + + std::shared_ptr get_transition(unsigned times_considered) const { xbt_assert(times_considered < this->pending_transitions_.size(), "Actor %ld does not have a state available transition with `times_considered = %u`,\n" "yet one was asked for", aid_, times_considered); - return this->pending_transitions_[times_considered].get(); + return this->pending_transitions_[times_considered]; } - inline void set_transition(std::shared_ptr t, unsigned times_considered) + void set_transition(std::shared_ptr t, unsigned times_considered) { xbt_assert(times_considered < this->pending_transitions_.size(), "Actor %ld does not have a state available transition with `times_considered = %u`, " diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp index 8430f525b6..da94f4cd9f 100644 --- a/src/mc/api/State.cpp +++ b/src/mc/api/State.cpp @@ -120,6 +120,21 @@ std::pair State::next_transition_guided() const return strategy_->next_transition(); } +aid_t State::next_odpor_transition() const +{ + const auto first_single_process_branch = + std::find_if(wakeup_tree_.begin(), wakeup_tree_.end(), + [=](const odpor::WakeupTreeNode* node) { return node->is_single_process(); }); + if (first_single_process_branch != wakeup_tree_.end()) { + const auto* wakeup_tree_node = *first_single_process_branch; + 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 -1; +} + // This should be done in GuidedState, or at least interact with it std::shared_ptr State::execute_next(aid_t next, RemoteApp& app) { @@ -132,7 +147,7 @@ std::shared_ptr State::execute_next(aid_t next, RemoteApp& app) // when simcall_handle will be called on it auto& actor_state = strategy_->actors_to_run_.at(next); const unsigned times_considered = actor_state.do_consider(); - const auto* expected_executed_transition = actor_state.get_transition(times_considered); + const auto* expected_executed_transition = actor_state.get_transition(times_considered).get(); xbt_assert(expected_executed_transition != nullptr, "Expected a transition with %u times considered to be noted in actor %ld", times_considered, next); @@ -173,4 +188,17 @@ std::unordered_set State::get_backtrack_set() const return actors; } +void State::seed_wakeup_tree_if_needed(const odpor::Execution& prior) +{ + // TODO: Note that the next action taken by the actor may be updated + // after it executes. But we will have already inserted it into the + // tree and decided upon "happens-before" at that point for different + // executions :( + if (wakeup_tree_.empty()) { + if (const aid_t next = std::get<0>(next_transition_guided()); next >= 0) { + wakeup_tree_.insert(prior, odpor::PartialExecution{strategy_->actors_to_run_.at(next).get_transition()}); + } + } +} + } // namespace simgrid::mc diff --git a/src/mc/api/State.hpp b/src/mc/api/State.hpp index fbacda384d..a991219bc2 100644 --- a/src/mc/api/State.hpp +++ b/src/mc/api/State.hpp @@ -10,6 +10,7 @@ #include "src/mc/api/ClockVector.hpp" #include "src/mc/api/RemoteApp.hpp" #include "src/mc/api/strategy/Strategy.hpp" +#include "src/mc/explo/odpor/WakeupTree.hpp" #include "src/mc/transition/Transition.hpp" #if SIMGRID_HAVE_STATEFUL_MC @@ -45,16 +46,29 @@ class XBT_PRIVATE State : public xbt::Extendable { * transition */ std::map sleep_set_; + /** + * The wakeup tree with respect to the execution represented + * by the totality of all states before and including this one + * and with respect to this state's sleep set + */ + odpor::WakeupTree wakeup_tree_; + public: explicit State(RemoteApp& remote_app); explicit State(RemoteApp& remote_app, std::shared_ptr parent_state); /* Returns a positive number if there is another transition to pick, or -1 if not */ aid_t next_transition() const; // this function should disapear as it is redundant with the next one - /* Same as next_transition, but choice is now guided, and an integer corresponding to the + /* Same as next_transition(), but choice is now guided, and an integer corresponding to the internal cost of the transition is returned */ std::pair next_transition_guided() const; + /** + * Same as next_transition(), but the choice is not based off the ODPOR + * wakeup tree associated with this state + */ + aid_t next_odpor_transition() const; + /** * @brief Explore a new path on the remote app; the parameter 'next' must be the result of a previous call to * next_transition() @@ -67,8 +81,8 @@ public: /* Marking as TODO some actor in this state: * + consider_one mark aid actor (and assert it is possible) - * + consider_best ensure one actor is marked by eventually marking the best regarding its guiding methode - * + conside_all mark all enabled actor that are not done yet */ + * + consider_best ensure one actor is marked by eventually marking the best regarding its guiding method + * + consider_all mark all enabled actor that are not done yet */ void consider_one(aid_t aid) const { strategy_->consider_one(aid); } void consider_best() const { strategy_->consider_best(); } unsigned long consider_all() const { return strategy_->consider_all(); } @@ -94,7 +108,7 @@ public: * in SimGrid consists of those actors marked as `todo` * (i.e. those that have yet to be explored) as well as those * marked `done` (i.e. those that have already been explored) - * since the pseudcode in none of the above algorithms explicitly + * since the pseudocode in none of the above algorithms explicitly * removes elements from the backtrack set. DPOR makes use * explicitly of the `done` set, but we again note that the * backtrack set still contains processes added to the done set. @@ -106,6 +120,22 @@ public: sleep_set_.insert_or_assign(t->aid_, Transition(t->type_, t->aid_, t->times_considered_)); } + /** + * @brief Inserts an arbitrary enabled actor into the wakeup tree + * associated with this state, if such an actor exists and if + * the wakeup tree is already not empty + * + * @param prior The sequence of steps leading up to this state + * with respec to which the tree associated with this state should be + * a wakeup tree (wakeup trees are defined relative to an execution) + * + * @invariant: You should not manipulate a wakeup tree with respect + * to more than one execution; doing so will almost certainly lead to + * unexpected results as wakeup trees are defined relative to a single + * execution + */ + void seed_wakeup_tree_if_needed(const odpor::Execution& prior); + /* 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 e7738b58e4..5a3ebaad78 100644 --- a/src/mc/explo/DFSExplorer.cpp +++ b/src/mc/explo/DFSExplorer.cpp @@ -93,8 +93,8 @@ void DFSExplorer::restore_stack(std::shared_ptr state) } XBT_DEBUG("Replaced stack by %s", get_record_trace().to_string().c_str()); - if (reduction_mode_ == ReductionMode::sdpor) { - execution_seq_ = sdpor::Execution(); + if (reduction_mode_ == ReductionMode::sdpor || reduction_mode_ == ReductionMode::odpor) { + execution_seq_ = odpor::Execution(); // NOTE: The outgoing transition for the top-most // state of the stack refers to that which was taken @@ -143,8 +143,14 @@ void DFSExplorer::run() XBT_ERROR("/!\\ Max depth of %d reached! THIS WILL PROBABLY BREAK the dpor reduction /!\\", _sg_mc_max_depth.get()); XBT_ERROR("/!\\ If bad things happen, disable dpor with --cfg=model-check/reduction:none /!\\"); - } else + } else if (reduction_mode_ == ReductionMode::sdpor || reduction_mode_ == ReductionMode::odpor) { + XBT_ERROR("/!\\ Max depth of %d reached! THIS **WILL** BREAK the reduction, which is not sound " + "when stopping at a fixed depth /!\\", + _sg_mc_max_depth.get()); + XBT_ERROR("/!\\ If bad things happen, disable dpor with --cfg=model-check/reduction:none /!\\"); + } else { XBT_WARN("/!\\ Max depth reached ! /!\\ "); + } this->backtrack(); continue; } @@ -161,9 +167,20 @@ void DFSExplorer::run() } #endif + if (reduction_mode_ == ReductionMode::odpor) { + // In the case of ODPOR, the wakeup tree for this + // state may be empty if we're exploring new territory + // (rather than following the partial execution of a + // wakeup tree). This corresponds to lines 9 to 13 of + // the ODPOR pseudocode + state->seed_wakeup_tree_if_needed(execution_seq_); + } + // Search for the next transition - // next_transition returns a pair in case we want to consider multiple state (eg. during backtrack) - auto [next, _] = state->next_transition_guided(); + // next_transition returns a pair + // in case we want to consider multiple states (eg. during backtrack) + const aid_t next = reduction_mode_ == ReductionMode::odpor ? state->next_odpor_transition() + : std::get<0>(state->next_transition_guided()); if (next < 0) { // If there is no more transition in the current state, backtrack. XBT_VERB("%lu actors remain, but none of them need to be interleaved (depth %zu).", state->get_actor_count(), @@ -295,6 +312,10 @@ void DFSExplorer::run() } } } + } else if (reduction_mode_ == ReductionMode::odpor) { + // In the case of ODPOR, we simply observe the transition that was executed + // until we've reached a maximal trace + execution_seq_.push_transition(executed_transition.get()); } // Before leaving that state, if the transition we just took can be taken multiple times, we @@ -373,6 +394,11 @@ std::shared_ptr DFSExplorer::best_opened_state() void DFSExplorer::backtrack() { + if (reduction_mode_ == ReductionMode::odpor) { + // TODO: In the case of ODPOR, adding in backtrack points occurs + // only after a full execution has been realized + } + XBT_VERB("Backtracking from %s", get_record_trace().to_string().c_str()); XBT_DEBUG("%lu alternatives are yet to be explored:", opened_states_.size()); diff --git a/src/mc/explo/odpor/WakeupTree.cpp b/src/mc/explo/odpor/WakeupTree.cpp index 662585e420..4b0bb65be3 100644 --- a/src/mc/explo/odpor/WakeupTree.cpp +++ b/src/mc/explo/odpor/WakeupTree.cpp @@ -128,7 +128,7 @@ void WakeupTree::insert(const Execution& E, const PartialExecution& w) shortest_sequence.has_value()) { // Insert the sequence as a child of `node`, but only // if the node is not already a leaf - if (not node->is_leaf()) { + if (not node->is_leaf() or node == this->root_) { WakeupTreeNode* new_node = this->make_node(shortest_sequence.value()); node->add_child(new_node); } diff --git a/src/mc/explo/odpor/WakeupTree.hpp b/src/mc/explo/odpor/WakeupTree.hpp index 28f549ecc2..32938f6e56 100644 --- a/src/mc/explo/odpor/WakeupTree.hpp +++ b/src/mc/explo/odpor/WakeupTree.hpp @@ -43,7 +43,7 @@ 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); } + bool is_single_process() const { return seq_.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); } @@ -66,6 +66,7 @@ private: void insert_node(std::unique_ptr node); void remove_node(WakeupTreeNode* node); + bool contains(WakeupTreeNode* node) const; /** * @brief Adds a new node to the tree, disconnected from @@ -74,8 +75,6 @@ private: */ WakeupTreeNode* make_node(const PartialExecution& u); - bool contains(WakeupTreeNode* node) const; - /* Allow the iterator to access the contents of the tree */ friend WakeupTreeIterator; @@ -96,7 +95,7 @@ public: * considered "empty" if it only contains the root node; * that is, if it is "uninteresting". In such a case, */ - bool is_empty() const { return nodes_.size() == static_cast(1); } + bool empty() const { return nodes_.size() == static_cast(1); } /** * @brief Inserts an sequence `seq` of processes into the tree diff --git a/src/mc/explo/odpor/WakeupTreeIterator.cpp b/src/mc/explo/odpor/WakeupTreeIterator.cpp index faaa90a7a4..eb3d2190a6 100644 --- a/src/mc/explo/odpor/WakeupTreeIterator.cpp +++ b/src/mc/explo/odpor/WakeupTreeIterator.cpp @@ -21,7 +21,7 @@ void WakeupTreeIterator::push_until_left_most_found() // one node in the tree won't have any children, // so the loop will eventually terminate auto* cur_top_node = *post_order_iteration.top(); - while (!cur_top_node->is_leaf()) { + while (not cur_top_node->is_leaf()) { // INVARIANT: Since we push children in // reverse order (right-most to left-most), // we ensure that we'll always process left-most @@ -29,8 +29,11 @@ void WakeupTreeIterator::push_until_left_most_found() auto& children = cur_top_node->children_; for (auto iter = children.rbegin(); iter != children.rend(); ++iter) { - post_order_iteration.push(iter.base()); + // iter.base() points one element past where we seek; hence, + // we move it over one position + post_order_iteration.push((--iter.base())); } + cur_top_node = *post_order_iteration.top(); } } diff --git a/src/mc/mc_config.cpp b/src/mc/mc_config.cpp index d451db1729..fe9b06fd1a 100644 --- a/src/mc/mc_config.cpp +++ b/src/mc/mc_config.cpp @@ -151,8 +151,7 @@ simgrid::mc::ReductionMode simgrid::mc::get_model_checking_reduction() } else if (cfg_mc_reduction.get() == "sdpor") { return ReductionMode::sdpor; } else if (cfg_mc_reduction.get() == "odpor") { - XBT_INFO("No reduction will be used: ODPOR is not yet supported in SimGrid"); - return simgrid::mc::ReductionMode::none; + return simgrid::mc::ReductionMode::odpor; } else if (cfg_mc_reduction.get() == "udpor") { XBT_INFO("No reduction will be used: " "UDPOR is has a dedicated invocation 'model-check/unfolding-checker' " -- 2.20.1