X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/790db8801f3ba7fd9001e6c8f31efcd9971980d5..7e625e5e848a284b522d69ec28cb111f1f88515b:/src/mc/explo/odpor/Execution.cpp diff --git a/src/mc/explo/odpor/Execution.cpp b/src/mc/explo/odpor/Execution.cpp index e514141d4b..0694161cd2 100644 --- a/src/mc/explo/odpor/Execution.cpp +++ b/src/mc/explo/odpor/Execution.cpp @@ -6,12 +6,30 @@ #include "src/mc/explo/odpor/Execution.hpp" #include "src/mc/api/State.hpp" #include "xbt/asserts.h" +#include "xbt/string.hpp" #include #include #include +XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_odpor_execution, mc_dfs, "ODPOR exploration algorithm of the model-checker"); + namespace simgrid::mc::odpor { +std::vector get_textual_trace(const PartialExecution& w) +{ + std::vector trace; + for (const auto& t : w) { + auto a = xbt::string_printf("Actor %ld: %s", t->aid_, t->to_string(true).c_str()); + trace.emplace_back(std::move(a)); + } + return trace; +} + +Execution::Execution(const PartialExecution& w) +{ + push_partial_execution(w); +} + void Execution::push_transition(std::shared_ptr t) { if (t == nullptr) { @@ -27,21 +45,42 @@ void Execution::push_transition(std::shared_ptr t) contents_.push_back(Event({std::move(t), max_clock_vector})); } +void Execution::push_partial_execution(const PartialExecution& w) +{ + for (const auto& t : w) { + push_transition(t); + } +} + +std::vector Execution::get_textual_trace() const +{ + std::vector trace; + for (const auto& t : this->contents_) { + auto a = xbt::string_printf("Actor %ld: %s", t.get_transition()->aid_, t.get_transition()->to_string(true).c_str()); + trace.emplace_back(std::move(a)); + } + return trace; +} + std::unordered_set Execution::get_racing_events_of(Execution::EventHandle target) const { std::unordered_set racing_events; + // This keep tracks of events that happens-before the target std::unordered_set disqualified_events; // For each event of the execution for (auto e_i = target; e_i != std::numeric_limits::max(); e_i--) { // We need `e_i -->_E target` as a necessary condition if (not happens_before(e_i, target)) { + XBT_DEBUG("ODPOR_RACING_EVENTS with `%u` : `%u` discarded because `%u` --\\-->_E `%u`", target, e_i, e_i, target); continue; } // Further, `proc(e_i) != proc(target)` if (get_actor_with_handle(e_i) == get_actor_with_handle(target)) { disqualified_events.insert(e_i); + XBT_DEBUG("ODPOR_RACING_EVENTS with `%u` : `%u` disqualified because proc(`%u`)=proc(`%u`)", target, e_i, e_i, + target); continue; } @@ -52,7 +91,9 @@ std::unordered_set Execution::get_racing_events_of(Execu // 2. disqualified_events.count(e_j) > 0 // then e_i --->_E target indirectly (either through // e_j directly, or transitively through e_j) - if (happens_before(e_i, e_j) and disqualified_events.count(e_j) > 0) { + if (disqualified_events.count(e_j) > 0 && happens_before(e_i, e_j)) { + XBT_DEBUG("ODPOR_RACING_EVENTS with `%u` : `%u` disqualified because `%u` happens-between `%u`-->`%u`-->`%u`)", + target, e_i, e_j, e_i, e_j, target); disqualified_events.insert(e_i); break; } @@ -64,6 +105,7 @@ std::unordered_set Execution::get_racing_events_of(Execu // it (since this would transitively make it the event // which "happens-between" `target` and `e`) if (disqualified_events.count(e_i) == 0) { + XBT_DEBUG("ODPOR_RACING_EVENTS with `%u` : `%u` is a valid racing event", target, e_i); racing_events.insert(e_i); disqualified_events.insert(e_i); } @@ -72,19 +114,33 @@ std::unordered_set Execution::get_racing_events_of(Execu return racing_events; } +std::unordered_set Execution::get_reversible_races_of(EventHandle handle) const +{ + std::unordered_set reversible_races; + const auto* this_transition = get_transition_for_handle(handle); + for (EventHandle race : get_racing_events_of(handle)) { + const auto* other_transition = get_transition_for_handle(race); + + if (this_transition->reversible_race(other_transition)) { + reversible_races.insert(race); + } + } + return reversible_races; +} + Execution Execution::get_prefix_before(Execution::EventHandle handle) const { return Execution(std::vector{contents_.begin(), contents_.begin() + handle}); } -std::optional Execution::get_first_sdpor_initial_from(EventHandle e, - std::unordered_set disqualified_actors) const +std::unordered_set +Execution::get_missing_source_set_actors_from(EventHandle e, const std::unordered_set& backtrack_set) 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; + return std::unordered_set{}; } // To actually compute `I_[E'](v) ∩ backtrack(E')`, we must @@ -93,14 +149,23 @@ std::optional Execution::get_first_sdpor_initial_from(EventHandle e, // note of any events which occur after `e` but don't // "happen-after" `e` by pushing them onto `E'`. Note that // correctness is still preserved in computing `v` "on-the-fly" - // to determine if an actor `q` is an initial for `E'` after `v`: - // only those events that "occur-before" `v` - // could happen-before `v` for any valid happens-before relation. + // to determine if an event `e` by actor `q` is an initial for `E'` + // after `v`: only those events that "occur-before" `e` in `v` could + // "happen-before" `ve for any valid "happens-before" relation + // (see property 1 in the ODPOR paper, viz. "is included in <_E") // First, grab `E' := pre(e, E)` and determine what actor `p` is const auto next_E_p = get_latest_event_handle().value(); + xbt_assert(e != next_E_p, + "This method assumes that the event `e` (%u) and `next_[E](p)` (%u)" + "are in a reversible race, yet we claim to have such a race between the" + "same event. This indicates the the SDPOR pseudocode implementation is broken " + "as it supplies these values.", + e, next_E_p); Execution E_prime_v = get_prefix_before(e); std::vector v; + std::unordered_set I_E_prime_v; + std::unordered_set disqualified_actors; // Note `e + 1` here: `notdep(e, E)` is defined as the // set of events that *occur-after* but don't *happen-after* `e` @@ -109,7 +174,7 @@ std::optional Execution::get_first_sdpor_initial_from(EventHandle e, // 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) { + if (not happens_before(e, e_prime) || e_prime == next_E_p) { // First, push the transition onto the hypothetical execution E_prime_v.push_transition(get_event_with_handle(e_prime).get_transition()); const EventHandle e_prime_in_E_prime_v = E_prime_v.get_latest_event_handle().value(); @@ -119,22 +184,29 @@ std::optional Execution::get_first_sdpor_initial_from(EventHandle e, // 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'` + // `-->_[E'.v]` about `E'.v`, we must build `v` relative to `E'`. + // + // Note that we add `q` to v regardless of whether `q` itself has been + // disqualified since we've determined that `e_prime` "occurs-after" but + // does not "happen-after" `e` v.push_back(e_prime_in_E_prime_v); - // 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_prime_in_E_prime_v); - if (disqualified_actors.count(q) > 0) { + if (disqualified_actors.count(q) > 0) { // Did we already note that `q` is not an initial? 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_v); }); if (is_initial) { - return q; + // If the backtrack set already contains `q`, we're done: + // they've made note to search for (or have already searched for) + // this initial + if (backtrack_set.count(q) > 0) { + return std::unordered_set{}; + } else { + I_E_prime_v.insert(q); + } } else { // If `q` is disqualified as a candidate, clearly // no event occurring after `e_prime` in `E` executed @@ -144,7 +216,14 @@ std::optional Execution::get_first_sdpor_initial_from(EventHandle e, } } } - return std::nullopt; + xbt_assert(not I_E_prime_v.empty(), + "For any non-empty execution, we know that " + "at minimum one actor is an initial since " + "some execution is possible with respect to a " + "prefix before event `%u`, yet we didn't find anyone. " + "This implies the implementation of this function is broken.", + e); + return I_E_prime_v; } std::optional Execution::get_odpor_extension_from(EventHandle e, EventHandle e_prime, @@ -164,10 +243,11 @@ std::optional Execution::get_odpor_extension_from(EventHandle } PartialExecution v; + std::vector v_handles; + std::unordered_set WI_E_prime_v; + std::unordered_set disqualified_actors; 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; + const std::unordered_set sleep_E_prime = state_at_e.get_sleeping_actors(); // Note `e + 1` here: `notdep(e, E)` is defined as the // set of events that *occur-after* but don't *happen-after* `e` @@ -183,7 +263,7 @@ std::optional Execution::get_odpor_extension_from(EventHandle // 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 + // all events `e_star` such that `e` "happens-before" `e_star` 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) { @@ -200,6 +280,9 @@ std::optional Execution::get_odpor_extension_from(EventHandle E_prime_v.push_transition(get_event_with_handle(e_star).get_transition()); v.push_back(get_event_with_handle(e_star).get_transition()); + XBT_DEBUG("Added Event `%u` (%ld:%s) to the construction of v", e_star, get_actor_with_handle(e_star), + get_event_with_handle(e_star).get_transition()->to_string().c_str()); + 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 @@ -210,25 +293,26 @@ std::optional Execution::get_odpor_extension_from(EventHandle // `-->_[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) { + if (disqualified_actors.count(q) > 0) { // Did we already note that `q` is not an initial? 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); + const bool is_initial = std::none_of(v_handles.begin(), v_handles.end(), [&](const auto& handle) { + return E_prime_v.happens_before(handle, e_star_in_E_prime_v); }); if (is_initial) { - located_actor_in_initial = true; + // If the sleep set already contains `q`, we're done: + // we've found an initial contained in the sleep set and + // so the intersection is non-empty + if (sleep_E_prime.count(q) > 0) { + return std::nullopt; + } else { + WI_E_prime_v.insert(q); + } } else { // If `q` is disqualified as a candidate, clearly // no event occurring after `e_prime` in `E` executed @@ -236,47 +320,51 @@ std::optional Execution::get_odpor_extension_from(EventHandle // relation orders actions taken by each actor disqualified_actors.insert(q); } + } else { + XBT_DEBUG("Event `%u` (%ld:%s) dismissed from the construction of v", e_star, get_actor_with_handle(e_star), + get_event_with_handle(e_star).get_transition()->to_string().c_str()); } } // Now we add `e_prime := ` to `E'.v` and repeat the same work - { - v.push_back(get_event_with_handle(e_prime).get_transition()); - - if (not located_actor_in_initial) { - // It's possible `proc(e_prime)` is an initial - E_prime_v.push_transition(get_event_with_handle(e_prime).get_transition()); - 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); - - const aid_t q = E_prime_v.get_actor_with_handle(e_prime_in_E_prime_v); - located_actor_in_initial = disqualified_actors.count(q) == 0 and - 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); - }); + // It's possible `proc(e_prime)` is an initial + // + // Note the form of `v` in the pseudocode: + // `v := notdep(e, E).e'^ + E_prime_v.push_transition(get_event_with_handle(e_prime).get_transition()); + v.push_back(get_event_with_handle(e_prime).get_transition()); + + 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); + + const bool is_initial = std::none_of(v_handles.begin(), v_handles.end(), [&](const auto& handle) { + return E_prime_v.happens_before(handle, e_prime_in_E_prime_v); + }); + if (is_initial) { + if (const aid_t q = E_prime_v.get_actor_with_handle(e_prime_in_E_prime_v); sleep_E_prime.count(q) > 0) { + return std::nullopt; + } else { + WI_E_prime_v.insert(q); } } - /** 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 + // Check if any enabled actor that is independent with + // this execution after `v` is contained in the sleep set for (const auto& [aid, astate] : state_at_e.get_actors_list()) { - // TODO: We have to be able to react appropriately here when adding new - // types of transitions (multiple choices can be made :( ) - if (sleeping_actors.count(aid) == 0 and pre_E_e.is_independent_with_execution_of(v, astate.get_transition(0))) { - return v; - } + const bool is_in_WI_E = + astate.is_enabled() and pre_E_e.is_independent_with_execution_of(v, astate.get_transition()); + const bool is_in_sleep_set = sleeping_actors.count(aid) > 0; + + // `action(aid)` is in `WI_[E](v)` but also is contained in the sleep set. + // This implies that the intersection between the two is non-empty + if (is_in_WI_E && is_in_sleep_set) + return std::nullopt; } - return std::nullopt; + return v; } bool Execution::is_initial_after_execution_of(const PartialExecution& w, aid_t p) const @@ -337,13 +425,11 @@ std::optional Execution::get_shortest_odpor_sq_subset_insertio auto w_now = w; for (const auto& next_E_p : v) { - const aid_t p = next_E_p->aid_; - // Is `p in `I_[E](w)`? - if (E_v.is_initial_after_execution_of(w_now, p)) { + if (const aid_t p = next_E_p->aid_; E_v.is_initial_after_execution_of(w_now, p)) { // Remove `p` from w and continue - // TODO: If `p` occurs in `w`, it had better refer to the same + // INVARIANT: 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, @@ -364,7 +450,7 @@ std::optional Execution::get_shortest_odpor_sq_subset_insertio w_now.erase(action_by_p_in_w); } // Is `E ⊢ p ◇ w`? - else if (E_v.is_independent_with_execution_of(w, next_E_p)) { + else if (E_v.is_independent_with_execution_of(w_now, next_E_p)) { // 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` (intuitively, the fact that `E ⊢ p ◇ w` @@ -412,4 +498,4 @@ bool Execution::happens_before(Execution::EventHandle e1_handle, Execution::Even return false; } -} // namespace simgrid::mc::odpor \ No newline at end of file +} // namespace simgrid::mc::odpor