From: Maxwell Pirtle Date: Fri, 5 May 2023 12:47:07 +0000 (+0200) Subject: Add more documentation to essential SDPOR methods X-Git-Tag: v3.34~68^2~49 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/94148943bcb501d24189abe2650070708776da04 Add more documentation to essential SDPOR methods --- diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp index ee6298857b..38e73f0ba6 100644 --- a/src/mc/explo/DFSExplorer.cpp +++ b/src/mc/explo/DFSExplorer.cpp @@ -251,11 +251,15 @@ void DFSExplorer::run() /** * SDPOR Source Set Procedure: * - * Find "reversible races" in the current execution with respect + * Find "reversible races" in the current execution `E` 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 + * `r` that doesn't depend on it (`v := notdep(r, E)`) and then `p` to + * flip the race. + * + * The intuition is that some subsequence of `v` may enable `p`, so + * we want to be sure that search "in that direction" */ execution_seq_.push_transition(executed_transition.get()); @@ -284,7 +288,7 @@ void DFSExplorer::run() // 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()); + execution_seq_.get_first_sdpor_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 4c8a5c1152..f3b44e74fb 100644 --- a/src/mc/explo/odpor/Execution.cpp +++ b/src/mc/explo/odpor/Execution.cpp @@ -20,8 +20,6 @@ void Execution::push_transition(const Transition* 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 stack max_clock_vector[t->aid_] = this->size(); contents_.push_back(Event({t, max_clock_vector})); } @@ -81,8 +79,8 @@ 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 +std::optional Execution::get_first_sdpor_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 @@ -146,12 +144,6 @@ std::optional Execution::get_first_ssdpor_initial_from(EventHandle e, 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" (-->_E) is a subset of "occurs before" (<_E) diff --git a/src/mc/explo/odpor/Execution.hpp b/src/mc/explo/odpor/Execution.hpp index b0f7c2df02..552f76b95a 100644 --- a/src/mc/explo/odpor/Execution.hpp +++ b/src/mc/explo/odpor/Execution.hpp @@ -97,27 +97,56 @@ public: auto begin() const { return this->contents_.begin(); } auto end() const { return this->contents_.end(); } - 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; + /** + * @brief Computes the "core" portion the SDPOR algorithm, + * viz. the intersection of the backtracking set and the + * set of initials with respect to the end + * + * See the SDPOR algorithm pseudocode in [1] for more + * details for the context of the function. + * + * @invariant: This method assumes that events `e` and + * `e' := get_latest_event_handle()` are in a *reversible* race + * as is the case in SDPOR + * + * @returns an actor not contained in `disqualified` which + * can serve as an initial to reverse the race between `e` + * and `e'` + */ + std::optional get_first_sdpor_initial_from(EventHandle e, std::unordered_set disqualified) const; + /** + * @brief Determines the event associated with + * the given handle `handle` + */ const Event& get_event_with_handle(EventHandle handle) const { return contents_[handle]; } + + /** + * @brief Determines the actor associated with + * the given event handle `handle` + */ aid_t get_actor_with_handle(EventHandle handle) const { return get_event_with_handle(handle).get_transition()->aid_; } /** - * @brief Returns a set of IDs of events which are in + * @brief Returns a set of events which are in * "immediate conflict" (according to the definition given - * in the ODPOR paper) with one another + * in the ODPOR paper) with the given event + * + * Two events `e` and `e'` in an execution `E` are said to + * race iff + * + * 1. `proc(e) != proc(e')`; that is, the events correspond to + * the execution of different actors + * 2. `e -->_E e'` and there is no `e''` in `E` such that + * `e -->_E e''` and `e'' -->_E e'`; that is, the two events + * "happen-before" one another in `E` and no other event in + * `E` "happens-between" `e` and `e'` + * + * @param handle the event with respect to which races are + * computed + * @returns a set of event handles from which race with `handle` */ - std::unordered_set get_racing_events_of(EventHandle) const; + std::unordered_set get_racing_events_of(EventHandle handle) const; /** * @brief Returns a handle to the newest event of the execution, @@ -128,6 +157,16 @@ public: return contents_.empty() ? std::nullopt : std::optional{static_cast(size() - 1)}; } + /** + * @brief Computes `pre(e, E)` as described in ODPOR [1] + * + * The execution `pre(e, E)` for an event `e` in an + * execution `E` is the contiguous prefix of events + * `E' <= E` up to by excluding the event `e` itself. + * The prefix intuitively represents the "history" of + * causes that permitted event `e` to exist (roughly + * speaking) + */ Execution get_prefix_up_to(EventHandle) const; /** diff --git a/src/mc/explo/odpor/Execution_test.cpp b/src/mc/explo/odpor/Execution_test.cpp index b23384823a..d8d3bb320f 100644 --- a/src/mc/explo/odpor/Execution_test.cpp +++ b/src/mc/explo/odpor/Execution_test.cpp @@ -181,7 +181,7 @@ TEST_CASE("simgrid::mc::odpor::Execution: Testing Racing Events and Initials") // Since e2 -->_E e3, actor 3 is not an initial for E' := pre(1, execution) // with respect to `v`. e2, however, has nothing happening before it in dom_E(v), // so it is an initial of E' wrt. `v` - const auto initial_wrt_event1 = execution.get_first_ssdpor_initial_from(1, std::unordered_set{}); + const auto initial_wrt_event1 = execution.get_first_sdpor_initial_from(1, std::unordered_set{}); REQUIRE(initial_wrt_event1.has_value()); REQUIRE(initial_wrt_event1.value() == static_cast(1)); } @@ -191,7 +191,7 @@ TEST_CASE("simgrid::mc::odpor::Execution: Testing Racing Events and Initials") // First, note that v := notdep(1, execution).p == {}.{e3} == {e3} // e3 has nothing happening before it in dom_E(v), so it is an initial // of E' wrt. `v` - const auto initial_wrt_event2 = execution.get_first_ssdpor_initial_from(2, std::unordered_set{}); + const auto initial_wrt_event2 = execution.get_first_sdpor_initial_from(2, std::unordered_set{}); REQUIRE(initial_wrt_event2.has_value()); REQUIRE(initial_wrt_event2.value() == static_cast(3)); }