From: mlaurent <mathieu.laurent@ens-rennes.fr>
Date: Thu, 9 Nov 2023 11:17:28 +0000 (+0100)
Subject: Add a missing independence theorem about Mutex
X-Git-Tag: v3.35~77^2~4
X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/a7cc502f224afb96f0203b94759cd0dabebf8de5

Add a missing independence theorem about Mutex
---

diff --git a/src/mc/transition/TransitionSynchro.cpp b/src/mc/transition/TransitionSynchro.cpp
index 230308f0a8..b1bea23de0 100644
--- a/src/mc/transition/TransitionSynchro.cpp
+++ b/src/mc/transition/TransitionSynchro.cpp
@@ -88,6 +88,12 @@ bool MutexTransition::depends(const Transition* o) const
     if (type_ == Type::MUTEX_ASYNC_LOCK && other->type_ == Type::MUTEX_UNLOCK)
       return false;
 
+    // Theorem 4.4.9: LOCK indep UNLOCK.
+    //  any combination of wait and test is indenpendent.
+    if ((type_ == Type::MUTEX_WAIT || type_ == Type::MUTEX_TEST) &&
+        (other->type_ == Type::MUTEX_WAIT || other->type_ == Type::MUTEX_TEST))
+      return false;
+
     // TEST is a pure function; TEST/WAIT won't change the owner; TRYLOCK will always fail if TEST is enabled (because a
     // request is queued)
     if (type_ == Type::MUTEX_TEST &&