From edb58d998573dba62c74537dcacce8b4b9a7df80 Mon Sep 17 00:00:00 2001 From: Maxwell Pirtle Date: Fri, 17 Feb 2023 13:59:59 +0100 Subject: [PATCH] "Finalize" interface to UnfoldingEvent The interface to the UnfoldingEvent was carried over from the previous implementation of UDPOR in the "tiny_simgrid" repository. However, the implementation needed to be adjusted to better suit how SimGrid is going to implement UDPOR. Instead of holding a string tag identifying a transition, each UnfoldingEvent now directly holds a reference to the transition from the state prior. This caused some changes to need to be made in the UdporChecker.cpp. These changes have moved the pseudocode of UDPOR one large step closer to the actual implementation that will be brought to life over the next few weeks --- src/mc/explo/UdporChecker.cpp | 95 +++++++++++++++------------ src/mc/explo/UdporChecker.hpp | 61 ++++++++--------- src/mc/explo/udpor/UnfoldingEvent.cpp | 12 +--- src/mc/explo/udpor/UnfoldingEvent.hpp | 26 ++++++-- src/mc/explo/udpor/udpor_forward.hpp | 1 + 5 files changed, 104 insertions(+), 91 deletions(-) diff --git a/src/mc/explo/UdporChecker.cpp b/src/mc/explo/UdporChecker.cpp index 48b2a01d1c..da236e29c8 100644 --- a/src/mc/explo/UdporChecker.cpp +++ b/src/mc/explo/UdporChecker.cpp @@ -24,23 +24,29 @@ void UdporChecker::run() // NOTE: `A`, `D`, and `C` are derived from the // original UDPOR paper [1], while `prev_exC` arises // from the incremental computation of ex(C) from [3] - EventSet A, D; - Configuration C; - EventSet prev_exC; + Configuration C_root; - auto initial_state = get_current_state(); - const auto initial_state_id = state_manager_.record_state(std::move(initial_state)); - const auto root_event = std::make_unique(-1, "", EventSet(), initial_state_id); - explore(std::move(C), std::move(A), std::move(D), {}, root_event.get(), std::move(prev_exC)); + // TODO: Move computing the root configuration into a method on the Unfolding + auto initial_state = get_current_state(); + auto root_event = std::make_unique(std::make_shared(), EventSet()); + auto* root_event_handle = root_event.get(); + unfolding.insert(std::move(root_event)); + C_root.add_event(root_event_handle); + + explore(std::move(C_root), EventSet(), EventSet(), std::move(initial_state), EventSet()); XBT_INFO("UDPOR exploration terminated -- model checking completed"); } -void UdporChecker::explore(Configuration C, EventSet D, EventSet A, std::list max_evt_history, - UnfoldingEvent* e_cur, EventSet prev_exC) +void UdporChecker::explore(Configuration C, EventSet D, EventSet A, std::unique_ptr stateC, EventSet prev_exC) { // Perform the incremental computation of exC - auto [exC, enC] = compute_extension(C, max_evt_history, e_cur, prev_exC); + // + // TODO: This method will have side effects on + // the unfolding, but the naming of the method + // suggests it is doesn't have side effects. We should + // reconcile this in the future + auto [exC, enC] = compute_extension(C, prev_exC); // If enC is a subset of D, intuitively // there aren't any enabled transitions @@ -73,25 +79,25 @@ void UdporChecker::explore(Configuration C, EventSet D, EventSet A, std::listset_state_id(next_state_id); + + // Move the application into stateCe and actually make note of that state + move_to_stateCe(*stateC, *e); + auto stateCe = record_current_state(); // Ce := C + {e} Configuration Ce = C; Ce.add_event(e); - max_evt_history.push_back(Ce.get_maximal_events()); A.remove(e); exC.remove(e); // Explore(C + {e}, D, A \ {e}) - explore(Ce, D, std::move(A), max_evt_history, e, std::move(exC)); + explore(Ce, D, std::move(A), std::move(stateCe), std::move(exC)); // D <-- D + {e} D.insert(e); @@ -101,10 +107,15 @@ void UdporChecker::explore(Configuration C, EventSet D, EventSet A, std::list UdporChecker::compute_extension(const Configuration& C, - const std::list& max_evt_history, - UnfoldingEvent* e_cur, const EventSet& prev_exC) const +std::tuple UdporChecker::compute_extension(const Configuration& C, const EventSet& prev_exC) const { // See eqs. 5.7 of section 5.2 of [3] - // ex(C + {e_cur}) = ex(C) / {e_cur} + U{ : H } - EventSet exC = prev_exC; + // C = C' + {e_cur}, i.e. C' = C - {e_cur} + // + // Then + // + // ex(C) = ex(C' + {e_cur}) = ex(C') / {e_cur} + U{ : H } + UnfoldingEvent* e_cur = C.get_latest_event(); + EventSet exC = prev_exC; exC.remove(e_cur); + // ... fancy computations + EventSet enC; return std::tuple(exC, enC); } -State& UdporChecker::get_state_referenced_by(const UnfoldingEvent& event) -{ - const auto state_id = event.get_state_id(); - const auto wrapped_state = this->state_manager_.get_state(state_id); - xbt_assert(wrapped_state != std::nullopt, - "\n\n****** INVARIANT VIOLATION ******\n" - "To each UDPOR event corresponds a state, but state %llu does not exist. " - "Please report this as a bug.\n" - "*********************************\n\n", - state_id); - return wrapped_state.value().get(); -} - -StateHandle UdporChecker::observe_unfolding_event(const UnfoldingEvent& event) +void UdporChecker::move_to_stateCe(State& state, const UnfoldingEvent& e) { - auto& state = this->get_state_referenced_by(event); - const aid_t next_actor = state.next_transition(); + 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" @@ -152,17 +154,22 @@ StateHandle UdporChecker::observe_unfolding_event(const UnfoldingEvent& event) "state was actually enabled. Please report this as a bug.\n" "*********************************\n\n"); state.execute_next(next_actor); - return this->record_current_state(); } -StateHandle UdporChecker::record_current_state() +void UdporChecker::restore_program_state_to(const State& stateC) +{ + // TODO: Perform state regeneration in the same manner as is done + // in the DFSChecker.cpp +} + +std::unique_ptr UdporChecker::record_current_state() { - auto next_state = this->get_current_state(); - const auto next_state_id = this->state_manager_.record_state(std::move(next_state)); + auto next_state = this->get_current_state(); // In UDPOR, we care about all enabled transitions in a given state next_state->mark_all_enabled_todo(); - return next_state_id; + + return next_state; } UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC) @@ -198,6 +205,8 @@ RecordTrace UdporChecker::get_record_trace() std::vector UdporChecker::get_textual_trace() { + // TODO: Topologically sort the events of the latest configuration + // and iterate through that topological sorting std::vector trace; return trace; } diff --git a/src/mc/explo/UdporChecker.hpp b/src/mc/explo/UdporChecker.hpp index 28c9d1955b..cc1604ab35 100644 --- a/src/mc/explo/UdporChecker.hpp +++ b/src/mc/explo/UdporChecker.hpp @@ -11,6 +11,7 @@ #include "src/mc/explo/udpor/Configuration.hpp" #include "src/mc/explo/udpor/EventSet.hpp" #include "src/mc/explo/udpor/StateManager.hpp" +#include "src/mc/explo/udpor/Unfolding.hpp" #include "src/mc/explo/udpor/UnfoldingEvent.hpp" #include "src/mc/mc_record.hpp" @@ -79,6 +80,11 @@ private: */ StateManager state_manager_; + /** + * @brief UDPOR's current "view" of the program it is exploring + */ + Unfolding unfolding = Unfolding(); + private: /** * @brief Explores the unfolding of the concurrent system @@ -95,18 +101,27 @@ private: * @param A the set of events to "guide" UDPOR in the correct direction * when it returns back to a node in the unfolding and must decide among * events to select from `ex(C)`. See [1] for more details - * @param max_evt_history - * - * @param e the event where UDPOR currently "rests", viz. the event UDPOR - * is now currently considering. This event is contained in the set `C` - * and is the last event that was added to C - * + * @param stateC the state of the program after having executed `C`, + * viz. `state(C)` using the notation of [1] * * TODO: Add the optimization where we can check if e == e_prior * to prevent repeated work when computing ex(C) */ - void explore(Configuration C, EventSet D, EventSet A, std::list max_evt_history, UnfoldingEvent* e_cur, - EventSet prev_exC); + void explore(Configuration C, EventSet D, EventSet A, std::unique_ptr stateC, EventSet prev_exC); + + /** + * @brief Identifies the next event from the unfolding of the concurrent system + * that should next be explored as an extension of a configuration with + * enabled events `enC` + * + * @param A The set of events `A` maintained by the UDPOR algorithm to help + * determine how events should be selected. See the original paper [1] for more details + * + * @param enC The set `enC` of enabled events from the extension set `exC` used + * by the UDPOR algorithm to select new events to search. See the original + * paper [1] for more details + */ + UnfoldingEvent* select_next_unfolding_event(const EventSet& A, const EventSet& enC); /** * @brief Computes the sets `ex(C)` and `en(C)` of the given configuration @@ -127,25 +142,21 @@ private: * * @param C the configuration based on which the two sets `ex(C)` and `en(C)` are * computed - * @param e the event where UDPOR currently "rests", viz. the event UDPOR - * is now currently considering * @param prev_exC the previous value of `ex(C)`, viz. that which was computed for * the configuration `C' := C - {e}` * @returns a tuple containing the pair of sets `ex(C)` and `en(C)` respectively */ - std::tuple compute_extension(const Configuration& C, const std::list& max_evt_history, - UnfoldingEvent* e, const EventSet& prev_exC) const; + std::tuple compute_extension(const Configuration& C, const EventSet& prev_exC) const; /** * */ - StateHandle observe_unfolding_event(const UnfoldingEvent& event); + EventSet compute_partial_alternative(const EventSet& D, const Configuration& C, const unsigned k) const; /** - * @brief Resolves the state handle maintained by an event - * into a concrete reference to a state + * */ - State& get_state_referenced_by(const UnfoldingEvent& event); + void move_to_stateCe(State& stateC, const UnfoldingEvent& e); /** * @brief Creates a new snapshot of the state of the progam undergoing @@ -155,26 +166,12 @@ private: * exploration of the unfolding. You provide this handle to an event in the * unfolding to regenerate past states */ - StateHandle record_current_state(); - - /** - * @brief Identifies the next event from the unfolding of the concurrent system - * that should next be explored as an extension of a configuration with - * enabled events `enC` - * - * @param A The set of events `A` maintained by the UDPOR algorithm to help - * determine how events should be selected. See the original paper [1] for more details - * - * @param enC The set `enC` of enabled events from the extension set `exC` used - * by the UDPOR algorithm to select new events to search. See the original - * paper [1] for more details - */ - UnfoldingEvent* select_next_unfolding_event(const EventSet& A, const EventSet& enC); + std::unique_ptr record_current_state(); /** * */ - EventSet compute_partial_alternative(const EventSet& D, const Configuration& C, const unsigned k) const; + void restore_program_state_to(const State& stateC); /** * diff --git a/src/mc/explo/udpor/UnfoldingEvent.cpp b/src/mc/explo/udpor/UnfoldingEvent.cpp index fd4d27309f..a2ab912e00 100644 --- a/src/mc/explo/udpor/UnfoldingEvent.cpp +++ b/src/mc/explo/udpor/UnfoldingEvent.cpp @@ -7,16 +7,10 @@ namespace simgrid::mc::udpor { -UnfoldingEvent::UnfoldingEvent(unsigned int nb_events, std::string const& trans_tag, EventSet const& immediate_causes) - : UnfoldingEvent(nb_events, trans_tag, immediate_causes, 0) +UnfoldingEvent::UnfoldingEvent(std::shared_ptr transition, EventSet immediate_causes, + unsigned long event_id) + : associated_transition(std::move(transition)), immediate_causes(std::move(immediate_causes)), event_id(event_id) { - // TODO: Implement this correctly -} - -UnfoldingEvent::UnfoldingEvent(unsigned int nb_events, std::string const& trans_tag, EventSet const& immediate_causes, - StateHandle sid) -{ - // TODO: Implement this } bool UnfoldingEvent::operator==(const UnfoldingEvent&) const diff --git a/src/mc/explo/udpor/UnfoldingEvent.hpp b/src/mc/explo/udpor/UnfoldingEvent.hpp index 5604362d21..812f02004c 100644 --- a/src/mc/explo/udpor/UnfoldingEvent.hpp +++ b/src/mc/explo/udpor/UnfoldingEvent.hpp @@ -8,16 +8,17 @@ #include "src/mc/explo/udpor/EventSet.hpp" #include "src/mc/explo/udpor/udpor_forward.hpp" +#include "src/mc/transition/Transition.hpp" +#include #include namespace simgrid::mc::udpor { class UnfoldingEvent { public: - UnfoldingEvent(unsigned int nb_events, std::string const& trans_tag, EventSet const& immediate_causes, - StateHandle sid); - UnfoldingEvent(unsigned int nb_events, std::string const& trans_tag, EventSet const& immediate_causes); + UnfoldingEvent(std::shared_ptr transition, EventSet immediate_causes, unsigned long event_id = 0); + UnfoldingEvent(const UnfoldingEvent&) = default; UnfoldingEvent& operator=(UnfoldingEvent const&) = default; UnfoldingEvent(UnfoldingEvent&&) = default; @@ -29,13 +30,23 @@ public: bool conflicts_with(const Configuration& config) const; bool immediately_conflicts_with(const UnfoldingEvent* otherEvt) const; - inline StateHandle get_state_id() const { return state_id; } - inline void set_state_id(StateHandle sid) { state_id = sid; } + Transition* get_transition() const { return this->associated_transition.get(); } bool operator==(const UnfoldingEvent&) const; private: - int id = -1; + /** + * @brief The transition that UDPOR "attaches" to this + * specific event for later use while computing e.g. extension + * sets + * + * The transition points to that of a particular actor + * in the state reached by the configuration C (recall + * this is denoted `state(C)`) that excludes this event. + * In other words, this transition was the "next" event + * of the actor that executes it in `state(C)`. + */ + std::shared_ptr associated_transition; /** * @brief The "immediate" causes of this event. @@ -54,7 +65,8 @@ private: * so on. */ EventSet immediate_causes; - StateHandle state_id = 0ul; + + unsigned long event_id = 0; }; } // namespace simgrid::mc::udpor diff --git a/src/mc/explo/udpor/udpor_forward.hpp b/src/mc/explo/udpor/udpor_forward.hpp index 6dff0eb5b5..ab28a5a970 100644 --- a/src/mc/explo/udpor/udpor_forward.hpp +++ b/src/mc/explo/udpor/udpor_forward.hpp @@ -17,6 +17,7 @@ class EventSet; class UnfoldingEvent; class Configuration; class StateManager; +class Unfolding; using StateHandle = unsigned long long; } // namespace simgrid::mc::udpor -- 2.20.1