src/mc/api/TransitionComm.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/api/TransitionComm.hpp"
   7 #include "xbt/asserts.h"
   8 #include <simgrid/config.h>
   9 #if SIMGRID_HAVE_MC
  10 #include "src/mc/ModelChecker.hpp"
  11 #include "src/mc/Session.hpp"
  12 #include "src/mc/api/State.hpp"
  13 #endif
  14
  15 #include <sstream>
  16
  17 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_trans_comm, mc_transition,
  18                                 "Logging specific to MC transitions about communications");
  19
  20 namespace simgrid {
  21 namespace mc {
  22
  23 CommWaitTransition::CommWaitTransition(aid_t issuer, int times_considered, std::stringstream& stream)
  24     : Transition(Type::COMM_WAIT, issuer, times_considered)
  25 {
  26   xbt_assert(stream >> timeout_ >> comm_ >> sender_ >> receiver_ >> mbox_ >> src_buff_ >> dst_buff_ >> size_);
  27   XBT_DEBUG("CommWaitTransition %s comm:%p, sender:%ld receiver:%ld mbox:%u sbuff:%p rbuff:%p size:%zu",
  28             (timeout_ ? "timeout" : "no-timeout"), comm_, sender_, receiver_, mbox_, src_buff_, dst_buff_, size_);
  29 }
  30 std::string CommWaitTransition::to_string(bool verbose) const
  31 {
  32   auto res = xbt::string_printf("%ld: WaitComm(from %ld to %ld, mbox=%u, %s", aid_, sender_, receiver_, mbox_,
  33                                 (timeout_ ? "timeout" : "no timeout"));
  34   if (verbose) {
  35     res += ", src_buff=" + xbt::string_printf("%p", src_buff_) + ", size=" + std::to_string(size_);
  36     res += ", dst_buff=" + xbt::string_printf("%p", dst_buff_);
  37   }
  38   res += ")";
  39   return res;
  40 }
  41 bool CommWaitTransition::depends(const Transition* other) const
  42 {
  43   if (aid_ == other->aid_)
  44     return false;
  45
  46   if (other->type_ < type_)
  47     return other->depends(this);
  48
  49   if (const auto* wait = dynamic_cast<const CommWaitTransition*>(other)) {
  50     if (timeout_ || wait->timeout_)
  51       return true; // Timeouts are not considered by the independence theorem, thus assumed dependent
  52
  53     if (src_buff_ == wait->src_buff_ && dst_buff_ == wait->dst_buff_)
  54       return false;
  55     if (src_buff_ != nullptr && dst_buff_ != nullptr && wait->src_buff_ != nullptr && wait->dst_buff_ != nullptr &&
  56         dst_buff_ != wait->src_buff_ && dst_buff_ != wait->dst_buff_ && dst_buff_ != src_buff_)
  57       return false;
  58   }
  59
  60   return true;
  61 }
  62 CommTestTransition::CommTestTransition(aid_t issuer, int times_considered, std::stringstream& stream)
  63     : Transition(Type::COMM_TEST, issuer, times_considered)
  64 {
  65   xbt_assert(stream >> comm_ >> sender_ >> receiver_ >> mbox_ >> src_buff_ >> dst_buff_ >> size_);
  66   XBT_DEBUG("CommTestTransition comm:%p, sender:%ld receiver:%ld mbox:%u sbuff:%p rbuff:%p size:%zu", comm_, sender_,
  67             receiver_, mbox_, src_buff_, dst_buff_, size_);
  68 }
  69 std::string CommTestTransition::to_string(bool verbose) const
  70 {
  71   auto res = xbt::string_printf("%ld: TestComm(from %ld to %ld, mbox=%u", aid_, sender_, receiver_, mbox_);
  72   if (verbose) {
  73     res += ", src_buff=" + xbt::string_printf("%p", src_buff_) + ", size=" + std::to_string(size_);
  74     res += ", dst_buff=" + xbt::string_printf("%p", dst_buff_);
  75   }
  76   res += ")";
  77   return res;
  78 }
  79 bool CommTestTransition::depends(const Transition* other) const
  80 {
  81   if (aid_ == other->aid_)
  82     return false;
  83
  84   if (other->type_ < type_)
  85     return other->depends(this);
  86
  87   if (dynamic_cast<const CommTestTransition*>(other) != nullptr)
  88     return false; // Test & Test are independent
  89
  90   if (const auto* wait = dynamic_cast<const CommWaitTransition*>(other)) {
  91     if (wait->timeout_)
  92       return true; // Timeouts are not considered by the independence theorem, thus assumed dependent
  93
  94     /* Wait & Test are independent */
  95     return false;
  96   }
  97
  98   return true;
  99 }
 100
 101 CommRecvTransition::CommRecvTransition(aid_t issuer, int times_considered, std::stringstream& stream)
 102     : Transition(Type::COMM_RECV, issuer, times_considered)
 103 {
 104   xbt_assert(stream >> comm_ >> mbox_ >> dst_buff_);
 105 }
 106 std::string CommRecvTransition::to_string(bool verbose) const
 107 {
 108   auto res = xbt::string_printf("%ld: iRecv(mbox=%u", aid_, mbox_);
 109   if (verbose)
 110     res += ", buff=" + xbt::string_printf("%p", dst_buff_);
 111   res += ")";
 112   return res;
 113 }
 114 bool CommRecvTransition::depends(const Transition* other) const
 115 {
 116   if (aid_ == other->aid_)
 117     return false;
 118
 119   if (other->type_ < type_)
 120     return other->depends(this);
 121
 122   if (const auto* recv = dynamic_cast<const CommRecvTransition*>(other))
 123     return mbox_ == recv->mbox_;
 124
 125   if (dynamic_cast<const CommSendTransition*>(other) != nullptr)
 126     return false;
 127
 128   if (const auto* test = dynamic_cast<const CommTestTransition*>(other)) {
 129     if (mbox_ != test->mbox_)
 130       return false;
 131
 132     if ((aid_ != test->sender_) && (aid_ != test->receiver_) && (test->dst_buff_ != dst_buff_))
 133       return false;
 134   }
 135
 136   if (auto* wait = dynamic_cast<const CommWaitTransition*>(other)) {
 137     if (wait->timeout_)
 138       return true;
 139
 140     if (mbox_ != wait->mbox_)
 141       return false;
 142
 143     if ((aid_ != wait->sender_) && (aid_ != wait->receiver_) && (wait->dst_buff_ != dst_buff_))
 144       return false;
 145   }
 146
 147   return true;
 148 }
 149
 150 CommSendTransition::CommSendTransition(aid_t issuer, int times_considered, std::stringstream& stream)
 151     : Transition(Type::COMM_SEND, issuer, times_considered)
 152 {
 153   xbt_assert(stream >> comm_ >> mbox_ >> src_buff_ >> size_);
 154   XBT_DEBUG("SendTransition comm:%p mbox:%u buff:%p size:%zu", comm_, mbox_, src_buff_, size_);
 155 }
 156 std::string CommSendTransition::to_string(bool verbose = false) const
 157 {
 158   auto res = xbt::string_printf("%ld: iSend(mbox=%u", aid_, mbox_);
 159   if (verbose)
 160     res += ", buff=" + xbt::string_printf("%p", src_buff_) + ", size=" + std::to_string(size_);
 161   res += ")";
 162   return res;
 163 }
 164 TestAnyTransition::TestAnyTransition(aid_t issuer, int times_considered, std::stringstream& stream)
 165     : Transition(Type::TESTANY, issuer, times_considered)
 166 {
 167   int size;
 168   xbt_assert(stream >> size);
 169   for (int i = 0; i < size; i++) {
 170     Transition* t = deserialize_transition(issuer, 0, stream);
 171     XBT_DEBUG("TestAny received a transition %s", t->to_string(true).c_str());
 172     transitions_.push_back(t);
 173   }
 174 }
 175 std::string TestAnyTransition::to_string(bool verbose) const
 176 {
 177   auto res = xbt::string_printf("%ld: TestAny{ ", aid_);
 178   for (auto const* t : transitions_)
 179     res += t->to_string(verbose);
 180   res += "}";
 181   return res;
 182 }
 183 bool TestAnyTransition::depends(const Transition* other) const
 184 {
 185   return transitions_[times_considered_]->depends(other);
 186 }
 187 WaitAnyTransition::WaitAnyTransition(aid_t issuer, int times_considered, std::stringstream& stream)
 188     : Transition(Type::WAITANY, issuer, times_considered)
 189 {
 190   int size;
 191   xbt_assert(stream >> size);
 192   for (int i = 0; i < size; i++) {
 193     Transition* t = deserialize_transition(issuer, 0, stream);
 194     transitions_.push_back(t);
 195   }
 196 }
 197 std::string WaitAnyTransition::to_string(bool verbose) const
 198 {
 199   auto res = xbt::string_printf("%ld: WaitAny{ ", aid_);
 200   for (auto const* t : transitions_)
 201     res += t->to_string(verbose);
 202   res += "}";
 203   return res;
 204 }
 205 bool WaitAnyTransition::depends(const Transition* other) const
 206 {
 207   return transitions_[times_considered_]->depends(other);
 208 }
 209
 210 bool CommSendTransition::depends(const Transition* other) const
 211 {
 212   if (aid_ == other->aid_)
 213     return false;
 214
 215   if (other->type_ < type_)
 216     return other->depends(this);
 217
 218   if (const auto* other_isend = dynamic_cast<const CommSendTransition*>(other))
 219     return mbox_ == other_isend->mbox_;
 220
 221   if (dynamic_cast<const CommRecvTransition*>(other) != nullptr)
 222     return false;
 223
 224   if (const auto* test = dynamic_cast<const CommTestTransition*>(other)) {
 225     if (mbox_ != test->mbox_)
 226       return false;
 227
 228     if ((aid_ != test->sender_) && (aid_ != test->receiver_) && (test->src_buff_ != src_buff_))
 229       return false;
 230   }
 231
 232   if (const auto* wait = dynamic_cast<const CommWaitTransition*>(other)) {
 233     if (wait->timeout_)
 234       return true;
 235
 236     if (mbox_ != wait->mbox_)
 237       return false;
 238
 239     if ((aid_ != wait->sender_) && (aid_ != wait->receiver_) && (wait->src_buff_ != src_buff_))
 240       return false;
 241   }
 242
 243   return true;
 244 }
 245
 246 Transition* deserialize_transition(aid_t issuer, int times_considered, std::stringstream& stream)
 247 {
 248   short type;
 249   xbt_assert(stream >> type);
 250   xbt_assert(type >= 0 && type <= static_cast<short>(Transition::Type::UNKNOWN), "Invalid transition type %d received",
 251              type);
 252
 253   auto simcall = static_cast<Transition::Type>(type);
 254
 255   switch (simcall) {
 256     case Transition::Type::COMM_RECV:
 257       return new CommRecvTransition(issuer, times_considered, stream);
 258     case Transition::Type::COMM_SEND:
 259       return new CommSendTransition(issuer, times_considered, stream);
 260     case Transition::Type::COMM_TEST:
 261       return new CommTestTransition(issuer, times_considered, stream);
 262     case Transition::Type::COMM_WAIT:
 263       return new CommWaitTransition(issuer, times_considered, stream);
 264
 265     case Transition::Type::TESTANY:
 266       return new TestAnyTransition(issuer, times_considered, stream);
 267     case Transition::Type::WAITANY:
 268       return new WaitAnyTransition(issuer, times_considered, stream);
 269
 270     case Transition::Type::RANDOM:
 271       return new RandomTransition(issuer, times_considered, stream);
 272
 273     case Transition::Type::UNKNOWN:
 274       return new Transition(Transition::Type::UNKNOWN, issuer, times_considered);
 275   }
 276   THROW_IMPOSSIBLE; // Some compilers don't detect that each branch of the above switch has a return
 277 }
 278
 279 } // namespace mc
 280 } // namespace simgrid