src/mc/transition/TransitionSynchro.cpp

   1 /* Copyright (c) 2015-2023. The SimGrid Team. All rights reserved.          */
   2
   3 /* This program is free software; you can redistribute it and/or modify it
   4  * under the terms of the license (GNU LGPL) which comes with this package. */
   5
   6 #include "src/mc/transition/TransitionSynchro.hpp"
   7 #include "src/mc/mc_forward.hpp"
   8 #include "src/mc/transition/TransitionObjectAccess.hpp"
   9 #include "xbt/asserts.h"
  10 #include "xbt/ex.h"
  11 #include "xbt/string.hpp"
  12
  13 #include <inttypes.h>
  14 #include <sstream>
  15
  16 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_trans_synchro, mc_transition, "Logging specific to MC synchronization transitions");
  17
  18 namespace simgrid::mc {
  19
  20 std::string BarrierTransition::to_string(bool verbose) const
  21 {
  22   return xbt::string_printf("%s(barrier: %u)", Transition::to_c_str(type_), bar_);
  23 }
  24 BarrierTransition::BarrierTransition(aid_t issuer, int times_considered, Type type, std::stringstream& stream)
  25     : Transition(type, issuer, times_considered)
  26 {
  27   xbt_assert(stream >> bar_);
  28 }
  29 bool BarrierTransition::depends(const Transition* o) const
  30 {
  31   if (o->type_ < type_)
  32     return o->depends(this);
  33
  34   // Actions executed by the same actor are always dependent
  35   if (o->aid_ == aid_)
  36     return true;
  37
  38   if (const auto* other = dynamic_cast<const BarrierTransition*>(o)) {
  39     if (bar_ != other->bar_)
  40       return false;
  41
  42     // LOCK indep LOCK: requests are not ordered in a barrier
  43     if (type_ == Type::BARRIER_ASYNC_LOCK && other->type_ == Type::BARRIER_ASYNC_LOCK)
  44       return false;
  45
  46     // WAIT indep WAIT: requests are not ordered
  47     if (type_ == Type::BARRIER_WAIT && other->type_ == Type::BARRIER_WAIT)
  48       return false;
  49
  50     return true; // LOCK/WAIT is dependent because lock may enable wait
  51   }
  52
  53   return false; // barriers are INDEP with non-barrier transitions
  54 }
  55 bool BarrierTransition::reversible_race(const Transition* other) const
  56 {
  57   switch (type_) {
  58     case Type::BARRIER_ASYNC_LOCK:
  59       return true; // BarrierAsyncLock is always enabled
  60     case Type::BARRIER_WAIT:
  61       // If the other event is a barrier lock event, then we are not reversible;
  62       // otherwise we are reversible.
  63       return other->type_ != Transition::Type::BARRIER_ASYNC_LOCK;
  64     default:
  65       xbt_die("Unexpected transition type %s", to_c_str(type_));
  66   }
  67 }
  68
  69 std::string MutexTransition::to_string(bool verbose) const
  70 {
  71   return xbt::string_printf("%s(mutex: %" PRIxPTR ", owner: %ld)", Transition::to_c_str(type_), mutex_, owner_);
  72 }
  73
  74 MutexTransition::MutexTransition(aid_t issuer, int times_considered, Type type, std::stringstream& stream)
  75     : Transition(type, issuer, times_considered)
  76 {
  77   xbt_assert(stream >> mutex_ >> owner_);
  78 }
  79
  80 bool MutexTransition::depends(const Transition* o) const
  81 {
  82   if (o->type_ < type_)
  83     return o->depends(this);
  84
  85   // Actions executed by the same actor are always dependent
  86   if (o->aid_ == aid_)
  87     return true;
  88
  89   // type_ <= other->type_ in  MUTEX_LOCK, MUTEX_TEST, MUTEX_TRYLOCK, MUTEX_UNLOCK, MUTEX_WAIT,
  90
  91   if (const auto* other = dynamic_cast<const MutexTransition*>(o)) {
  92     // Theorem 4.4.7: Any pair of synchronization actions of distinct actors concerning distinct mutexes are independent
  93     if (mutex_ != other->mutex_)
  94       return false;
  95
  96     // Theorem 4.4.11: LOCK indep TEST/WAIT.
  97     //  If both enabled, the result does not depend on their order. If WAIT is not enabled, LOCK won't enable it.
  98     if (type_ == Type::MUTEX_ASYNC_LOCK && (other->type_ == Type::MUTEX_TEST || other->type_ == Type::MUTEX_WAIT))
  99       return false;
 100
 101     // Theorem 4.4.8: LOCK indep UNLOCK.
 102     //  pop_front and push_back are independent.
 103     if (type_ == Type::MUTEX_ASYNC_LOCK && other->type_ == Type::MUTEX_UNLOCK)
 104       return false;
 105
 106     // Theorem 4.4.9: LOCK indep UNLOCK.
 107     //  any combination of wait and test is indenpendent.
 108     if ((type_ == Type::MUTEX_WAIT || type_ == Type::MUTEX_TEST) &&
 109         (other->type_ == Type::MUTEX_WAIT || other->type_ == Type::MUTEX_TEST))
 110       return false;
 111
 112     // TEST is a pure function; TEST/WAIT won't change the owner; TRYLOCK will always fail if TEST is enabled (because a
 113     // request is queued)
 114     if (type_ == Type::MUTEX_TEST &&
 115         (other->type_ == Type::MUTEX_TEST || other->type_ == Type::MUTEX_TRYLOCK || other->type_ == Type::MUTEX_WAIT))
 116       return false;
 117
 118     // TRYLOCK will always fail if TEST is enabled (because a request is queued), and may not overpass the WAITed
 119     // request in the queue
 120     if (type_ == Type::MUTEX_TRYLOCK && other->type_ == Type::MUTEX_WAIT)
 121       return false;
 122
 123     // FIXME: UNLOCK indep WAIT/TEST iff wait/test are not first in the waiting queue
 124     return true;
 125   }
 126
 127   return false; // mutexes are INDEP with non-mutex transitions
 128 }
 129
 130 bool SemaphoreTransition::reversible_race(const Transition* other) const
 131 {
 132   switch (type_) {
 133     case Type::SEM_ASYNC_LOCK:
 134       return true; // SemAsyncLock is always enabled
 135     case Type::SEM_UNLOCK:
 136       return true; // SemUnlock is always enabled
 137     case Type::SEM_WAIT:
 138       if (other->type_ == Transition::Type::SEM_UNLOCK &&
 139           static_cast<const SemaphoreTransition*>(other)->get_capacity() <= 1) {
 140         return false;
 141       }
 142       xbt_die("SEM_WAIT that is dependent with a SEM_UNLOCK should not be reversible. FixMe");
 143       return true;
 144     default:
 145       xbt_die("Unexpected transition type %s", to_c_str(type_));
 146   }
 147 }
 148
 149 std::string SemaphoreTransition::to_string(bool verbose) const
 150 {
 151   if (type_ == Type::SEM_ASYNC_LOCK || type_ == Type::SEM_UNLOCK)
 152     return xbt::string_printf("%s(semaphore: %u, capacity: %u)", Transition::to_c_str(type_), sem_, capacity_);
 153   if (type_ == Type::SEM_WAIT)
 154     return xbt::string_printf("%s(semaphore: %u, capacity: %u, granted: %s)", Transition::to_c_str(type_), sem_,
 155                               capacity_, granted_ ? "yes" : "no");
 156   THROW_IMPOSSIBLE;
 157 }
 158 SemaphoreTransition::SemaphoreTransition(aid_t issuer, int times_considered, Type type, std::stringstream& stream)
 159     : Transition(type, issuer, times_considered)
 160 {
 161   xbt_assert(stream >> sem_ >> granted_ >> capacity_);
 162 }
 163 bool SemaphoreTransition::depends(const Transition* o) const
 164 {
 165   if (o->type_ < type_)
 166     return o->depends(this);
 167
 168   // Actions executed by the same actor are always dependent
 169   if (o->aid_ == aid_)
 170     return true;
 171
 172   if (const auto* other = dynamic_cast<const SemaphoreTransition*>(o)) {
 173     if (sem_ != other->sem_)
 174       return false;
 175
 176     // LOCK indep UNLOCK: pop_front and push_back are independent.
 177     if (type_ == Type::SEM_ASYNC_LOCK && other->type_ == Type::SEM_UNLOCK)
 178       return false;
 179
 180     // LOCK indep WAIT: If both enabled, ordering has no impact on the result. If WAIT is not enabled, LOCK won't enable
 181     // it.
 182     if (type_ == Type::SEM_ASYNC_LOCK && other->type_ == Type::SEM_WAIT)
 183       return false;
 184
 185     // UNLOCK indep UNLOCK: ordering of two pop_front has no impact
 186     if (type_ == Type::SEM_UNLOCK && other->type_ == Type::SEM_UNLOCK)
 187       return false;
 188
 189     // UNLOCK indep with a WAIT if the semaphore had enought capacity anyway
 190     if (type_ == Type::SEM_UNLOCK && capacity_ > 1 && other->type_ == Type::SEM_WAIT)
 191       return false;
 192
 193     // WAIT indep WAIT:
 194     // if both enabled (may happen in the initial value is sufficient), the ordering has no impact on the result.
 195     // If only one enabled, the other won't be enabled by the first one.
 196     // If none enabled, well, nothing will change.
 197     if (type_ == Type::SEM_WAIT && other->type_ == Type::SEM_WAIT)
 198       return false;
 199
 200     return true; // Other semaphore cases are dependent
 201   }
 202
 203   return false; // semaphores are INDEP with non-semaphore transitions
 204 }
 205
 206 bool MutexTransition::reversible_race(const Transition* other) const
 207 {
 208   switch (type_) {
 209     case Type::MUTEX_ASYNC_LOCK:
 210       return true; // MutexAsyncLock is always enabled
 211     case Type::MUTEX_TEST:
 212       return true; // MutexTest is always enabled
 213     case Type::MUTEX_TRYLOCK:
 214       return true; // MutexTrylock is always enabled
 215     case Type::MUTEX_UNLOCK:
 216       return true; // MutexUnlock is always enabled
 217
 218     case Type::MUTEX_WAIT:
 219       // Only an Unlock can be dependent with a Wait
 220       // and in this case, that Unlock enabled the wait
 221       // Not reversible
 222       return false;
 223     default:
 224       xbt_die("Unexpected transition type %s", to_c_str(type_));
 225   }
 226 }
 227
 228 } // namespace simgrid::mc