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 }
  54 std::string CommWaitTransition::to_string(bool verbose)
  55 {
  56   textual_ = Transition::to_string(verbose);
  57   textual_ +=
  58       xbt::string_printf("%ld: WaitComm(from %ld to %ld, mbox=%u, tout=%f", aid_, sender_, receiver_, mbox_, timeout_);
  59   if (verbose) {
  60     textual_ += ", src_buff=" + xbt::string_printf("%p", src_buff_) + ", size=" + std::to_string(size_);
  61     textual_ += ", dst_buff=" + xbt::string_printf("%p", dst_buff_);
  62   }
  63   textual_ += ")";
  64   return textual_;
  65 }
  66 bool CommWaitTransition::depends(const Transition* other) const
  67 {
  68   if (aid_ == other->aid_)
  69     return false;
  70
  71   if (auto* send = dynamic_cast<const CommSendTransition*>(other))
  72     return send->depends(this);
  73
  74   if (auto* recv = dynamic_cast<const CommRecvTransition*>(other))
  75     return recv->depends(this);
  76
  77   /* Timeouts in wait transitions are not considered by the independence theorem, thus assumed dependent */
  78   if (const auto* wait = dynamic_cast<const CommWaitTransition*>(other)) {
  79     if (timeout_ > 0 || wait->timeout_ > 0)
  80       return true;
  81
  82     if (src_buff_ == wait->src_buff_ && dst_buff_ == wait->dst_buff_)
  83       return false;
  84     if (src_buff_ != nullptr && dst_buff_ != nullptr && wait->src_buff_ != nullptr && wait->dst_buff_ != nullptr &&
  85         dst_buff_ != wait->src_buff_ && dst_buff_ != wait->dst_buff_ && dst_buff_ != src_buff_)
  86       return false;
  87   }
  88
  89   return true;
  90 }
  91
  92 CommRecvTransition::CommRecvTransition(aid_t issuer, int times_considered, char* buffer)
  93     : Transition(issuer, times_considered)
  94 {
  95   std::stringstream stream(buffer);
  96   stream >> mbox_ >> dst_buff_;
  97 }
  98 std::string CommRecvTransition::to_string(bool verbose)
  99 {
 100   textual_ = xbt::string_printf("%ld: Recv(mbox=%u", aid_, mbox_);
 101   if (verbose)
 102     textual_ += ", buff=" + xbt::string_printf("%p", dst_buff_);
 103   textual_ += ")";
 104   return textual_;
 105 }
 106 bool CommRecvTransition::depends(const Transition* other) const
 107 {
 108   if (aid_ == other->aid_)
 109     return false;
 110
 111   if (const auto* other_irecv = dynamic_cast<const CommRecvTransition*>(other))
 112     return mbox_ == other_irecv->mbox_;
 113
 114   if (auto* isend = dynamic_cast<const CommSendTransition*>(other))
 115     return isend->depends(this);
 116
 117   if (auto* wait = dynamic_cast<const CommWaitTransition*>(other)) {
 118     if (wait->timeout_ > 0)
 119       return true;
 120
 121     if (mbox_ != wait->mbox_)
 122       return false;
 123
 124     if ((aid_ != wait->sender_) && (aid_ != wait->receiver_))
 125       return false;
 126
 127     if (wait->dst_buff_ != dst_buff_)
 128       return false;
 129   }
 130
 131   /* FIXME: the following rule assumes that the result of the isend/irecv call is not stored in a buffer used in the
 132    * test call. */
 133 #if 0
 134   if (dynamic_cast<ActivityTestSimcall*>(other))
 135     return false;
 136 #endif
 137
 138   return true;
 139 }
 140
 141 CommSendTransition::CommSendTransition(aid_t issuer, int times_considered, char* buffer)
 142     : Transition(issuer, times_considered)
 143 {
 144   std::stringstream stream(buffer);
 145   stream >> mbox_ >> src_buff_ >> size_;
 146 }
 147 std::string CommSendTransition::to_string(bool verbose = false)
 148 {
 149   textual_ = xbt::string_printf("%ld: Send(mbox=%u", aid_, mbox_);
 150   if (verbose)
 151     textual_ += ", buff=" + xbt::string_printf("%p", src_buff_) + ", size=" + std::to_string(size_);
 152   textual_ += ")";
 153   return textual_;
 154 }
 155 bool CommSendTransition::depends(const Transition* other) const
 156 {
 157   if (aid_ == other->aid_)
 158     return false;
 159
 160   if (const auto* other_isend = dynamic_cast<const CommSendTransition*>(other))
 161     return mbox_ == other_isend->mbox_;
 162
 163   // FIXME: Not in the former dependency check because of the ordering but seems logical to add it
 164   if (dynamic_cast<const CommRecvTransition*>(other) != nullptr)
 165     return false;
 166
 167   if (const auto* wait = dynamic_cast<const CommWaitTransition*>(other)) {
 168     if (wait->timeout_ > 0)
 169       return true;
 170
 171     if (mbox_ != wait->mbox_)
 172       return false;
 173
 174     if ((aid_ != wait->sender_) && (aid_ != wait->receiver_))
 175       return false;
 176
 177     if (wait->src_buff_ != src_buff_)
 178       return false;
 179   }
 180
 181   /* FIXME: the following rule assumes that the result of the isend/irecv call is not stored in a buffer used in the
 182    * test call. */
 183 #if 0
 184   if (dynamic_cast<ActivityTestSimcall*>(other))
 185     return false;
 186 #endif
 187
 188   return true;
 189 }
 190
 191 Transition* recv_transition(aid_t issuer, int times_considered, kernel::actor::SimcallObserver::Simcall simcall,
 192                             char* buffer)
 193 {
 194   switch (simcall) {
 195     case kernel::actor::SimcallObserver::Simcall::COMM_WAIT:
 196       return new CommWaitTransition(issuer, times_considered, buffer);
 197     case kernel::actor::SimcallObserver::Simcall::IRECV:
 198       return new CommRecvTransition(issuer, times_considered, buffer);
 199     case kernel::actor::SimcallObserver::Simcall::ISEND:
 200       return new CommSendTransition(issuer, times_considered, buffer);
 201     case kernel::actor::SimcallObserver::Simcall::UNKNOWN:
 202       return new Transition(issuer, times_considered);
 203     default:
 204       xbt_die("recv_transition of type %s unimplemented", kernel::actor::SimcallObserver::to_c_str(simcall));
 205   }
 206 }
 207
 208 } // namespace mc
 209 } // namespace simgrid