From: Maxwell Pirtle Date: Wed, 5 Apr 2023 08:04:18 +0000 (+0200) Subject: Fix conflict detection between configs + history X-Git-Tag: v3.34~153^2~3 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/3529af6d632ac8a5f36352711acae57b10208c2c Fix conflict detection between configs + history The computation of K-partial alternatives requires that we can determine whether or not `[e] + C` for some event `e` is a valid configuration. There was a subtlety in the code prior to the this commit that caused UDPOR to incorrectly compute whether or not `[e] + C` was a valid configuration. Specifically, it was not sufficient to look at the difference between the event's history and the events in the configuration and checking *dependency*. You have to check *conflicts*: it's possible that two events are dependent in a configuration but are related to each other causally (and thus would not be in conflict with one another) --- diff --git a/src/mc/explo/UdporChecker.cpp b/src/mc/explo/UdporChecker.cpp index d4cb4eddaa..42a8f54f86 100644 --- a/src/mc/explo/UdporChecker.cpp +++ b/src/mc/explo/UdporChecker.cpp @@ -164,7 +164,7 @@ EventSet UdporChecker::compute_enC(const Configuration& C, const EventSet& exC) { EventSet enC; for (const auto e : exC) { - if (not e->conflicts_with(C)) { + if (C.is_compatible_with(e)) { enC.insert(e); } } @@ -294,7 +294,7 @@ void UdporChecker::clean_up_explore(const UnfoldingEvent* e, const Configuration // // foreach ê in #ⁱ_U(e) // for (const auto* e_hat : this->unfolding.get_immediate_conflicts_of(e)) { // // Move [ê] \ Q_CDU from U to G - // const EventSet to_remove = e_hat->get_history().subtracting(Q_CDU); + // const EventSet to_remove = e_hat->get_local_config().subtracting(Q_CDU); // XBT_DEBUG("Moving {%s} from U to G...", to_remove.to_string().c_str()); // clean_up_set.form_union(to_remove); // } diff --git a/src/mc/explo/udpor/Configuration.cpp b/src/mc/explo/udpor/Configuration.cpp index 8d114e6643..44ec27005f 100644 --- a/src/mc/explo/udpor/Configuration.cpp +++ b/src/mc/explo/udpor/Configuration.cpp @@ -9,6 +9,7 @@ #include "src/mc/explo/udpor/Unfolding.hpp" #include "src/mc/explo/udpor/UnfoldingEvent.hpp" #include "src/mc/explo/udpor/maximal_subsets_iterator.hpp" +#include "src/xbt/utils/iter/variable_for_loop.hpp" #include "xbt/asserts.h" #include @@ -21,7 +22,7 @@ Configuration::Configuration(std::initializer_list events { } -Configuration::Configuration(const UnfoldingEvent* e) : Configuration(e->get_history()) +Configuration::Configuration(const UnfoldingEvent* e) : Configuration(e->get_local_config()) { // The local configuration should always be a valid configuration. We // check the invariant regardless as a sanity check @@ -48,12 +49,14 @@ void Configuration::add_event(const UnfoldingEvent* e) throw std::invalid_argument("Expected a nonnull `UnfoldingEvent*` but received NULL instead"); } + // The event is already a member of the configuration: there's + // nothing to do in this case if (this->events_.contains(e)) { return; } // Preserves the property that the configuration is conflict-free - if (e->conflicts_with(*this)) { + if (e->conflicts_with_any(this->events_)) { throw std::invalid_argument("The newly added event conflicts with the events already " "contained in the configuration. Adding this event violates " "the property that a configuration is conflict-free"); @@ -72,13 +75,41 @@ void Configuration::add_event(const UnfoldingEvent* e) bool Configuration::is_compatible_with(const UnfoldingEvent* e) const { - return not e->conflicts_with(*this); + // 1. `e`'s history must be contained in the configuration; + // otherwise adding the event would violate the invariant + // that a configuration is causally-closed + // + // 2. `e` itself must not conflict with any events of + // the configuration; otherwise adding the event would + // violate the invariant that a configuration is conflict-free + return contains(e->get_history()) and (not e->conflicts_with_any(this->events_)); } bool Configuration::is_compatible_with(const History& history) const { - return std::none_of(history.begin(), history.end(), - [&](const UnfoldingEvent* e) { return e->conflicts_with(*this); }); + // Note: We don't need to check if the `C` will be causally-closed + // after adding `history` to it since a) `C` itself is already + // causally-closed and b) the history is already causally closed + const auto event_diff = history.get_event_diff_with(*this); + + // The events that are contained outside of the configuration + // must themselves be free of conflicts. + if (not event_diff.is_conflict_free()) { + return false; + } + + // Now we need only ensure that there are no conflicts + // between events of the configuration and the events + // that lie outside of the configuration. There is no + // need to check if there are conflicts in `C`: we already + // know that it's conflict free + const auto begin = simgrid::xbt::variable_for_loop{{event_diff}, {this->events_}}; + const auto end = simgrid::xbt::variable_for_loop(); + return std::none_of(begin, end, [=](const auto event_pair) { + const UnfoldingEvent* e1 = *event_pair[0]; + const UnfoldingEvent* e2 = *event_pair[1]; + return e1->conflicts_with(e2); + }); } std::vector Configuration::get_topologically_sorted_events() const diff --git a/src/mc/explo/udpor/Configuration.hpp b/src/mc/explo/udpor/Configuration.hpp index 89e3d50069..b1f6f933d2 100644 --- a/src/mc/explo/udpor/Configuration.hpp +++ b/src/mc/explo/udpor/Configuration.hpp @@ -33,6 +33,7 @@ public: auto cend() const { return this->events_.cend(); } bool contains(const UnfoldingEvent* e) const { return this->events_.contains(e); } + bool contains(const EventSet& events) const { return events.is_subset_of(this->events_); } const EventSet& get_events() const { return this->events_; } const UnfoldingEvent* get_latest_event() const { return this->newest_event; } std::string to_string() const { return this->events_.to_string(); } @@ -68,8 +69,16 @@ public: /** * @brief Whether or not the given event can be added to - * this configuration while keeping the set of events causally closed - * and conflict-free + * this configuration while preserving that the configuration + * is causally closed and conflict-free + * + * A configuration `C` is compatible with an event iff + * the event can be added to `C` while preserving that + * the configuration is causally closed and conflict-free. + * + * The method effectively answers the following question: + * + * "Is `C + {e}` a valid configuration?" */ bool is_compatible_with(const UnfoldingEvent* e) const; @@ -77,6 +86,14 @@ public: * @brief Whether or not the events in the given history can be added to * this configuration while keeping the set of events causally closed * and conflict-free + * + * A configuration `C` is compatible with a history iff all + * events of the history can be added to `C` while preserving + * that the configuration is causally closed and conflict-free. + * + * The method effectively answers the following question: + * + * "Is `C + (U_i [e_i])` a valid configuration?" */ bool is_compatible_with(const History& history) const; diff --git a/src/mc/explo/udpor/History.hpp b/src/mc/explo/udpor/History.hpp index c5e60872d7..dc17c27e58 100644 --- a/src/mc/explo/udpor/History.hpp +++ b/src/mc/explo/udpor/History.hpp @@ -96,6 +96,17 @@ public: */ EventSet get_all_maximal_events() const; + /** + * @brief Computes the set of events that are not contained + * in the given configuration + * + * A configuration is a causally-closed, conflict-free set + * of events. Thus, you can determine which events lie outside + * of a configuration during the search more efficiently: the moment + * you discover an event contained in the configuration, you + * do not need to search that event or any of its ancestors as + * they will all be contained in the configuration + */ EventSet get_event_diff_with(const Configuration& config) const; private: diff --git a/src/mc/explo/udpor/UnfoldingEvent.cpp b/src/mc/explo/udpor/UnfoldingEvent.cpp index 2ad01bd9df..a14b1f3cbd 100644 --- a/src/mc/explo/udpor/UnfoldingEvent.cpp +++ b/src/mc/explo/udpor/UnfoldingEvent.cpp @@ -52,12 +52,19 @@ std::string UnfoldingEvent::to_string() const } dependencies_string += "]"; - return xbt::string_printf("Actor %ld: %s (%zu dependencies { %s })", associated_transition->aid_, + return xbt::string_printf("Actor %ld: %s (%zu dependencies: %s)", associated_transition->aid_, associated_transition->to_string().c_str(), immediate_causes.size(), dependencies_string.c_str()); } EventSet UnfoldingEvent::get_history() const +{ + EventSet local_config = get_local_config(); + local_config.remove(this); + return local_config; +} + +EventSet UnfoldingEvent::get_local_config() const { return History(this).get_all_events(); } @@ -81,8 +88,8 @@ bool UnfoldingEvent::conflicts_with(const UnfoldingEvent* other) const return false; } - const EventSet my_history = get_history(); - const EventSet other_history = other->get_history(); + const EventSet my_history = get_local_config(); + const EventSet other_history = other->get_local_config(); const EventSet unique_to_me = my_history.subtracting(other_history); const EventSet unique_to_other = other_history.subtracting(my_history); @@ -93,16 +100,9 @@ bool UnfoldingEvent::conflicts_with(const UnfoldingEvent* other) const return conflicts_with_me or conflicts_with_other; } -bool UnfoldingEvent::conflicts_with(const Configuration& config) const +bool UnfoldingEvent::conflicts_with_any(const EventSet& events) const { - // A configuration is itself already conflict-free. Thus, it is - // simply a matter of testing whether or not the transition associated - // with the event is dependent with any already in `config` that are - // OUTSIDE this event's history (in an unfolding, events only conflict - // if they are not related) - const EventSet potential_conflicts = config.get_events().subtracting(get_history()); - return std::any_of(potential_conflicts.cbegin(), potential_conflicts.cend(), - [&](const UnfoldingEvent* e) { return this->is_dependent_with(e); }); + return std::any_of(events.begin(), events.end(), [&](const auto e) { return e->conflicts_with(this); }); } bool UnfoldingEvent::immediately_conflicts_with(const UnfoldingEvent* other) const diff --git a/src/mc/explo/udpor/UnfoldingEvent.hpp b/src/mc/explo/udpor/UnfoldingEvent.hpp index 65328244e5..bad411cfe2 100644 --- a/src/mc/explo/udpor/UnfoldingEvent.hpp +++ b/src/mc/explo/udpor/UnfoldingEvent.hpp @@ -27,6 +27,7 @@ public: UnfoldingEvent(UnfoldingEvent&&) = default; EventSet get_history() const; + EventSet get_local_config() const; bool in_history_of(const UnfoldingEvent* other) const; /** @@ -40,8 +41,8 @@ public: bool conflicts_with(const UnfoldingEvent* other) const; /// @brief Whether or not this event is in conflict with - /// any event in the given configuration - bool conflicts_with(const Configuration& config) const; + /// any event in the given set + bool conflicts_with_any(const EventSet& events) const; /// @brief Computes "this #ⁱ other" bool immediately_conflicts_with(const UnfoldingEvent* other) const; diff --git a/src/mc/explo/udpor/maximal_subsets_iterator.cpp b/src/mc/explo/udpor/maximal_subsets_iterator.cpp index d6ed9888e9..3e4a76ad75 100644 --- a/src/mc/explo/udpor/maximal_subsets_iterator.cpp +++ b/src/mc/explo/udpor/maximal_subsets_iterator.cpp @@ -161,16 +161,16 @@ maximal_subsets_iterator::bookkeeper::find_next_candidate_event(topological_orde void maximal_subsets_iterator::bookkeeper::mark_included_in_maximal_set(const UnfoldingEvent* e) { - const auto e_history = e->get_history(); - for (const auto e_hist : e_history) { + const auto e_local_config = e->get_local_config(); + for (const auto e_hist : e_local_config) { event_counts[e_hist]++; } } void maximal_subsets_iterator::bookkeeper::mark_removed_from_maximal_set(const UnfoldingEvent* e) { - const auto e_history = e->get_history(); - for (const auto e_hist : e_history) { + const auto e_local_config = e->get_local_config(); + for (const auto e_hist : e_local_config) { xbt_assert(event_counts.find(e_hist) != event_counts.end(), "Invariant Violation: Attempted to remove an event which was not previously added"); xbt_assert(event_counts[e_hist] > 0, "Invariant Violation: An event `e` had a count of `0` at this point "