return res;
}*/
-
-bool ActivityTestSimcall::depends(SimcallObserver* other)
-{
- if (get_issuer() == other->get_issuer())
- return false;
-
- if (dynamic_cast<ActivityTestSimcall*>(other))
- return true;
-
- const auto* comm1 = dynamic_cast<activity::CommImpl*>(activity_);
- if (comm1 == nullptr)
- return false;
-
- if (dynamic_cast<ActivityWaitSimcall*>(other) != nullptr &&
- (comm1->src_actor_.get() == nullptr || comm1->dst_actor_.get() == nullptr))
- return false;
-
- if (comm1->src_buff_ == nullptr || comm1->dst_buff_ == nullptr)
- return false;
-
- if (const auto* test = dynamic_cast<ActivityTestSimcall*>(other)) {
- const auto* comm2 = dynamic_cast<activity::CommImpl*>(test->get_activity());
- if (comm2 == nullptr)
- return false;
- else if (comm2->src_buff_ == nullptr || comm2->dst_buff_ == nullptr)
- return false;
- }
-
- if (auto* wait = dynamic_cast<ActivityWaitSimcall*>(other)) {
- auto* comm2 = dynamic_cast<activity::CommImpl*>(wait->get_activity());
- if (comm2 == nullptr)
- return false;
- if (comm1->src_buff_ == comm2->src_buff_ && comm1->dst_buff_ == comm2->dst_buff_)
- return false;
- if (comm1->src_buff_ != nullptr && comm1->dst_buff_ != nullptr && comm2->src_buff_ != nullptr &&
- comm2->dst_buff_ != nullptr && comm1->dst_buff_ != comm2->src_buff_ && comm1->dst_buff_ != comm2->dst_buff_ &&
- comm2->dst_buff_ != comm1->src_buff_)
- return false;
- }
-
- return true;
-}
void ActivityWaitSimcall::serialize(mc::Transition::Type& type, std::stringstream& stream)
{
if (auto* comm = dynamic_cast<activity::CommImpl*>(activity_)) {
type = mc::Transition::Type::UNKNOWN;
}
}
-
-/*
-std::string ActivityTestSimcall::to_string(int times_considered) const
+void ActivityTestSimcall::serialize(mc::Transition::Type& type, std::stringstream& stream)
{
- std::string res = SimcallObserver::to_string(times_considered) + "Test ";
- if (const auto* comm = dynamic_cast<activity::CommImpl*>(activity_)) {
- if (comm->src_actor_.get() == nullptr || comm->dst_actor_.get() == nullptr) {
- res += "FALSE(comm=";
- res += XBT_LOG_ISENABLED(mc_observer, xbt_log_priority_verbose) ? xbt::string_printf("%p)", comm)
- : "(verbose only))";
- } else {
- res += "TRUE(comm=";
-
- auto src = comm->src_actor_;
- auto dst = comm->dst_actor_;
- res +=
- XBT_LOG_ISENABLED(mc_observer, xbt_log_priority_verbose) ? xbt::string_printf("%p", comm) : "(verbose only) ";
- res += xbt::string_printf("[(%ld)%s (%s) ", src->get_pid(), src->get_host()->get_cname(), src->get_cname()) +
- "-> " +
- xbt::string_printf("(%ld)%s (%s)])", dst->get_pid(), dst->get_host()->get_cname(), dst->get_cname());
- }
- } else
- xbt_die("Only Comms are supported here for now");
- return res;
-}*/
+ if (auto* comm = dynamic_cast<activity::CommImpl*>(activity_)) {
+ type = mc::Transition::Type::COMM_TEST;
+ stream << ' ' << (comm->src_actor_ != nullptr ? comm->src_actor_->get_pid() : -1);
+ stream << ' ' << (comm->dst_actor_ != nullptr ? comm->dst_actor_->get_pid() : -1);
+ stream << ' ' << comm->get_mailbox_id();
+ stream << ' ' << (void*)comm->src_buff_ << ' ' << (void*)comm->dst_buff_ << ' ' << comm->src_buff_size_;
+ } else {
+ type = mc::Transition::Type::UNKNOWN;
+ }
+}
bool ActivityWaitSimcall::is_enabled() const
{
void CommIsendSimcall::serialize(mc::Transition::Type& type, std::stringstream& stream)
{
- type = mc::Transition::Type::ISEND;
+ type = mc::Transition::Type::COMM_SEND;
stream << mbox_->get_id() << ' ' << (void*)src_buff_ << ' ' << src_buff_size_;
XBT_DEBUG("SendObserver mbox:%u buff:%p size:%zu", mbox_->get_id(), src_buff_, src_buff_size_);
}
void CommIrecvSimcall::serialize(mc::Transition::Type& type, std::stringstream& stream)
{
- type = mc::Transition::Type::IRECV;
+ type = mc::Transition::Type::COMM_RECV;
stream << mbox_->get_id() << dst_buff_;
}
if (dynamic_cast<const RandomTransition*>(other) != nullptr)
return false; // Random is indep with any transition
+ if (auto* recv = dynamic_cast<const CommRecvTransition*>(other))
+ return recv->depends(this);
+
if (auto* send = dynamic_cast<const CommSendTransition*>(other))
return send->depends(this);
- if (auto* recv = dynamic_cast<const CommRecvTransition*>(other))
- return recv->depends(this);
+ if (auto* test = dynamic_cast<const CommTestTransition*>(other))
+ return test->depends(this);
- /* Timeouts in wait transitions are not considered by the independence theorem, thus assumed dependent */
if (const auto* wait = dynamic_cast<const CommWaitTransition*>(other)) {
if (timeout_ || wait->timeout_)
- return true;
+ return true; // Timeouts are not considered by the independence theorem, thus assumed dependent
if (src_buff_ == wait->src_buff_ && dst_buff_ == wait->dst_buff_)
return false;
return true;
}
+CommTestTransition::CommTestTransition(aid_t issuer, int times_considered, char* buffer)
+ : Transition(Type::COMM_TEST, issuer, times_considered)
+{
+ std::stringstream stream(buffer);
+ stream >> comm_ >> sender_ >> receiver_ >> mbox_ >> src_buff_ >> dst_buff_ >> size_;
+ XBT_DEBUG("CommTestTransition comm:%p, sender:%ld receiver:%ld mbox:%u sbuff:%p rbuff:%p size:%zu", comm_, sender_,
+ receiver_, mbox_, src_buff_, dst_buff_, size_);
+}
+std::string CommTestTransition::to_string(bool verbose) const
+{
+ auto res = xbt::string_printf("%ld: TestComm(from %ld to %ld, mbox=%u", aid_, sender_, receiver_, mbox_);
+ if (verbose) {
+ res += ", src_buff=" + xbt::string_printf("%p", src_buff_) + ", size=" + std::to_string(size_);
+ res += ", dst_buff=" + xbt::string_printf("%p", dst_buff_);
+ }
+ res += ")";
+ return res;
+}
+bool CommTestTransition::depends(const Transition* other) const
+{
+ if (aid_ == other->aid_)
+ return false;
+
+ if (dynamic_cast<const RandomTransition*>(other) != nullptr)
+ return false; // Test & Random are independent (Random is independent with anything)
+
+ if (auto* recv = dynamic_cast<const CommRecvTransition*>(other))
+ return recv->depends(this); // Recv < Test (alphabetical ordering)
+
+ if (auto* send = dynamic_cast<const CommSendTransition*>(other))
+ return send->depends(this); // Send < Test (alphabetical ordering)
+
+ if (dynamic_cast<const CommTestTransition*>(other) != nullptr)
+ return false; // Test & Test are independent
+
+ if (const auto* wait = dynamic_cast<const CommWaitTransition*>(other)) {
+ if (wait->timeout_)
+ return true; // Timeouts are not considered by the independence theorem, thus assumed dependent
+
+ /* Wait & Test are independent */
+ return false;
+ }
+
+ return true;
+}
CommRecvTransition::CommRecvTransition(aid_t issuer, int times_considered, char* buffer)
- : Transition(Type::IRECV, issuer, times_considered)
+ : Transition(Type::COMM_RECV, issuer, times_considered)
{
std::stringstream stream(buffer);
stream >> mbox_ >> dst_buff_;
if (dynamic_cast<const RandomTransition*>(other) != nullptr)
return false; // Random is indep with any transition
- if (const auto* other_irecv = dynamic_cast<const CommRecvTransition*>(other))
- return mbox_ == other_irecv->mbox_;
+ if (const auto* recv = dynamic_cast<const CommRecvTransition*>(other))
+ return mbox_ == recv->mbox_;
- if (auto* isend = dynamic_cast<const CommSendTransition*>(other))
- return isend->depends(this);
+ if (dynamic_cast<const CommSendTransition*>(other) != nullptr)
+ return false;
+
+ if (const auto* test = dynamic_cast<const CommTestTransition*>(other)) {
+ if (mbox_ != test->mbox_)
+ return false;
+
+ if ((aid_ != test->sender_) && (aid_ != test->receiver_) && (test->dst_buff_ != dst_buff_))
+ return false;
+ }
if (auto* wait = dynamic_cast<const CommWaitTransition*>(other)) {
if (wait->timeout_)
return false;
}
- /* FIXME: the following rule assumes that the result of the isend/irecv call is not stored in a buffer used in the
- * test call. */
-#if 0
- if (dynamic_cast<ActivityTestSimcall*>(other))
- return false;
-#endif
-
return true;
}
CommSendTransition::CommSendTransition(aid_t issuer, int times_considered, char* buffer)
- : Transition(Type::ISEND, issuer, times_considered)
+ : Transition(Type::COMM_SEND, issuer, times_considered)
{
std::stringstream stream(buffer);
stream >> mbox_ >> src_buff_ >> size_;
if (dynamic_cast<const CommRecvTransition*>(other) != nullptr)
return false;
+ if (const auto* test = dynamic_cast<const CommTestTransition*>(other)) {
+ if (mbox_ != test->mbox_)
+ return false;
+
+ if ((aid_ != test->sender_) && (aid_ != test->receiver_) && (test->src_buff_ != src_buff_))
+ return false;
+ }
+
if (const auto* wait = dynamic_cast<const CommWaitTransition*>(other)) {
if (wait->timeout_)
return true;
return false;
}
- /* FIXME: the following rule assumes that the result of the isend/irecv call is not stored in a buffer used in the
- * test call. */
-#if 0
- if (dynamic_cast<ActivityTestSimcall*>(other))
- return false;
-#endif
-
return true;
}
Transition* recv_transition(aid_t issuer, int times_considered, Transition::Type simcall, char* buffer)
{
switch (simcall) {
- case Transition::Type::COMM_WAIT:
- return new CommWaitTransition(issuer, times_considered, buffer);
- case Transition::Type::IRECV:
+ case Transition::Type::COMM_RECV:
return new CommRecvTransition(issuer, times_considered, buffer);
- case Transition::Type::ISEND:
+ case Transition::Type::COMM_SEND:
return new CommSendTransition(issuer, times_considered, buffer);
+ case Transition::Type::COMM_TEST:
+ return new CommTestTransition(issuer, times_considered, buffer);
+ case Transition::Type::COMM_WAIT:
+ return new CommWaitTransition(issuer, times_considered, buffer);
case Transition::Type::RANDOM:
return new RandomTransition(issuer, times_considered, buffer);