From 86a552c797938ffe6db296e12b7043c3c7fdf14f Mon Sep 17 00:00:00 2001 From: Maxwell Pirtle Date: Wed, 3 May 2023 11:35:01 +0200 Subject: [PATCH] Move SDPOR core computation into a method The core component of SDPOR involves selecting an "initial" for a hypothetical computation extending from a prefix of the current execution that results in the reversal of the reversible race SDPOR detected. This comomit moves that computation as much as possible into the `Execution` class itself to make the SDPOR implementation easier to read --- src/mc/api/State.cpp | 4 +- src/mc/api/State.hpp | 15 ++++- src/mc/explo/DFSExplorer.cpp | 91 +++++++++---------------- src/mc/explo/odpor/Execution.cpp | 112 ++++++++++++++++++++++--------- src/mc/explo/odpor/Execution.hpp | 27 ++++---- 5 files changed, 143 insertions(+), 106 deletions(-) diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp index aa315cf17e..8430f525b6 100644 --- a/src/mc/api/State.cpp +++ b/src/mc/api/State.cpp @@ -162,11 +162,11 @@ std::shared_ptr State::execute_next(aid_t next, RemoteApp& app) return outgoing_transition_; } -std::unordered_set State::get_todo_actors() const +std::unordered_set State::get_backtrack_set() const { std::unordered_set actors; for (const auto& [aid, state] : get_actors_list()) { - if (state.is_todo()) { + if (state.is_todo() or state.is_done()) { actors.insert(aid); } } diff --git a/src/mc/api/State.hpp b/src/mc/api/State.hpp index 6e963ca276..fbacda384d 100644 --- a/src/mc/api/State.hpp +++ b/src/mc/api/State.hpp @@ -86,7 +86,20 @@ public: Snapshot* get_system_state() const { return system_state_.get(); } void set_system_state(std::shared_ptr state) { system_state_ = std::move(state); } - std::unordered_set get_todo_actors() const; + /** + * @brief Computes the backtrack set for this state + * according to its definition in Simgrid. + * + * The backtrack set as it appears in DPOR, SDPOR, and ODPOR + * 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 + * 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. + */ + std::unordered_set get_backtrack_set() const; std::map const& get_sleep_set() const { return sleep_set_; } void add_sleep_set(std::shared_ptr t) { diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp index c52b0fec1c..3f44ee29bf 100644 --- a/src/mc/explo/DFSExplorer.cpp +++ b/src/mc/explo/DFSExplorer.cpp @@ -94,7 +94,11 @@ 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_ = execution_seq_.get_prefix_up_to(stack_.size()); + if (stack_.empty()) { + execution_seq_ = sdpor::Execution(); + } else { + execution_seq_ = execution_seq_.get_prefix_up_to(stack_.size() - 1); + } XBT_DEBUG("Additionally replaced corresponding SDPOR execution stack"); } } @@ -239,19 +243,15 @@ void DFSExplorer::run() } else if (reduction_mode_ == ReductionMode::sdpor) { /** * SDPOR Source Set Procedure: + * + * Find "reversible races" in the current execution with respect + * to the latest action `p`. For each such race, determine one thread + * not contained in the backtrack set at the "race point" `r` which + * "represents" the trace formed by first executing everything after + * `r` and then `p` to flip the race */ execution_seq_.push_transition(executed_transition.get()); - // To determine if the race is reversible, we have to ensure - // that actor `p` running `next_E_p` (viz. the event such that - // `racing_event -> (E_p) next_E_p` and no other event - // "happens-between" the two) is enabled in any equivalent - // execution where `racing_event` happens before `next_E_p`. - // - // Importantly, it is equivalent to checking if in ANY - // such equivalent execution sequence where `racing_event` - // happens-before `next_E_p` that `p` is enabled in `pre(racing_event, E.p)`. - // Thus it suffices to check THIS execution xbt_assert(execution_seq_.get_latest_event_handle().has_value(), "No events are contained in the SDPOR/OPDPOR execution " "even though one was just added"); @@ -259,57 +259,28 @@ void DFSExplorer::run() const auto next_E_p = execution_seq_.get_latest_event_handle().value(); for (const auto racing_event_handle : execution_seq_.get_racing_events_of(next_E_p)) { + // To determine if the race is reversible, we have to ensure + // that actor `p` running `next_E_p` (viz. the event such that + // `racing_event -> (E_p) next_E_p` and no other event + // "happens-between" the two) is enabled in any equivalent + // execution where `racing_event` happens before `next_E_p`. + // + // Importantly, it is equivalent to checking if in ANY + // such equivalent execution sequence where `racing_event` + // happens-before `next_E_p` that `p` is enabled in `pre(racing_event, E.p)`. + // Thus it suffices to check THIS execution + // // If the actor `p` is not enabled at s_[E'], it is not a *reversible* race const std::shared_ptr prev_state = stack_[racing_event_handle]; - if (not prev_state->is_actor_enabled(p)) { - continue; - } - - // This is a reversible race! First, grab `E' := pre(e, E)` - // 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 - sdpor::Execution E_prime_v = execution_seq_.get_prefix_up_to(racing_event_handle); - - // The vector `v` is constructed as `v := notdep(e, E) - std::vector v; - std::unordered_set disqualified_actors = state->get_todo_actors(); - - for (auto e_prime = racing_event_handle; e_prime <= next_E_p; ++e_prime) { - // Any event `e` which occurs after `racing_event_handle` but which does not - // happen after `racing_event_handle` is a member of `v`. - // In addition to marking the event in `v`, we also "simulate" running - // the action `v` from E'. - if (not execution_seq_.happens_before(racing_event_handle, e_prime) or e_prime == next_E_p) { - v.push_back(e_prime); - E_prime_v.push_transition(execution_seq_.get_event_with_handle(e_prime).get_transition()); - } else { - continue; - } - - xbt_assert(E_prime_v.get_latest_event_handle().has_value(), - "No events are contained in the SDPOR/OPDPOR execution " - "even though one was just added"); - const sdpor::Execution::EventHandle e_prime_in_E_prime = E_prime_v.get_latest_event_handle().value(); - - const aid_t q = E_prime_v.get_actor_with_handle(e_prime_in_E_prime); - if (disqualified_actors.count(q) > 0) { - continue; - } - - const bool is_initial = std::none_of(v.begin(), v.end(), [&](const auto& e_star) { - return E_prime_v.happens_before(e_star, e_prime_in_E_prime); - }); - if (is_initial) { - if (not prev_state->is_actor_done(q)) { - prev_state->consider_one(q); - opened_states_.emplace_back(std::move(prev_state)); - } - break; - } else { - disqualified_actors.insert(q); + if (prev_state->is_actor_enabled(p)) { + // NOTE: To incorporate the idea of attempting to select the "best" + // backtrack point into SDPOR, instead of selecting the `first` initial, + // we should instead compute all choices and decide which is bes + const std::optional q = + execution_seq_.get_first_ssdpor_initial_from(racing_event_handle, prev_state->get_backtrack_set()); + if (q.has_value()) { + prev_state->consider_one(q.value()); + opened_states_.emplace_back(std::move(prev_state)); } } } diff --git a/src/mc/explo/odpor/Execution.cpp b/src/mc/explo/odpor/Execution.cpp index cc722f0a79..1bc01d82fe 100644 --- a/src/mc/explo/odpor/Execution.cpp +++ b/src/mc/explo/odpor/Execution.cpp @@ -9,6 +9,29 @@ namespace simgrid::mc::odpor { +void Execution::push_transition(const Transition* t) +{ + if (t == nullptr) { + throw std::invalid_argument("Unexpectedly received `nullptr`"); + } + ClockVector max_clock_vector; + for (const Event& e : this->contents_) { + if (e.get_transition()->depends(t)) { + max_clock_vector = ClockVector::max(max_clock_vector, e.get_clock_vector()); + } + } + // The entry in the vector for `t->aid_` is the size + // of the new stack, which will have a size one greater + // than that before we insert the new events + max_clock_vector[t->aid_] = this->size() + 1; + contents_.push_back(Event({t, max_clock_vector})); +} + +void Execution::pop_latest() +{ + contents_.pop_back(); +} + std::unordered_set Execution::get_racing_events_of(Execution::EventHandle target) const { std::unordered_set racing_events; @@ -54,6 +77,64 @@ std::unordered_set Execution::get_racing_events_of(Execu return racing_events; } +Execution Execution::get_prefix_up_to(Execution::EventHandle handle) const +{ + return Execution(std::vector{contents_.begin(), contents_.begin() + handle}); +} + +std::optional Execution::get_first_ssdpor_initial_from(EventHandle e, + std::unordered_set disqualified_actors) const +{ + // If this execution is empty, there are no initials + // relative to the last transition added to the execution + // since such a transition does not exist + if (empty()) { + return std::nullopt; + } + + // 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; + + for (auto e_prime = e; e_prime <= next_E_p; ++e_prime) { + // Any event `e*` which occurs after `e` but which does not + // happen after `e` is a member of `v`. In addition to marking + // the event in `v`, we also "simulate" running the action `v` + // from E' + if (not happens_before(e, e_prime) or e_prime == next_E_p) { + v.push_back(e_prime); + E_prime_v.push_transition(get_event_with_handle(e_prime).get_transition()); + } else { + continue; + } + const EventHandle e_prime_in_E_prime = E_prime_v.get_latest_event_handle().value(); + const aid_t q = E_prime_v.get_actor_with_handle(e_prime_in_E_prime); + if (disqualified_actors.count(q) > 0) { + continue; + } + const bool is_initial = std::none_of( + v.begin(), v.end(), [&](const auto& e_star) { return E_prime_v.happens_before(e_star, e_prime_in_E_prime); }); + if (is_initial) { + return q; + } else { + disqualified_actors.insert(q); + } + } + return std::nullopt; +} + +std::unordered_set Execution::get_ssdpor_initials_from(EventHandle e, + std::unordered_set disqualified) const +{ + return std::unordered_set(); +} + bool Execution::happens_before(Execution::EventHandle e1_handle, Execution::EventHandle e2_handle) const { // 1. "happens-before" is a subset of "occurs before" @@ -68,35 +149,4 @@ bool Execution::happens_before(Execution::EventHandle e1_handle, Execution::Even return e1_handle <= e2.get_clock_vector().get(proc_e1).value_or(0); } -Execution Execution::get_prefix_up_to(Execution::EventHandle handle) -{ - if (handle == static_cast(0)) { - return Execution(); - } - return Execution(std::vector{contents_.begin(), contents_.begin() + (handle - 1)}); -} - -void Execution::push_transition(const Transition* t) -{ - if (t == nullptr) { - throw std::invalid_argument("Unexpectedly received `nullptr`"); - } - ClockVector max_clock_vector; - for (const Event& e : this->contents_) { - if (e.get_transition()->depends(t)) { - max_clock_vector = ClockVector::max(max_clock_vector, e.get_clock_vector()); - } - } - // The entry in the vector for `t->aid_` is the size - // of the new stack, which will have a size one greater - // than that before we insert the new events - max_clock_vector[t->aid_] = this->size() + 1; - contents_.push_back(Event({t, max_clock_vector})); -} - -void Execution::pop_latest() -{ - contents_.pop_back(); -} - } // namespace simgrid::mc::odpor \ No newline at end of file diff --git a/src/mc/explo/odpor/Execution.hpp b/src/mc/explo/odpor/Execution.hpp index 4a5c2c50e2..672788edf6 100644 --- a/src/mc/explo/odpor/Execution.hpp +++ b/src/mc/explo/odpor/Execution.hpp @@ -89,15 +89,23 @@ public: Execution(const Execution&) = default; Execution& operator=(Execution const&) = default; Execution(Execution&&) = default; + Execution(ExecutionSequence&& seq); + Execution(const ExecutionSequence& seq); - Execution(ExecutionSequence&& seq, std::optional base = {}); - Execution(const ExecutionSequence& seq, std::optional base = {}); + size_t size() const { return this->contents_.size(); } + bool empty() const { return this->contents_.empty(); } + + std::optional get_first_ssdpor_initial_from(EventHandle e, std::unordered_set disqualified) const; + std::unordered_set get_ssdpor_initials_from(EventHandle e, std::unordered_set disqualified) const; - std::unordered_set get_initials_after(const Hypothetical& w) const; - std::unordered_set get_weak_initials_after(const Hypothetical& w) const; + // std::unordered_set get_initials_after(const Hypothetical& w) const; + // std::unordered_set get_weak_initials_after(const Hypothetical& w) const; - bool is_initial(aid_t p, const Hypothetical& w) const; - bool is_weak_initial(aid_t p, const Hypothetical& w) const; + // std::unordered_set get_initials_after(const Hypothetical& w) const; + // std::unordered_set get_weak_initials_after(const Hypothetical& w) const; + + // bool is_initial(aid_t p, const Hypothetical& w) const; + // bool is_weak_initial(aid_t p, const Hypothetical& w) const; const Event& get_event_with_handle(EventHandle handle) const { return contents_[handle]; } aid_t get_actor_with_handle(EventHandle handle) const { return get_event_with_handle(handle).get_transition()->aid_; } @@ -118,7 +126,7 @@ public: return contents_.empty() ? std::nullopt : std::optional{static_cast(size() - 1)}; } - Execution get_prefix_up_to(EventHandle); + Execution get_prefix_up_to(EventHandle) const; /** * @brief Whether the event represented by `e1` @@ -159,11 +167,6 @@ public: * actor which executed transition `t`. */ void push_transition(const Transition*); - - /** - * @brief The total number of steps contained in the execution - */ - size_t size() const { return this->contents_.size(); } }; } // namespace simgrid::mc::odpor -- 2.20.1