From f93ca07b547007d26fed4c9c4cb3aed290448205 Mon Sep 17 00:00:00 2001 From: Maxwell Pirtle Date: Fri, 17 Mar 2023 11:42:46 +0100 Subject: [PATCH] Begin tracking latest events for each actor Computing specialized extensions for each transition type frequently requires knowing the "latest" event that some given actor is associated with in some configuration (denoted `preEvt(C, a)`). We now track this information as new events are added and pre-compute the information when constructing a configuration with a set of events using once again our favorite topological ordering function. Subsequent commits will introduce some unit tests to ensure that the Configuration is tracking the new events appropriately. --- src/mc/explo/UdporChecker.cpp | 14 ++----- src/mc/explo/udpor/Configuration.cpp | 29 +++++++++++-- src/mc/explo/udpor/Configuration.hpp | 47 ++++++++++++++++++++++ src/mc/explo/udpor/Configuration_test.cpp | 34 +++++++++++----- src/mc/explo/udpor/Unfolding.cpp | 23 +++++------ src/mc/explo/udpor/Unfolding.hpp | 46 ++++++++++++--------- src/mc/explo/udpor/UnfoldingEvent.hpp | 1 + src/mc/explo/udpor/Unfolding_test.cpp | 25 ++---------- src/mc/explo/udpor/udpor_forward.hpp | 5 +++ src/mc/explo/udpor/udpor_tests_private.hpp | 6 +-- 10 files changed, 149 insertions(+), 81 deletions(-) diff --git a/src/mc/explo/UdporChecker.cpp b/src/mc/explo/UdporChecker.cpp index 98bab5e046..c7603372f4 100644 --- a/src/mc/explo/UdporChecker.cpp +++ b/src/mc/explo/UdporChecker.cpp @@ -16,10 +16,7 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_udpor, mc, "Logging specific to verification namespace simgrid::mc::udpor { -UdporChecker::UdporChecker(const std::vector& args) : Exploration(args, true) -{ - // Initialize the map -} +UdporChecker::UdporChecker(const std::vector& args) : Exploration(args, true) {} void UdporChecker::run() { @@ -165,12 +162,9 @@ EventSet UdporChecker::compute_exC_by_enumeration(const Configuration& C, const const bool enabled_at_config_k = false; if (enabled_at_config_k) { - auto candidate_handle = std::make_unique(maximal_subset, action); - if (auto candidate_event = candidate_handle.get(); not unfolding.contains_event_equivalent_to(candidate_event)) { - // This is a new event (i.e. one we haven't yet seen) - unfolding.insert(std::move(candidate_handle)); - incremental_exC.insert(candidate_event); - } + auto event = std::make_unique(maximal_subset, action); + const auto handle = unfolding.insert(std::move(event)); + incremental_exC.insert(handle); } } return incremental_exC; diff --git a/src/mc/explo/udpor/Configuration.cpp b/src/mc/explo/udpor/Configuration.cpp index 98d004b22d..7f7e80a15a 100644 --- a/src/mc/explo/udpor/Configuration.cpp +++ b/src/mc/explo/udpor/Configuration.cpp @@ -27,14 +27,20 @@ Configuration::Configuration(const UnfoldingEvent* e) : Configuration(e->get_his // check the invariant regardless as a sanity check } +Configuration::Configuration(const History& history) : Configuration(history.get_all_events()) {} + Configuration::Configuration(const EventSet& events) : events_(events) { if (!events_.is_valid_configuration()) { throw std::invalid_argument("The events do not form a valid configuration"); } -} -Configuration::Configuration(const History& history) : Configuration(history.get_all_events()) {} + // Since we add in topological order under `<`, we know that the "most-recent" + // transition executed by each actor will appear last + for (const UnfoldingEvent* e : get_topologically_sorted_events()) { + this->latest_event_mapping[e->get_actor()] = e; + } +} void Configuration::add_event(const UnfoldingEvent* e) { @@ -54,7 +60,8 @@ void Configuration::add_event(const UnfoldingEvent* e) } this->events_.insert(e); - this->newest_event = e; + this->newest_event = e; + this->latest_event_mapping[e->get_actor()] = e; // Preserves the property that the configuration is causally closed if (auto history = History(e); !this->events_.contains(history)) { @@ -190,4 +197,20 @@ std::optional Configuration::compute_k_partial_alternative_to(con return Configuration(History(map_events(*alternative))); } +std::optional Configuration::get_latest_event_of(aid_t aid) const +{ + if (const auto latest_event = latest_event_mapping.find(aid); latest_event != latest_event_mapping.end()) { + return std::optional{latest_event->second}; + } + return std::nullopt; +} + +std::optional Configuration::get_latest_action_of(aid_t aid) const +{ + if (const auto latest_event = get_latest_event_of(aid); latest_event.has_value()) { + return std::optional{latest_event.value()->get_transition()}; + } + return std::nullopt; +} + } // namespace simgrid::mc::udpor diff --git a/src/mc/explo/udpor/Configuration.hpp b/src/mc/explo/udpor/Configuration.hpp index 619871eac2..b3db77a1a7 100644 --- a/src/mc/explo/udpor/Configuration.hpp +++ b/src/mc/explo/udpor/Configuration.hpp @@ -10,6 +10,7 @@ #include "src/mc/explo/udpor/udpor_forward.hpp" #include +#include namespace simgrid::mc::udpor { @@ -134,6 +135,40 @@ public: */ EventSet get_minimally_reproducible_events() const; + /** + * @brief Determines the event in the configuration whose associated + * transition is the latest of the given actor + * + * @invariant: At most one event in the configuration will correspond + * to `preEvt(C, a)` for any action `a`. This can be argued by contradiction. + * + * If there were more than one event (`e` and `e'`) in any configuration whose + * associated transitions `a` were run by the same actor at the same step, then they + * could not be causally related (`<`) since `a` could not be enabled in + * both subconfigurations C' and C'' containing the hypothetical events + * `e` and `e` + `e'`. Since they would not be contained in each other's histories, + * they would be in conflict, which cannot happen between any pair of events + * in a configuration. Thus `e` and `e'` cannot exist simultaneously + */ + std::optional get_latest_event_of(aid_t) const; + /** + * @brief Determines the most recent transition of the given actor + * in this configuration, or `pre(a)` as denoted in the thesis of + * The Anh Pham + * + * Conceptually, the execution of an interleaving of the transitions + * (i.e. a topological ordering) of a configuration yields a unique + * state `state(C)`. Since actions taken by the same actor are always + * dependent with one another, any such interleaving always yields a + * unique + * + * @returns the most recent transition of the given actor + * in this configuration, or `std::nullopt` if there are no transitions + * in this configuration run by the given actor + */ + std::optional get_latest_action_of(aid_t aid) const; + std::optional pre_event(aid_t aid) const { return get_latest_event_of(aid); } + private: /** * @brief The most recent event added to the configuration @@ -145,8 +180,20 @@ private: * * @invariant For each event `e` in `events_`, the set of * dependencies of `e` is also contained in `events_` + * + * @invariant For each pair of events `e` and `e'` in + * `events_`, `e` and `e'` are not in conflict */ EventSet events_; + + /** + * @brief Maps actors to the latest events which + * are executed by the actor + * + * @invariant: The events that are contained in the map + * are also contained in the set `events_` + */ + std::unordered_map latest_event_mapping; }; } // namespace simgrid::mc::udpor diff --git a/src/mc/explo/udpor/Configuration_test.cpp b/src/mc/explo/udpor/Configuration_test.cpp index 8deb62e814..e7f3e6f297 100644 --- a/src/mc/explo/udpor/Configuration_test.cpp +++ b/src/mc/explo/udpor/Configuration_test.cpp @@ -14,6 +14,7 @@ #include +using namespace simgrid::mc; using namespace simgrid::mc::udpor; TEST_CASE("simgrid::mc::udpor::Configuration: Constructing Configurations") @@ -620,37 +621,48 @@ TEST_CASE("simgrid::mc::udpor:Configuration: Computing Full Alternatives in Read // then `e4`, and then `e7` Unfolding U; - auto e0 = std::make_unique(EventSet(), std::make_shared()); + auto e0 = std::make_unique( + EventSet(), std::make_shared(Transition::Type::UNKNOWN, 0)); auto e0_handle = e0.get(); - auto e1 = std::make_unique(EventSet({e0_handle}), std::make_shared()); + auto e1 = std::make_unique(EventSet({e0_handle}), + std::make_shared(Transition::Type::UNKNOWN, 0)); auto e1_handle = e1.get(); - auto e2 = std::make_unique(EventSet({e1_handle}), std::make_shared()); + auto e2 = std::make_unique( + EventSet({e1_handle}), std::make_shared(Transition::Type::UNKNOWN, 1)); auto e2_handle = e2.get(); - auto e3 = std::make_unique(EventSet({e1_handle}), std::make_shared()); + auto e3 = std::make_unique( + EventSet({e1_handle}), std::make_shared(Transition::Type::UNKNOWN, 2)); auto e3_handle = e3.get(); - auto e4 = std::make_unique(EventSet({e0_handle}), std::make_shared()); + auto e4 = std::make_unique( + EventSet({e0_handle}), std::make_shared(Transition::Type::UNKNOWN, 1)); auto e4_handle = e4.get(); - auto e5 = std::make_unique(EventSet({e4_handle}), std::make_shared()); + auto e5 = std::make_unique(EventSet({e4_handle}), + std::make_shared(Transition::Type::UNKNOWN, 0)); auto e5_handle = e5.get(); - auto e6 = std::make_unique(EventSet({e5_handle}), std::make_shared()); + auto e6 = std::make_unique( + EventSet({e5_handle}), std::make_shared(Transition::Type::UNKNOWN, 2)); auto e6_handle = e6.get(); - auto e7 = std::make_unique(EventSet({e0_handle}), std::make_shared()); + auto e7 = std::make_unique( + EventSet({e0_handle}), std::make_shared(Transition::Type::UNKNOWN, 2)); auto e7_handle = e7.get(); - auto e8 = std::make_unique(EventSet({e4_handle, e7_handle}), std::make_shared()); + auto e8 = std::make_unique(EventSet({e4_handle, e7_handle}), + std::make_shared(Transition::Type::UNKNOWN, 0)); auto e8_handle = e8.get(); - auto e9 = std::make_unique(EventSet({e7_handle}), std::make_shared()); + auto e9 = std::make_unique(EventSet({e7_handle}), + std::make_shared(Transition::Type::UNKNOWN, 0)); auto e9_handle = e9.get(); - auto e10 = std::make_unique(EventSet({e9_handle}), std::make_shared()); + auto e10 = std::make_unique( + EventSet({e9_handle}), std::make_shared(Transition::Type::UNKNOWN, 1)); auto e10_handle = e10.get(); SECTION("Alternative computation call 1") diff --git a/src/mc/explo/udpor/Unfolding.cpp b/src/mc/explo/udpor/Unfolding.cpp index 1b63328bbb..d17274b67f 100644 --- a/src/mc/explo/udpor/Unfolding.cpp +++ b/src/mc/explo/udpor/Unfolding.cpp @@ -25,7 +25,7 @@ void Unfolding::remove(const UnfoldingEvent* e) this->event_handles.remove(e); } -void Unfolding::insert(std::unique_ptr e) +const UnfoldingEvent* Unfolding::insert(std::unique_ptr e) { const UnfoldingEvent* handle = e.get(); if (auto loc = this->global_events_.find(handle); loc != this->global_events_.end()) { @@ -36,21 +36,16 @@ void Unfolding::insert(std::unique_ptr e) "This will result in a double free error and must be fixed."); } - // Map the handle to its owner + if (auto loc = this->find_equivalent(handle); loc != this->end()) { + // There's already an event in the unfolding that is semantically + // equivalent. Return the handle to that event and ignore adding in + // a duplicate event + return *loc; + } + this->event_handles.insert(handle); this->global_events_[handle] = std::move(e); -} - -bool Unfolding::contains_event_equivalent_to(const UnfoldingEvent* e) const -{ - // Notice the use of `==` equality here. `e` may not be contained in the - // unfolding; but some event which is "equivalent" to it could be. - for (const auto event : *this) { - if (*event == *e) { - return true; - } - } - return false; + return handle; } EventSet Unfolding::get_immediate_conflicts_of(const UnfoldingEvent* e) const diff --git a/src/mc/explo/udpor/Unfolding.hpp b/src/mc/explo/udpor/Unfolding.hpp index 0107692670..1c6ff6c04f 100644 --- a/src/mc/explo/udpor/Unfolding.hpp +++ b/src/mc/explo/udpor/Unfolding.hpp @@ -16,6 +16,29 @@ namespace simgrid::mc::udpor { class Unfolding { +public: + Unfolding() = default; + Unfolding& operator=(Unfolding&&) = default; + Unfolding(Unfolding&&) = default; + + auto begin() const { return this->event_handles.begin(); } + auto end() const { return this->event_handles.end(); } + auto cbegin() const { return this->event_handles.cbegin(); } + auto cend() const { return this->event_handles.cend(); } + size_t size() const { return this->event_handles.size(); } + bool empty() const { return this->event_handles.empty(); } + + void remove(const UnfoldingEvent* e); + void remove(const EventSet& events); + + /// @brief Adds a new event `e` to the Unfolding if that + /// event is not equivalent to any of those already contained + /// in the unfolding + const UnfoldingEvent* insert(std::unique_ptr e); + + /// @brief Computes "#ⁱ_U(e)" for the given event + EventSet get_immediate_conflicts_of(const UnfoldingEvent*) const; + private: /** * @brief All of the events that are currently are a part of the unfolding @@ -47,25 +70,10 @@ private: */ EventSet G; -public: - Unfolding() = default; - Unfolding& operator=(Unfolding&&) = default; - Unfolding(Unfolding&&) = default; - - void remove(const UnfoldingEvent* e); - void remove(const EventSet& events); - void insert(std::unique_ptr e); - bool contains_event_equivalent_to(const UnfoldingEvent* e) const; - - auto begin() const { return this->event_handles.begin(); } - auto end() const { return this->event_handles.end(); } - auto cbegin() const { return this->event_handles.cbegin(); } - auto cend() const { return this->event_handles.cend(); } - size_t size() const { return this->global_events_.size(); } - bool empty() const { return this->global_events_.empty(); } - - /// @brief Computes "#ⁱ_U(e)" for the given event - EventSet get_immediate_conflicts_of(const UnfoldingEvent*) const; + auto find_equivalent(const UnfoldingEvent* e) + { + return std::find_if(begin(), end(), [=](const UnfoldingEvent* e_i) { return *e == *e_i; }); + } }; } // namespace simgrid::mc::udpor diff --git a/src/mc/explo/udpor/UnfoldingEvent.hpp b/src/mc/explo/udpor/UnfoldingEvent.hpp index aeb4902e98..442aabee41 100644 --- a/src/mc/explo/udpor/UnfoldingEvent.hpp +++ b/src/mc/explo/udpor/UnfoldingEvent.hpp @@ -45,6 +45,7 @@ public: const EventSet& get_immediate_causes() const { return this->immediate_causes; } Transition* get_transition() const { return this->associated_transition.get(); } + aid_t get_actor() const { return get_transition()->aid_; } bool operator==(const UnfoldingEvent&) const; bool operator!=(const UnfoldingEvent& other) const { return not(*this == other); } diff --git a/src/mc/explo/udpor/Unfolding_test.cpp b/src/mc/explo/udpor/Unfolding_test.cpp index d75fb28763..1b60375db0 100644 --- a/src/mc/explo/udpor/Unfolding_test.cpp +++ b/src/mc/explo/udpor/Unfolding_test.cpp @@ -20,8 +20,10 @@ TEST_CASE("simgrid::mc::udpor::Unfolding: Creating an unfolding") TEST_CASE("simgrid::mc::udpor::Unfolding: Inserting and removing events with an unfolding") { Unfolding unfolding; - auto e1 = std::make_unique(); - auto e2 = std::make_unique(); + auto e1 = std::make_unique( + EventSet(), std::make_shared(Transition::Type::UNKNOWN, 0)); + auto e2 = + std::make_unique(EventSet(), std::make_shared(Transition::Type::UNKNOWN, 1)); const auto e1_handle = e1.get(); const auto e2_handle = e2.get(); @@ -42,23 +44,4 @@ TEST_CASE("simgrid::mc::udpor::Unfolding: Inserting and removing events with an REQUIRE(unfolding.empty()); } -TEST_CASE("simgrid::mc::udpor::Unfolding: Checking for semantically equivalent events") -{ - Unfolding unfolding; - auto e1 = std::make_unique( - EventSet(), std::make_shared(Transition::Type::BARRIER_ASYNC_LOCK, 6, 2)); - auto e2 = std::make_unique( - EventSet(), std::make_shared(Transition::Type::BARRIER_ASYNC_LOCK, 6, 2)); - - // e1 and e2 are equivalent - REQUIRE(*e1 == *e2); - - const auto e1_handle = e1.get(); - const auto e2_handle = e2.get(); - unfolding.insert(std::move(e1)); - - REQUIRE(unfolding.contains_event_equivalent_to(e1_handle)); - REQUIRE(unfolding.contains_event_equivalent_to(e2_handle)); -} - TEST_CASE("simgrid::mc::udpor::Unfolding: Checking all immediate conflicts restricted to an unfolding") {} \ No newline at end of file diff --git a/src/mc/explo/udpor/udpor_forward.hpp b/src/mc/explo/udpor/udpor_forward.hpp index 1cbdb2e0e5..23c13f3bec 100644 --- a/src/mc/explo/udpor/udpor_forward.hpp +++ b/src/mc/explo/udpor/udpor_forward.hpp @@ -11,8 +11,13 @@ #ifndef SIMGRID_MC_UDPOR_FORWARD_HPP #define SIMGRID_MC_UDPOR_FORWARD_HPP +#include "src/mc/mc_forward.hpp" +#include + namespace simgrid::mc::udpor { +class Comb; +class ExtensionSetCalculator; class EventSet; class Configuration; class History; diff --git a/src/mc/explo/udpor/udpor_tests_private.hpp b/src/mc/explo/udpor/udpor_tests_private.hpp index 276edfca79..fabc2fc229 100644 --- a/src/mc/explo/udpor/udpor_tests_private.hpp +++ b/src/mc/explo/udpor/udpor_tests_private.hpp @@ -18,7 +18,7 @@ namespace simgrid::mc::udpor { struct IndependentAction : public Transition { IndependentAction() = default; - IndependentAction(Type type, aid_t issuer, int times_considered) : Transition(type, issuer, times_considered) {} + IndependentAction(Type type, aid_t issuer, int times_considered = 0) : Transition(type, issuer, times_considered) {} // Independent with everyone else bool depends(const Transition* other) const override { return false; } @@ -26,7 +26,7 @@ struct IndependentAction : public Transition { struct DependentAction : public Transition { DependentAction() = default; - DependentAction(Type type, aid_t issuer, int times_considered) : Transition(type, issuer, times_considered) {} + DependentAction(Type type, aid_t issuer, int times_considered = 0) : Transition(type, issuer, times_considered) {} // Dependent with everyone else (except IndependentAction) bool depends(const Transition* other) const override @@ -37,7 +37,7 @@ struct DependentAction : public Transition { struct ConditionallyDependentAction : public Transition { ConditionallyDependentAction() = default; - ConditionallyDependentAction(Type type, aid_t issuer, int times_considered) + ConditionallyDependentAction(Type type, aid_t issuer, int times_considered = 0) : Transition(type, issuer, times_considered) { } -- 2.20.1