Add events with implicit bottom event

A bug was caught whereby events of the
form MUTEX* were not added properly
when following the pseudocode directly.
The problem is that SimGrid does not
explicitly represent the "bottom" event
with which every event in an unfolding is
implicitly dependent; instead, events are
simply processed without it. The implication
is such that technically, all events would
have the "previously-executed event" as
the bottom event if it was the first action taken
by the actor in the configuration, while SimGrid
will return a `std::nullopt_t` if no such
action has been taken.

The solution is very simple: we simply
add the event without any dependencies
(representing the root event) if the
previous event can't be found for the
action. This is the case in the
other pseudocode that exists, but
is a bit more subtle when readingh the
pseudocode for mutexes

diff --git a/src/mc/explo/UdporChecker.cpp b/src/mc/explo/UdporChecker.cpp
index 6416c49..3221c2a 100644 (file)
--- a/src/mc/explo/UdporChecker.cpp
+++ b/src/mc/explo/UdporChecker.cpp
@@ -114,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)

diff --git a/src/mc/explo/udpor/ExtensionSetCalculator.cpp b/src/mc/explo/udpor/ExtensionSetCalculator.cpp
index 5f42231..d9d8e26 100644 (file)
--- a/src/mc/explo/udpor/ExtensionSetCalculator.cpp
+++ b/src/mc/explo/udpor/ExtensionSetCalculator.cpp
@@ -84,10 +84,8 @@ EventSet ExtensionSetCalculator::partially_extend_CommSend(const Configuration&
       const EventSet K = EventSet({e, pre_event_a_C.value_or(e)}).get_largest_maximal_subset();
 
       // TODO: Check D_K(a, lambda(e)) (only matters in the case of CommTest)
-      if (true) {
-        const auto* e_prime = U->discover_event(std::move(K), send_action);
-        exC.insert(e_prime);
-      }
+      const auto e_prime = U->discover_event(std::move(K), send_action);
+      exC.insert(e_prime);
     }
   }
 
@@ -542,11 +540,15 @@ EventSet ExtensionSetCalculator::partially_extend_MutexAsyncLock(const Configura
   const auto pre_event_a_C = C.pre_event(mutex_lock->aid_);
 
   // for each event e in C
-  // 1. If lambda(e) := pre(a) -> add it, otherwise don't bother if
-  // it's not there
+  // 1. If lambda(e) := pre(a) -> add it. Note that if
+  // pre_event_a_C.has_value() == false, this implies `C` is
+  // empty or which we treat as implicitly containing the bottom event
   if (pre_event_a_C.has_value()) {
     const auto e_prime = U->discover_event(EventSet({pre_event_a_C.value()}), mutex_lock);
     exC.insert(e_prime);
+  } else {
+    const auto e_prime = U->discover_event(EventSet(), mutex_lock);
+    exC.insert(e_prime);
   }
 
   // for each event e in C
@@ -572,11 +574,15 @@ EventSet ExtensionSetCalculator::partially_extend_MutexUnlock(const Configuratio
   const auto pre_event_a_C = C.pre_event(mutex_unlock->aid_);
 
   // for each event e in C
-  // 1. If lambda(e) := pre(a) -> add it, otherwise don't bother if
-  // it's not there
+  // 1. If lambda(e) := pre(a) -> add it. Note that if
+  // pre_event_a_C.has_value() == false, this implies `C` is
+  // empty or which we treat as implicitly containing the bottom event
   if (pre_event_a_C.has_value()) {
     const auto e_prime = U->discover_event(EventSet({pre_event_a_C.value()}), mutex_unlock);
     exC.insert(e_prime);
+  } else {
+    const auto e_prime = U->discover_event(EventSet(), mutex_unlock);
+    exC.insert(e_prime);
   }
 
   // for each event e in C
@@ -606,12 +612,14 @@ EventSet ExtensionSetCalculator::partially_extend_MutexWait(const Configuration&
   const auto pre_event_a_C = C.pre_event(mutex_wait->aid_);
 
   // for each event e in C
-  // 1. If lambda(e) := pre(a) -> add it, otherwise don't bother if
-  // it's not there. In the case of MutexWait, we also check that the
+  // 1. If lambda(e) := pre(a) -> add it. In the case of MutexWait, we also check that the
   // actor which is executing the MutexWait is the owner of the mutex
   if (pre_event_a_C.has_value() && mutex_wait->get_owner() == mutex_wait->aid_) {
     const auto e_prime = U->discover_event(EventSet({pre_event_a_C.value()}), mutex_wait);
     exC.insert(e_prime);
+  } else {
+    const auto e_prime = U->discover_event(EventSet(), mutex_wait);
+    exC.insert(e_prime);
   }
 
   // for each event e in C
@@ -638,11 +646,15 @@ EventSet ExtensionSetCalculator::partially_extend_MutexTest(const Configuration&
   const auto pre_event_a_C = C.pre_event(mutex_test->aid_);
 
   // for each event e in C
-  // 1. If lambda(e) := pre(a) -> add it, otherwise don't bother if
-  // it's not there
+  // 1. If lambda(e) := pre(a) -> add it. Note that if
+  // pre_evevnt_a_C.has_value() == false, this implies `C` is
+  // empty or which we treat as implicitly containing the bottom event
   if (pre_event_a_C.has_value()) {
     const auto e_prime = U->discover_event(EventSet({pre_event_a_C.value()}), mutex_test);
     exC.insert(e_prime);
+  } else {
+    const auto e_prime = U->discover_event(EventSet(), mutex_test);
+    exC.insert(e_prime);
   }
 
   // for each event e in C

diff --git a/src/mc/transition/TransitionComm.cpp b/src/mc/transition/TransitionComm.cpp
index 2e71920..c9fe6bc 100644 (file)
--- a/src/mc/transition/TransitionComm.cpp
+++ b/src/mc/transition/TransitionComm.cpp
@@ -185,7 +185,7 @@ bool CommRecvTransition::depends(const Transition* other) const
 
     // If the wait is waiting on a paired comm already, we're independent!
     // If we happen to make up that pair, then we're dependent...
-    if (wait->comm_ != comm_)
+    if ((aid_ != wait->aid_) && wait->comm_ != comm_)
       return false;
 
     return true; // DEP with other wait transitions
@@ -261,7 +261,7 @@ bool CommSendTransition::depends(const Transition* other) const
 
     // If the wait is waiting on a paired comm already, we're independent!
     // If we happen to make up that pair, then we're dependent...
-    if (wait->comm_ != comm_)
+    if ((aid_ != wait->aid_) && wait->comm_ != comm_)
       return false;
 
     return true; // DEP with other wait transitions