From f7227d2fbe79ad5b4c8f4c109b41e649ccf0db86 Mon Sep 17 00:00:00 2001 From: Maxwell Pirtle Date: Fri, 26 May 2023 15:12:42 +0200 Subject: [PATCH] Resolve misconception with ODPOR pseudocode impl. Like the SDPOR implementation before it, the ODPOR implementation suffered from a similar fault in its implementation. Determining whether an insertion was necessary into a wakeup tree for some point in the past requires determining whether the sleep set and the set of weak initials overlap one another. If their intersection is the empty set, THEN we attempt to insert an actor. The prior implementation attempted to find the first such actor that was not contained in the sleep set, but this is semantically different --- src/mc/explo/odpor/Execution.cpp | 91 +++++++++++++++++--------------- src/mc/mc_config.cpp | 2 +- 2 files changed, 48 insertions(+), 45 deletions(-) diff --git a/src/mc/explo/odpor/Execution.cpp b/src/mc/explo/odpor/Execution.cpp index bf5172233e..b7b0cbb1bd 100644 --- a/src/mc/explo/odpor/Execution.cpp +++ b/src/mc/explo/odpor/Execution.cpp @@ -221,10 +221,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` @@ -240,7 +241,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) { @@ -267,25 +268,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& e_star) { + return E_prime_v.happens_before(e_star, 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 @@ -297,44 +299,45 @@ std::optional Execution::get_odpor_extension_from(EventHandle } // Now we add `e_prime := ` to `E'.v` and repeat the same work + // 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()); - 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 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); - }); + const bool is_initial = std::none_of(v_handles.begin(), v_handles.end(), [&](const auto& e_star) { + return E_prime_v.happens_before(e_star, 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 - 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 (astate.is_enabled() and sleeping_actors.count(aid) == 0 and - pre_E_e.is_independent_with_execution_of(v, astate.get_transition(0))) { - return v; + { + const Execution pre_E_e = get_prefix_before(e); + const auto sleeping_actors = state_at_e.get_sleeping_actors(); + + // Check if any enabled actor 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 (astate.is_enabled() and pre_E_e.is_independent_with_execution_of(v, astate.get_transition(0))) { + if (sleeping_actors.count(aid) > 0) { + return std::nullopt; + } + } } } - - return std::nullopt; + return v; } bool Execution::is_initial_after_execution_of(const PartialExecution& w, aid_t p) const diff --git a/src/mc/mc_config.cpp b/src/mc/mc_config.cpp index fe9b06fd1a..2174f3a4f8 100644 --- a/src/mc/mc_config.cpp +++ b/src/mc/mc_config.cpp @@ -151,7 +151,7 @@ simgrid::mc::ReductionMode simgrid::mc::get_model_checking_reduction() } else if (cfg_mc_reduction.get() == "sdpor") { return ReductionMode::sdpor; } else if (cfg_mc_reduction.get() == "odpor") { - return simgrid::mc::ReductionMode::odpor; + return ReductionMode::odpor; } else if (cfg_mc_reduction.get() == "udpor") { XBT_INFO("No reduction will be used: " "UDPOR is has a dedicated invocation 'model-check/unfolding-checker' " -- 2.20.1