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/string.hpp"
   9
  10 #include <inttypes.h>
  11 #include <sstream>
  12
  13 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_trans_synchro, mc_transition, "Logging specific to MC synchronization transitions");
  14
  15 namespace simgrid {
  16 namespace mc {
  17 std::string MutexTransition::to_string(bool verbose) const
  18 {
  19   return xbt::string_printf("%s(%" PRIxPTR ", owner:%ld)", Transition::to_c_str(type_), mutex_, owner_);
  20 }
  21
  22 MutexTransition::MutexTransition(aid_t issuer, int times_considered, Type type, std::stringstream& stream)
  23     : Transition(type, issuer, times_considered)
  24 {
  25   xbt_assert(stream >> mutex_ >> owner_);
  26 }
  27
  28 bool MutexTransition::depends(const Transition* o) const
  29 {
  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
  38     // Theorem 4.4.7: Any pair of synchronization actions of distinct actors concerning distinct mutexes are independent
  39     if (mutex_ != other->mutex_)
  40       return false;
  41
  42     // Theorem 4.4.11: LOCK indep TEST/WAIT.
  43     //  If both enabled, the result does not depend on their order. If WAIT is not enabled, LOCK won't enable it.
  44     if (type_ == Type::MUTEX_LOCK && (other->type_ == Type::MUTEX_TEST || other->type_ == Type::MUTEX_WAIT))
  45       return false;
  46
  47     // Theorem 4.4.8: LOCK indep UNLOCK.
  48     //  pop_front and push_back are independent.
  49     if (type_ == Type::MUTEX_LOCK && other->type_ == Type::MUTEX_UNLOCK)
  50       return false;
  51
  52     // TEST is a pure function; TEST/WAIT won't change the owner; TRYLOCK will always fail if TEST is enabled (because a
  53     // request is queued)
  54     if (type_ == Type::MUTEX_TEST &&
  55         (other->type_ == Type::MUTEX_TEST || other->type_ == Type::MUTEX_TRYLOCK || other->type_ == Type::MUTEX_WAIT))
  56       return false;
  57
  58     // TRYLOCK will always fail if TEST is enabled (because a request is queued), and may not overpass the WAITed
  59     // request in the queue
  60     if (type_ == Type::MUTEX_TRYLOCK && other->type_ == Type::MUTEX_WAIT)
  61       return false;
  62
  63     // FIXME: UNLOCK indep WAIT/TEST iff wait/test are not first in the waiting queue
  64   }
  65
  66   return true; // FIXME: TODO
  67 }
  68
  69 } // namespace mc
  70 } // namespace simgrid