X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/6260d187764dc644d699e1a53454f7efdcc682df..7e625e5e848a284b522d69ec28cb111f1f88515b:/src/mc/transition/TransitionSynchro.cpp diff --git a/src/mc/transition/TransitionSynchro.cpp b/src/mc/transition/TransitionSynchro.cpp index dbd39a5de7..3d0e0cd794 100644 --- a/src/mc/transition/TransitionSynchro.cpp +++ b/src/mc/transition/TransitionSynchro.cpp @@ -4,6 +4,8 @@ * under the terms of the license (GNU LGPL) which comes with this package. */ #include "src/mc/transition/TransitionSynchro.hpp" +#include "src/mc/mc_forward.hpp" +#include "src/mc/transition/TransitionObjectAccess.hpp" #include "xbt/asserts.h" #include "xbt/ex.h" #include "xbt/string.hpp" @@ -29,7 +31,11 @@ bool BarrierTransition::depends(const Transition* o) const if (o->type_ < type_) return o->depends(this); - if (auto* other = dynamic_cast(o)) { + // Actions executed by the same actor are always dependent + if (o->aid_ == aid_) + return true; + + if (const auto* other = dynamic_cast(o)) { if (bar_ != other->bar_) return false; @@ -46,6 +52,19 @@ bool BarrierTransition::depends(const Transition* o) const return false; // barriers are INDEP with non-barrier transitions } +bool BarrierTransition::reversible_race(const Transition* other) const +{ + switch (type_) { + case Type::BARRIER_ASYNC_LOCK: + return true; // BarrierAsyncLock is always enabled + case Type::BARRIER_WAIT: + // If the other event is a barrier lock event, then we are not reversible; + // otherwise we are reversible. + return other->type_ != Transition::Type::BARRIER_ASYNC_LOCK; + default: + xbt_die("Unexpected transition type %s", to_c_str(type_)); + } +} std::string MutexTransition::to_string(bool verbose) const { @@ -69,7 +88,7 @@ bool MutexTransition::depends(const Transition* o) const // type_ <= other->type_ in MUTEX_LOCK, MUTEX_TEST, MUTEX_TRYLOCK, MUTEX_UNLOCK, MUTEX_WAIT, - if (auto* other = dynamic_cast(o)) { + if (const auto* other = dynamic_cast(o)) { // Theorem 4.4.7: Any pair of synchronization actions of distinct actors concerning distinct mutexes are independent if (mutex_ != other->mutex_) return false; @@ -84,6 +103,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 && @@ -102,26 +127,49 @@ bool MutexTransition::depends(const Transition* o) const return false; // mutexes are INDEP with non-mutex transitions } +bool SemaphoreTransition::reversible_race(const Transition* other) const +{ + switch (type_) { + case Type::SEM_ASYNC_LOCK: + return true; // SemAsyncLock is always enabled + case Type::SEM_UNLOCK: + return true; // SemUnlock is always enabled + case Type::SEM_WAIT: + if (other->type_ == Transition::Type::SEM_UNLOCK && + static_cast(other)->get_capacity() <= 1) { + return false; + } + xbt_die("SEM_WAIT that is dependent with a SEM_UNLOCK should not be reversible. FixMe"); + return true; + default: + xbt_die("Unexpected transition type %s", to_c_str(type_)); + } +} + std::string SemaphoreTransition::to_string(bool verbose) const { if (type_ == Type::SEM_ASYNC_LOCK || type_ == Type::SEM_UNLOCK) - return xbt::string_printf("%s(semaphore: %" PRIxPTR ")", Transition::to_c_str(type_), sem_); + return xbt::string_printf("%s(semaphore: %u, capacity: %u)", Transition::to_c_str(type_), sem_, capacity_); if (type_ == Type::SEM_WAIT) - return xbt::string_printf("%s(semaphore: %" PRIxPTR ", granted: %s)", Transition::to_c_str(type_), sem_, - granted_ ? "yes" : "no"); + return xbt::string_printf("%s(semaphore: %u, capacity: %u, granted: %s)", Transition::to_c_str(type_), sem_, + capacity_, granted_ ? "yes" : "no"); THROW_IMPOSSIBLE; } SemaphoreTransition::SemaphoreTransition(aid_t issuer, int times_considered, Type type, std::stringstream& stream) : Transition(type, issuer, times_considered) { - xbt_assert(stream >> sem_ >> granted_); + xbt_assert(stream >> sem_ >> granted_ >> capacity_); } bool SemaphoreTransition::depends(const Transition* o) const { if (o->type_ < type_) return o->depends(this); - if (auto* other = dynamic_cast(o)) { + // Actions executed by the same actor are always dependent + if (o->aid_ == aid_) + return true; + + if (const auto* other = dynamic_cast(o)) { if (sem_ != other->sem_) return false; @@ -138,6 +186,10 @@ bool SemaphoreTransition::depends(const Transition* o) const if (type_ == Type::SEM_UNLOCK && other->type_ == Type::SEM_UNLOCK) return false; + // UNLOCK indep with a WAIT if the semaphore had enought capacity anyway + if (type_ == Type::SEM_UNLOCK && capacity_ > 1 && other->type_ == Type::SEM_WAIT) + return false; + // WAIT indep WAIT: // if both enabled (may happen in the initial value is sufficient), the ordering has no impact on the result. // If only one enabled, the other won't be enabled by the first one. @@ -151,4 +203,26 @@ bool SemaphoreTransition::depends(const Transition* o) const return false; // semaphores are INDEP with non-semaphore transitions } +bool MutexTransition::reversible_race(const Transition* other) const +{ + switch (type_) { + case Type::MUTEX_ASYNC_LOCK: + return true; // MutexAsyncLock is always enabled + case Type::MUTEX_TEST: + return true; // MutexTest is always enabled + case Type::MUTEX_TRYLOCK: + return true; // MutexTrylock is always enabled + case Type::MUTEX_UNLOCK: + return true; // MutexUnlock is always enabled + + case Type::MUTEX_WAIT: + // Only an Unlock can be dependent with a Wait + // and in this case, that Unlock enabled the wait + // Not reversible + return false; + default: + xbt_die("Unexpected transition type %s", to_c_str(type_)); + } +} + } // namespace simgrid::mc