From cc4e47adb7dcf6aa76c9e9c43f4ef0bc390684e6 Mon Sep 17 00:00:00 2001 From: Maxwell Pirtle Date: Thu, 1 Jun 2023 13:21:23 +0200 Subject: [PATCH] Introduce ODPOR integration with multiple actions Prior commits had missing integration with transitions which could be executed multiple times in the form of variants. This commit resolves those issues by making two important modifications: 1. Determining the "current thing that actor X is running" from a given state `s` has been modified to reflect what we would expect if we asked the question even after having exhausted all combinations; the the case where all combinations have been executed, the last variant is that which we would expect to be considered the transition which were enabled at `s`. This allows us to "fix" the spot in ODPOR where we need to determine those actions enabled at a given state `s`. We need to treat it as if only one variant actually exists; for if there are differences in the dependency structure for each variant, we wouldn't want to erroneously deduce that an actor `X` were a weak initial for some prefix `E'` of `E` and for some extension `v` of `E'` based on what it HAD run in the past. 2. In ODPOR, we now only insert members into the sleep set when all variants of a transition have been executed. This ensures that we are effectively treating each variant in isolation from one another; it is only when we reach the last variant that we can finally go ahead and say "OK actor X you can go into the sleep set now". Note that it's perfectly possible for the actor to later end up in sleep sets of states that occur *later on*; but for the sleep set that is at *this* state, we'd want to be sure only to add it after having explored the state space with each variant. The reasoning is the same as in point 1: we wouldn't want the sleep set to be based on an action that the actor HAD run in the past as the proxy representing what that actor is doing IN THE PRESENT. If the dependencies were different among the different variants, we'd have an issue if we had previously added the other variants --- src/mc/api/ActorState.hpp | 28 +++++++++++++++++++++++++++- src/mc/api/State.cpp | 14 ++++++++++---- src/mc/explo/odpor/Execution.cpp | 18 ++++++++++-------- 3 files changed, 47 insertions(+), 13 deletions(-) diff --git a/src/mc/api/ActorState.hpp b/src/mc/api/ActorState.hpp index 8b5e03fe04..2e8e136e8c 100644 --- a/src/mc/api/ActorState.hpp +++ b/src/mc/api/ActorState.hpp @@ -9,6 +9,7 @@ #include "src/kernel/activity/CommImpl.hpp" #include "src/mc/remote/RemotePtr.hpp" +#include #include #include @@ -100,6 +101,7 @@ public: 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_; } + bool has_more_to_consider() const { return get_times_not_considered() > 0; } aid_t get_aid() const { return aid_; } /* returns whether the actor is marked as enabled in the application side */ @@ -116,7 +118,31 @@ public: } void mark_done() { this->state_ = InterleavingType::done; } - std::shared_ptr get_transition() const { return get_transition(get_times_considered()); } + /** + * @brief Retrieves the transition that we should consider for execution by + * this actor from the State instance with respect to which this ActorState object + * is considered + */ + std::shared_ptr get_transition() const + { + // The rationale for this selection is as follows: + // + // 1. For transitions with only one possibility of execution, + // we always wish to select action `0` even if we've + // marked the transition already as considered (which + // we'll do if we explore a trace following that transition). + // + // 2. For transitions that can be considered multiple + // times, we want to be sure to select the most up-to-date + // action. In general, this means selecting that which is + // now being considered at this state. If, however, we've + // executed the + // + // The formula satisfies both of the above conditions: + // + // > std::clamp(times_considered_, 0u, max_consider_ - 1) + return get_transition(std::clamp(times_considered_, 0u, max_consider_ - 1)); + } std::shared_ptr get_transition(unsigned times_considered) const { diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp index 1f8786d1a5..b05bf39fcf 100644 --- a/src/mc/api/State.cpp +++ b/src/mc/api/State.cpp @@ -213,9 +213,7 @@ void State::seed_wakeup_tree_if_needed(const odpor::Execution& prior) 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? + // that all variants are searched for (unsigned times = 0; times < actor.get_max_considered(); ++times) { wakeup_tree_.insert(prior, odpor::PartialExecution{actor.get_transition(times)}); } @@ -273,7 +271,15 @@ void State::do_odpor_unwind() { if (auto out_transition = get_transition_out(); out_transition != nullptr) { remove_subtree_using_current_out_transition(); - add_sleep_set(std::move(out_transition)); + + // Only when we've exhausted all variants of the transition which + // can be chosen from this state do we finally add the actor to the + // sleep set. This ensures that the current logic handling sleep sets + // works with ODPOR in the way we intend it to work. There is not a + // good way to perform transition equality in SimGrid; instead, we + // effectively simply check for the presence of an actor in the sleep set. + if (!get_actors_list().at(out_transition->aid_).has_more_to_consider()) + add_sleep_set(std::move(out_transition)); } } diff --git a/src/mc/explo/odpor/Execution.cpp b/src/mc/explo/odpor/Execution.cpp index 1c01e2b48a..ef10e4f45f 100644 --- a/src/mc/explo/odpor/Execution.cpp +++ b/src/mc/explo/odpor/Execution.cpp @@ -337,15 +337,17 @@ std::optional Execution::get_odpor_extension_from(EventHandle 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 + // 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 (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; - } + 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; } } } -- 2.20.1