From 7fd6faa16a89c1019a9fe562be79942add51842e Mon Sep 17 00:00:00 2001 From: Maxwell Pirtle Date: Fri, 12 May 2023 09:55:10 +0200 Subject: [PATCH] Add ODPOR race detection phase rough-draft ODPOR is decoposed into two parts: the "passive" observer phase, where ODPOR selects search points based on the work it did before to fill in its wakeup trees, and the active race-detection phase, where ODPOR looks at all reversible races in an execution and performs the work to determine if new traces need be searched. This commit adds in an outline for the latter phase. Note that there is still much work to be done with respect to the race detection -- we still need to implement the partial execution function for example. Likewise, handling the issue of multiple execution possibilities for a given process will be particularly tricky. --- src/mc/api/State.cpp | 25 ++++++++++++++++++ src/mc/api/State.hpp | 7 +++++ src/mc/explo/DFSExplorer.cpp | 45 +++++++++++++++++++++++++++++--- src/mc/explo/odpor/Execution.cpp | 12 +++++++-- src/mc/explo/odpor/Execution.hpp | 38 ++++++++++++++------------- 5 files changed, 104 insertions(+), 23 deletions(-) diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp index 3a1a0ac47d..54d71cfee3 100644 --- a/src/mc/api/State.cpp +++ b/src/mc/api/State.cpp @@ -188,6 +188,26 @@ std::unordered_set State::get_backtrack_set() const return actors; } +std::unordered_set State::get_sleeping_set() const +{ + std::unordered_set actors; + for (const auto& [aid, _] : get_sleep_set()) { + actors.insert(aid); + } + return actors; +} + +std::unordered_set State::get_enabled_actors() const +{ + std::unordered_set actors; + for (const auto& [aid, state] : get_actors_list()) { + if (state.is_enabled()) { + actors.insert(aid); + } + } + return actors; +} + void State::seed_wakeup_tree_if_needed(const odpor::Execution& prior) { // TODO: It would be better not to have such a flag. @@ -236,4 +256,9 @@ void State::remove_subtree_starting_with(aid_t p) this->wakeup_tree_.remove_subtree_rooted_at(*branch); } +void State::mark_path_interesting_for_odpor(const odpor::PartialExecution& pe, const odpor::Execution& E) +{ + this->wakeup_tree_.insert(E, pe); +} + } // namespace simgrid::mc diff --git a/src/mc/api/State.hpp b/src/mc/api/State.hpp index fb1429a434..cb1297daf2 100644 --- a/src/mc/api/State.hpp +++ b/src/mc/api/State.hpp @@ -115,6 +115,8 @@ public: * backtrack set still contains processes added to the done set. */ std::unordered_set get_backtrack_set() const; + std::unordered_set get_sleeping_set() const; + std::unordered_set get_enabled_actors() const; std::map const& get_sleep_set() const { return sleep_set_; } void add_sleep_set(std::shared_ptr t) { @@ -150,6 +152,11 @@ public: */ void remove_subtree_starting_with(aid_t p); + /** + * @brief + */ + void mark_path_interesting_for_odpor(const odpor::PartialExecution&, const odpor::Execution&); + /* 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 a4f5bc3303..849055bd41 100644 --- a/src/mc/explo/DFSExplorer.cpp +++ b/src/mc/explo/DFSExplorer.cpp @@ -234,6 +234,10 @@ void DFSExplorer::run() // The latter evidently must be done BEFORE the former next_state->sprout_tree_from_parent_state(); state->remove_subtree_starting_with(next); + + // TODO: Consider what we have to do to handle transitions + // with multiple possible executions. We probably have to re-insert + // something into `state` and make note of that for later (opened_states_) } /* DPOR persistent set procedure: @@ -407,9 +411,44 @@ 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 + if (const auto last_event = execution_seq_.get_latest_event_handle(); + reduction_mode_ == ReductionMode::odpor and last_event.has_value()) { + /** + * ODPOR Race Detection Procedure: + * + * For each reversible race in the current execution, we + * note if there are any continuations `C` equivalent to that which + * would reverse the race that have already either a) been searched by ODPOR or + * b) been *noted* to be searched by the wakeup tree at the + * appropriate reversal point, either as `C` directly or + * an as equivalent to `C` ("eventually looks like C", viz. the `~_E` + * relation) + */ + for (auto e_prime = static_cast(0); e_prime <= last_event; e_prime++) { + for (const auto e : execution_seq_.get_racing_events_of(e_prime)) { + // To determine if the race is reversible, we have to ensure + // that actor `p` running `e_i` (viz. the event such that + // `racing_event -> (E_p) e_i` and no other event + // "happens-between" the two) is enabled in any equivalent + // execution where `racing_event` happens before `e_i`. + // + // 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 aid_t p = execution_seq_.get_actor_with_handle(e_prime); + const std::shared_ptr prev_state = stack_[e]; + if (prev_state->is_actor_enabled(p)) { + const std::optional v = execution_seq_.get_odpor_extension_from( + e, e_prime, prev_state->get_sleeping_set(), prev_state->get_enabled_actors()); + if (v.has_value()) { + prev_state->mark_path_interesting_for_odpor(v.value(), execution_seq_.get_prefix_before(e)); + } + } + } + } } XBT_VERB("Backtracking from %s", get_record_trace().to_string().c_str()); diff --git a/src/mc/explo/odpor/Execution.cpp b/src/mc/explo/odpor/Execution.cpp index c8df4d87e1..57c00a36e5 100644 --- a/src/mc/explo/odpor/Execution.cpp +++ b/src/mc/explo/odpor/Execution.cpp @@ -71,7 +71,7 @@ std::unordered_set Execution::get_racing_events_of(Execu return racing_events; } -Execution Execution::get_prefix_up_to(Execution::EventHandle handle) const +Execution Execution::get_prefix_before(Execution::EventHandle handle) const { return Execution(std::vector{contents_.begin(), contents_.begin() + handle}); } @@ -98,7 +98,7 @@ std::optional Execution::get_first_sdpor_initial_from(EventHandle e, // First, grab `E' := pre(e, E)` and determine what actor `p` is const auto next_E_p = get_latest_event_handle().value(); - Execution E_prime_v = get_prefix_up_to(e); + Execution E_prime_v = get_prefix_before(e); std::vector v; // Note `e + 1` here: `notdep(e, E)` is defined as the @@ -146,6 +146,14 @@ std::optional Execution::get_first_sdpor_initial_from(EventHandle e, return std::nullopt; } +std::optional Execution::get_odpor_extension_from(EventHandle e, EventHandle e_prime, + std::unordered_set sleep_set, + std::unordered_set enabled_actors) const +{ + // TODO: Implement this :( + return std::nullopt; +} + bool Execution::is_initial_after_execution(const PartialExecution& w, aid_t p) const { auto E_w = *this; diff --git a/src/mc/explo/odpor/Execution.hpp b/src/mc/explo/odpor/Execution.hpp index 13571d6c83..b0a7a50d31 100644 --- a/src/mc/explo/odpor/Execution.hpp +++ b/src/mc/explo/odpor/Execution.hpp @@ -80,12 +80,7 @@ public: */ class Execution { private: - /** - * @brief The actual steps that are taken by the process - * during exploration, relative to the - */ std::vector contents_; - Execution(std::vector&& contents) : contents_(std::move(contents)) {} public: @@ -144,9 +139,6 @@ 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 @@ -155,6 +147,16 @@ public: std::optional get_shortest_odpor_sq_subset_insertion(const PartialExecution& v, const PartialExecution& w) const; + /** + * @brief For a given reversible race + */ + std::optional get_odpor_extension_from(EventHandle, EventHandle, + std::unordered_set sleep_set, + std::unordered_set enabled_actors) 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 Determines the event associated with * the given handle `handle` @@ -167,6 +169,15 @@ public: */ aid_t get_actor_with_handle(EventHandle handle) const { return get_event_with_handle(handle).get_transition()->aid_; } + /** + * @brief Returns a handle to the newest event of the execution, + * if such an event exists + */ + std::optional get_latest_event_handle() const + { + return contents_.empty() ? std::nullopt : std::optional{static_cast(size() - 1)}; + } + /** * @brief Returns a set of events which are in * "immediate conflict" (according to the definition given @@ -188,15 +199,6 @@ public: */ std::unordered_set get_racing_events_of(EventHandle handle) const; - /** - * @brief Returns a handle to the newest event of the execution, - * if such an event exists - */ - std::optional get_latest_event_handle() const - { - return contents_.empty() ? std::nullopt : std::optional{static_cast(size() - 1)}; - } - /** * @brief Computes `pre(e, E)` as described in ODPOR [1] * @@ -207,7 +209,7 @@ public: * causes that permitted event `e` to exist (roughly * speaking) */ - Execution get_prefix_up_to(EventHandle) const; + Execution get_prefix_before(EventHandle) const; /** * @brief Whether the event represented by `e1` -- 2.20.1