From a7cc502f224afb96f0203b94759cd0dabebf8de5 Mon Sep 17 00:00:00 2001 From: mlaurent Date: Thu, 9 Nov 2023 12:17:28 +0100 Subject: [PATCH] Add a missing independence theorem about Mutex --- src/mc/transition/TransitionSynchro.cpp | 6 ++++++ 1 file changed, 6 insertions(+) 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 && -- 2.20.1