Add first round of debug logging to UDPOR

Several XBT_DEBUG() statements were added throughout
the functions in UdporChecker to better understand
the evolution of UDPOR in the context of SimGrid.
Several `to_string()` statements were added where
appropriate to aid in the visualization of the
unfolding structure. Until we potentially add
a more complicated tree-drawing algorithm to SimGrid
that can render the unfolding structure systematically,
this is the best we have

diff --git a/src/mc/explo/UdporChecker.cpp b/src/mc/explo/UdporChecker.cpp
index 03b39e5..a3ff975 100644 (file)
--- a/src/mc/explo/UdporChecker.cpp
+++ b/src/mc/explo/UdporChecker.cpp
@@ -34,6 +34,15 @@ void UdporChecker::explore(const Configuration& C, EventSet D, EventSet A, Event
   auto& stateC   = *state_stack.back();
   auto exC       = compute_exC(C, stateC, prev_exC);
   const auto enC = compute_enC(C, exC);
+  XBT_DEBUG("explore(C, D, A) with:\n"
+            "C\t := %s \n"
+            "D\t := %s \n"
+            "A\t := %s \n"
+            "ex(C)\t := %s \n"
+            "en(C)\t := %s \n",
+            C.to_string().c_str(), D.to_string().c_str(), A.to_string().c_str(), exC.to_string().c_str(),
+            enC.to_string().c_str());
+  XBT_DEBUG("ex(C) has %zu elements, of which %zu are in en(C)", exC.size(), enC.size());
 
   // If enC is a subset of D, intuitively
   // there aren't any enabled transitions
@@ -41,9 +50,10 @@ void UdporChecker::explore(const Configuration& C, EventSet D, EventSet A, Event
   // exploration would lead to a so-called
   // "sleep-set blocked" trace.
   if (enC.is_subset_of(D)) {
-    if (not C.get_events().empty()) {
-      // Report information...
-    }
+    XBT_DEBUG("en(C) is a subset of the sleep set D (size %zu); if we"
+              "kept exploring, we'd hit a sleep-set blocked trace",
+              D.size());
+    XBT_DEBUG("The current configuration has %zu elements", C.get_events().size());
 
     // When `en(C)` is empty, intuitively this means that there
     // are no enabled transitions that can be executed from the
@@ -53,19 +63,20 @@ void UdporChecker::explore(const Configuration& C, EventSet D, EventSet A, Event
     // possibility is that we've finished running everything, and
     // we wouldn't be in deadlock then)
     if (enC.empty()) {
+      XBT_VERB("Maximal configuration detected. Checking for deadlock...");
       get_remote_app().check_deadlock();
     }
 
     return;
   }
-
-  // TODO: Add verbose logging about which event is being explored
-
   UnfoldingEvent* e = select_next_unfolding_event(A, enC);
   xbt_assert(e != nullptr, "\n\n****** INVARIANT VIOLATION ******\n"
                            "UDPOR guarantees that an event will be chosen at each point in\n"
                            "the search, yet no events were actually chosen\n"
                            "*********************************\n\n");
+  XBT_DEBUG("Selected event `%s` (%zu dependencies) to extend the configuration", e->to_string().c_str(),
+            e->get_immediate_causes().size());
+
   // Ce := C + {e}
   Configuration Ce = C;
   Ce.add_event(e);
@@ -81,7 +92,7 @@ void UdporChecker::explore(const Configuration& C, EventSet D, EventSet A, Event
 
   explore(Ce, D, std::move(A), std::move(exC));
 
-  //  Prepare to move the application back one state.
+  // Prepare to move the application back one state.
   // We need only remove the state from the stack here: if we perform
   // another `Explore()` after computing an alternative, at that
   // point we'll actually create a fresh RemoteProcess
@@ -90,8 +101,8 @@ void UdporChecker::explore(const Configuration& C, EventSet D, EventSet A, Event
   // D <-- D + {e}
   D.insert(e);
 
-  constexpr unsigned K = 10;
-  if (auto J = C.compute_k_partial_alternative_to(D, this->unfolding, K); J.has_value()) {
+  XBT_DEBUG("Checking for the existence of an alternative...");
+  if (auto J = C.compute_alternative_to(D, this->unfolding); J.has_value()) {
     // Before searching the "right half", we need to make
     // sure the program actually reflects the fact
     // that we are searching again from `state(C)`. While the
@@ -103,7 +114,19 @@ void UdporChecker::explore(const Configuration& C, EventSet D, EventSet A, Event
 
     // Explore(C, D + {e}, J \ C)
     auto J_minus_C = J.value().get_events().subtracting(C.get_events());
+
+    XBT_DEBUG("Alternative detected! The alternative is:\n"
+              "J\t := %s \n"
+              "J / C := %s\n"
+              "UDPOR is going to explore it...",
+              J.value().to_string().c_str(), J_minus_C.to_string().c_str());
     explore(C, D, std::move(J_minus_C), std::move(prev_exC));
+  } else {
+    XBT_DEBUG("No alternative detected with:\n"
+              "C\t := %s \n"
+              "D\t := %s \n"
+              "A\t := %s \n",
+              C.to_string().c_str(), D.to_string().c_str(), A.to_string().c_str());
   }
 
   // D <-- D - {e}
@@ -182,6 +205,7 @@ void UdporChecker::move_to_stateCe(State* state, UnfoldingEvent* e)
 
 void UdporChecker::restore_program_state_with_current_stack()
 {
+  XBT_DEBUG("Restoring state using the current stack");
   get_remote_app().restore_initial_state();
 
   /* Traverse the stack from the state at position start and re-execute the transitions */
@@ -229,7 +253,8 @@ void UdporChecker::clean_up_explore(const UnfoldingEvent* e, const Configuration
   const EventSet Q_CDU                  = C_union_D.make_union(es_immediate_conflicts.get_local_config());
 
   // Move {e} \ Q_CDU from U to G
-  if (Q_CDU.contains(e)) {
+  if (not Q_CDU.contains(e)) {
+    XBT_DEBUG("Removing %s from U to G...", e->to_string().c_str());
     this->unfolding.remove(e);
   }
 
@@ -237,6 +262,7 @@ void UdporChecker::clean_up_explore(const UnfoldingEvent* e, const Configuration
   for (const auto* e_hat : es_immediate_conflicts) {
     // Move [ê] \ Q_CDU from U to G
     const EventSet to_remove = e_hat->get_history().subtracting(Q_CDU);
+    XBT_DEBUG("Removing {%s} from U to G...", to_remove.to_string().c_str());
     this->unfolding.remove(to_remove);
   }
 }

diff --git a/src/mc/explo/udpor/Configuration.cpp b/src/mc/explo/udpor/Configuration.cpp
index 7f7e80a..8d114e6 100644 (file)
--- a/src/mc/explo/udpor/Configuration.cpp
+++ b/src/mc/explo/udpor/Configuration.cpp
@@ -132,9 +132,9 @@ std::optional<Configuration> Configuration::compute_k_partial_alternative_to(con
                                                                              size_t k) const
 {
   // 1. Select k (of |D|, whichever is smaller) arbitrary events e_1, ..., e_k from D
-  const auto D_hat = [&]() {
-    const size_t size = std::min(k, D.size());
-    std::vector<const UnfoldingEvent*> D_hat(size);
+  const size_t k_alt_size = std::min(k, D.size());
+  const auto D_hat        = [&k_alt_size, &D]() {
+    std::vector<const UnfoldingEvent*> D_hat(k_alt_size);
     // TODO: Since any subset suffices for computing `k`-partial alternatives,
     // potentially select intelligently here (e.g. perhaps pick events
     // with transitions that we know are totally independent). This may be
@@ -142,7 +142,7 @@ std::optional<Configuration> Configuration::compute_k_partial_alternative_to(con
     // UDPOR
     //
     // For now, simply pick the first `k` events
-    std::copy_n(D.begin(), size, D_hat.begin());
+    std::copy_n(D.begin(), k_alt_size, D_hat.begin());
     return D_hat;
   }();
 
@@ -160,7 +160,7 @@ std::optional<Configuration> Configuration::compute_k_partial_alternative_to(con
   Comb comb(k);
 
   for (const auto* e : U) {
-    for (unsigned i = 0; i < k; i++) {
+    for (size_t i = 0; i < k_alt_size; i++) {
       const UnfoldingEvent* e_i = D_hat[i];
       if (const auto e_local_config = History(e);
           e_i->conflicts_with(e) and (not D.intersects(e_local_config)) and is_compatible_with(e_local_config)) {

diff --git a/src/mc/explo/udpor/Configuration.hpp b/src/mc/explo/udpor/Configuration.hpp
index b3db77a..89e3d50 100644 (file)
--- 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 <optional>
+#include <string>
 #include <unordered_map>
 
 namespace simgrid::mc::udpor {
@@ -34,6 +35,7 @@ public:
   bool contains(const UnfoldingEvent* e) const { return this->events_.contains(e); }
   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(); }
 
   /**
    * @brief Insert a new event into the configuration

diff --git a/src/mc/explo/udpor/EventSet.cpp b/src/mc/explo/udpor/EventSet.cpp
index c8b2ae2..2113e1e 100644 (file)
--- a/src/mc/explo/udpor/EventSet.cpp
+++ b/src/mc/explo/udpor/EventSet.cpp
@@ -238,6 +238,18 @@ std::vector<const UnfoldingEvent*> EventSet::get_topological_ordering_of_reverse
   return topological_events;
 }
 
+std::string EventSet::to_string() const
+{
+  std::string contents;
+
+  for (const auto* event : *this) {
+    contents += event->to_string();
+    contents += "\n";
+  }
+
+  return contents;
+}
+
 std::vector<const UnfoldingEvent*> EventSet::move_into_vector() const&&
 {
   std::vector<const UnfoldingEvent*> contents;

diff --git a/src/mc/explo/udpor/EventSet.hpp b/src/mc/explo/udpor/EventSet.hpp
index 18fb0d6..f682e3c 100644 (file)
--- a/src/mc/explo/udpor/EventSet.hpp
+++ b/src/mc/explo/udpor/EventSet.hpp
@@ -59,6 +59,7 @@ public:
 
   bool operator==(const EventSet& other) const { return this->events_ == other.events_; }
   bool operator!=(const EventSet& other) const { return this->events_ != other.events_; }
+  std::string to_string() const;
 
   /**
    * @brief Whether or not this set of events could

diff --git a/src/mc/explo/udpor/UnfoldingEvent.cpp b/src/mc/explo/udpor/UnfoldingEvent.cpp
index b9814fa..2ad01bd 100644 (file)
--- a/src/mc/explo/udpor/UnfoldingEvent.cpp
+++ b/src/mc/explo/udpor/UnfoldingEvent.cpp
@@ -44,8 +44,17 @@ bool UnfoldingEvent::operator==(const UnfoldingEvent& other) const
 
 std::string UnfoldingEvent::to_string() const
 {
-  return xbt::string_printf("e(%s) (%zu dependencies)", associated_transition->to_string().c_str(),
-                            immediate_causes.size());
+  std::string dependencies_string;
+
+  dependencies_string += "[";
+  for (const auto* e : immediate_causes) {
+    dependencies_string += e->to_string();
+  }
+  dependencies_string += "]";
+
+  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