From a9a21312483780dd659eba21102f79f207984f7c Mon Sep 17 00:00:00 2001 From: Maxwell Pirtle Date: Wed, 10 May 2023 09:08:27 +0200 Subject: [PATCH] Add skeleton of implementation for tree insertion The `insert` method on a Wakeup tree is an essential component of the ODPOR algorithm. Tree insertion guides the ODPOR algorithm towards the unique, unsearched traces of the state space. Insertion is based heavily on the correctness of computing the `~` relation over a given execution. Subsequent commits will fill in this method as well as several others that will be needed to implement that functionality --- src/mc/explo/odpor/Execution.cpp | 6 ++++++ src/mc/explo/odpor/Execution.hpp | 9 ++++++-- src/mc/explo/odpor/WakeupTree.cpp | 26 ++++++++++++++++++++++- src/mc/explo/odpor/WakeupTree.hpp | 24 ++++++++++++++++++--- src/mc/explo/odpor/WakeupTreeIterator.cpp | 1 + src/mc/explo/odpor/WakeupTreeIterator.hpp | 8 +++---- src/mc/explo/odpor/odpor_forward.hpp | 1 + 7 files changed, 65 insertions(+), 10 deletions(-) diff --git a/src/mc/explo/odpor/Execution.cpp b/src/mc/explo/odpor/Execution.cpp index d190a72a1f..3d2832dc03 100644 --- a/src/mc/explo/odpor/Execution.cpp +++ b/src/mc/explo/odpor/Execution.cpp @@ -149,6 +149,12 @@ std::optional Execution::get_first_sdpor_initial_from(EventHandle e, return std::nullopt; } +std::optional Execution::get_shortest_odpor_sq_subset_insertion(const ProcessSequence& v, + const ExecutionSequence& w) const +{ + return std::nullopt; +} + bool Execution::happens_before(Execution::EventHandle e1_handle, Execution::EventHandle e2_handle) const { // 1. "happens-before" (-->_E) is a subset of "occurs before" (<_E) diff --git a/src/mc/explo/odpor/Execution.hpp b/src/mc/explo/odpor/Execution.hpp index f851cf47f7..58b28c291a 100644 --- a/src/mc/explo/odpor/Execution.hpp +++ b/src/mc/explo/odpor/Execution.hpp @@ -144,8 +144,13 @@ public: */ std::optional get_first_sdpor_initial_from(EventHandle e, std::unordered_set backtrack_set) const; - std::optional get_shortest_odpor_sq_subset_insert(const ProcessSequence& v, - const ExecutionSequence& w) const; + /** + * @brief For a given sequence of actors `v` and a sequence of transitions `w`, + * computes the sequence, if any, that should be inserted as a child a WakeupTree for + * this execution + */ + std::optional get_shortest_odpor_sq_subset_insertion(const ProcessSequence& v, + const ExecutionSequence& w) const; /** * @brief Determines the event associated with diff --git a/src/mc/explo/odpor/WakeupTree.cpp b/src/mc/explo/odpor/WakeupTree.cpp index bbe6b698c1..93cab13a8a 100644 --- a/src/mc/explo/odpor/WakeupTree.cpp +++ b/src/mc/explo/odpor/WakeupTree.cpp @@ -12,10 +12,34 @@ namespace simgrid::mc::odpor { WakeupTree::WakeupTree() : root(nullptr) {} +WakeupTreeNode* WakeupTree::make_node(const ProcessSequence& u) +{ + auto node = std::unique_ptr(new WakeupTreeNode(u)); + auto* node_handle = node.get(); + this->nodes_[node.get()] = std::move(node); + return node_handle; +} + void WakeupTree::insert(const Execution& E, const ExecutionSequence& w) { + // See section 6.2 of Abdulla. et al.'s 2017 ODPOR paper for details + // Find the first node `v` in the tree such that - // `v ~_[E] w` + // `v ~_[E] w` and `v` is not a leaf node + for (WakeupTreeNode* node : *this) { + if (const auto shortest_sequence = E.get_shortest_odpor_sq_subset_insertion(node->get_sequence(), 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()) { + WakeupTreeNode* new_node = this->make_node(shortest_sequence.value()); + node->add_child(new_node); + } + // Since we're following the post-order traversal of the tree, + // the first such node we see is the smallest w.r.t "<" + return; + } + } } } // namespace simgrid::mc::odpor \ No newline at end of file diff --git a/src/mc/explo/odpor/WakeupTree.hpp b/src/mc/explo/odpor/WakeupTree.hpp index 81356cd4cf..552e582afc 100644 --- a/src/mc/explo/odpor/WakeupTree.hpp +++ b/src/mc/explo/odpor/WakeupTree.hpp @@ -6,6 +6,7 @@ #ifndef SIMGRID_MC_ODPOR_WAKEUP_TREE_HPP #define SIMGRID_MC_ODPOR_WAKEUP_TREE_HPP +#include "src/mc/explo/odpor/WakeupTreeIterator.hpp" #include "src/mc/explo/odpor/odpor_forward.hpp" #include @@ -15,12 +16,17 @@ namespace simgrid::mc::odpor { class WakeupTreeNode { private: + explicit WakeupTreeNode(const ProcessSequence& u) : seq_(u) {} + /** An ordered list of children of for this node in the tree */ - std::list children_; + std::list children_; /** @brief The contents of the node */ ProcessSequence seq_; + /** Allows the owning tree to insert directly into the child */ + friend WakeupTree; + public: const auto begin() const { return this->children_.begin(); } const auto end() const { return this->children_.end(); } @@ -28,9 +34,12 @@ public: const auto rend() const { return this->children_.rend(); } const ProcessSequence& get_sequence() const { return seq_; } - const std::list& get_ordered_children() const { return children_; } + const std::list& get_ordered_children() const { return children_; } bool is_leaf() const { return children_.empty(); } + + /** Insert a node `node` as a new child of this node */ + void add_child(WakeupTreeNode* node) { this->children_.push_back(node); } }; class WakeupTree { @@ -46,13 +55,22 @@ private: * of the addresses that are referenced by the nodes WakeupTreeNode and Configuration. * ODPOR guarantees that nodes are persisted as long as needed. */ - std::unordered_map> nodes_; + std::unordered_map> nodes_; + + /** + * @brief Creates a new, disconnected node in this tree + */ + WakeupTreeNode* make_node(const ProcessSequence& u); /* Allow the iterator to access the contents of the tree */ friend WakeupTreeIterator; public: WakeupTree(); + ~WakeupTree() = default; + + auto begin() const { return WakeupTreeIterator(*this); } + auto end() const { return WakeupTreeIterator(); } /** * @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 684a63304a..bb479f37cf 100644 --- a/src/mc/explo/odpor/WakeupTreeIterator.cpp +++ b/src/mc/explo/odpor/WakeupTreeIterator.cpp @@ -4,6 +4,7 @@ * under the terms of the license (GNU LGPL) which comes with this package. */ #include "src/mc/explo/odpor/WakeupTreeIterator.hpp" +#include "src/mc/explo/odpor/WakeupTree.hpp" namespace simgrid::mc::odpor { diff --git a/src/mc/explo/odpor/WakeupTreeIterator.hpp b/src/mc/explo/odpor/WakeupTreeIterator.hpp index 2aae9b5107..9254829867 100644 --- a/src/mc/explo/odpor/WakeupTreeIterator.hpp +++ b/src/mc/explo/odpor/WakeupTreeIterator.hpp @@ -6,7 +6,7 @@ #ifndef SIMGRID_MC_ODPOR_WAKEUP_TREE_ITERATOR_HPP #define SIMGRID_MC_ODPOR_WAKEUP_TREE_ITERATOR_HPP -#include "src/mc/explo/odpor/WakeupTree.hpp" +#include "src/mc/explo/odpor/odpor_forward.hpp" #include #include @@ -15,13 +15,13 @@ namespace simgrid::mc::odpor { struct WakeupTreeIterator - : public boost::iterator_facade { + : public boost::iterator_facade { public: WakeupTreeIterator() = default; explicit WakeupTreeIterator(const WakeupTree& tree); private: - using node_handle = std::list::iterator; + using node_handle = std::list::iterator; /** * @brief The current "view" of the iteration in post-order traversal @@ -36,7 +36,7 @@ private: // boost::iterator_facade<...> interface to implement void increment(); bool equal(const WakeupTreeIterator& other) const { return post_order_iteration == other.post_order_iteration; } - const WakeupTreeNode*& dereference() const { return *post_order_iteration.top(); } + WakeupTreeNode*& dereference() const { return *post_order_iteration.top(); } // Allows boost::iterator_facade<...> to function properly friend class boost::iterator_core_access; diff --git a/src/mc/explo/odpor/odpor_forward.hpp b/src/mc/explo/odpor/odpor_forward.hpp index dc1e4bd2a0..33366e1251 100644 --- a/src/mc/explo/odpor/odpor_forward.hpp +++ b/src/mc/explo/odpor/odpor_forward.hpp @@ -23,6 +23,7 @@ using ExecutionSequence = std::list; class Event; class Execution; class WakeupTree; +class WakeupTreeNode; class WakeupTreeIterator; } // namespace simgrid::mc::odpor -- 2.20.1