Add events with implicit bottom event

[simgrid.git] / src / mc / explo / UdporChecker.cpp

diff --git a/src/mc/explo/UdporChecker.cpp b/src/mc/explo/UdporChecker.cpp
index 6bd87a67303ffe1e3d1bb66ee487aadd1709f5b7..3221c2ac47b8e8ba88740089608120811f70eae5 100644 (file)
--- a/src/mc/explo/UdporChecker.cpp
+++ b/src/mc/explo/UdporChecker.cpp
@@ -64,7 +64,12 @@ 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...");
+      XBT_VERB("**************************");
+      XBT_VERB("*** TRACE INVESTIGATED ***");
+      XBT_VERB("**************************");
+      XBT_VERB("Execution sequence:");
+      for (auto const& s : get_textual_trace())
+        XBT_VERB("  %s", s.c_str());
       get_remote_app().check_deadlock();
     }
 
@@ -109,8 +114,8 @@ void UdporChecker::explore(const Configuration& C, EventSet D, EventSet A, Event
     // that we are searching again from `state(C)`. While the
     // stack of states is properly adjusted to represent
     // `state(C)` all together, the RemoteApp is currently sitting
-    // at some *future* state with resepct to `state(C)` since the
-    // recursive calls have moved it there.
+    // at some *future* state with respect to `state(C)` since the
+    // recursive calls had moved it there.
     restore_program_state_with_current_stack();
 
     // Explore(C, D + {e}, J \ C)
@@ -150,6 +155,11 @@ EventSet UdporChecker::compute_exC(const Configuration& C, const State& stateC,
   EventSet exC                = prev_exC;
   exC.remove(e_cur);
 
+  // IMPORTANT NOTE: In order to have deterministic results, we need to process
+  // the actors in a deterministic manner so that events are discovered by
+  // UDPOR in a deterministic order. The processing done here always processes
+  // actors in a consistent order since `std::map` is by-default ordered using
+  // `std::less<Key>` (see the return type of `State::get_actors_list()`)
   for (const auto& [aid, actor_state] : stateC.get_actors_list()) {
     for (const auto& transition : actor_state.get_enabled_transitions()) {
       XBT_DEBUG("\t Considering partial extension for %s", transition->to_string().c_str());
@@ -236,16 +246,23 @@ UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, con
                                 "empty before attempting to select an event from it?");
   }
 
+  // UDPOR's exploration is non-deterministic (as is DPOR's)
+  // in the sense that at any given point there may
+  // be multiple paths that can be followed. The correctness and optimality
+  // of the algorithm remains unaffected by the route taken by UDPOR when
+  // given multiple choices; but to ensure that SimGrid itself has deterministic
+  // behavior on all platforms, we always pick events with lower id's
+  // to ensure we explore the unfolding deterministically.
   if (A.empty()) {
-    return const_cast<UnfoldingEvent*>(*(enC.begin()));
-  }
-
-  for (const auto& event : A) {
-    if (enC.contains(event)) {
-      return const_cast<UnfoldingEvent*>(event);
-    }
+    const auto min_event = std::min_element(enC.begin(), enC.end(),
+                                            [](const auto e1, const auto e2) { return e1->get_id() < e2->get_id(); });
+    return const_cast<UnfoldingEvent*>(*min_event);
+  } else {
+    const auto intersection = A.make_intersection(enC);
+    const auto min_event    = std::min_element(intersection.begin(), intersection.end(),
+                                               [](const auto e1, const auto e2) { return e1->get_id() < e2->get_id(); });
+    return const_cast<UnfoldingEvent*>(*min_event);
   }
-  return nullptr;
 }
 
 void UdporChecker::clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D)