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 d4cb4ed..42a8f54 100644 (file)
--- 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 8d114e6..44ec270 100644 (file)
--- 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 <algorithm>
@@ -21,7 +22,7 @@ Configuration::Configuration(std::initializer_list<const UnfoldingEvent*> 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<const EventSet>{{event_diff}, {this->events_}};
+  const auto end   = simgrid::xbt::variable_for_loop<const EventSet>();
+  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<const UnfoldingEvent*> Configuration::get_topologically_sorted_events() const

diff --git a/src/mc/explo/udpor/Configuration.hpp b/src/mc/explo/udpor/Configuration.hpp
index 89e3d50..b1f6f93 100644 (file)
--- 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 c5e6087..dc17c27 100644 (file)
--- 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 2ad01bd..a14b1f3 100644 (file)
--- 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 6532824..bad411c 100644 (file)
--- 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 d6ed988..3e4a76a 100644 (file)
--- 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 "