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 "xbt/asserts.h"
   8 #include "xbt/ex.h"
   9 #include "xbt/string.hpp"
  10
  11 #include <inttypes.h>
  12 #include <sstream>
  13
  14 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_trans_synchro, mc_transition, "Logging specific to MC synchronization transitions");
  15
  16 namespace simgrid::mc {
  17
  18 std::string BarrierTransition::to_string(bool verbose) const
  19 {
  20   return xbt::string_printf("%s(barrier: %u)", Transition::to_c_str(type_), bar_);
  21 }
  22 BarrierTransition::BarrierTransition(aid_t issuer, int times_considered, Type type, std::stringstream& stream)
  23     : Transition(type, issuer, times_considered)
  24 {
  25   xbt_assert(stream >> bar_);
  26 }
  27 bool BarrierTransition::depends(const Transition* o) const
  28 {
  29   if (o->type_ < type_)
  30     return o->depends(this);
  31
  32   // Actions executed by the same actor are always dependent
  33   if (o->aid_ == aid_)
  34     return true;
  35
  36   if (const auto* other = dynamic_cast<const BarrierTransition*>(o)) {
  37     if (bar_ != other->bar_)
  38       return false;
  39
  40     // LOCK indep LOCK: requests are not ordered in a barrier
  41     if (type_ == Type::BARRIER_ASYNC_LOCK && other->type_ == Type::BARRIER_ASYNC_LOCK)
  42       return false;
  43
  44     // WAIT indep WAIT: requests are not ordered
  45     if (type_ == Type::BARRIER_WAIT && other->type_ == Type::BARRIER_WAIT)
  46       return false;
  47
  48     return true; // LOCK/WAIT is dependent because lock may enable wait
  49   }
  50
  51   return false; // barriers are INDEP with non-barrier transitions
  52 }
  53
  54 std::string MutexTransition::to_string(bool verbose) const
  55 {
  56   return xbt::string_printf("%s(mutex: %" PRIxPTR ", owner: %ld)", Transition::to_c_str(type_), mutex_, owner_);
  57 }
  58
  59 MutexTransition::MutexTransition(aid_t issuer, int times_considered, Type type, std::stringstream& stream)
  60     : Transition(type, issuer, times_considered)
  61 {
  62   xbt_assert(stream >> mutex_ >> owner_);
  63 }
  64
  65 bool MutexTransition::depends(const Transition* o) const
  66 {
  67   if (o->type_ < type_)
  68     return o->depends(this);
  69
  70   // Actions executed by the same actor are always dependent
  71   if (o->aid_ == aid_)
  72     return true;
  73
  74   // type_ <= other->type_ in  MUTEX_LOCK, MUTEX_TEST, MUTEX_TRYLOCK, MUTEX_UNLOCK, MUTEX_WAIT,
  75
  76   if (const auto* other = dynamic_cast<const MutexTransition*>(o)) {
  77     // Theorem 4.4.7: Any pair of synchronization actions of distinct actors concerning distinct mutexes are independent
  78     if (mutex_ != other->mutex_)
  79       return false;
  80
  81     // Theorem 4.4.11: LOCK indep TEST/WAIT.
  82     //  If both enabled, the result does not depend on their order. If WAIT is not enabled, LOCK won't enable it.
  83     if (type_ == Type::MUTEX_ASYNC_LOCK && (other->type_ == Type::MUTEX_TEST || other->type_ == Type::MUTEX_WAIT))
  84       return false;
  85
  86     // Theorem 4.4.8: LOCK indep UNLOCK.
  87     //  pop_front and push_back are independent.
  88     if (type_ == Type::MUTEX_ASYNC_LOCK && other->type_ == Type::MUTEX_UNLOCK)
  89       return false;
  90
  91     // Theorem 4.4.9: LOCK indep UNLOCK.
  92     //  any combination of wait and test is indenpendent.
  93     if ((type_ == Type::MUTEX_WAIT || type_ == Type::MUTEX_TEST) &&
  94         (other->type_ == Type::MUTEX_WAIT || other->type_ == Type::MUTEX_TEST))
  95       return false;
  96
  97     // TEST is a pure function; TEST/WAIT won't change the owner; TRYLOCK will always fail if TEST is enabled (because a
  98     // request is queued)
  99     if (type_ == Type::MUTEX_TEST &&
 100         (other->type_ == Type::MUTEX_TEST || other->type_ == Type::MUTEX_TRYLOCK || other->type_ == Type::MUTEX_WAIT))
 101       return false;
 102
 103     // TRYLOCK will always fail if TEST is enabled (because a request is queued), and may not overpass the WAITed
 104     // request in the queue
 105     if (type_ == Type::MUTEX_TRYLOCK && other->type_ == Type::MUTEX_WAIT)
 106       return false;
 107
 108     // FIXME: UNLOCK indep WAIT/TEST iff wait/test are not first in the waiting queue
 109     return true;
 110   }
 111
 112   return false; // mutexes are INDEP with non-mutex transitions
 113 }
 114
 115 std::string SemaphoreTransition::to_string(bool verbose) const
 116 {
 117   if (type_ == Type::SEM_ASYNC_LOCK || type_ == Type::SEM_UNLOCK)
 118     return xbt::string_printf("%s(semaphore: %u, capacity: %u)", Transition::to_c_str(type_), sem_, capacity_);
 119   if (type_ == Type::SEM_WAIT)
 120     return xbt::string_printf("%s(semaphore: %u, capacity: %u, granted: %s)", Transition::to_c_str(type_), sem_,
 121                               capacity_, granted_ ? "yes" : "no");
 122   THROW_IMPOSSIBLE;
 123 }
 124 SemaphoreTransition::SemaphoreTransition(aid_t issuer, int times_considered, Type type, std::stringstream& stream)
 125     : Transition(type, issuer, times_considered)
 126 {
 127   xbt_assert(stream >> sem_ >> granted_ >> capacity_);
 128 }
 129 bool SemaphoreTransition::depends(const Transition* o) const
 130 {
 131   if (o->type_ < type_)
 132     return o->depends(this);
 133
 134   // Actions executed by the same actor are always dependent
 135   if (o->aid_ == aid_)
 136     return true;
 137
 138   if (const auto* other = dynamic_cast<const SemaphoreTransition*>(o)) {
 139     if (sem_ != other->sem_)
 140       return false;
 141
 142     // LOCK indep UNLOCK: pop_front and push_back are independent.
 143     if (type_ == Type::SEM_ASYNC_LOCK && other->type_ == Type::SEM_UNLOCK)
 144       return false;
 145
 146     // LOCK indep WAIT: If both enabled, ordering has no impact on the result. If WAIT is not enabled, LOCK won't enable
 147     // it.
 148     if (type_ == Type::SEM_ASYNC_LOCK && other->type_ == Type::SEM_WAIT)
 149       return false;
 150
 151     // UNLOCK indep UNLOCK: ordering of two pop_front has no impact
 152     if (type_ == Type::SEM_UNLOCK && other->type_ == Type::SEM_UNLOCK)
 153       return false;
 154
 155     // UNLOCK indep with a WAIT if the semaphore had enought capacity anyway
 156     if (type_ == Type::SEM_UNLOCK && capacity_ > 1 && other->type_ == Type::SEM_WAIT)
 157       return false;
 158
 159     // WAIT indep WAIT:
 160     // if both enabled (may happen in the initial value is sufficient), the ordering has no impact on the result.
 161     // If only one enabled, the other won't be enabled by the first one.
 162     // If none enabled, well, nothing will change.
 163     if (type_ == Type::SEM_WAIT && other->type_ == Type::SEM_WAIT)
 164       return false;
 165
 166     return true; // Other semaphore cases are dependent
 167   }
 168
 169   return false; // semaphores are INDEP with non-semaphore transitions
 170 }
 171
 172 } // namespace simgrid::mc