From 26501dd7026096ebf4d7a8e4ca5d16cea63e2a87 Mon Sep 17 00:00:00 2001 From: Maxwell Pirtle Date: Tue, 23 May 2023 10:18:24 +0200 Subject: [PATCH] Add first round of execution independence tests This commit adds the first set of tests for checking whether a particular transition `t` is independent with an extension `w` of an execution sequence `E`. This is needed to determine whether the transition `t` satisfies condition (2) of the procedure outlined in the ODPOR paper for testing whether `v ~_[E] w` holds between two sequences --- src/mc/api/ActorState.hpp | 1 + src/mc/api/State.cpp | 15 +++- src/mc/explo/DFSExplorer.cpp | 4 -- src/mc/explo/odpor/Execution.cpp | 10 +-- src/mc/explo/odpor/Execution.hpp | 4 +- src/mc/explo/odpor/Execution_test.cpp | 96 ++++++++++++++++++++++++++ src/mc/explo/odpor/WakeupTree_test.cpp | 9 --- 7 files changed, 116 insertions(+), 23 deletions(-) diff --git a/src/mc/api/ActorState.hpp b/src/mc/api/ActorState.hpp index 18be326da7..8b5e03fe04 100644 --- a/src/mc/api/ActorState.hpp +++ b/src/mc/api/ActorState.hpp @@ -97,6 +97,7 @@ public: mark_done(); return times_considered_++; } + unsigned int get_max_considered() const { return max_consider_; } unsigned int get_times_considered() const { return times_considered_; } unsigned int get_times_not_considered() const { return max_consider_ - times_considered_; } aid_t get_aid() const { return aid_; } diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp index 298913153a..1680ca07cf 100644 --- a/src/mc/api/State.cpp +++ b/src/mc/api/State.cpp @@ -209,9 +209,18 @@ void State::seed_wakeup_tree_if_needed(const odpor::Execution& prior) // tree and decided upon "happens-before" at that point for different // executions :( if (wakeup_tree_.empty()) { - strategy_->consider_best(); - if (const aid_t next = std::get<0>(strategy_->next_transition()); next >= 0) { - wakeup_tree_.insert(prior, odpor::PartialExecution{strategy_->actors_to_run_.at(next).get_transition()}); + // Find an enabled transition to pick + for (const auto& [_, actor] : get_actors_list()) { + if (actor.is_enabled()) { + // For each variant of the transition, we want + // to insert the action into the tree. This ensures + // that all variants are searched? + // + // TODO: How do we modify sleep sets then? + for (unsigned times = 0; times < actor.get_max_considered(); ++times) { + wakeup_tree_.insert(prior, odpor::PartialExecution{actor.get_transition(times)}); + } + } } } has_initialized_wakeup_tree = true; diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp index 198b2d6008..5844878650 100644 --- a/src/mc/explo/DFSExplorer.cpp +++ b/src/mc/explo/DFSExplorer.cpp @@ -229,10 +229,6 @@ void DFSExplorer::run() // fully down a single path before we consider adding // any elements to the sleep set according to the pseudocode next_state->sprout_tree_from_parent_state(); - - // TODO: Consider what we have to do to handle transitions - // with multiple possible executions. We probably have to re-insert - // something into `state` and make note of that for later (opened_states_) } else { /* Sleep set procedure: * adding the taken transition to the sleep set of the original state. diff --git a/src/mc/explo/odpor/Execution.cpp b/src/mc/explo/odpor/Execution.cpp index 981adee615..1e9bdbc6d9 100644 --- a/src/mc/explo/odpor/Execution.cpp +++ b/src/mc/explo/odpor/Execution.cpp @@ -271,7 +271,7 @@ std::optional Execution::get_odpor_extension_from(EventHandle 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(v, astate.get_transition(0))) { + if (sleeping_actors.count(aid) == 0 and pre_E_e.is_independent_with_execution_of(v, astate.get_transition(0))) { return v; } } @@ -279,7 +279,7 @@ std::optional Execution::get_odpor_extension_from(EventHandle return std::nullopt; } -bool Execution::is_initial_after_execution(const PartialExecution& w, aid_t p) const +bool Execution::is_initial_after_execution_of(const PartialExecution& w, aid_t p) const { auto E_w = *this; std::vector w_handles; @@ -302,7 +302,7 @@ bool Execution::is_initial_after_execution(const PartialExecution& w, aid_t p) c return false; } -bool Execution::is_independent_with_execution(const PartialExecution& w, std::shared_ptr next_E_p) const +bool Execution::is_independent_with_execution_of(const PartialExecution& w, std::shared_ptr next_E_p) const { // INVARIANT: Here, we assume that for any process `p_i` of `w`, // the events of this execution followed by the execution of all @@ -340,7 +340,7 @@ std::optional Execution::get_shortest_odpor_sq_subset_insertio const aid_t p = next_E_p->aid_; // Is `p in `I_[E](w)`? - if (E_v.is_initial_after_execution(w_now, p)) { + if (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 @@ -364,7 +364,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(w, next_E_p)) { + else if (E_v.is_independent_with_execution_of(w, 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`. We assert this is the case here diff --git a/src/mc/explo/odpor/Execution.hpp b/src/mc/explo/odpor/Execution.hpp index 9f5005d95b..cfe24bd544 100644 --- a/src/mc/explo/odpor/Execution.hpp +++ b/src/mc/explo/odpor/Execution.hpp @@ -213,12 +213,12 @@ public: * `N` actors, we can process them "in-parallel" as is done with the * computation of SDPOR initials) */ - bool is_initial_after_execution(const PartialExecution& w, aid_t p) const; + bool is_initial_after_execution_of(const PartialExecution& w, aid_t p) const; /** * @brief Determines whether `E ⊢ p ◊ w` given the next action taken by `p` */ - bool is_independent_with_execution(const PartialExecution& w, std::shared_ptr next_E_p) const; + bool is_independent_with_execution_of(const PartialExecution& w, std::shared_ptr next_E_p) const; /** * @brief Determines the event associated with diff --git a/src/mc/explo/odpor/Execution_test.cpp b/src/mc/explo/odpor/Execution_test.cpp index 0ed54f9052..06485ab707 100644 --- a/src/mc/explo/odpor/Execution_test.cpp +++ b/src/mc/explo/odpor/Execution_test.cpp @@ -294,3 +294,99 @@ TEST_CASE("simgrid::mc::odpor::Execution: Testing Races and Conditions") execution.push_transition(a4); execution.push_transition(a5); } + +TEST_CASE("simgrid::mc::odpor::Execution: Independence Tests") +{ + SECTION("Complete independence") + { + // Every transition is independent with every other and run by different actors. Hopefully + // we say that the events are independent with each other... + const auto a0 = std::make_shared(Transition::Type::UNKNOWN, 1); + const auto a1 = std::make_shared(Transition::Type::UNKNOWN, 2); + const auto a2 = std::make_shared(Transition::Type::UNKNOWN, 3); + const auto a3 = std::make_shared(Transition::Type::UNKNOWN, 4); + const auto a4 = std::make_shared(Transition::Type::UNKNOWN, 5); + const auto a5 = std::make_shared(Transition::Type::UNKNOWN, 6); + const auto a6 = std::make_shared(Transition::Type::UNKNOWN, 7); + const auto a7 = std::make_shared(Transition::Type::UNKNOWN, 7); + Execution execution; + execution.push_transition(a0); + execution.push_transition(a1); + execution.push_transition(a2); + execution.push_transition(a3); + + REQUIRE(execution.is_independent_with_execution_of(PartialExecution{a4, a5}, a6)); + + // In this case, we notice that `a6` and `a7` are executed by the same actor. + // Hence, a6 cannot be independent with extending the execution with a4.a5.a7. + // Notice that we are treating *a6* as the next step of actor 7 (that is what we + // supplied as an argument) + REQUIRE_FALSE(execution.is_independent_with_execution_of(PartialExecution{a4, a5, a7}, a6)); + } + + SECTION("Dependencies stopping independence from being possible") + { + const auto a0 = std::make_shared(Transition::Type::UNKNOWN, 1); + const auto a1 = std::make_shared(Transition::Type::UNKNOWN, 1); + const auto a2 = std::make_shared(Transition::Type::UNKNOWN, 3); + const auto a3 = std::make_shared(Transition::Type::UNKNOWN, 4); + const auto a4 = std::make_shared(Transition::Type::UNKNOWN, 4); + const auto a5 = std::make_shared(Transition::Type::UNKNOWN, 2); + const auto a6 = std::make_shared(Transition::Type::UNKNOWN, 3); + const auto a7 = std::make_shared(Transition::Type::UNKNOWN, 1); + const auto a8 = std::make_shared(Transition::Type::UNKNOWN, 4); + const auto indep = 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); + + // We see that although `a4` comes after `a1` with which it is dependent, it + // would come before "a6" in the partial execution `w`, so it would not be independent + REQUIRE_FALSE(execution.is_independent_with_execution_of(PartialExecution{a5, a6, a7}, a4)); + + // Removing `a6` from the picture, though, gives us the independence we're looking for. + REQUIRE(execution.is_independent_with_execution_of(PartialExecution{a5, a7}, a4)); + + // BUT, we we ask about a transition which is run by the same actor, even if they would be + // independent otherwise, we again lose independence + REQUIRE_FALSE(execution.is_independent_with_execution_of(PartialExecution{a5, a7, a8}, a4)); + + // This is a more interesting case: + // `indep` clearly is independent with the rest of the series, even though + // there are dependencies among the other events in the partial execution + REQUIRE(Execution().is_independent_with_execution_of(PartialExecution{a1, a6, a7}, indep)); + } +} + +TEST_CASE("simgrid::mc::odpor::Execution: ODPOR Smallest Sequence Tests") +{ + const auto a0 = std::make_shared(Transition::Type::UNKNOWN, 2); + const auto a1 = std::make_shared(Transition::Type::UNKNOWN, 4); + const auto a2 = std::make_shared(Transition::Type::UNKNOWN, 3); + const auto a3 = std::make_shared(Transition::Type::UNKNOWN, 1); + const auto a4 = std::make_shared(Transition::Type::UNKNOWN, 2); + const auto a5 = std::make_shared(Transition::Type::UNKNOWN, 4); + + SECTION("Equivalent insertions") + { + // TODO: Is this even a sensible question to ask if the two sequences + // don't agree upon what each actor executed after `E`? + const auto insertion = + Execution().get_shortest_odpor_sq_subset_insertion(PartialExecution{a1, a2}, PartialExecution{a2, a5}); + REQUIRE(insertion.has_value()); + REQUIRE(insertion.value() == PartialExecution{}); + } + + SECTION("") + { + Execution execution; + execution.push_transition(a0); + execution.push_transition(a1); + execution.push_transition(a2); + execution.push_transition(a3); + execution.push_transition(a4); + execution.push_transition(a5); + } +} diff --git a/src/mc/explo/odpor/WakeupTree_test.cpp b/src/mc/explo/odpor/WakeupTree_test.cpp index ddea4b0599..a30e761181 100644 --- a/src/mc/explo/odpor/WakeupTree_test.cpp +++ b/src/mc/explo/odpor/WakeupTree_test.cpp @@ -257,15 +257,6 @@ TEST_CASE("simgrid::mc::odpor::WakeupTree: Testing Insertion for Empty Execution const auto a3 = std::make_shared(Transition::Type::UNKNOWN, 1); const auto a4 = std::make_shared(Transition::Type::UNKNOWN, 2); const auto a5 = std::make_shared(Transition::Type::UNKNOWN, 4); - - Execution execution; - execution.push_transition(a0); - execution.push_transition(a1); - execution.push_transition(a2); - execution.push_transition(a3); - execution.push_transition(a4); - execution.push_transition(a5); - WakeupTree tree; SECTION("Attempting to insert the empty sequence into an empty tree should have no effect") -- 2.20.1