src/mc/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/TransitionComm.hpp"
   7 #include "src/mc/Transition.hpp"
   8 #include "xbt/asserts.h"
   9 #include <simgrid/config.h>
  10 #if SIMGRID_HAVE_MC
  11 #include "src/mc/ModelChecker.hpp"
  12 #include "src/mc/Session.hpp"
  13 #include "src/mc/mc_state.hpp"
  14 #endif
  15
  16 #include <sstream>
  17
  18 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_trans_comm, mc_transition,
  19                                 "Logging specific to MC transitions about communications");
  20
  21 namespace simgrid {
  22 namespace mc {
  23
  24 CommWaitTransition::CommWaitTransition(aid_t issuer, int times_considered, char* buffer)
  25     : Transition(issuer, times_considered)
  26 {
  27   std::stringstream stream(buffer);
  28   stream >> timeout_ >> comm_ >> sender_ >> receiver_ >> mbox_ >> src_buff_ >> dst_buff_ >> size_;
  29   XBT_DEBUG("CommWaitTransition %s comm:%p, sender:%ld receiver:%ld mbox:%u sbuff:%p rbuff:%p size:%zu",
  30             (timeout_ ? "timeout" : "no-timeout"), comm_, sender_, receiver_, mbox_, src_buff_, dst_buff_, size_);
  31 }
  32 std::string CommWaitTransition::to_string(bool verbose)
  33 {
  34   textual_ = xbt::string_printf("%ld: WaitComm(from %ld to %ld, mbox=%u, %s", aid_, sender_, receiver_, mbox_,
  35                                 (timeout_ ? "timeout" : "no timeout"));
  36   if (verbose) {
  37     textual_ += ", src_buff=" + xbt::string_printf("%p", src_buff_) + ", size=" + std::to_string(size_);
  38     textual_ += ", dst_buff=" + xbt::string_printf("%p", dst_buff_);
  39   }
  40   textual_ += ")";
  41   return textual_;
  42 }
  43 bool CommWaitTransition::depends(const Transition* other) const
  44 {
  45   if (aid_ == other->aid_)
  46     return false;
  47
  48   if (auto* send = dynamic_cast<const CommSendTransition*>(other))
  49     return send->depends(this);
  50
  51   if (auto* recv = dynamic_cast<const CommRecvTransition*>(other))
  52     return recv->depends(this);
  53
  54   /* Timeouts in wait transitions are not considered by the independence theorem, thus assumed dependent */
  55   if (const auto* wait = dynamic_cast<const CommWaitTransition*>(other)) {
  56     if (timeout_ || wait->timeout_)
  57       return true;
  58
  59     if (src_buff_ == wait->src_buff_ && dst_buff_ == wait->dst_buff_)
  60       return false;
  61     if (src_buff_ != nullptr && dst_buff_ != nullptr && wait->src_buff_ != nullptr && wait->dst_buff_ != nullptr &&
  62         dst_buff_ != wait->src_buff_ && dst_buff_ != wait->dst_buff_ && dst_buff_ != src_buff_)
  63       return false;
  64   }
  65
  66   return true;
  67 }
  68
  69 CommRecvTransition::CommRecvTransition(aid_t issuer, int times_considered, char* buffer)
  70     : Transition(issuer, times_considered)
  71 {
  72   std::stringstream stream(buffer);
  73   stream >> mbox_ >> dst_buff_;
  74 }
  75 std::string CommRecvTransition::to_string(bool verbose)
  76 {
  77   textual_ = xbt::string_printf("%ld: iRecv(mbox=%u", aid_, mbox_);
  78   if (verbose)
  79     textual_ += ", buff=" + xbt::string_printf("%p", dst_buff_);
  80   textual_ += ")";
  81   return textual_;
  82 }
  83 bool CommRecvTransition::depends(const Transition* other) const
  84 {
  85   if (aid_ == other->aid_)
  86     return false;
  87
  88   if (const auto* other_irecv = dynamic_cast<const CommRecvTransition*>(other))
  89     return mbox_ == other_irecv->mbox_;
  90
  91   if (auto* isend = dynamic_cast<const CommSendTransition*>(other))
  92     return isend->depends(this);
  93
  94   if (auto* wait = dynamic_cast<const CommWaitTransition*>(other)) {
  95     if (wait->timeout_)
  96       return true;
  97
  98     if (mbox_ != wait->mbox_)
  99       return false;
 100
 101     if ((aid_ != wait->sender_) && (aid_ != wait->receiver_))
 102       return false;
 103
 104     if (wait->dst_buff_ != dst_buff_)
 105       return false;
 106   }
 107
 108   /* FIXME: the following rule assumes that the result of the isend/irecv call is not stored in a buffer used in the
 109    * test call. */
 110 #if 0
 111   if (dynamic_cast<ActivityTestSimcall*>(other))
 112     return false;
 113 #endif
 114
 115   return true;
 116 }
 117
 118 CommSendTransition::CommSendTransition(aid_t issuer, int times_considered, char* buffer)
 119     : Transition(issuer, times_considered)
 120 {
 121   std::stringstream stream(buffer);
 122   stream >> mbox_ >> src_buff_ >> size_;
 123   XBT_DEBUG("SendTransition mbox:%u buff:%p size:%zu", mbox_, src_buff_, size_);
 124 }
 125 std::string CommSendTransition::to_string(bool verbose = false)
 126 {
 127   textual_ = xbt::string_printf("%ld: iSend(mbox=%u", aid_, mbox_);
 128   if (verbose)
 129     textual_ += ", buff=" + xbt::string_printf("%p", src_buff_) + ", size=" + std::to_string(size_);
 130   textual_ += ")";
 131   return textual_;
 132 }
 133 bool CommSendTransition::depends(const Transition* other) const
 134 {
 135   if (aid_ == other->aid_)
 136     return false;
 137
 138   if (const auto* other_isend = dynamic_cast<const CommSendTransition*>(other))
 139     return mbox_ == other_isend->mbox_;
 140
 141   // FIXME: Not in the former dependency check because of the ordering but seems logical to add it
 142   if (dynamic_cast<const CommRecvTransition*>(other) != nullptr)
 143     return false;
 144
 145   if (const auto* wait = dynamic_cast<const CommWaitTransition*>(other)) {
 146     if (wait->timeout_)
 147       return true;
 148
 149     if (mbox_ != wait->mbox_)
 150       return false;
 151
 152     if ((aid_ != wait->sender_) && (aid_ != wait->receiver_))
 153       return false;
 154
 155     if (wait->src_buff_ != src_buff_)
 156       return false;
 157   }
 158
 159   /* FIXME: the following rule assumes that the result of the isend/irecv call is not stored in a buffer used in the
 160    * test call. */
 161 #if 0
 162   if (dynamic_cast<ActivityTestSimcall*>(other))
 163     return false;
 164 #endif
 165
 166   return true;
 167 }
 168
 169 Transition* recv_transition(aid_t issuer, int times_considered, kernel::actor::SimcallObserver::Simcall simcall,
 170                             char* buffer)
 171 {
 172   switch (simcall) {
 173     case kernel::actor::SimcallObserver::Simcall::COMM_WAIT:
 174       return new CommWaitTransition(issuer, times_considered, buffer);
 175     case kernel::actor::SimcallObserver::Simcall::IRECV:
 176       return new CommRecvTransition(issuer, times_considered, buffer);
 177     case kernel::actor::SimcallObserver::Simcall::ISEND:
 178       return new CommSendTransition(issuer, times_considered, buffer);
 179     case kernel::actor::SimcallObserver::Simcall::UNKNOWN:
 180       return new Transition(issuer, times_considered);
 181     default:
 182       xbt_die("recv_transition of type %s unimplemented", kernel::actor::SimcallObserver::to_c_str(simcall));
 183   }
 184 }
 185
 186 } // namespace mc
 187 } // namespace simgrid