From 714db2034b160bdacbbacd76693209ec412463d8 Mon Sep 17 00:00:00 2001 From: Maxwell Pirtle Date: Wed, 10 May 2023 11:38:07 +0200 Subject: [PATCH] Add complicated computation of v ~_E w to Execution The relation `v ~_E w` is used when traversing a WakeupTree to determine is an "equivalent" execution is already noted in the tree. This commit adds the first "working" implementation of several components to this process, viz. 1. Assuming that iteration has been implemented (which is to come in future commits), the WakeupTree now implements the `insert_E(v, B)` operation, where `B` refers to the tree instance itself. 2. The `Execution` class can now determine what is needed to complete the `insert()` operation, specifically determining first if a) two sequences `v` and `w` are related by `v ~_E w` and b) what the smallest sequence `w'` is such that `w [= v.w'`. The latter computation uses the neat observation that (w / v) is the smallest such sequence (viz. removing anything in `w` that's in `v` "one at a time") and computes this value as it is in the process of determining whether the `~_E` relation noted holds --- src/mc/explo/odpor/Execution.cpp | 123 +++++++++++++++++++++++++-- src/mc/explo/odpor/Execution.hpp | 7 +- src/mc/explo/odpor/WakeupTree.cpp | 4 +- src/mc/explo/odpor/WakeupTree.hpp | 11 +-- src/mc/explo/odpor/odpor_forward.hpp | 3 +- 5 files changed, 129 insertions(+), 19 deletions(-) diff --git a/src/mc/explo/odpor/Execution.cpp b/src/mc/explo/odpor/Execution.cpp index 3d2832dc03..c8df4d87e1 100644 --- a/src/mc/explo/odpor/Execution.cpp +++ b/src/mc/explo/odpor/Execution.cpp @@ -4,8 +4,10 @@ * under the terms of the license (GNU LGPL) which comes with this package. */ #include "src/mc/explo/odpor/Execution.hpp" -#include +#include "xbt/asserts.h" +#include #include +#include namespace simgrid::mc::odpor { @@ -95,11 +97,6 @@ std::optional Execution::get_first_sdpor_initial_from(EventHandle e, // could happen-before `v` for any valid happens-before relation. // First, grab `E' := pre(e, E)` and determine what actor `p` is - // TODO: Instead of copying around these big structs, it - // would behoove us to incorporate some way to reference - // portions of an execution. For simplicity and for a - // "proof of concept" version, we opt to simply copy - // the contents instead of making a view into the execution const auto next_E_p = get_latest_event_handle().value(); Execution E_prime_v = get_prefix_up_to(e); std::vector v; @@ -149,10 +146,118 @@ 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 +bool Execution::is_initial_after_execution(const PartialExecution& w, aid_t p) const { - return std::nullopt; + auto E_w = *this; + std::vector w_handles; + for (const auto& w_i : w) { + // Take one step in the direction of `w` + E_w.push_transition(w_i.get()); + + // If that step happened to be executed by `p`, + // great: we know that `p` is contained in `w`. + // We now need to verify that it doens't "happen-after" + // any events which occur before it + if (w_i->aid_ == p) { + const auto p_handle = E_w.get_latest_event_handle().value(); + return std::none_of(w_handles.begin(), w_handles.end(), + [&](const auto handle) { return E_w.happens_before(handle, p_handle); }); + } else { + w_handles.push_back(E_w.get_latest_event_handle().value()); + } + } + return false; +} + +bool Execution::is_independent_with_execution(const PartialExecution& w, const Transition* next_E_p) const +{ + // INVARIANT: Here, we assume that for any process `p_i` of `w`, + // the events of this execution followed by the execution of all + // actors occurring before `p_i` in `v` (`p_j`, `0 <= j < i`) + // are sufficient to enable `p_i`. This is fortunately the case + // with what ODPOR requires of us, viz. to ask the question about + // `v := notdep(e, E)` for some execution `E` and event `e` of + // that execution. + auto E_p_w = *this; + E_p_w.push_transition(next_E_p); + const auto p_handle = E_p_w.get_latest_event_handle().value(); + + // As we add events to `w`, verify that none + // of them "happen-after" the event associated with + // the step `next_E_p` (viz. p_handle) + for (const auto& w_i : w) { + E_p_w.push_transition(w_i.get()); + const auto w_i_handle = E_p_w.get_latest_event_handle().value(); + if (E_p_w.happens_before(p_handle, w_i_handle)) { + return false; + } + } + return true; +} + +std::optional Execution::get_shortest_odpor_sq_subset_insertion(const PartialExecution& v, + const PartialExecution& w) const +{ + // See section 4 of Abdulla. et al.'s 2017 ODPOR paper for details (specifically + // where the [iterative] computation of `v ~_[E] w` is described) + auto E_v = *this; + auto w_now = w; + + for (const auto& next_p_E : v) { + const aid_t p = next_p_E->aid_; + + // Is `p in `I_[E](w)`? + if (E_v.is_initial_after_execution(w_now, p)) { + // Remove `p` from w and continue + + // TODO: If `p` occurs in `w`, it had better refer to the same + // transition referenced by `v`. Unfortunately, we have two + // sources of truth here which can be manipulated at the same + // time as arguments to the function. If ODPOR works correctly, + // they should always refer to the same value; but as a sanity check, + // we have an assert that tests that at least the types are the same. + const auto action_by_p_in_w = + std::find_if(w_now.begin(), w_now.end(), [=](const auto& action) { return action->aid_ == p; }); + xbt_assert(action_by_p_in_w != w_now.end(), "Invariant violated: actor `p` " + "is claimed to be an initial after `w` but is " + "not actually contained in `w`. This indicates that there " + "is a bug computing initials"); + const auto& w_action = *action_by_p_in_w; + xbt_assert(w_action->type_ == next_p_E->type_, + "Invariant violated: `v` claims that actor `%ld` executes '%s' while " + "`w` claims that it executes '%s'. These two partial executions both " + "refer to `next_[E](p)`, which should be the same", + p, next_p_E->to_string(false).c_str(), w_action->to_string(false).c_str()); + w_now.erase(action_by_p_in_w); + } + // Is `E ⊢ p ◇ w`? + else if (E_v.is_independent_with_execution(w, next_p_E.get())) { + // INVARIANT: Note that it is impossible for `p` to be + // excluded from the set `I_[E](w)` BUT ALSO be contained in + // `w` itself if `E ⊢ p ◇ w`. We assert this is the case here + const auto action_by_p_in_w = + std::find_if(w_now.begin(), w_now.end(), [=](const auto& action) { return action->aid_ == p; }); + xbt_assert(action_by_p_in_w == w_now.end(), + "Invariant violated: We claimed that actor `%ld` is not an initial " + "after `w`, yet it's independent with all actions of `w` AND occurs in `w`." + "This indicates that there is a bug computing initials", + p); + } else { + // Neither of the two above conditions hold, so the relation fails + return std::nullopt; + } + + // Move one step forward in the direction of `v` and repeat + E_v.push_transition(next_p_E.get()); + } + + // Construct, finally, v.w' by adding `v` to the front of + // what remains of `w` after removing `v` as above + for (auto it = v.rbegin(); it != v.rend(); ++it) { + w_now.push_front(*it); + } + + return std::optional{std::move(w_now)}; } bool Execution::happens_before(Execution::EventHandle e1_handle, Execution::EventHandle e2_handle) const diff --git a/src/mc/explo/odpor/Execution.hpp b/src/mc/explo/odpor/Execution.hpp index 58b28c291a..13571d6c83 100644 --- a/src/mc/explo/odpor/Execution.hpp +++ b/src/mc/explo/odpor/Execution.hpp @@ -144,13 +144,16 @@ public: */ std::optional get_first_sdpor_initial_from(EventHandle e, std::unordered_set backtrack_set) const; + bool is_initial_after_execution(const PartialExecution& w, aid_t p) const; + bool is_independent_with_execution(const PartialExecution& w, const Transition* next_E_p) 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; + std::optional get_shortest_odpor_sq_subset_insertion(const PartialExecution& v, + const PartialExecution& 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 93cab13a8a..0365208c42 100644 --- a/src/mc/explo/odpor/WakeupTree.cpp +++ b/src/mc/explo/odpor/WakeupTree.cpp @@ -12,7 +12,7 @@ namespace simgrid::mc::odpor { WakeupTree::WakeupTree() : root(nullptr) {} -WakeupTreeNode* WakeupTree::make_node(const ProcessSequence& u) +WakeupTreeNode* WakeupTree::make_node(const PartialExecution& u) { auto node = std::unique_ptr(new WakeupTreeNode(u)); auto* node_handle = node.get(); @@ -20,7 +20,7 @@ WakeupTreeNode* WakeupTree::make_node(const ProcessSequence& u) return node_handle; } -void WakeupTree::insert(const Execution& E, const ExecutionSequence& w) +void WakeupTree::insert(const Execution& E, const PartialExecution& w) { // See section 6.2 of Abdulla. et al.'s 2017 ODPOR paper for details diff --git a/src/mc/explo/odpor/WakeupTree.hpp b/src/mc/explo/odpor/WakeupTree.hpp index 552e582afc..56b3988c15 100644 --- a/src/mc/explo/odpor/WakeupTree.hpp +++ b/src/mc/explo/odpor/WakeupTree.hpp @@ -16,13 +16,14 @@ namespace simgrid::mc::odpor { class WakeupTreeNode { private: - explicit WakeupTreeNode(const ProcessSequence& u) : seq_(u) {} + explicit WakeupTreeNode(const PartialExecution& u) : seq_(u) {} + explicit WakeupTreeNode(PartialExecution&& u) : seq_(std::move(u)) {} /** An ordered list of children of for this node in the tree */ std::list children_; /** @brief The contents of the node */ - ProcessSequence seq_; + PartialExecution seq_; /** Allows the owning tree to insert directly into the child */ friend WakeupTree; @@ -33,7 +34,7 @@ public: const auto rbegin() const { return this->children_.rbegin(); } const auto rend() const { return this->children_.rend(); } - const ProcessSequence& get_sequence() const { return seq_; } + const PartialExecution& get_sequence() const { return seq_; } const std::list& get_ordered_children() const { return children_; } bool is_leaf() const { return children_.empty(); } @@ -60,7 +61,7 @@ private: /** * @brief Creates a new, disconnected node in this tree */ - WakeupTreeNode* make_node(const ProcessSequence& u); + WakeupTreeNode* make_node(const PartialExecution& u); /* Allow the iterator to access the contents of the tree */ friend WakeupTreeIterator; @@ -77,7 +78,7 @@ public: * such that that this tree is a wakeup tree relative to the * given execution */ - void insert(const Execution&, const ExecutionSequence& seq); + void insert(const Execution&, const PartialExecution& seq); }; } // namespace simgrid::mc::odpor diff --git a/src/mc/explo/odpor/odpor_forward.hpp b/src/mc/explo/odpor/odpor_forward.hpp index 33366e1251..11161c640a 100644 --- a/src/mc/explo/odpor/odpor_forward.hpp +++ b/src/mc/explo/odpor/odpor_forward.hpp @@ -13,11 +13,12 @@ #include "src/mc/mc_forward.hpp" #include +#include #include namespace simgrid::mc::odpor { -using ProcessSequence = std::list; +using PartialExecution = std::list>; using ExecutionSequence = std::list; class Event; -- 2.20.1