From: Maxwell Pirtle Date: Mon, 3 Apr 2023 08:18:31 +0000 (+0200) Subject: Add first round of debug logging to UDPOR X-Git-Tag: v3.34~153^2~6 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/1a43705d13b6418986f3c87317b2ddf92c5c60fe 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 03b39e58e3..a3ff975159 100644 --- 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 7f7e80a15a..8d114e6643 100644 --- a/src/mc/explo/udpor/Configuration.cpp +++ b/src/mc/explo/udpor/Configuration.cpp @@ -132,9 +132,9 @@ std::optional 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 D_hat(size); + const size_t k_alt_size = std::min(k, D.size()); + const auto D_hat = [&k_alt_size, &D]() { + std::vector 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::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::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 b3db77a1a7..89e3d50069 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 #include 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 c8b2ae26cb..2113e1e33b 100644 --- a/src/mc/explo/udpor/EventSet.cpp +++ b/src/mc/explo/udpor/EventSet.cpp @@ -238,6 +238,18 @@ std::vector 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 EventSet::move_into_vector() const&& { std::vector contents; diff --git a/src/mc/explo/udpor/EventSet.hpp b/src/mc/explo/udpor/EventSet.hpp index 18fb0d67e6..f682e3c43a 100644 --- 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 b9814fa77c..2ad01bd9df 100644 --- 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