From 623108a0b5b82da1c8d27a6b4c897961d352b8de Mon Sep 17 00:00:00 2001 From: Maxwell Pirtle Date: Tue, 9 May 2023 16:34:04 +0200 Subject: [PATCH] Add WakeupTreeIterator and WakeupTree skeletons --- MANIFEST.in | 2 + src/mc/explo/odpor/Execution.hpp | 9 ++-- src/mc/explo/odpor/WakeupTree.cpp | 21 ++++++++ src/mc/explo/odpor/WakeupTree.hpp | 66 +++++++++++++++++++++++ src/mc/explo/odpor/WakeupTreeIterator.cpp | 65 ++++++++++++++++++++++ src/mc/explo/odpor/WakeupTreeIterator.hpp | 46 ++++++++++++++++ src/mc/explo/odpor/odpor_forward.hpp | 6 ++- tools/cmake/DefinePackages.cmake | 2 + 8 files changed, 210 insertions(+), 7 deletions(-) create mode 100644 src/mc/explo/odpor/WakeupTreeIterator.cpp create mode 100644 src/mc/explo/odpor/WakeupTreeIterator.hpp diff --git a/MANIFEST.in b/MANIFEST.in index ec8c8d1b1a..02e695c03d 100644 --- a/MANIFEST.in +++ b/MANIFEST.in @@ -2197,6 +2197,8 @@ include src/mc/explo/odpor/Execution.hpp include src/mc/explo/odpor/Execution_test.cpp include src/mc/explo/odpor/WakeupTree.cpp include src/mc/explo/odpor/WakeupTree.hpp +include src/mc/explo/odpor/WakeupTreeIterator.cpp +include src/mc/explo/odpor/WakeupTreeIterator.hpp include src/mc/explo/odpor/odpor_forward.hpp include src/mc/explo/simgrid_mc.cpp include src/mc/explo/udpor/Comb.hpp diff --git a/src/mc/explo/odpor/Execution.hpp b/src/mc/explo/odpor/Execution.hpp index dca1c5df74..f851cf47f7 100644 --- a/src/mc/explo/odpor/Execution.hpp +++ b/src/mc/explo/odpor/Execution.hpp @@ -17,10 +17,6 @@ namespace simgrid::mc::odpor { -using ProcessSequence = std::list; -using ExecutionSequence = std::list; -using Hypothetical = ExecutionSequence; - /** * @brief The occurrence of a transition in an execution * @@ -100,8 +96,6 @@ public: Execution(const Execution&) = default; Execution& operator=(Execution const&) = default; Execution(Execution&&) = default; - Execution(ExecutionSequence&& seq); - Execution(const ExecutionSequence& seq); size_t size() const { return this->contents_.size(); } bool empty() const { return this->contents_.empty(); } @@ -150,6 +144,9 @@ 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 Determines the event associated with * the given handle `handle` diff --git a/src/mc/explo/odpor/WakeupTree.cpp b/src/mc/explo/odpor/WakeupTree.cpp index e69de29bb2..bbe6b698c1 100644 --- a/src/mc/explo/odpor/WakeupTree.cpp +++ b/src/mc/explo/odpor/WakeupTree.cpp @@ -0,0 +1,21 @@ +/* Copyright (c) 2008-2023. The SimGrid Team. All rights reserved. */ + +/* This program is free software; you can redistribute it and/or modify it + * under the terms of the license (GNU LGPL) which comes with this package. */ + +#include "src/mc/explo/odpor/WakeupTree.hpp" +#include "src/mc/explo/odpor/Execution.hpp" + +#include + +namespace simgrid::mc::odpor { + +WakeupTree::WakeupTree() : root(nullptr) {} + +void WakeupTree::insert(const Execution& E, const ExecutionSequence& w) +{ + // Find the first node `v` in the tree such that + // `v ~_[E] w` +} + +} // 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 e69de29bb2..81356cd4cf 100644 --- a/src/mc/explo/odpor/WakeupTree.hpp +++ b/src/mc/explo/odpor/WakeupTree.hpp @@ -0,0 +1,66 @@ +/* Copyright (c) 2007-2023. The SimGrid Team. All rights reserved. */ + +/* This program is free software; you can redistribute it and/or modify it + * under the terms of the license (GNU LGPL) which comes with this package. */ + +#ifndef SIMGRID_MC_ODPOR_WAKEUP_TREE_HPP +#define SIMGRID_MC_ODPOR_WAKEUP_TREE_HPP + +#include "src/mc/explo/odpor/odpor_forward.hpp" + +#include +#include + +namespace simgrid::mc::odpor { + +class WakeupTreeNode { +private: + /** An ordered list of children of for this node in the tree */ + std::list children_; + + /** @brief The contents of the node */ + ProcessSequence seq_; + +public: + const auto begin() const { return this->children_.begin(); } + const auto end() const { return this->children_.end(); } + const auto rbegin() const { return this->children_.rbegin(); } + const auto rend() const { return this->children_.rend(); } + + const ProcessSequence& get_sequence() const { return seq_; } + const std::list& get_ordered_children() const { return children_; } + + bool is_leaf() const { return children_.empty(); } +}; + +class WakeupTree { +private: + /** @brief The root node of the tree */ + const WakeupTreeNode* const root; + + /** + * @brief All of the nodes that are currently are a part of the tree + * + * @invariant Each node event maps itself to the owner of that node, + * i.e. the unique pointer that manages the data at the address. The tree owns all + * 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_; + + /* Allow the iterator to access the contents of the tree */ + friend WakeupTreeIterator; + +public: + WakeupTree(); + + /** + * @brief Inserts an sequence `seq` of processes into the tree + * such that that this tree is a wakeup tree relative to the + * given execution + */ + void insert(const Execution&, const ExecutionSequence& seq); +}; + +} // namespace simgrid::mc::odpor +#endif diff --git a/src/mc/explo/odpor/WakeupTreeIterator.cpp b/src/mc/explo/odpor/WakeupTreeIterator.cpp new file mode 100644 index 0000000000..684a63304a --- /dev/null +++ b/src/mc/explo/odpor/WakeupTreeIterator.cpp @@ -0,0 +1,65 @@ +/* Copyright (c) 2008-2023. The SimGrid Team. All rights reserved. */ + +/* This program is free software; you can redistribute it and/or modify it + * under the terms of the license (GNU LGPL) which comes with this package. */ + +#include "src/mc/explo/odpor/WakeupTreeIterator.hpp" + +namespace simgrid::mc::odpor { + +WakeupTreeIterator::WakeupTreeIterator(const WakeupTree& tree) +{ + // post_order_iteration.push(tree.root); + push_until_left_most_found(); +} + +void WakeupTreeIterator::push_until_left_most_found() +{ + // INVARIANT: Since we are traversing over a tree, + // there are no cycles. This means that at least + // 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()) { + // INVARIANT: Since we push children in + // reverse order (right-most to left-most), + // we ensure that we'll always process left-most + // children first + } +} + +void WakeupTreeIterator::increment() +{ + // If there are no nodes in the stack, we've + // completed the traversal: there's nothing left + // to do + if (post_order_iteration.empty()) { + return; + } + + auto prev_top_handle = post_order_iteration.top(); + post_order_iteration.pop(); + + // If there are now no longer any nodes left, + // we know that `prev_top` must be the original + // root; that is, we were *just* pointing at the + // original root, so we're done + if (post_order_iteration.empty()) { + return; + } + + // Otherwise, look at the next top node. If + // `prev_top` is that node's right-most child, + // then we don't attempt to re-add `next_top`'s + // children again for we would have already seen them + const auto* next_top_node = *post_order_iteration.top(); + + // To actually determine "right-most", we check if + // moving over to the right one spot brings us to the + // end of the candidate parent's list + if ((++prev_top_handle) != next_top_node->get_ordered_children().end()) { + push_until_left_most_found(); + } +} + +} // namespace simgrid::mc::odpor \ No newline at end of file diff --git a/src/mc/explo/odpor/WakeupTreeIterator.hpp b/src/mc/explo/odpor/WakeupTreeIterator.hpp new file mode 100644 index 0000000000..2aae9b5107 --- /dev/null +++ b/src/mc/explo/odpor/WakeupTreeIterator.hpp @@ -0,0 +1,46 @@ +/* Copyright (c) 2007-2023. The SimGrid Team. All rights reserved. */ + +/* This program is free software; you can redistribute it and/or modify it + * under the terms of the license (GNU LGPL) which comes with this package. */ + +#ifndef SIMGRID_MC_ODPOR_WAKEUP_TREE_ITERATOR_HPP +#define SIMGRID_MC_ODPOR_WAKEUP_TREE_ITERATOR_HPP + +#include "src/mc/explo/odpor/WakeupTree.hpp" + +#include +#include +#include + +namespace simgrid::mc::odpor { + +struct WakeupTreeIterator + : public boost::iterator_facade { +public: + WakeupTreeIterator() = default; + explicit WakeupTreeIterator(const WakeupTree& tree); + +private: + using node_handle = std::list::iterator; + + /** + * @brief The current "view" of the iteration in post-order traversal + */ + std::stack post_order_iteration; + + /** + * + */ + void push_until_left_most_found(); + + // 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(); } + + // Allows boost::iterator_facade<...> to function properly + friend class boost::iterator_core_access; +}; + +} // namespace simgrid::mc::odpor +#endif diff --git a/src/mc/explo/odpor/odpor_forward.hpp b/src/mc/explo/odpor/odpor_forward.hpp index 1a439c1855..dc1e4bd2a0 100644 --- a/src/mc/explo/odpor/odpor_forward.hpp +++ b/src/mc/explo/odpor/odpor_forward.hpp @@ -12,14 +12,18 @@ #define SIMGRID_MC_ODPOR_FORWARD_HPP #include "src/mc/mc_forward.hpp" +#include #include namespace simgrid::mc::odpor { +using ProcessSequence = std::list; +using ExecutionSequence = std::list; + class Event; class Execution; -class ExecutionView; class WakeupTree; +class WakeupTreeIterator; } // namespace simgrid::mc::odpor diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake index 95e2a37f9b..c395235315 100644 --- a/tools/cmake/DefinePackages.cmake +++ b/tools/cmake/DefinePackages.cmake @@ -539,6 +539,8 @@ set(MC_SRC_STATELESS src/mc/explo/odpor/Execution.hpp src/mc/explo/odpor/WakeupTree.cpp src/mc/explo/odpor/WakeupTree.hpp + src/mc/explo/odpor/WakeupTreeIterator.cpp + src/mc/explo/odpor/WakeupTreeIterator.hpp src/mc/explo/odpor/odpor_forward.hpp src/mc/remote/AppSide.cpp -- 2.20.1