From e85d120681d3aa69b6b56b9bc0aa2a54498294f2 Mon Sep 17 00:00:00 2001 From: Martin Quinson Date: Thu, 3 Mar 2022 15:42:57 +0100 Subject: [PATCH] Mutex are now DPOR compatible --- src/kernel/activity/MutexImpl.cpp | 11 ----------- 1 file changed, 11 deletions(-) diff --git a/src/kernel/activity/MutexImpl.cpp b/src/kernel/activity/MutexImpl.cpp index ba67c348a0..17b3936f59 100644 --- a/src/kernel/activity/MutexImpl.cpp +++ b/src/kernel/activity/MutexImpl.cpp @@ -6,16 +6,6 @@ #include "src/kernel/activity/MutexImpl.hpp" #include "src/kernel/activity/Synchro.hpp" -#if SIMGRID_HAVE_MC -#include "simgrid/modelchecker.h" -#include "src/mc/mc_safety.hpp" -#define MC_CHECK_NO_DPOR() \ - xbt_assert(not MC_is_active() || mc::reduction_mode != mc::ReductionMode::dpor, \ - "Mutex is currently not supported with DPOR, use --cfg=model-check/reduction:none") -#else -#define MC_CHECK_NO_DPOR() (void)0 -#endif - XBT_LOG_NEW_DEFAULT_SUBCATEGORY(ker_mutex, ker_synchro, "Mutex kernel-space implementation"); namespace simgrid { @@ -77,7 +67,6 @@ MutexAcquisitionImplPtr MutexImpl::lock_async(actor::ActorImpl* issuer) bool MutexImpl::try_lock(actor::ActorImpl* issuer) { XBT_IN("(%p, %p)", this, issuer); - MC_CHECK_NO_DPOR(); if (owner_ != nullptr) { XBT_OUT(); return false; -- 2.20.1