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   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 (dynamic_cast<const RandomTransition*>(other) != nullptr)
  47     return false; // Random is indep with any transition
  48
  49   if (auto* any = dynamic_cast<const WaitAnyTransition*>(other))
  50     return any->depends(this);
  51   if (auto* any = dynamic_cast<const TestAnyTransition*>(other))
  52     return any->depends(this);
  53
  54   if (auto* recv = dynamic_cast<const CommRecvTransition*>(other))
  55     return recv->depends(this);
  56
  57   if (auto* send = dynamic_cast<const CommSendTransition*>(other))
  58     return send->depends(this);
  59
  60   if (auto* test = dynamic_cast<const CommTestTransition*>(other))
  61     return test->depends(this);
  62
  63   if (const auto* wait = dynamic_cast<const CommWaitTransition*>(other)) {
  64     if (timeout_ || wait->timeout_)
  65       return true; // Timeouts are not considered by the independence theorem, thus assumed dependent
  66
  67     if (src_buff_ == wait->src_buff_ && dst_buff_ == wait->dst_buff_)
  68       return false;
  69     if (src_buff_ != nullptr && dst_buff_ != nullptr && wait->src_buff_ != nullptr && wait->dst_buff_ != nullptr &&
  70         dst_buff_ != wait->src_buff_ && dst_buff_ != wait->dst_buff_ && dst_buff_ != src_buff_)
  71       return false;
  72   }
  73
  74   return true;
  75 }
  76 CommTestTransition::CommTestTransition(aid_t issuer, int times_considered, std::stringstream& stream)
  77     : Transition(Type::COMM_TEST, issuer, times_considered)
  78 {
  79   stream >> comm_ >> sender_ >> receiver_ >> mbox_ >> src_buff_ >> dst_buff_ >> size_;
  80   XBT_DEBUG("CommTestTransition comm:%p, sender:%ld receiver:%ld mbox:%u sbuff:%p rbuff:%p size:%zu", comm_, sender_,
  81             receiver_, mbox_, src_buff_, dst_buff_, size_);
  82 }
  83 std::string CommTestTransition::to_string(bool verbose) const
  84 {
  85   auto res = xbt::string_printf("%ld: TestComm(from %ld to %ld, mbox=%u", aid_, sender_, receiver_, mbox_);
  86   if (verbose) {
  87     res += ", src_buff=" + xbt::string_printf("%p", src_buff_) + ", size=" + std::to_string(size_);
  88     res += ", dst_buff=" + xbt::string_printf("%p", dst_buff_);
  89   }
  90   res += ")";
  91   return res;
  92 }
  93 bool CommTestTransition::depends(const Transition* other) const
  94 {
  95   if (aid_ == other->aid_)
  96     return false;
  97
  98   if (dynamic_cast<const RandomTransition*>(other) != nullptr)
  99     return false; // Test & Random are independent (Random is independent with anything)
 100
 101   if (auto* any = dynamic_cast<const WaitAnyTransition*>(other))
 102     return any->depends(this);
 103   if (auto* any = dynamic_cast<const TestAnyTransition*>(other))
 104     return any->depends(this);
 105
 106   if (auto* recv = dynamic_cast<const CommRecvTransition*>(other))
 107     return recv->depends(this); // Recv < Test (alphabetical ordering)
 108
 109   if (auto* send = dynamic_cast<const CommSendTransition*>(other))
 110     return send->depends(this); // Send < Test (alphabetical ordering)
 111
 112   if (dynamic_cast<const CommTestTransition*>(other) != nullptr)
 113     return false; // Test & Test are independent
 114
 115   if (const auto* wait = dynamic_cast<const CommWaitTransition*>(other)) {
 116     if (wait->timeout_)
 117       return true; // Timeouts are not considered by the independence theorem, thus assumed dependent
 118
 119     /* Wait & Test are independent */
 120     return false;
 121   }
 122
 123   return true;
 124 }
 125
 126 CommRecvTransition::CommRecvTransition(aid_t issuer, int times_considered, std::stringstream& stream)
 127     : Transition(Type::COMM_RECV, issuer, times_considered)
 128 {
 129   stream >> mbox_ >> dst_buff_;
 130 }
 131 std::string CommRecvTransition::to_string(bool verbose) const
 132 {
 133   auto res = xbt::string_printf("%ld: iRecv(mbox=%u", aid_, mbox_);
 134   if (verbose)
 135     res += ", buff=" + xbt::string_printf("%p", dst_buff_);
 136   res += ")";
 137   return res;
 138 }
 139 bool CommRecvTransition::depends(const Transition* other) const
 140 {
 141   if (aid_ == other->aid_)
 142     return false;
 143
 144   if (dynamic_cast<const RandomTransition*>(other) != nullptr)
 145     return false; // Random is indep with any transition
 146   if (auto* any = dynamic_cast<const WaitAnyTransition*>(other))
 147     return any->depends(this);
 148   if (auto* any = dynamic_cast<const TestAnyTransition*>(other))
 149     return any->depends(this);
 150
 151   if (const auto* recv = dynamic_cast<const CommRecvTransition*>(other))
 152     return mbox_ == recv->mbox_;
 153
 154   if (dynamic_cast<const CommSendTransition*>(other) != nullptr)
 155     return false;
 156
 157   if (const auto* test = dynamic_cast<const CommTestTransition*>(other)) {
 158     if (mbox_ != test->mbox_)
 159       return false;
 160
 161     if ((aid_ != test->sender_) && (aid_ != test->receiver_) && (test->dst_buff_ != dst_buff_))
 162       return false;
 163   }
 164
 165   if (auto* wait = dynamic_cast<const CommWaitTransition*>(other)) {
 166     if (wait->timeout_)
 167       return true;
 168
 169     if (mbox_ != wait->mbox_)
 170       return false;
 171
 172     if ((aid_ != wait->sender_) && (aid_ != wait->receiver_) && (wait->dst_buff_ != dst_buff_))
 173       return false;
 174   }
 175
 176   return true;
 177 }
 178
 179 CommSendTransition::CommSendTransition(aid_t issuer, int times_considered, std::stringstream& stream)
 180     : Transition(Type::COMM_SEND, issuer, times_considered)
 181 {
 182   stream >> mbox_ >> src_buff_ >> size_;
 183   XBT_DEBUG("SendTransition mbox:%u buff:%p size:%zu", mbox_, src_buff_, size_);
 184 }
 185 std::string CommSendTransition::to_string(bool verbose = false) const
 186 {
 187   auto res = xbt::string_printf("%ld: iSend(mbox=%u", aid_, mbox_);
 188   if (verbose)
 189     res += ", buff=" + xbt::string_printf("%p", src_buff_) + ", size=" + std::to_string(size_);
 190   res += ")";
 191   return res;
 192 }
 193 TestAnyTransition::TestAnyTransition(aid_t issuer, int times_considered, std::stringstream& stream)
 194     : Transition(Type::TESTANY, issuer, times_considered)
 195 {
 196   int size;
 197   stream >> size;
 198   for (int i = 0; i < size; i++) {
 199
 200     Transition* t = deserialize_transition(issuer, 0, stream);
 201     XBT_DEBUG("TestAny received a transition %s", t->to_string(true).c_str());
 202     transitions_.push_back(t);
 203   }
 204 }
 205 std::string TestAnyTransition::to_string(bool verbose) const
 206 {
 207   auto res = xbt::string_printf("%ld: TestAny{ ", aid_);
 208   for (auto const* t : transitions_)
 209     res += t->to_string(verbose);
 210   res += "}";
 211   return res;
 212 }
 213 bool TestAnyTransition::depends(const Transition* other) const
 214 {
 215   return transitions_[times_considered_]->depends(other);
 216 }
 217 WaitAnyTransition::WaitAnyTransition(aid_t issuer, int times_considered, std::stringstream& stream)
 218     : Transition(Type::WAITANY, issuer, times_considered)
 219 {
 220   int size;
 221   stream >> size;
 222   for (int i = 0; i < size; i++) {
 223     Transition* t = deserialize_transition(issuer, 0, stream);
 224     transitions_.push_back(t);
 225   }
 226 }
 227 std::string WaitAnyTransition::to_string(bool verbose) const
 228 {
 229   auto res = xbt::string_printf("%ld: WaitAny{ ", aid_);
 230   for (auto const* t : transitions_)
 231     res += t->to_string(verbose);
 232   res += "}";
 233   return res;
 234 }
 235 bool WaitAnyTransition::depends(const Transition* other) const
 236 {
 237   return transitions_[times_considered_]->depends(other);
 238 }
 239
 240 bool CommSendTransition::depends(const Transition* other) const
 241 {
 242   if (aid_ == other->aid_)
 243     return false;
 244
 245   if (dynamic_cast<const RandomTransition*>(other) != nullptr)
 246     return false; // Random is indep with any transition
 247
 248   if (auto* any = dynamic_cast<const WaitAnyTransition*>(other))
 249     return any->depends(this);
 250   if (auto* any = dynamic_cast<const TestAnyTransition*>(other))
 251     return any->depends(this);
 252
 253   if (const auto* other_isend = dynamic_cast<const CommSendTransition*>(other))
 254     return mbox_ == other_isend->mbox_;
 255
 256   if (dynamic_cast<const CommRecvTransition*>(other) != nullptr)
 257     return false;
 258
 259   if (const auto* test = dynamic_cast<const CommTestTransition*>(other)) {
 260     if (mbox_ != test->mbox_)
 261       return false;
 262
 263     if ((aid_ != test->sender_) && (aid_ != test->receiver_) && (test->src_buff_ != src_buff_))
 264       return false;
 265   }
 266
 267   if (const auto* wait = dynamic_cast<const CommWaitTransition*>(other)) {
 268     if (wait->timeout_)
 269       return true;
 270
 271     if (mbox_ != wait->mbox_)
 272       return false;
 273
 274     if ((aid_ != wait->sender_) && (aid_ != wait->receiver_) && (wait->src_buff_ != src_buff_))
 275       return false;
 276   }
 277
 278   return true;
 279 }
 280
 281 Transition* deserialize_transition(aid_t issuer, int times_considered, std::stringstream& stream)
 282 {
 283   short type;
 284   stream >> type;
 285   xbt_assert(type >= 0 && type <= static_cast<short>(Transition::Type::UNKNOWN), "Invalid transition type %d received",
 286              type);
 287
 288   auto simcall = static_cast<Transition::Type>(type);
 289
 290   switch (simcall) {
 291     case Transition::Type::COMM_RECV:
 292       return new CommRecvTransition(issuer, times_considered, stream);
 293     case Transition::Type::COMM_SEND:
 294       return new CommSendTransition(issuer, times_considered, stream);
 295     case Transition::Type::COMM_TEST:
 296       return new CommTestTransition(issuer, times_considered, stream);
 297     case Transition::Type::COMM_WAIT:
 298       return new CommWaitTransition(issuer, times_considered, stream);
 299
 300     case Transition::Type::TESTANY:
 301       return new TestAnyTransition(issuer, times_considered, stream);
 302     case Transition::Type::WAITANY:
 303       return new WaitAnyTransition(issuer, times_considered, stream);
 304
 305     case Transition::Type::RANDOM:
 306       return new RandomTransition(issuer, times_considered, stream);
 307
 308     case Transition::Type::UNKNOWN:
 309       return new Transition(Transition::Type::UNKNOWN, issuer, times_considered);
 310   }
 311   THROW_IMPOSSIBLE; // Some compilers don't detect that each branch of the above switch has a return
 312 }
 313
 314 } // namespace mc
 315 } // namespace simgrid