src/mc/transition/TransitionSynchro.cpp

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