From 06610286385a7f265621445ea9baf0e8876f299d Mon Sep 17 00:00:00 2001 From: Maxwell Pirtle Date: Wed, 15 Feb 2023 10:50:16 +0100 Subject: [PATCH] Replace pending transition with latest execution The `State::execute_next(aid_t)` method was adjusted to use the newest copy of the transition that was executed by an actor in lieu of the copy of the transition that was previously stored by the actor, as more information may be gained during the execution of a transition. --- src/mc/api/ActorState.hpp | 31 ++++++++++++++++++++++++++++--- src/mc/api/State.cpp | 32 ++++++++++++++++++++++++-------- src/mc/api/State.hpp | 8 +++++--- 3 files changed, 57 insertions(+), 14 deletions(-) diff --git a/src/mc/api/ActorState.hpp b/src/mc/api/ActorState.hpp index d0752d25a9..16232ff53a 100644 --- a/src/mc/api/ActorState.hpp +++ b/src/mc/api/ActorState.hpp @@ -29,7 +29,23 @@ class ActorState { /** * @brief The transitions that the actor is allowed to execute from this - * state. + * state, viz. those that are enabled for this actor + * + * Most actors can take only a single action from any given state. + * However, when an actor executes a transition with multiple + * possible variations (e.g. an MC_Random() [see class: RandomTransition] + * for more details]), multiple enabled actions are defined + * + * @invariant The transitions are arranged such that an actor + * with multiple possible paths of execution will contain all + * such transitions such that `pending_transitions_[i]` represents + * the variation of the transition with `times_considered = i`. + * + * TODO: If only a subset of transitions of an actor that can + * take multiple transitions in some state are truly enabled, + * we would instead need to map `times_considered` to a transition, + * as the map is currently implicit in the ordering of the transitions + * in the vector * * TODO: If a single transition is taken at a time in a concurrent system, * then nearly all of the transitions from in a state `s'` after taking @@ -99,14 +115,23 @@ public: } void set_done() { this->state_ = InterleavingType::done; } - Transition* get_transition(unsigned times_considered) + inline Transition* get_transition(unsigned times_considered) { - xbt_assert(times_considered <= this->pending_transitions_.size(), + xbt_assert(times_considered < this->pending_transitions_.size(), "Actor %lu does not have a state available transition with `times_considered = %d`,\n" "yet one was asked for", aid_, times_considered); return this->pending_transitions_[times_considered].get(); } + + inline void set_transition(std::unique_ptr t, unsigned times_considered) + { + xbt_assert(times_considered < this->pending_transitions_.size(), + "Actor %lu does not have a state available transition with `times_considered = %d`, " + "yet one was attempted to be set", + aid_, times_considered); + this->pending_transitions_[times_considered] = std::move(t); + } }; } // namespace simgrid::mc diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp index d17d402ac8..f91a36959a 100644 --- a/src/mc/api/State.cpp +++ b/src/mc/api/State.cpp @@ -46,26 +46,42 @@ aid_t State::next_transition() const } return -1; } + void State::execute_next(aid_t next) { - /* This actor is ready to be executed. Prepare its execution when simcall_handle will be called on it */ - const unsigned times_considered = actors_to_run_.at(next).do_consider(); - auto* expected_executed_transition = actors_to_run_.at(next).get_transition(times_considered); + // This actor is ready to be executed. Execution involves three phases: + + // 1. Identify the appropriate ActorState to prepare for execution + // when simcall_handle will be called on it + auto& actor_state = actors_to_run_.at(next); + const unsigned times_considered = actor_state.do_consider(); + const auto* expected_executed_transition = actor_state.get_transition(times_considered); xbt_assert(expected_executed_transition != nullptr, "Expected a transition with %d times considered to be noted in actor %lu", times_considered, next); XBT_DEBUG("Let's run actor %ld (times_considered = %u)", next, times_considered); + // 2. Execute the actor according to the preparation above Transition::executed_transitions_++; - - const auto* executed_transition = mc_model_checker->handle_simcall(next, times_considered, true); - xbt_assert(executed_transition->type_ == expected_executed_transition->type_, + auto* just_executed = mc_model_checker->handle_simcall(next, times_considered, true); + xbt_assert(just_executed->type_ == expected_executed_transition->type_, "The transition that was just executed by actor %lu, viz:\n" "%s\n" "is not what was purportedly scheduled to execute, which was:\n" "%s\n", - next, executed_transition->to_string().c_str(), expected_executed_transition->to_string().c_str()); - transition_ = expected_executed_transition; + next, just_executed->to_string().c_str(), expected_executed_transition->to_string().c_str()); + + // 3. Update the state with the newest information. This means recording + // both + // 1. what action was last taken from this state (viz. `executed_transition`) + // 2. what action actor `next` was able to take given `times_considered` + // The latter update is important as *more* information is potentially available + // about a transition AFTER it has executed. + transition_ = just_executed; + + auto executed_transition = std::unique_ptr(just_executed); + actor_state.set_transition(std::move(executed_transition), times_considered); + mc_model_checker->wait_for_requests(); } } // namespace simgrid::mc diff --git a/src/mc/api/State.hpp b/src/mc/api/State.hpp index 700691779c..08a4ecf30d 100644 --- a/src/mc/api/State.hpp +++ b/src/mc/api/State.hpp @@ -18,9 +18,11 @@ class XBT_PRIVATE State : public xbt::Extendable { static long expended_states_; /* Count total amount of states, for stats */ /** - * Outgoing transition: what was the last transition that we took to leave this state? - * The owner of the transition is the ActorState instance which exists in the State - * object from which this state is derived, or nullptr if the state represents the root + * @brief The outgoing transition: what was the last transition that + * we took to leave this state? + * + * The owner of the transition is the `ActorState` instance which exists in this state, + * or nullptr if the state represents the root */ Transition* transition_ = nullptr; -- 2.20.1