From e80fc92c523fadeda71f4f7c2f0ca6a5a7dea7a7 Mon Sep 17 00:00:00 2001 From: mlaurent Date: Thu, 9 Nov 2023 12:18:06 +0100 Subject: [PATCH] Raffine reversible race calculation for MutexWait --- src/mc/explo/odpor/ReversibleRaceCalculator.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/mc/explo/odpor/ReversibleRaceCalculator.cpp b/src/mc/explo/odpor/ReversibleRaceCalculator.cpp index a7de9b92ec..5fcb30e2c3 100644 --- a/src/mc/explo/odpor/ReversibleRaceCalculator.cpp +++ b/src/mc/explo/odpor/ReversibleRaceCalculator.cpp @@ -153,9 +153,10 @@ bool ReversibleRaceCalculator::is_race_reversible_MutexUnlock(const Execution&, bool ReversibleRaceCalculator::is_race_reversible_MutexWait(const Execution& E, Execution::EventHandle e1, const Transition* /*e2*/) { - // TODO: for now we over approximate the reversibility - - return true; + // Only an Unlock can be dependent with a Wait + // and in this case, the Unlock enbaled the wait + // Not reversibled + return false; } bool ReversibleRaceCalculator::is_race_reversible_SemAsyncLock(const Execution&, Execution::EventHandle /*e1*/, -- 2.20.1