From: Maxwell Pirtle Date: Tue, 30 May 2023 11:42:32 +0000 (+0200) Subject: Fix subtle bug in ~_E computation X-Git-Tag: v3.34~68^2~9 X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/983ff2d3ba0217acac8e5c963f6669be3b4f9e02 Fix subtle bug in ~_E computation The computation for the action ~_E requires that we compute whether `p` is independent with some sequence of transitions `w` after an execution `E`. The algorithm for computing whether an equivalent trace was found works to iteratively eliminate events from the equivalent sequence, leaving behind only the remaining "bits" that are needed for insertion into a wakeup tree. The bug involved a typo of `w` for `w_now` :( :( which broke everything :/ --- diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp index 1e693ed79e..1f8786d1a5 100644 --- a/src/mc/api/State.cpp +++ b/src/mc/api/State.cpp @@ -235,13 +235,13 @@ void State::sprout_tree_from_parent_state() "parent with an empty wakeup tree. This indicates either that ODPOR " "actor selection in State.cpp is incorrect, or that the code " "deciding when to make subtrees in ODPOR is incorrect"); - xbt_assert((parent_state_->get_transition_out()->aid_ == min_process_node.value()->get_actor()) && - (parent_state_->get_transition_out()->type_ == min_process_node.value()->get_action()->type_), + xbt_assert((get_transition_in()->aid_ == min_process_node.value()->get_actor()) && + (get_transition_in()->type_ == min_process_node.value()->get_action()->type_), "We tried to make a subtree from a parent state who claimed to have executed `%s` " "but whose wakeup tree indicates it should have executed `%s`. This indicates " "that exploration is not following ODPOR. Are you sure you're choosing actors " "to schedule from the wakeup tree?", - parent_state_->get_transition_out()->to_string(false).c_str(), + get_transition_in()->to_string(false).c_str(), min_process_node.value()->get_action()->to_string(false).c_str()); this->wakeup_tree_ = odpor::WakeupTree::make_subtree_rooted_at(min_process_node.value()); } diff --git a/src/mc/explo/odpor/Execution.cpp b/src/mc/explo/odpor/Execution.cpp index b7b0cbb1bd..12e258a899 100644 --- a/src/mc/explo/odpor/Execution.cpp +++ b/src/mc/explo/odpor/Execution.cpp @@ -425,7 +425,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` diff --git a/src/mc/explo/odpor/Execution_test.cpp b/src/mc/explo/odpor/Execution_test.cpp index f18d696fca..f6043428ec 100644 --- a/src/mc/explo/odpor/Execution_test.cpp +++ b/src/mc/explo/odpor/Execution_test.cpp @@ -111,6 +111,29 @@ TEST_CASE("simgrid::mc::odpor::Execution: Testing Happens-Before") REQUIRE_FALSE(execution.happens_before(3, 2)); } } + + SECTION("Example 3: Happens-before is transitively-closed") + { + // Given a reversible race between events `e1` and `e3` in a simulation, + // we assert that `e5` would be eliminated from being contained in + // the sequence `notdep(e1, E)` + const auto e0 = std::make_shared(Transition::Type::UNKNOWN, 2); + const auto e1 = std::make_shared(Transition::Type::UNKNOWN, 1); + const auto e2 = std::make_shared(Transition::Type::UNKNOWN, 3); + const auto e3 = std::make_shared(Transition::Type::UNKNOWN, 1); + const auto e4 = std::make_shared(Transition::Type::UNKNOWN, 3); + + Execution execution; + execution.push_transition(e0); + execution.push_transition(e1); + execution.push_transition(e2); + execution.push_transition(e3); + execution.push_transition(e4); + + REQUIRE(execution.happens_before(0, 2)); + REQUIRE(execution.happens_before(2, 4)); + REQUIRE(execution.happens_before(0, 4)); + } } TEST_CASE("simgrid::mc::odpor::Execution: Testing Racing Events and Initials") @@ -197,20 +220,20 @@ TEST_CASE("simgrid::mc::odpor::Execution: Testing Racing Events and Initials") SECTION("Example 3: Testing 'Lock' Example") { - // In this example, - const auto a1 = std::make_shared(Transition::Type::UNKNOWN, 2); - const auto a2 = std::make_shared(Transition::Type::UNKNOWN, 2); - const auto a3 = std::make_shared(Transition::Type::UNKNOWN, 2); - const auto a4 = std::make_shared(Transition::Type::UNKNOWN, 1); - const auto a5 = std::make_shared(Transition::Type::UNKNOWN, 3); + // In this example, `e0` and `e1` are lock actions that + // are in a race. We assert that + const auto e0 = std::make_shared(Transition::Type::UNKNOWN, 2); + const auto e1 = std::make_shared(Transition::Type::UNKNOWN, 2); + const auto e2 = std::make_shared(Transition::Type::UNKNOWN, 2); + const auto e3 = std::make_shared(Transition::Type::UNKNOWN, 1); + const auto e4 = std::make_shared(Transition::Type::UNKNOWN, 3); Execution execution; - execution.push_transition(a1); - execution.push_transition(a2); - execution.push_transition(a3); - execution.push_transition(a4); - execution.push_transition(a5); - + execution.push_transition(e0); + execution.push_transition(e1); + execution.push_transition(e2); + execution.push_transition(e3); + execution.push_transition(e4); REQUIRE(execution.get_racing_events_of(4) == std::unordered_set{0}); } @@ -277,20 +300,25 @@ TEST_CASE("simgrid::mc::odpor::Execution: Testing Racing Events and Initials") } } -TEST_CASE("simgrid::mc::odpor::Execution: Testing Races and Conditions") +TEST_CASE("simgrid::mc::odpor::Execution: notdep(e, E) Simulation") { - const auto a1 = std::make_shared(Transition::Type::UNKNOWN, 2); - const auto a2 = std::make_shared(Transition::Type::UNKNOWN, 2); - const auto a3 = std::make_shared(Transition::Type::UNKNOWN, 2); - const auto a4 = std::make_shared(Transition::Type::UNKNOWN, 1); - const auto a5 = std::make_shared(Transition::Type::UNKNOWN, 3); + // Given a reversible race between events `e1` and `e3` in a simulation, + // we assert that `e5` would be eliminated from being contained in + // the sequence `notdep(e1, E)` + const auto e0 = std::make_shared(Transition::Type::UNKNOWN, 2); + const auto e1 = std::make_shared(Transition::Type::UNKNOWN, 1); + const auto e2 = std::make_shared(Transition::Type::UNKNOWN, 3); + const auto e3 = std::make_shared(Transition::Type::UNKNOWN, 1); + const auto e4 = std::make_shared(Transition::Type::UNKNOWN, 3); Execution execution; - execution.push_transition(a1); - execution.push_transition(a2); - execution.push_transition(a3); - execution.push_transition(a4); - execution.push_transition(a5); + execution.push_transition(e0); + execution.push_transition(e1); + execution.push_transition(e2); + execution.push_transition(e3); + execution.push_transition(e4); + + REQUIRE(execution.happens_before(0, 4)); } TEST_CASE("simgrid::mc::odpor::Execution: Independence Tests") @@ -513,6 +541,4 @@ TEST_CASE("simgrid::mc::odpor::Execution: ODPOR Smallest Sequence Tests") REQUIRE(insertion.value() == PartialExecution{}); } } - - SECTION("") {} } diff --git a/src/mc/explo/odpor/ReversibleRaceCalculator.cpp b/src/mc/explo/odpor/ReversibleRaceCalculator.cpp index 68d9eadbdf..efab9d3952 100644 --- a/src/mc/explo/odpor/ReversibleRaceCalculator.cpp +++ b/src/mc/explo/odpor/ReversibleRaceCalculator.cpp @@ -45,15 +45,13 @@ bool ReversibleRaceCalculator::is_race_reversible(const Execution& E, Execution: if (const auto handler = handlers.find(e2_action->type_); handler != handlers.end()) { return handler->second(E, e1, e2_action); } else { - xbt_assert(false, - "There is currently no specialized computation for the transition " - "'%s' for computing reversible races in ODPOR, so the model checker cannot " - "determine how to proceed. Please submit a bug report requesting " - "that the transition be supported in SimGrid using ODPPR and consider " - "using the other model-checking algorithms supported by SimGrid instead " - "in the meantime", - e2_action->to_string().c_str()); - DIE_IMPOSSIBLE; + xbt_die("There is currently no specialized computation for the transition " + "'%s' for computing reversible races in ODPOR, so the model checker cannot " + "determine how to proceed. Please submit a bug report requesting " + "that the transition be supported in SimGrid using ODPPR and consider " + "using the other model-checking algorithms supported by SimGrid instead " + "in the meantime", + e2_action->to_string().c_str()); } } diff --git a/src/mc/explo/odpor/WakeupTree_test.cpp b/src/mc/explo/odpor/WakeupTree_test.cpp index f45a0914ca..4db64edba3 100644 --- a/src/mc/explo/odpor/WakeupTree_test.cpp +++ b/src/mc/explo/odpor/WakeupTree_test.cpp @@ -193,12 +193,14 @@ TEST_CASE("simgrid::mc::odpor::WakeupTree: Testing Insertion for Empty Execution const auto a1 = std::make_shared(Transition::Type::UNKNOWN, 4); const auto a2 = std::make_shared(Transition::Type::UNKNOWN, 1); const auto a3 = std::make_shared(Transition::Type::UNKNOWN, 4); + const auto a4 = std::make_shared(Transition::Type::UNKNOWN, 2); Execution execution; execution.push_transition(a0); execution.push_transition(a1); execution.push_transition(a2); execution.push_transition(a3); + execution.push_transition(a4); REQUIRE(execution.get_racing_events_of(2) == std::unordered_set{0}); REQUIRE(execution.get_racing_events_of(3) == std::unordered_set{0}); @@ -253,16 +255,36 @@ TEST_CASE("simgrid::mc::odpor::WakeupTree: Testing Insertion for Empty Execution // / / // a0 a1 // / / - // a3 a2 + // a3 a4 // // Recall that new nodes (in this case the one with // action `a2`) are added such that they are "greater than" (under // the tree's `<` relation) all those that exist under the given parent. - tree.insert(Execution(), {a1, a2}); + tree.insert(Execution(), {a1, a4}); test_tree_iterator(tree, std::vector{PartialExecution{a0}, PartialExecution{a1, a3}, - PartialExecution{a1, a2}, PartialExecution{a1}, + PartialExecution{a1, a4}, PartialExecution{a1}, PartialExecution{}}); } + + SECTION("Inserting an equivalent sequence to a leaf should preserve the tree as-is") + { + // `a1.a2` is equivalent to `a1.a3` since `a2` and `a3` are independent + // (`E ⊢ p ◊ w` where `p := proc(a2)` and `w := a3`). Thus, the tree + // should now STILL look as follows: + // + // {} + // / / + // a0 a1 + // / + // a3 + // + // Recall that new nodes (in this case the one with + // action `a2`) are added such that they are "greater than" (under + // the tree's `<` relation) all those that exist under the given parent. + tree.insert(Execution(), {a1, a3}); + test_tree_iterator(tree, std::vector{PartialExecution{a0}, PartialExecution{a1, a3}, + PartialExecution{a1}, PartialExecution{}}); + } } SECTION("Performing Arbitrary Insertions") diff --git a/src/mc/mc_config.cpp b/src/mc/mc_config.cpp index 2174f3a4f8..1d9375f627 100644 --- a/src/mc/mc_config.cpp +++ b/src/mc/mc_config.cpp @@ -154,8 +154,8 @@ simgrid::mc::ReductionMode simgrid::mc::get_model_checking_reduction() 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' " - "but is not yet supported in SimGrid"); + "UDPOR has a dedicated invocation 'model-check/unfolding-checker' " + "but is not yet fully supported in SimGrid"); return ReductionMode::none; } else { XBT_INFO("Unknown reduction mode: defaulting to no reduction");