From a5bb6aa5b6d52231221a808537688e5ed1b7e8ec Mon Sep 17 00:00:00 2001 From: Maxwell Pirtle Date: Wed, 3 May 2023 09:34:12 +0200 Subject: [PATCH] Add tentatively-working SDPOR implementation This commit introduces SDPOR into SimGrid (well, mostly). The current implementation will be improved upon by cleaning up some of the code that was added to improve its testability --- src/mc/explo/DFSExplorer.cpp | 30 ++++++++--- src/mc/explo/odpor/Execution.cpp | 89 +++++++++++++++++++++++++++++--- src/mc/explo/odpor/Execution.hpp | 8 +++ 3 files changed, 112 insertions(+), 15 deletions(-) diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp index 48376263f2..c52b0fec1c 100644 --- a/src/mc/explo/DFSExplorer.cpp +++ b/src/mc/explo/DFSExplorer.cpp @@ -92,6 +92,11 @@ void DFSExplorer::restore_stack(std::shared_ptr state) stack_.emplace_front(current_state); } XBT_DEBUG("Replaced stack by %s", get_record_trace().to_string().c_str()); + + if (reduction_mode_ == ReductionMode::sdpor) { + execution_seq_ = execution_seq_.get_prefix_up_to(stack_.size()); + XBT_DEBUG("Additionally replaced corresponding SDPOR execution stack"); + } } void DFSExplorer::log_state() // override @@ -266,25 +271,36 @@ void DFSExplorer::run() // 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); + 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::vector v; 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) { + // happen after `racing_event_handle` is a member of `v`. + // In addition to marking the event in `v`, we also "simulate" running + // the action `v` from E'. + if (not execution_seq_.happens_before(racing_event_handle, e_prime) or e_prime == next_E_p) { v.push_back(e_prime); + E_prime_v.push_transition(execution_seq_.get_event_with_handle(e_prime).get_transition()); + } else { + continue; } - const aid_t q = E_prime_v.get_actor_with_handle(e_prime); + + xbt_assert(E_prime_v.get_latest_event_handle().has_value(), + "No events are contained in the SDPOR/OPDPOR execution " + "even though one was just added"); + const sdpor::Execution::EventHandle e_prime_in_E_prime = E_prime_v.get_latest_event_handle().value(); + + const aid_t q = E_prime_v.get_actor_with_handle(e_prime_in_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); + const bool is_initial = std::none_of(v.begin(), v.end(), [&](const auto& e_star) { + return E_prime_v.happens_before(e_star, e_prime_in_E_prime); }); if (is_initial) { if (not prev_state->is_actor_done(q)) { diff --git a/src/mc/explo/odpor/Execution.cpp b/src/mc/explo/odpor/Execution.cpp index 34c5e0de66..cc722f0a79 100644 --- a/src/mc/explo/odpor/Execution.cpp +++ b/src/mc/explo/odpor/Execution.cpp @@ -4,26 +4,99 @@ * under the terms of the license (GNU LGPL) which comes with this package. */ #include "src/mc/explo/odpor/Execution.hpp" +#include +#include namespace simgrid::mc::odpor { -std::unordered_set Execution::get_racing_events_of(Execution::EventHandle e1) const +std::unordered_set Execution::get_racing_events_of(Execution::EventHandle target) const { - return {}; + std::unordered_set racing_events; + std::unordered_set disqualified_events; + + // For each event of the execution + for (auto e_i = target; e_i > 0 && e_i != std::numeric_limits::max(); e_i--) { + // We need `e_i -->_E target` as a necessary condition + if (not happens_before(e_i, target)) { + continue; + } + + // Further, `proc(e_i) != proc(target)` + if (get_actor_with_handle(e_i) == get_actor_with_handle(target)) { + disqualified_events.insert(e_i); + continue; + } + + // There could an event that "happens-between" the two events which would discount `e_i` as a race + for (auto e_j = e_i; e_j < target; e_j++) { + // If both: + // 1. e_i --->_E e_j; and + // 2. disqualified_events.count(e_j) > 0 + // then e_i --->_E target indirectly (either through + // e_j directly, or transitively through e_j) + if (happens_before(e_i, e_j) and disqualified_events.count(e_j) > 0) { + disqualified_events.insert(e_i); + break; + } + } + + // If `e_i` wasn't disqualified in the last round, + // it's in a race with `target`. After marking it + // as such, we ensure no other event `e` can happen-before + // it (since this would transitively make it the event + // which "happens-between" `target` and `e`) + if (disqualified_events.count(e_i) == 0) { + racing_events.insert(e_i); + disqualified_events.insert(e_i); + } + } + + return racing_events; } -bool Execution::happens_before(Execution::EventHandle e1, Execution::EventHandle e2) const +bool Execution::happens_before(Execution::EventHandle e1_handle, Execution::EventHandle e2_handle) const { - return true; + // 1. "happens-before" is a subset of "occurs before" + if (e1_handle > e2_handle) { + return false; + } + + // Each execution maintains a stack of clock vectors which are updated + // according to the procedure outlined in section 4 of the original DPOR paper + const Event& e2 = get_event_with_handle(e2_handle); + const aid_t proc_e1 = get_actor_with_handle(e1_handle); + return e1_handle <= e2.get_clock_vector().get(proc_e1).value_or(0); } -Execution Execution::get_prefix_up_to(Execution::EventHandle) +Execution Execution::get_prefix_up_to(Execution::EventHandle handle) { - return *this; + if (handle == static_cast(0)) { + return Execution(); + } + return Execution(std::vector{contents_.begin(), contents_.begin() + (handle - 1)}); } -void Execution::pop_latest() {} +void Execution::push_transition(const Transition* 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)) { + max_clock_vector = ClockVector::max(max_clock_vector, e.get_clock_vector()); + } + } + // The entry in the vector for `t->aid_` is the size + // of the new stack, which will have a size one greater + // than that before we insert the new events + max_clock_vector[t->aid_] = this->size() + 1; + contents_.push_back(Event({t, max_clock_vector})); +} -void Execution::push_transition(const Transition*) {} +void Execution::pop_latest() +{ + contents_.pop_back(); +} } // 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 fc75fa997a..4a5c2c50e2 100644 --- a/src/mc/explo/odpor/Execution.hpp +++ b/src/mc/explo/odpor/Execution.hpp @@ -79,6 +79,8 @@ private: */ std::vector contents_; + Execution(std::vector&& contents) : contents_(std::move(contents)) {} + public: using Handle = decltype(contents_)::const_iterator; using EventHandle = uint32_t; @@ -129,6 +131,12 @@ public: * `e1 --->_E e2` * * where `E` is this execution + * + * @note: The happens-before relation computed by this + * execution is "coarse" in the sense that context-sensitive + * independence is not exploited. To include such context-sensitive + * dependencies requires a new method of keeping track of + * the happens-before procedure, which is nontrivial... */ bool happens_before(EventHandle e1, EventHandle e2) const; -- 2.20.1