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