From: Maxwell Pirtle Date: Wed, 24 May 2023 11:09:05 +0000 (+0200) Subject: Add reversible race calculator X-Git-Tag: v3.34~68^2~17 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/cc5bf26ad13a2d285a6f416a4e54ce95a01bf180 Add reversible race calculator Determining whether or not a race between two events is reversible is a critical component of ODPOR. It turns out that we need to specialize the race detection to the action types themselves. Knowing the types of the transitions will help us determine whether the race is reversible. --- diff --git a/MANIFEST.in b/MANIFEST.in index 6ed7f62e48..b9ca4f9299 100644 --- a/MANIFEST.in +++ b/MANIFEST.in @@ -2195,6 +2195,8 @@ include src/mc/explo/odpor/ClockVector_test.cpp include src/mc/explo/odpor/Execution.cpp include src/mc/explo/odpor/Execution.hpp include src/mc/explo/odpor/Execution_test.cpp +include src/mc/explo/odpor/ReversibleRaceCalculator.cpp +include src/mc/explo/odpor/ReversibleRaceCalculator.hpp include src/mc/explo/odpor/WakeupTree.cpp include src/mc/explo/odpor/WakeupTree.hpp include src/mc/explo/odpor/WakeupTree_test.cpp diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp index 5844878650..cdc31dfc28 100644 --- a/src/mc/explo/DFSExplorer.cpp +++ b/src/mc/explo/DFSExplorer.cpp @@ -295,37 +295,22 @@ 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" */ - 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 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 - // `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 - // - // If the actor `p` is not enabled at s_[E'], it is not a *reversible* race + for (const auto racing_event_handle : execution_seq_.get_reversible_races_of(next_E_p)) { const std::shared_ptr prev_state = stack_[racing_event_handle]; - if (prev_state->is_actor_enabled(p)) { - // NOTE: To incorporate the idea of attempting to select the "best" - // backtrack point into SDPOR, instead of selecting the `first` initial, - // we should instead compute all choices and decide which is best - const std::optional q = - execution_seq_.get_first_sdpor_initial_from(racing_event_handle, prev_state->get_backtrack_set()); - if (q.has_value()) { - prev_state->consider_one(q.value()); - opened_states_.emplace_back(std::move(prev_state)); - } + // NOTE: To incorporate the idea of attempting to select the "best" + // backtrack point into SDPOR, instead of selecting the `first` initial, + // we should instead compute all choices and decide which is best + if (const auto q = + execution_seq_.get_first_sdpor_initial_from(racing_event_handle, prev_state->get_backtrack_set()); + q.has_value()) { + prev_state->consider_one(q.value()); + opened_states_.emplace_back(std::move(prev_state)); } } } else if (reduction_mode_ == ReductionMode::odpor) { @@ -437,27 +422,14 @@ void DFSExplorer::backtrack() * relation) */ for (auto e_prime = static_cast(0); e_prime <= last_event.value(); ++e_prime) { - for (const auto e : execution_seq_.get_racing_events_of(e_prime)) { - // To determine if the race is reversible, we have to ensure - // that actor `p` running `e_i` (viz. the event such that - // `racing_event -> (E_p) e_i` and no other event - // "happens-between" the two) is enabled in any equivalent - // execution where `racing_event` happens before `e_i`. - // - // 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 - // - // If the actor `p` is not enabled at s_[E'], it is not a *reversible* race - const aid_t p = execution_seq_.get_actor_with_handle(e_prime); + for (const auto e : execution_seq_.get_reversible_races_of(e_prime)) { + XBT_DEBUG("ODPOR: Reversible race detected between events `%u` and `%u`", e, e_prime); State& prev_state = *stack_[e]; - if (prev_state.is_actor_enabled(p)) { - const std::optional v = - execution_seq_.get_odpor_extension_from(e, e_prime, prev_state); - if (v.has_value()) { - prev_state.mark_path_interesting_for_odpor(v.value(), execution_seq_.get_prefix_before(e)); - } + if (const auto v = execution_seq_.get_odpor_extension_from(e, e_prime, prev_state); v.has_value()) { + XBT_DEBUG("ODPOR: Reversible race unaccounted for in the wakeup tree for " + "the execution prior to event `%u`, inserting a sequence", + e); + prev_state.mark_path_interesting_for_odpor(v.value(), execution_seq_.get_prefix_before(e)); } } } diff --git a/src/mc/explo/odpor/Execution.cpp b/src/mc/explo/odpor/Execution.cpp index e514141d4b..c95b36ef06 100644 --- a/src/mc/explo/odpor/Execution.cpp +++ b/src/mc/explo/odpor/Execution.cpp @@ -72,6 +72,12 @@ std::unordered_set Execution::get_racing_events_of(Execu return racing_events; } +std::unordered_set Execution::get_reversible_races_of(EventHandle handle) const +{ + // TODO: Implement this + return std::unordered_set{}; +} + Execution Execution::get_prefix_before(Execution::EventHandle handle) const { return Execution(std::vector{contents_.begin(), contents_.begin() + handle}); diff --git a/src/mc/explo/odpor/Execution.hpp b/src/mc/explo/odpor/Execution.hpp index cfe24bd544..bbdaf971fd 100644 --- a/src/mc/explo/odpor/Execution.hpp +++ b/src/mc/explo/odpor/Execution.hpp @@ -262,6 +262,25 @@ public: */ std::unordered_set get_racing_events_of(EventHandle handle) const; + /** + * @brief Returns a set of events which are in a reversible + * race with the given event handle `handle` + * + * Two events `e` and `e'` in an execution `E` are said to + * be in a reversible race iff + * + * 1. `e` and `e'` race + * 2. In any equivalent execution sequence `E'` to `E` + * where `e` occurs immediately before `e'`, the actor + * running `e'` was enabled in the state prior to `e` + * + * @param handle the event with respect to which + * reversible races are computed + * @returns a set of event handles from which are in a reversible + * race with `handle` + */ + std::unordered_set get_reversible_races_of(EventHandle handle) const; + /** * @brief Computes `pre(e, E)` as described in ODPOR [1] * diff --git a/src/mc/explo/odpor/ReversibleRaceCalculator.cpp b/src/mc/explo/odpor/ReversibleRaceCalculator.cpp new file mode 100644 index 0000000000..e69de29bb2 diff --git a/src/mc/explo/odpor/ReversibleRaceCalculator.hpp b/src/mc/explo/odpor/ReversibleRaceCalculator.hpp new file mode 100644 index 0000000000..1396af9c59 --- /dev/null +++ b/src/mc/explo/odpor/ReversibleRaceCalculator.hpp @@ -0,0 +1,43 @@ +/* Copyright (c) 2007-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. */ + +#ifndef SIMGRID_MC_ODPOR_REVERSIBLE_RACE_CALCULATOR_HPP +#define SIMGRID_MC_ODPOR_REVERSIBLE_RACE_CALCULATOR_HPP + +#include "src/mc/explo/udpor/EventSet.hpp" +#include "src/mc/explo/udpor/udpor_forward.hpp" +#include "src/mc/transition/Transition.hpp" +#include "src/mc/transition/TransitionActorJoin.hpp" +#include "src/mc/transition/TransitionAny.hpp" +#include "src/mc/transition/TransitionComm.hpp" +#include "src/mc/transition/TransitionObjectAccess.hpp" +#include "src/mc/transition/TransitionRandom.hpp" +#include "src/mc/transition/TransitionSynchro.hpp" + +#include + +namespace simgrid::mc::odpor { + +/** + * @brief Computes whether a race between two events + * in a given execution is a reversible race. + * + * @note: All of the methods assume that there is + * indeed a race between the two events in the + * execution; indeed, the question the method answers + * is only sensible in the context of a race + */ +struct ReversibleRaceCalculator final { + static EventSet is_race_reversible(const Execution&, Execution::Handle e1, std::shared_ptr); + static EventSet is_race_reversible(const Execution&, Execution::Handle e1, std::shared_ptr); + static EventSet is_race_reversible(const Execution&, Execution::Handle e1, std::shared_ptr); + static EventSet is_race_reversible(const Execution&, Execution::Handle e1, std::shared_ptr); + +public: + static EventSet is_race_reversible(const Execution&, Execution::Handle e1, Execution::Handle e2); +}; + +} // namespace simgrid::mc::odpor +#endif diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake index c395235315..35be16c7a5 100644 --- a/tools/cmake/DefinePackages.cmake +++ b/tools/cmake/DefinePackages.cmake @@ -537,6 +537,8 @@ set(MC_SRC_STATELESS src/mc/explo/odpor/Execution.cpp src/mc/explo/odpor/Execution.hpp + src/mc/explo/odpor/ReversibleRaceCalculator.cpp + src/mc/explo/odpor/ReversibleRaceCalculator.hpp src/mc/explo/odpor/WakeupTree.cpp src/mc/explo/odpor/WakeupTree.hpp src/mc/explo/odpor/WakeupTreeIterator.cpp