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