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