From ecccd1691488e7e0644dcf321822c428839e35be Mon Sep 17 00:00:00 2001 From: Maxwell Pirtle Date: Fri, 12 May 2023 10:11:33 +0200 Subject: [PATCH] Use `std::shared_ptr` for Execution Prior to this commit, the `Execution` class maintained raw pointers to the transitions maintained by the stack used in DFSExplorer. Instead, we opt for the execution to contain a collection of shared pointers to facilitate the creation of partial executions --- src/mc/explo/DFSExplorer.cpp | 11 +++++------ src/mc/explo/odpor/Execution.cpp | 22 +++++++++++----------- src/mc/explo/odpor/Execution.hpp | 10 +++++----- 3 files changed, 21 insertions(+), 22 deletions(-) diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp index 849055bd41..e654056185 100644 --- a/src/mc/explo/DFSExplorer.cpp +++ b/src/mc/explo/DFSExplorer.cpp @@ -104,7 +104,7 @@ void DFSExplorer::restore_stack(std::shared_ptr state) // when reconstructing the Exploration for SDPOR. for (auto iter = stack_.begin(); iter != stack_.end() - 1 and iter != stack_.end(); ++iter) { const auto& state = *(iter); - execution_seq_.push_transition(state->get_transition_out().get()); + execution_seq_.push_transition(state->get_transition_out()); } } XBT_DEBUG("Additionally replaced corresponding SDPOR execution stack"); @@ -295,14 +295,13 @@ void DFSExplorer::run() * The intuition is that some subsequence of `v` may enable `p`, so * we want to be sure that search "in that direction" */ - execution_seq_.push_transition(executed_transition.get()); - + const aid_t p = executed_transition->aid_; + execution_seq_.push_transition(std::move(executed_transition)); xbt_assert(execution_seq_.get_latest_event_handle().has_value(), "No events are contained in the SDPOR/OPDPOR execution " "even though one was just added"); - const aid_t p = executed_transition->aid_; - const auto next_E_p = execution_seq_.get_latest_event_handle().value(); + const auto next_E_p = execution_seq_.get_latest_event_handle().value(); for (const auto racing_event_handle : execution_seq_.get_racing_events_of(next_E_p)) { // To determine if the race is reversible, we have to ensure // that actor `p` running `next_E_p` (viz. the event such that @@ -332,7 +331,7 @@ void DFSExplorer::run() } else if (reduction_mode_ == ReductionMode::odpor) { // In the case of ODPOR, we simply observe the transition that was executed // until we've reached a maximal trace - execution_seq_.push_transition(executed_transition.get()); + execution_seq_.push_transition(std::move(executed_transition)); } // Before leaving that state, if the transition we just took can be taken multiple times, we diff --git a/src/mc/explo/odpor/Execution.cpp b/src/mc/explo/odpor/Execution.cpp index 57c00a36e5..dbf215eb26 100644 --- a/src/mc/explo/odpor/Execution.cpp +++ b/src/mc/explo/odpor/Execution.cpp @@ -11,19 +11,19 @@ namespace simgrid::mc::odpor { -void Execution::push_transition(const Transition* t) +void Execution::push_transition(std::shared_ptr t) { if (t == nullptr) { throw std::invalid_argument("Unexpectedly received `nullptr`"); } ClockVector max_clock_vector; for (const Event& e : this->contents_) { - if (e.get_transition()->depends(t)) { + if (e.get_transition()->depends(t.get())) { max_clock_vector = ClockVector::max(max_clock_vector, e.get_clock_vector()); } } max_clock_vector[t->aid_] = this->size(); - contents_.push_back(Event({t, max_clock_vector})); + contents_.push_back(Event({std::move(t), max_clock_vector})); } std::unordered_set Execution::get_racing_events_of(Execution::EventHandle target) const @@ -160,7 +160,7 @@ bool Execution::is_initial_after_execution(const PartialExecution& w, aid_t p) c std::vector w_handles; for (const auto& w_i : w) { // Take one step in the direction of `w` - E_w.push_transition(w_i.get()); + E_w.push_transition(w_i); // If that step happened to be executed by `p`, // great: we know that `p` is contained in `w`. @@ -177,7 +177,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, const Transition* next_E_p) const +bool Execution::is_independent_with_execution(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 @@ -187,14 +187,14 @@ bool Execution::is_independent_with_execution(const PartialExecution& w, const T // `v := notdep(e, E)` for some execution `E` and event `e` of // that execution. auto E_p_w = *this; - E_p_w.push_transition(next_E_p); + E_p_w.push_transition(std::move(next_E_p)); const auto p_handle = E_p_w.get_latest_event_handle().value(); // As we add events to `w`, verify that none // of them "happen-after" the event associated with // the step `next_E_p` (viz. p_handle) for (const auto& w_i : w) { - E_p_w.push_transition(w_i.get()); + E_p_w.push_transition(w_i); const auto w_i_handle = E_p_w.get_latest_event_handle().value(); if (E_p_w.happens_before(p_handle, w_i_handle)) { return false; @@ -211,8 +211,8 @@ std::optional Execution::get_shortest_odpor_sq_subset_insertio auto E_v = *this; auto w_now = w; - for (const auto& next_p_E : v) { - const aid_t p = next_p_E->aid_; + for (const auto& next_E_p : v) { + const aid_t p = next_E_p->aid_; // Is `p in `I_[E](w)`? if (E_v.is_initial_after_execution(w_now, p)) { @@ -239,7 +239,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_p_E.get())) { + else if (E_v.is_independent_with_execution(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 @@ -256,7 +256,7 @@ std::optional Execution::get_shortest_odpor_sq_subset_insertio } // Move one step forward in the direction of `v` and repeat - E_v.push_transition(next_p_E.get()); + E_v.push_transition(next_p_E); } // Construct, finally, v.w' by adding `v` to the front of diff --git a/src/mc/explo/odpor/Execution.hpp b/src/mc/explo/odpor/Execution.hpp index b0a7a50d31..ad818a6d15 100644 --- a/src/mc/explo/odpor/Execution.hpp +++ b/src/mc/explo/odpor/Execution.hpp @@ -25,16 +25,16 @@ namespace simgrid::mc::odpor { * actor `j` */ class Event { - std::pair contents_; + std::pair, ClockVector> contents_; public: Event() = default; Event(Event&&) = default; Event(const Event&) = default; Event& operator=(const Event&) = default; - explicit Event(std::pair pair) : contents_(std::move(pair)) {} + explicit Event(std::pair, ClockVector> pair) : contents_(std::move(pair)) {} - const Transition* get_transition() const { return std::get<0>(contents_); } + std::shared_ptr get_transition() const { return std::get<0>(contents_); } const ClockVector& get_clock_vector() const { return std::get<1>(contents_); } }; @@ -155,7 +155,7 @@ public: std::unordered_set enabled_actors) const; bool is_initial_after_execution(const PartialExecution& w, aid_t p) const; - bool is_independent_with_execution(const PartialExecution& w, const Transition* next_E_p) const; + bool is_independent_with_execution(const PartialExecution& w, std::shared_ptr next_E_p) const; /** * @brief Determines the event associated with @@ -239,7 +239,7 @@ public: * notation of [1]) `E.proc(t)` where `proc(t)` is the * actor which executed transition `t`. */ - void push_transition(const Transition*); + void push_transition(std::shared_ptr); }; } // namespace simgrid::mc::odpor -- 2.20.1