From: Maxwell Pirtle Date: Fri, 12 May 2023 11:19:50 +0000 (+0200) Subject: Add ODPOR extension computation (lines 4-6) X-Git-Tag: v3.34~68^2~31 X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/04b710673e7f793c0cb96ef8e10c0ab9723c583b Add ODPOR extension computation (lines 4-6) ODPOR asks us to compute, for each reversible race in the current maximal execution `E`, whether some subsequence `v` of events extending a prefix `E'` of `E` should be inserted into a wakeup tree. There's a few subtle details that should be noted in this computation. ODPOR asks us to compute `notdep(e, E)`, which means possibly looking at events that occur *after* `e'` and THEN adding `proc(e')`. The subtlety lies in the fact that the actual transition associated with `e'` must be added AFTER all of the others. We got lucky with SDPOR since next_E_p was already in the last position and thus required no special treatment. With ODPOR, we have to be more careful. Even more subtle is the observation that any events in `notdep(e, E)` can neither affect the enabledness of `e'` nor can `e'` affect the enabledness of any of those events, or else if they do affect the enabledness of `e'` they will necessarily be contained "between" `e` and `e'` --- diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp index 54d71cfee3..2488c33c86 100644 --- a/src/mc/api/State.cpp +++ b/src/mc/api/State.cpp @@ -188,7 +188,7 @@ std::unordered_set State::get_backtrack_set() const return actors; } -std::unordered_set State::get_sleeping_set() const +std::unordered_set State::get_sleeping_actors() const { std::unordered_set actors; for (const auto& [aid, _] : get_sleep_set()) { diff --git a/src/mc/api/State.hpp b/src/mc/api/State.hpp index cb1297daf2..4b6b123ca3 100644 --- a/src/mc/api/State.hpp +++ b/src/mc/api/State.hpp @@ -115,7 +115,7 @@ 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_sleeping_actors() 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) diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp index e654056185..4b2d631831 100644 --- a/src/mc/explo/DFSExplorer.cpp +++ b/src/mc/explo/DFSExplorer.cpp @@ -437,13 +437,13 @@ void DFSExplorer::backtrack() // 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()); + const aid_t p = execution_seq_.get_actor_with_handle(e_prime); + State& 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); if (v.has_value()) { - prev_state->mark_path_interesting_for_odpor(v.value(), execution_seq_.get_prefix_before(e)); + prev_state.mark_path_interesting_for_odpor(v.value(), execution_seq_.get_prefix_before(e)); } } } diff --git a/src/mc/explo/odpor/Execution.cpp b/src/mc/explo/odpor/Execution.cpp index dbf215eb26..568b233c24 100644 --- a/src/mc/explo/odpor/Execution.cpp +++ b/src/mc/explo/odpor/Execution.cpp @@ -4,6 +4,7 @@ * under the terms of the license (GNU LGPL) which comes with this package. */ #include "src/mc/explo/odpor/Execution.hpp" +#include "src/mc/api/State.hpp" #include "xbt/asserts.h" #include #include @@ -147,10 +148,128 @@ std::optional Execution::get_first_sdpor_initial_from(EventHandle e, } std::optional Execution::get_odpor_extension_from(EventHandle e, EventHandle e_prime, - std::unordered_set sleep_set, - std::unordered_set enabled_actors) const + const State& state_at_e) const { - // TODO: Implement this :( + // `e` is assumed to be in a reversible race with `e_prime`. + // If `e > e_prime`, then `e` occurs-after `e_prime` which means + // `e` could not race with if + if (e > e_prime) { + throw std::invalid_argument("ODPOR extensions can only be computed for " + "events in a reversible race, which is claimed, " + "yet the racing event 'occurs-after' the target"); + } + + if (empty()) { + return std::nullopt; + } + + PartialExecution v; + Execution E_prime_v = get_prefix_before(e); + std::unordered_set disqualified_actors = state_at_e.get_sleeping_actors(); + std::vector v_handles; + bool located_actor_in_initial = false; + + // Note `e + 1` here: `notdep(e, E)` is defined as the + // set of events that *occur-after* but don't *happen-after* `e` + // + // SUBTLE NOTE: ODPOR requires us to compute `notdep(e, E)` EVEN THOUGH + // the race is between `e` and `e'`; that is, events occurring in `E` + // that "occur-after" `e'` may end up in the partial execution `v`. + // + // Observe that `notdep(e, E).proc(e')` will contain all transitions + // that don't happen-after `e` in the order they appear FOLLOWED BY + // THE **TRANSITION** ASSOCIATED WITH **`e'`**!! + // + // SUBTLE NOTE: Observe that any event that "happens-after" `e'` + // must necessarily "happen-after" `e` as well, since `e` and + // `e'` are presumed to be in a reversible race. Hence, we know that + // all events `e_star` that `e` "happens-before" cannot affect + // the enabledness of `e'`; furthermore, `e'` cannot affect the enabledness + // of any event independent with `e` that "occurs-after" `e'` + for (auto e_star = e + 1; e_star <= get_latest_event_handle().value(); ++e_star) { + // 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' + // to be able to compute `--->[E'.v]` + if (not happens_before(e, e_star)) { + xbt_assert(e_star != e_prime, + "Invariant Violation: We claimed events %u and %u were in a reversible race, yet we also " + "claim that they do not happen-before one another. This is impossible: " + "are you sure that the two events are in a reversible race?", + e, e_prime); + E_prime_v.push_transition(get_event_with_handle(e_star).get_transition()); + v.push_back(get_event_with_handle(e_star).get_transition()); + + const EventHandle e_star_in_E_prime_v = E_prime_v.get_latest_event_handle().value(); + + // When checking whether any event in `dom_[E'](v)` happens before + // `next_[E'](q)` below for thread `q`, we must consider that the + // events relative to `E` (this execution) are different than those + // relative to `E'.v`. Thus e.g. event `7` in `E` may be event `4` + // in `E'.v`. Since we are asking about "happens-before" + // `-->_[E'.v]` about `E'.v`, we must build `v` relative to `E'` + v_handles.push_back(e_star_in_E_prime_v); + + if (located_actor_in_initial) { + // It suffices that we find one initial. If we've already found + // one, we simply need to finish building `v` + continue; + } + + // Note that we add `q` to v regardless of whether `q` itself has been + // disqualified since `q` may itself disqualify other actors + // (i.e. even if `q` is disqualified from being an initial, it + // is still contained in the sequence `v`) + const aid_t q = E_prime_v.get_actor_with_handle(e_star_in_E_prime_v); + if (disqualified_actors.count(q) > 0) { + continue; + } + const bool is_initial = std::none_of(v_handles.begin(), v_handles.end(), [&](const auto& e_loc) { + return E_prime_v.happens_before(e_loc, e_star_in_E_prime_v); + }); + if (is_initial) { + located_actor_in_initial = true; + } else { + // If `q` is disqualified as a candidate, clearly + // no event occurring after `e_prime` in `E` executed + // by actor `q` will qualify since any (valid) happens-before + // relation orders actions taken by each actor + disqualified_actors.insert(q); + } + } + } + + // Now we add `e_prime := ` to `E'.v` and repeat the same work + { + E_prime_v.push_transition(get_event_with_handle(e_prime).get_transition()); + if (not located_actor_in_initial) { + // It's possible `proc(e_prime)` is an initial + const EventHandle e_prime_in_E_prime_v = E_prime_v.get_latest_event_handle().value(); + v_handles.push_back(e_prime_in_E_prime_v); + located_actor_in_initial = std::none_of(v_handles.begin(), v_handles.end(), [&](const auto& e_loc) { + return E_prime_v.happens_before(e_loc, e_prime_in_E_prime_v); + }); + } + } + + /** Some actor `p` in `v` is an initial for `E' := pre(e, E)`*/ + if (located_actor_in_initial) { + return v; + } + + const Execution pre_E_e = get_prefix_before(e); + const auto sleeping_actors = state_at_e.get_sleeping_actors(); + + // Otherwise, for each enabled actor also not in the sleep set, check if + // any of them are independent with this execution after `v`. This + // completes the check for weak initials + for (const auto& [aid, astate] : state_at_e.get_actors_list()) { + if (sleeping_actors.count(astate.get_transition()->aid_) == 0 and + pre_E_e.is_independent_with_execution(v, astate.get_transition())) { + return v; + } + } + return std::nullopt; } @@ -231,11 +350,11 @@ std::optional Execution::get_shortest_odpor_sq_subset_insertio "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_, + xbt_assert(w_action->type_ == next_E_p->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()); + p, next_E_p->to_string(false).c_str(), w_action->to_string(false).c_str()); w_now.erase(action_by_p_in_w); } // Is `E ⊢ p ◇ w`? @@ -256,7 +375,7 @@ std::optional Execution::get_shortest_odpor_sq_subset_insertio } // Move one step forward in the direction of `v` and repeat - E_v.push_transition(next_p_E); + E_v.push_transition(next_E_p); } // Construct, finally, v.w' by adding `v` to the front of diff --git a/src/mc/explo/odpor/Execution.hpp b/src/mc/explo/odpor/Execution.hpp index ad818a6d15..0131b195a7 100644 --- a/src/mc/explo/odpor/Execution.hpp +++ b/src/mc/explo/odpor/Execution.hpp @@ -8,6 +8,7 @@ #include "src/mc/api/ClockVector.hpp" #include "src/mc/explo/odpor/odpor_forward.hpp" +#include "src/mc/mc_forward.hpp" #include "src/mc/transition/Transition.hpp" #include @@ -141,7 +142,7 @@ public: /** * @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 + * computes the sequence, if any, that should be inserted as a child a wakeup tree for * this execution */ std::optional get_shortest_odpor_sq_subset_insertion(const PartialExecution& v, @@ -149,10 +150,13 @@ public: /** * @brief For a given reversible race + * + * @invariant: This method assumes that events `e` and + * `e_prime` are in a *reversible* race as is the case + * in ODPOR */ - std::optional get_odpor_extension_from(EventHandle, EventHandle, - std::unordered_set sleep_set, - std::unordered_set enabled_actors) const; + std::optional get_odpor_extension_from(EventHandle e, EventHandle e_prime, + const State& state_at_e) const; bool is_initial_after_execution(const PartialExecution& w, aid_t p) const; bool is_independent_with_execution(const PartialExecution& w, std::shared_ptr next_E_p) const;