From 222bdffb8f8c4d7e5660c049c2c2bdadd8f7cc07 Mon Sep 17 00:00:00 2001 From: Maxwell Pirtle Date: Tue, 2 May 2023 12:38:43 +0200 Subject: [PATCH] Add initial outline of SDPOR implementation The SDPOR algorithm is nearing an implementation into SimGrid (sans a few technical details and code clean ups that will be nice to add). The algorithm largely builds off the existing infrastructure of DFSExplorer fortunately. --- src/mc/api/State.cpp | 13 +++++ src/mc/api/State.hpp | 1 + src/mc/explo/DFSExplorer.cpp | 73 ++++++++++++++++++++++++- src/mc/explo/DFSExplorer.hpp | 10 +++- src/mc/explo/odpor/Execution.cpp | 29 ++++++++++ src/mc/explo/odpor/Execution.hpp | 81 +++++++++++++++++++--------- src/mc/explo/odpor/odpor_forward.hpp | 12 ++++- 7 files changed, 190 insertions(+), 29 deletions(-) diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp index a178f55aef..aa315cf17e 100644 --- a/src/mc/api/State.cpp +++ b/src/mc/api/State.cpp @@ -9,6 +9,7 @@ #include "src/mc/explo/Exploration.hpp" #include "src/mc/mc_config.hpp" +#include #include XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_state, mc, "Logging specific to MC states"); @@ -160,4 +161,16 @@ std::shared_ptr State::execute_next(aid_t next, RemoteApp& app) return outgoing_transition_; } + +std::unordered_set State::get_todo_actors() const +{ + std::unordered_set actors; + for (const auto& [aid, state] : get_actors_list()) { + if (state.is_todo()) { + actors.insert(aid); + } + } + return actors; +} + } // namespace simgrid::mc diff --git a/src/mc/api/State.hpp b/src/mc/api/State.hpp index 0bbc686b77..6e963ca276 100644 --- a/src/mc/api/State.hpp +++ b/src/mc/api/State.hpp @@ -86,6 +86,7 @@ public: Snapshot* get_system_state() const { return system_state_.get(); } void set_system_state(std::shared_ptr state) { system_state_ = std::move(state); } + std::unordered_set get_todo_actors() const; std::map const& get_sleep_set() const { return sleep_set_; } void add_sleep_set(std::shared_ptr t) { diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp index a8faec6fd7..48376263f2 100644 --- a/src/mc/explo/DFSExplorer.cpp +++ b/src/mc/explo/DFSExplorer.cpp @@ -22,8 +22,10 @@ #include #include +#include #include #include +#include #include XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dfs, mc, "DFS exploration algorithm of the model-checker"); @@ -168,7 +170,7 @@ void DFSExplorer::run() } /* Actually answer the request: let's execute the selected request (MCed does one step) */ - state->execute_next(next, get_remote_app()); + const auto executed_transition = state->execute_next(next, get_remote_app()); on_transition_execute_signal(state->get_transition_out().get(), get_remote_app()); // If there are processes to interleave and the maximum depth has not been @@ -229,6 +231,72 @@ void DFSExplorer::run() } tmp_stack.pop_back(); } + } else if (reduction_mode_ == ReductionMode::sdpor) { + /** + * SDPOR Source Set Procedure: + */ + execution_seq_.push_transition(executed_transition.get()); + + // To determine if the race is reversible, we have to ensure + // that actor `p` running `next_E_p` (viz. the event such that + // `racing_event -> (E_p) next_E_p` and no other event + // "happens-between" the two) is enabled in any equivalent + // execution where `racing_event` happens before `next_E_p`. + // + // Importantly, it is equivalent to checking if in ANY + // such equivalent execution sequence where `racing_event` + // happens-before `next_E_p` that `p` is enabled in `pre(racing_event, E.p)`. + // Thus it suffices to check THIS execution + 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(); + + for (const auto racing_event_handle : execution_seq_.get_racing_events_of(next_E_p)) { + // If the actor `p` is not enabled at s_[E'], it is not a *reversible* race + const std::shared_ptr prev_state = stack_[racing_event_handle]; + if (not prev_state->is_actor_enabled(p)) { + continue; + } + + // This is a reversible race! First, grab `E' := pre(e, E)` + // TODO: Instead of copying around these big structs, it + // would behoove us to incorporate some way to reference + // portions of an execution. For simplicity and for a + // "proof of concept" version, we opt to simply copy + // the contents instead of making a view into the execution + const sdpor::Execution E_prime_v = execution_seq_.get_prefix_up_to(racing_event_handle); + + // The vector `v` is constructed as `v := notdep(e, E) + std::vector v(execution_seq_.size()); + std::unordered_set disqualified_actors = state->get_todo_actors(); + + for (auto e_prime = racing_event_handle; e_prime <= next_E_p; ++e_prime) { + // Any event `e` which occurs after `racing_event_handle` but which does not + // happen after `racing_event_handle` is a member of `v` + if (not E_prime_v.happens_before(racing_event_handle, e_prime) or e_prime == next_E_p) { + v.push_back(e_prime); + } + const aid_t q = E_prime_v.get_actor_with_handle(e_prime); + if (disqualified_actors.count(q) > 0) { + continue; + } + + const bool is_initial = std::none_of(v.begin(), v.end(), [&E_prime_v, e_prime](const auto& e_star) { + return E_prime_v.happens_before(e_star, e_prime); + }); + if (is_initial) { + if (not prev_state->is_actor_done(q)) { + prev_state->consider_one(q); + opened_states_.emplace_back(std::move(prev_state)); + } + break; + } else { + disqualified_actors.insert(q); + } + } + } } // Before leaving that state, if the transition we just took can be taken multiple times, we @@ -240,7 +308,8 @@ void DFSExplorer::run() this->check_non_termination(next_state.get()); #if SIMGRID_HAVE_STATEFUL_MC - /* Check whether we already explored next_state in the past (but only if interested in state-equality reduction) */ + /* Check whether we already explored next_state in the past (but only if interested in state-equality reduction) + */ if (_sg_mc_max_visited_states > 0) visited_state_ = visited_states_.addVisitedState(next_state->get_num(), next_state.get(), get_remote_app()); #endif diff --git a/src/mc/explo/DFSExplorer.hpp b/src/mc/explo/DFSExplorer.hpp index 087e06f13c..320754dc35 100644 --- a/src/mc/explo/DFSExplorer.hpp +++ b/src/mc/explo/DFSExplorer.hpp @@ -9,11 +9,13 @@ #include "src/mc/api/ClockVector.hpp" #include "src/mc/api/State.hpp" #include "src/mc/explo/Exploration.hpp" +#include "src/mc/explo/odpor/Execution.hpp" #if SIMGRID_HAVE_STATEFUL_MC #include "src/mc/VisitedState.hpp" #endif +#include #include #include #include @@ -23,7 +25,7 @@ namespace simgrid::mc { -using stack_t = std::list>; +using stack_t = std::deque>; class XBT_PRIVATE DFSExplorer : public Exploration { XBT_DECLARE_ENUM_CLASS(ReductionMode, none, dpor, sdpor); @@ -96,6 +98,12 @@ private: /** Stack representing the position in the exploration graph */ stack_t stack_; + /** + * Provides additional metadata about the position in the exploration graph + * which is used by SDPOR and ODPOR + */ + odpor::Execution execution_seq_; + /** Per-actor clock vectors used to compute the "happens-before" relation */ std::unordered_map per_actor_clocks_; diff --git a/src/mc/explo/odpor/Execution.cpp b/src/mc/explo/odpor/Execution.cpp index e69de29bb2..34c5e0de66 100644 --- a/src/mc/explo/odpor/Execution.cpp +++ b/src/mc/explo/odpor/Execution.cpp @@ -0,0 +1,29 @@ +/* Copyright (c) 2008-2023. The SimGrid Team. All rights reserved. */ + +/* This program is free software; you can redistribute it and/or modify it + * under the terms of the license (GNU LGPL) which comes with this package. */ + +#include "src/mc/explo/odpor/Execution.hpp" + +namespace simgrid::mc::odpor { + +std::unordered_set Execution::get_racing_events_of(Execution::EventHandle e1) const +{ + return {}; +} + +bool Execution::happens_before(Execution::EventHandle e1, Execution::EventHandle e2) const +{ + return true; +} + +Execution Execution::get_prefix_up_to(Execution::EventHandle) +{ + return *this; +} + +void Execution::pop_latest() {} + +void Execution::push_transition(const Transition*) {} + +} // namespace simgrid::mc::odpor \ No newline at end of file diff --git a/src/mc/explo/odpor/Execution.hpp b/src/mc/explo/odpor/Execution.hpp index 3b8ebca348..fc75fa997a 100644 --- a/src/mc/explo/odpor/Execution.hpp +++ b/src/mc/explo/odpor/Execution.hpp @@ -7,9 +7,11 @@ #define SIMGRID_MC_ODPOR_EXECUTION_HPP #include "src/mc/api/ClockVector.hpp" +#include "src/mc/explo/odpor/odpor_forward.hpp" #include "src/mc/transition/Transition.hpp" -#include +#include +#include #include #include @@ -26,17 +28,16 @@ class Event { std::pair contents_; public: - Event() = default; - Event(Event&&) = default; - Event(const Event&) = default; - Event& operator=(const Event&) = default; - Event& operator=(const Event&&) = default; + Event() = default; + Event(Event&&) = default; + Event(const Event&) = default; + Event& operator=(const Event&) = default; explicit Event(std::pair pair) : contents_(std::move(pair)) {} - const Transition* get_transition() const { return contents_.get<0>(); } - const ClockVector& get_clock_vector() const { return contents_.get<1>(); } -} + const Transition* get_transition() const { return std::get<0>(contents_); } + const ClockVector& get_clock_vector() const { return std::get<1>(contents_); } +}; /** * @brief An ordered sequence of transitions which describe @@ -71,8 +72,16 @@ public: * the two concepts are analogous if not identical */ class Execution { +private: + /** + * @brief The actual steps that are taken by the process + * during exploration, relative to the + */ + std::vector contents_; + public: - using Handle = decltype(contents_)::const_iterator; + using Handle = decltype(contents_)::const_iterator; + using EventHandle = uint32_t; Execution() = default; Execution(const Execution&) = default; @@ -88,6 +97,41 @@ public: bool is_initial(aid_t p, const Hypothetical& w) const; bool is_weak_initial(aid_t p, const Hypothetical& w) const; + const Event& get_event_with_handle(EventHandle handle) const { return contents_[handle]; } + aid_t get_actor_with_handle(EventHandle handle) const { return get_event_with_handle(handle).get_transition()->aid_; } + + /** + * @brief Returns a set of IDs of events which are in + * "immediate conflict" (according to the definition given + * in the ODPOR paper) with one another + */ + std::unordered_set get_racing_events_of(EventHandle) const; + + /** + * @brief Returns a handle to the newest event of the execution, + * if such an event exists + */ + std::optional get_latest_event_handle() const + { + return contents_.empty() ? std::nullopt : std::optional{static_cast(size() - 1)}; + } + + Execution get_prefix_up_to(EventHandle); + + /** + * @brief Whether the event represented by `e1` + * "happens-before" the event represented by + * `e2` in the context of this execution + * + * In the terminology of the ODPOR paper, + * this function computes + * + * `e1 --->_E e2` + * + * where `E` is this execution + */ + bool happens_before(EventHandle e1, EventHandle e2) const; + /** * @brief Removes the last event of the execution, * if such an event exists @@ -108,23 +152,10 @@ public: */ void push_transition(const Transition*); - size_t size() const { return this->contents_.size(); } - size_t size() const { return this->contents_.size(); } - -private: - /** - * @brief A pointer into the execution off of which this - * execution extends computation - * - * Conceptually, the `prior` - */ - std::optional prior; - /** - * @brief The actual steps that are taken by the process - * during exploration, relative to the + * @brief The total number of steps contained in the execution */ - std::list contents_; + size_t size() const { return this->contents_.size(); } }; } // namespace simgrid::mc::odpor diff --git a/src/mc/explo/odpor/odpor_forward.hpp b/src/mc/explo/odpor/odpor_forward.hpp index 65810615b9..1a439c1855 100644 --- a/src/mc/explo/odpor/odpor_forward.hpp +++ b/src/mc/explo/odpor/odpor_forward.hpp @@ -18,10 +18,20 @@ namespace simgrid::mc::odpor { class Event; class Execution; -class ExecutionSequence; class ExecutionView; class WakeupTree; } // namespace simgrid::mc::odpor +namespace simgrid::mc { + +// Permit ODPOR or SDPOR to be used as namespaces +// Many of the structures overlap, so it doesn't +// make sense to some in one and not the other. +// Having one for each algorithm makes the corresponding +// code easier to read +namespace sdpor = simgrid::mc::odpor; + +} // namespace simgrid::mc + #endif -- 2.20.1