Add "working" UDPOR on small examples with CommWait independence

In forcing each CommWait transition to be
independent with all other CommWait transitions as
assumed in The Anh Pham's thesis, UDPOR appears to
correctly identify the errors in the few programs
that are used to test SimGrid's model checking
component.

diff --git a/src/mc/explo/UdporChecker.cpp b/src/mc/explo/UdporChecker.cpp
index 74ead2a..6416c49 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();
     }
 

diff --git a/src/mc/transition/TransitionComm.cpp b/src/mc/transition/TransitionComm.cpp
index 2cfd93f..e836f73 100644 (file)
--- a/src/mc/transition/TransitionComm.cpp
+++ b/src/mc/transition/TransitionComm.cpp
@@ -165,6 +165,11 @@ bool CommRecvTransition::depends(const Transition* other) const
     if ((aid_ != wait->sender_) && (aid_ != wait->receiver_) && (wait->rbuff_ != rbuff_))
       return false;
 
+    // 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_)
+      return false;
+
     return true; // DEP with other wait transitions
   }
 
@@ -231,6 +236,11 @@ bool CommSendTransition::depends(const Transition* other) const
     if ((aid_ != wait->sender_) && (aid_ != wait->receiver_) && (wait->sbuff_ != sbuff_))
       return false;
 
+    // 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_)
+      return false;
+
     return true; // DEP with other wait transitions
   }