From 07437dfc06522a67cf136cb6161e0782f100a525 Mon Sep 17 00:00:00 2001 From: Maxwell Pirtle Date: Tue, 28 Mar 2023 13:44:12 +0200 Subject: [PATCH] Intermediate commit to prove that UDPOR functions This commit returns a const_cast<>-ed UnfoldingEvent from the intersection of the sets A and ex(C) in the Unfolding. We use this work around currently as there is no way currently to distinguish between a set of events and a set of constant events with EventSet. To do so would require a number of changes and probably a class that would be entirely duplicated and more difficult to read without the help of e.g. a template (which itself is not always the easiest to read). --- src/mc/api/ActorState.hpp | 2 +- src/mc/api/State.cpp | 9 ++++--- src/mc/api/State.hpp | 8 +++--- src/mc/explo/UdporChecker.cpp | 37 +++++++++++++++++++++------ src/mc/explo/UdporChecker.hpp | 4 +-- src/mc/explo/udpor/UnfoldingEvent.hpp | 2 ++ 6 files changed, 44 insertions(+), 18 deletions(-) diff --git a/src/mc/api/ActorState.hpp b/src/mc/api/ActorState.hpp index a7fee78b51..315ed8af38 100644 --- a/src/mc/api/ActorState.hpp +++ b/src/mc/api/ActorState.hpp @@ -124,7 +124,7 @@ public: return this->pending_transitions_[times_considered].get(); } - inline void set_transition(std::unique_ptr t, unsigned times_considered) + inline void set_transition(std::shared_ptr t, unsigned times_considered) { xbt_assert(times_considered < this->pending_transitions_.size(), "Actor %ld does not have a state available transition with `times_considered = %u`, " diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp index b5f8eba6a3..e701c72033 100644 --- a/src/mc/api/State.cpp +++ b/src/mc/api/State.cpp @@ -127,7 +127,7 @@ std::pair State::next_transition_guided() const } // This should be done in GuidedState, or at least interact with it -void State::execute_next(aid_t next, RemoteApp& app) +std::shared_ptr State::execute_next(aid_t next, RemoteApp& app) { // First, warn the guide, so it knows how to build a proper child state strategy_->execute_next(next, app); @@ -162,9 +162,10 @@ void State::execute_next(aid_t next, RemoteApp& app) // 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); - + const auto executed_transition = std::shared_ptr(just_executed); + actor_state.set_transition(executed_transition, times_considered); app.wait_for_requests(); + + return executed_transition; } } // namespace simgrid::mc diff --git a/src/mc/api/State.hpp b/src/mc/api/State.hpp index 6d984370d2..111c4af99c 100644 --- a/src/mc/api/State.hpp +++ b/src/mc/api/State.hpp @@ -66,9 +66,11 @@ public: internal cost of the transition is returned */ std::pair next_transition_guided() const; - /* Explore a new path on the remote app; the parameter 'next' must be the result of a previous call to - * next_transition() */ - void execute_next(aid_t next, RemoteApp& app); + /** + * @brief Explore a new path on the remote app; the parameter 'next' must be the result of a previous call to + * next_transition() + */ + std::shared_ptr execute_next(aid_t next, RemoteApp& app); long get_num() const { return num_; } std::size_t count_todo() const; diff --git a/src/mc/explo/UdporChecker.cpp b/src/mc/explo/UdporChecker.cpp index 15cc3ec9fb..03b39e58e3 100644 --- a/src/mc/explo/UdporChecker.cpp +++ b/src/mc/explo/UdporChecker.cpp @@ -61,7 +61,7 @@ void UdporChecker::explore(const Configuration& C, EventSet D, EventSet A, Event // TODO: Add verbose logging about which event is being explored - const UnfoldingEvent* e = select_next_unfolding_event(A, enC); + UnfoldingEvent* e = select_next_unfolding_event(A, enC); xbt_assert(e != nullptr, "\n\n****** INVARIANT VIOLATION ******\n" "UDPOR guarantees that an event will be chosen at each point in\n" "the search, yet no events were actually chosen\n" @@ -76,7 +76,7 @@ void UdporChecker::explore(const Configuration& C, EventSet D, EventSet A, Event // Explore(C + {e}, D, A \ {e}) // Move the application into stateCe (i.e. `state(C + {e})`) and make note of that state - move_to_stateCe(stateC, *e); + move_to_stateCe(&stateC, e); state_stack.push_back(record_current_state()); explore(Ce, D, std::move(A), std::move(exC)); @@ -146,9 +146,9 @@ EventSet UdporChecker::compute_enC(const Configuration& C, const EventSet& exC) return enC; } -void UdporChecker::move_to_stateCe(State& state, const UnfoldingEvent& e) +void UdporChecker::move_to_stateCe(State* state, UnfoldingEvent* e) { - const aid_t next_actor = e.get_transition()->aid_; + const aid_t next_actor = e->get_transition()->aid_; // TODO: Add the trace if possible for reporting a bug xbt_assert(next_actor >= 0, "\n\n****** INVARIANT VIOLATION ******\n" @@ -156,7 +156,28 @@ void UdporChecker::move_to_stateCe(State& state, const UnfoldingEvent& e) "one transition of the state of an visited event is enabled, yet no\n" "state was actually enabled. Please report this as a bug.\n" "*********************************\n\n"); - state.execute_next(next_actor, get_remote_app()); + auto latest_transition_by_next_actor = state->execute_next(next_actor, get_remote_app()); + + // The transition that is associated with the event was just + // executed, so it's possible that the new version of the transition + // (i.e. the one after execution) has *more* information than + // that which existed *prior* to execution. + // + // + // ------- !!!!! UDPOR INVARIANT !!!!! ------- + // + // At this point, we are leveraging the fact that + // UDPOR will not contain more than one copy of any + // transition executed by any actor for any + // particular step taken by that actor. That is, + // if transition `i` of the `j`th actor is contained in the + // configuration `C` currently under consideration + // by UDPOR, then only one and only one copy exists in `C` + // + // This means that we can referesh the transitions associated + // with each event lazily, i.e. only after we have chosen the + // event to continue our execution. + e->set_transition(std::move(latest_transition_by_next_actor)); } void UdporChecker::restore_program_state_with_current_stack() @@ -181,7 +202,7 @@ std::unique_ptr UdporChecker::record_current_state() return next_state; } -const UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC) +UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC) { if (enC.empty()) { throw std::invalid_argument("There are no unfolding events to select. " @@ -190,12 +211,12 @@ const UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& } if (A.empty()) { - return *(enC.begin()); + return const_cast(*(enC.begin())); } for (const auto& event : A) { if (enC.contains(event)) { - return event; + return const_cast(event); } } return nullptr; diff --git a/src/mc/explo/UdporChecker.hpp b/src/mc/explo/UdporChecker.hpp index 6e907a3c13..6706d2bc6b 100644 --- a/src/mc/explo/UdporChecker.hpp +++ b/src/mc/explo/UdporChecker.hpp @@ -81,7 +81,7 @@ private: * by the UDPOR algorithm to select new events to search. See the original * paper [1] for more details */ - const UnfoldingEvent* select_next_unfolding_event(const EventSet& A, const EventSet& enC); + UnfoldingEvent* select_next_unfolding_event(const EventSet& A, const EventSet& enC); /** * @brief Computes the sets `ex(C)` and `en(C)` of the given configuration @@ -113,7 +113,7 @@ private: /** * */ - void move_to_stateCe(State& stateC, const UnfoldingEvent& e); + void move_to_stateCe(State* stateC, UnfoldingEvent* e); /** * @brief Creates a new snapshot of the state of the application diff --git a/src/mc/explo/udpor/UnfoldingEvent.hpp b/src/mc/explo/udpor/UnfoldingEvent.hpp index fb04db53b4..65328244e5 100644 --- a/src/mc/explo/udpor/UnfoldingEvent.hpp +++ b/src/mc/explo/udpor/UnfoldingEvent.hpp @@ -52,6 +52,8 @@ public: Transition* get_transition() const { return this->associated_transition.get(); } aid_t get_actor() const { return get_transition()->aid_; } + void set_transition(std::shared_ptr t) { this->associated_transition = std::move(t); } + std::string to_string() const; bool operator==(const UnfoldingEvent&) const; -- 2.20.1