> [0.000000] [mc_global/INFO] **************************
> [0.000000] [ker_engine/INFO] 2 actors are still running, waiting for something.
> [0.000000] [ker_engine/INFO] Legend of the following listing: "Actor <pid> (<name>@<host>): <status>"
-> [0.000000] [ker_engine/INFO] Actor 1 (0@node-0.simgrid.org) simcall CommWait(comm_id:1 src:1 dst:-1 mbox:SMPI-2(id:2) srcbuf:1 dstbuf:- bufsize:4)
-> [0.000000] [ker_engine/INFO] Actor 2 (1@node-1.simgrid.org) simcall CommWait(comm_id:2 src:2 dst:-1 mbox:SMPI-1(id:0) srcbuf:2 dstbuf:- bufsize:4)
+> [0.000000] [ker_engine/INFO] Actor 1 (0@node-0.simgrid.org) simcall CommWait(comm_id:1 src:1 dst:-1 mbox:SMPI-2(id:2))
+> [0.000000] [ker_engine/INFO] Actor 2 (1@node-1.simgrid.org) simcall CommWait(comm_id:2 src:2 dst:-1 mbox:SMPI-1(id:0))
> [0.000000] [mc_global/INFO] Counter-example execution trace:
> [0.000000] [mc_global/INFO] Actor 1 in :0:() ==> simcall: iSend(mbox=2)
> [0.000000] [mc_global/INFO] Actor 2 in :0:() ==> simcall: iSend(mbox=0)
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 << ' ' << (uintptr_t)comm->src_buff_ << ' ' << (uintptr_t)comm->dst_buff_ << ' ' << comm->src_buff_size_;
} else {
stream << (short)mc::Transition::Type::UNKNOWN;
XBT_CRITICAL("Unknown transition in a test any. Bad things may happen");
static std::string to_string_activity_test(const activity::ActivityImpl* act)
{
if (const auto* comm = dynamic_cast<activity::CommImpl const*>(act)) {
- const std::string src_buff_id = ptr_to_id<unsigned char>(comm->src_buff_);
- const std::string dst_buff_id = ptr_to_id<unsigned char>(comm->dst_buff_);
return "CommTest(comm_id:" + std::to_string(comm->get_id()) +
" src:" + std::to_string(comm->src_actor_ != nullptr ? comm->src_actor_->get_pid() : -1) +
" dst:" + std::to_string(comm->dst_actor_ != nullptr ? comm->dst_actor_->get_pid() : -1) +
- " mbox:" + std::to_string(comm->get_mailbox_id()) + " srcbuf:" + src_buff_id + " dstbuf:" + dst_buff_id +
- " bufsize:" + std::to_string(comm->src_buff_size_);
+ " mbox:" + std::to_string(comm->get_mailbox_id());
} else {
return "TestUnknownType()";
}
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 << ' ' << (uintptr_t)comm->src_buff_ << ' ' << (uintptr_t)comm->dst_buff_ << ' ' << comm->src_buff_size_;
} else {
stream << (short)mc::Transition::Type::UNKNOWN;
}
static std::string to_string_activity_wait(const activity::ActivityImpl* act)
{
if (const auto* comm = dynamic_cast<activity::CommImpl const*>(act)) {
- const std::string src_buff_id = ptr_to_id<unsigned char>(comm->src_buff_);
- const std::string dst_buff_id = ptr_to_id<unsigned char>(comm->dst_buff_);
return "CommWait(comm_id:" + std::to_string(comm->get_id()) +
" src:" + std::to_string(comm->src_actor_ != nullptr ? comm->src_actor_->get_pid() : -1) +
" dst:" + std::to_string(comm->dst_actor_ != nullptr ? comm->dst_actor_->get_pid() : -1) +
" mbox:" + (comm->get_mailbox() == nullptr ? "-" : comm->get_mailbox()->get_name()) +
- "(id:" + std::to_string(comm->get_mailbox_id()) + ") srcbuf:" + src_buff_id + " dstbuf:" + dst_buff_id +
- " bufsize:" + std::to_string(comm->src_buff_size_) + ")";
+ "(id:" + std::to_string(comm->get_mailbox_id()) + "))";
} else {
return "WaitUnknownType()";
}
{
/* Note that the comm_ is 0 until after the execution of the simcall */
stream << (short)mc::Transition::Type::COMM_ASYNC_SEND << ' ';
- stream << (comm_ ? comm_->get_id() : 0) << ' ' << mbox_->get_id() << ' ' << (uintptr_t)src_buff_ << ' '
- << src_buff_size_ << ' ' << tag_;
- XBT_DEBUG("SendObserver comm:%p mbox:%u buff:%p size:%zu tag:%d", comm_, mbox_->get_id(), src_buff_, src_buff_size_,
- tag_);
+ stream << (comm_ ? comm_->get_id() : 0) << ' ' << mbox_->get_id() << ' ' << tag_;
+ XBT_DEBUG("SendObserver comm:%p mbox:%u tag:%d", comm_, mbox_->get_id(), tag_);
stream << ' ' << fun_call_;
}
std::string CommIsendSimcall::to_string() const
{
return "CommAsyncSend(comm_id: " + std::to_string(comm_->get_id()) + " mbox:" + std::to_string(mbox_->get_id()) +
- " srcbuf:" + ptr_to_id<unsigned char>(src_buff_) + " bufsize:" + std::to_string(src_buff_size_) +
" tag: " + std::to_string(tag_) + ")";
}
{
/* Note that the comm_ is 0 until after the execution of the simcall */
stream << (short)mc::Transition::Type::COMM_ASYNC_RECV << ' ';
- stream << (comm_ ? comm_->get_id() : 0) << ' ' << mbox_->get_id() << ' ' << (uintptr_t)dst_buff_ << ' ' << tag_;
- XBT_DEBUG("RecvObserver comm:%p mbox:%u buff:%p tag:%d", comm_, mbox_->get_id(), dst_buff_, tag_);
+ stream << (comm_ ? comm_->get_id() : 0) << ' ' << mbox_->get_id() << ' ' << tag_;
+ XBT_DEBUG("RecvObserver comm:%p mbox:%u tag:%d", comm_, mbox_->get_id(), tag_);
stream << ' ' << fun_call_;
}
std::string CommIrecvSimcall::to_string() const
{
return "CommAsyncRecv(comm_id: " + std::to_string(comm_->get_id()) + " mbox:" + std::to_string(mbox_->get_id()) +
- " dstbuf:" + ptr_to_id<unsigned char>(dst_buff_) + " tag: " + std::to_string(tag_) + ")";
+ " tag: " + std::to_string(tag_) + ")";
}
} // namespace simgrid::kernel::actor
{
// Consider the extension with `1: AsyncSend(m)`
Configuration C;
- aid_t issuer = 1;
- const uintptr_t sbuff = 0;
- const size_t size = 100;
+ aid_t issuer = 1;
- const auto async_send =
- std::make_shared<CommSendTransition>(issuer, times_considered, comm, mbox, sbuff, size, tag);
+ const auto async_send = std::make_shared<CommSendTransition>(issuer, times_considered, comm, mbox, tag);
const auto incremental_exC = ExtensionSetCalculator::partially_extend(C, &U, async_send);
// Check that the events have been added to `U`
{
// Consider the extension with `2: AsyncRecv(m)`
Configuration C;
- aid_t issuer = 2;
- const uintptr_t rbuff = 0;
+ aid_t issuer = 2;
- const auto async_recv = std::make_shared<CommRecvTransition>(issuer, times_considered, comm, mbox, rbuff, tag);
+ const auto async_recv = std::make_shared<CommRecvTransition>(issuer, times_considered, comm, mbox, tag);
const auto incremental_exC = ExtensionSetCalculator::partially_extend(C, &U, async_recv);
// Check that the events have been added to `U`
{
// Consider the extension with `1: AsyncSend(m)`
Configuration C;
- const uintptr_t rbuff = 0;
- const uintptr_t sbuff = 0;
- const size_t size = 100;
- const auto async_send = std::make_shared<CommSendTransition>(1, times_considered, comm, mbox, sbuff, size, tag);
+ const auto async_send = std::make_shared<CommSendTransition>(1, times_considered, comm, mbox, tag);
const auto incremental_exC_send = ExtensionSetCalculator::partially_extend(C, &U, async_send);
// Check that the events have been added to `U`
REQUIRE(incremental_exC_send.contains_equivalent_to(&e_send));
// Consider the extension with `2: AsyncRecv(m)`
- const auto async_recv = std::make_shared<CommRecvTransition>(2, times_considered, comm, mbox, rbuff, tag);
+ const auto async_recv = std::make_shared<CommRecvTransition>(2, times_considered, comm, mbox, tag);
const auto incremental_exC_recv = ExtensionSetCalculator::partially_extend(C, &U, async_recv);
// Check that the events have been added to `U`
SECTION("Computing the full sequence of extensions")
{
Configuration C;
- const uintptr_t rbuff = 0;
- const uintptr_t sbuff = 0;
- const size_t size = 100;
// Consider the extension with `1: AsyncSend(m)`
- const auto async_send = std::make_shared<CommSendTransition>(1, times_considered, comm, mbox, sbuff, size, tag);
+ const auto async_send = std::make_shared<CommSendTransition>(1, times_considered, comm, mbox, tag);
const auto incremental_exC_send = ExtensionSetCalculator::partially_extend(C, &U, async_send);
// Check that event `a` has been added to `U`
REQUIRE(incremental_exC_send.contains_equivalent_to(&e_send));
// Consider the extension with `2: AsyncRecv(m)`
- const auto async_recv = std::make_shared<CommRecvTransition>(2, times_considered, comm, mbox, rbuff, tag);
+ const auto async_recv = std::make_shared<CommRecvTransition>(2, times_considered, comm, mbox, tag);
const auto incremental_exC_recv = ExtensionSetCalculator::partially_extend(C, &U, async_recv);
// Check that event `b` has been added to `U`
const int tag = 0;
const unsigned mbox = 0;
const uintptr_t comm = 0x800;
- const uintptr_t rbuff = 0x200;
- const uintptr_t sbuff = 0x400;
- const size_t size = 100;
const bool timeout = false;
Unfolding U;
- const auto comm_send = std::make_shared<CommSendTransition>(1, times_considered, comm, mbox, sbuff, size, tag);
- const auto comm_recv = std::make_shared<CommRecvTransition>(2, times_considered, comm, mbox, rbuff, tag);
- const auto comm_wait_1 =
- std::make_shared<CommWaitTransition>(1, times_considered, timeout, comm, 1, 2, mbox, sbuff, rbuff, size);
- const auto comm_wait_2 =
- std::make_shared<CommWaitTransition>(2, times_considered, timeout, comm, 1, 2, mbox, sbuff, rbuff, size);
+ const auto comm_send = std::make_shared<CommSendTransition>(1, times_considered, comm, mbox, tag);
+ const auto comm_recv = std::make_shared<CommRecvTransition>(2, times_considered, comm, mbox, tag);
+ const auto comm_wait_1 = std::make_shared<CommWaitTransition>(1, times_considered, timeout, comm, 1, 2, mbox);
+ const auto comm_wait_2 = std::make_shared<CommWaitTransition>(2, times_considered, timeout, comm, 1, 2, mbox);
// 1. UDPOR will attempt to expand first ex({⊥})
namespace simgrid::mc {
CommWaitTransition::CommWaitTransition(aid_t issuer, int times_considered, bool timeout_, unsigned comm_, aid_t sender_,
- aid_t receiver_, unsigned mbox_, uintptr_t sbuff_, uintptr_t rbuff_,
- size_t size_)
+ aid_t receiver_, unsigned mbox_)
: Transition(Type::COMM_WAIT, issuer, times_considered)
, timeout_(timeout_)
, comm_(comm_)
, mbox_(mbox_)
, sender_(sender_)
, receiver_(receiver_)
- , sbuff_(sbuff_)
- , rbuff_(rbuff_)
- , size_(size_)
{
}
CommWaitTransition::CommWaitTransition(aid_t issuer, int times_considered, std::stringstream& stream)
: Transition(Type::COMM_WAIT, issuer, times_considered)
{
- xbt_assert(stream >> timeout_ >> comm_ >> sender_ >> receiver_ >> mbox_ >> sbuff_ >> rbuff_ >> size_ >>
- call_location_);
- XBT_DEBUG("CommWaitTransition %s comm:%u, sender:%ld receiver:%ld mbox:%u sbuff:%" PRIxPTR " rbuff:%" PRIxPTR
- " size:%zu",
- (timeout_ ? "timeout" : "no-timeout"), comm_, sender_, receiver_, mbox_, sbuff_, rbuff_, size_);
+ xbt_assert(stream >> timeout_ >> comm_ >> sender_ >> receiver_ >> mbox_ >> call_location_);
+ XBT_DEBUG("CommWaitTransition %s comm:%u, sender:%ld receiver:%ld mbox:%u", (timeout_ ? "timeout" : "no-timeout"),
+ comm_, sender_, receiver_, mbox_);
}
std::string CommWaitTransition::to_string(bool verbose) const
{
- auto res = xbt::string_printf("WaitComm(from %ld to %ld, mbox=%u, %s", sender_, receiver_, mbox_,
- (timeout_ ? "timeout" : "no timeout"));
- if (verbose) {
- res += ", sbuff=" + xbt::string_printf("%" PRIxPTR, sbuff_) + ", size=" + std::to_string(size_);
- res += ", rbuff=" + xbt::string_printf("%" PRIxPTR, rbuff_);
- }
- res += ")";
- return res;
+ return xbt::string_printf("WaitComm(from %ld to %ld, mbox=%u, %s)", sender_, receiver_, mbox_,
+ (timeout_ ? "timeout" : "no timeout"));
}
bool CommWaitTransition::depends(const Transition* other) const
{
return false; // Comm transitions are INDEP with non-comm transitions
}
CommTestTransition::CommTestTransition(aid_t issuer, int times_considered, unsigned comm_, aid_t sender_,
- aid_t receiver_, unsigned mbox_, uintptr_t sbuff_, uintptr_t rbuff_,
- size_t size_)
+ aid_t receiver_, unsigned mbox_)
: Transition(Type::COMM_TEST, issuer, times_considered)
, comm_(comm_)
, mbox_(mbox_)
, sender_(sender_)
, receiver_(receiver_)
- , sbuff_(sbuff_)
- , rbuff_(rbuff_)
- , size_(size_)
{
}
CommTestTransition::CommTestTransition(aid_t issuer, int times_considered, std::stringstream& stream)
: Transition(Type::COMM_TEST, issuer, times_considered)
{
- xbt_assert(stream >> comm_ >> sender_ >> receiver_ >> mbox_ >> sbuff_ >> rbuff_ >> size_ >> call_location_);
- XBT_DEBUG("CommTestTransition comm:%u, sender:%ld receiver:%ld mbox:%u sbuff:%" PRIxPTR " rbuff:%" PRIxPTR
- " size:%zu",
- comm_, sender_, receiver_, mbox_, sbuff_, rbuff_, size_);
+ xbt_assert(stream >> comm_ >> sender_ >> receiver_ >> mbox_ >> call_location_);
+ XBT_DEBUG("CommTestTransition comm:%u, sender:%ld receiver:%ld mbox:%u", comm_, sender_, receiver_, mbox_);
}
std::string CommTestTransition::to_string(bool verbose) const
{
- auto res = xbt::string_printf("TestComm(from %ld to %ld, mbox=%u", sender_, receiver_, mbox_);
- if (verbose) {
- res += ", sbuff=" + xbt::string_printf("%" PRIxPTR, sbuff_) + ", size=" + std::to_string(size_);
- res += ", rbuff=" + xbt::string_printf("%" PRIxPTR, rbuff_);
- }
- res += ")";
- return res;
+ return xbt::string_printf("TestComm(from %ld to %ld, mbox=%u)", sender_, receiver_, mbox_);
}
bool CommTestTransition::depends(const Transition* other) const
{
return false; // Comm transitions are INDEP with non-comm transitions
}
-CommRecvTransition::CommRecvTransition(aid_t issuer, int times_considered, unsigned comm_, unsigned mbox_,
- uintptr_t rbuff_, int tag_)
- : Transition(Type::COMM_ASYNC_RECV, issuer, times_considered)
- , comm_(comm_)
- , mbox_(mbox_)
- , rbuff_(rbuff_)
- , tag_(tag_)
+CommRecvTransition::CommRecvTransition(aid_t issuer, int times_considered, unsigned comm_, unsigned mbox_, int tag_)
+ : Transition(Type::COMM_ASYNC_RECV, issuer, times_considered), comm_(comm_), mbox_(mbox_), tag_(tag_)
{
}
CommRecvTransition::CommRecvTransition(aid_t issuer, int times_considered, std::stringstream& stream)
: Transition(Type::COMM_ASYNC_RECV, issuer, times_considered)
{
- xbt_assert(stream >> comm_ >> mbox_ >> rbuff_ >> tag_ >> call_location_);
+ xbt_assert(stream >> comm_ >> mbox_ >> tag_ >> call_location_);
}
std::string CommRecvTransition::to_string(bool verbose) const
{
- auto res = xbt::string_printf("iRecv(mbox=%u", mbox_);
- if (verbose)
- res += ", rbuff=" + xbt::string_printf("%" PRIxPTR, rbuff_);
- res += ")";
- return res;
+ return xbt::string_printf("iRecv(mbox=%u)", mbox_);
}
bool CommRecvTransition::depends(const Transition* other) const
{
return false; // Comm transitions are INDEP with non-comm transitions
}
-CommSendTransition::CommSendTransition(aid_t issuer, int times_considered, unsigned comm_, unsigned mbox_,
- uintptr_t sbuff_, size_t size_, int tag_)
- : Transition(Type::COMM_ASYNC_SEND, issuer, times_considered)
- , comm_(comm_)
- , mbox_(mbox_)
- , sbuff_(sbuff_)
- , size_(size_)
- , tag_(tag_)
+CommSendTransition::CommSendTransition(aid_t issuer, int times_considered, unsigned comm_, unsigned mbox_, int tag_)
+ : Transition(Type::COMM_ASYNC_SEND, issuer, times_considered), comm_(comm_), mbox_(mbox_), tag_(tag_)
{
}
CommSendTransition::CommSendTransition(aid_t issuer, int times_considered, std::stringstream& stream)
: Transition(Type::COMM_ASYNC_SEND, issuer, times_considered)
{
- xbt_assert(stream >> comm_ >> mbox_ >> sbuff_ >> size_ >> tag_ >> call_location_);
- XBT_DEBUG("SendTransition comm:%u mbox:%u sbuff:%" PRIxPTR " size:%zu", comm_, mbox_, sbuff_, size_);
+ xbt_assert(stream >> comm_ >> mbox_ >> tag_ >> call_location_);
+ XBT_DEBUG("SendTransition comm:%u mbox:%u", comm_, mbox_);
}
std::string CommSendTransition::to_string(bool verbose = false) const
{
- auto res = xbt::string_printf("iSend(mbox=%u", mbox_);
- if (verbose)
- res += ", sbuff=" + xbt::string_printf("%" PRIxPTR, sbuff_) + ", size=" + std::to_string(size_);
- res += ")";
- return res;
+ return xbt::string_printf("iSend(mbox=%u)", mbox_);
}
bool CommSendTransition::depends(const Transition* other) const
unsigned mbox_;
aid_t sender_;
aid_t receiver_;
- uintptr_t sbuff_;
- uintptr_t rbuff_;
- size_t size_;
friend CommRecvTransition;
friend CommSendTransition;
friend CommTestTransition;
public:
CommWaitTransition(aid_t issuer, int times_considered, bool timeout_, unsigned comm_, aid_t sender_, aid_t receiver_,
- unsigned mbox_, uintptr_t sbuff_, uintptr_t rbuff_, size_t size_);
+ unsigned mbox_);
CommWaitTransition(aid_t issuer, int times_considered, std::stringstream& stream);
std::string to_string(bool verbose) const override;
bool depends(const Transition* other) const override;
aid_t get_receiver() const { return receiver_; }
/** Mailbox ID */
unsigned get_mailbox() const { return mbox_; }
- /** Sender buffer */
- uintptr_t get_sbuff() const { return sbuff_; }
- /** Receiver buffer */
- uintptr_t get_rbuff() const { return rbuff_; }
- /** data size */
- size_t get_size() const { return size_; }
};
class CommTestTransition : public Transition {
unsigned comm_;
unsigned mbox_;
aid_t sender_;
aid_t receiver_;
- uintptr_t sbuff_;
- uintptr_t rbuff_;
- size_t size_;
friend CommSendTransition;
friend CommRecvTransition;
public:
- CommTestTransition(aid_t issuer, int times_considered, unsigned comm_, aid_t sender_, aid_t receiver_, unsigned mbox_,
- uintptr_t sbuff_, uintptr_t rbuff_, size_t size_);
+ CommTestTransition(aid_t issuer, int times_considered, unsigned comm_, aid_t sender_, aid_t receiver_,
+ unsigned mbox_);
CommTestTransition(aid_t issuer, int times_considered, std::stringstream& stream);
std::string to_string(bool verbose) const override;
bool depends(const Transition* other) const override;
aid_t get_receiver() const { return receiver_; }
/** Mailbox ID */
unsigned get_mailbox() const { return mbox_; }
- /** Sender buffer */
- uintptr_t get_sbuff() const { return sbuff_; }
- /** Receiver buffer */
- uintptr_t get_rbuff() const { return rbuff_; }
- /** data size */
- size_t get_size() const { return size_; }
};
class CommRecvTransition : public Transition {
unsigned comm_; /* ID of the CommImpl or 0 if not known */
unsigned mbox_;
- uintptr_t rbuff_;
int tag_;
public:
- CommRecvTransition(aid_t issuer, int times_considered, unsigned comm_, unsigned mbox_, uintptr_t rbuff_, int tag_);
+ CommRecvTransition(aid_t issuer, int times_considered, unsigned comm_, unsigned mbox_, int tag_);
CommRecvTransition(aid_t issuer, int times_considered, std::stringstream& stream);
std::string to_string(bool verbose) const override;
bool depends(const Transition* other) const override;
unsigned get_comm() const { return comm_; }
/** Mailbox ID */
unsigned get_mailbox() const { return mbox_; }
- /** Receiver buffer */
- uintptr_t get_rbuff() const { return rbuff_; }
/** If using SMPI, the tag */
int get_tag() const { return tag_; }
};
class CommSendTransition : public Transition {
unsigned comm_;
unsigned mbox_;
- uintptr_t sbuff_;
- size_t size_;
int tag_;
public:
- CommSendTransition(aid_t issuer, int times_considered, unsigned comm_, unsigned mbox_, uintptr_t sbuff_, size_t size_,
- int tag_);
+ CommSendTransition(aid_t issuer, int times_considered, unsigned comm_, unsigned mbox_, int tag_);
CommSendTransition(aid_t issuer, int times_considered, std::stringstream& stream);
std::string to_string(bool verbose) const override;
bool depends(const Transition* other) const override;
unsigned get_comm() const { return comm_; }
/** Mailbox ID */
unsigned get_mailbox() const { return mbox_; }
- /** Sender buffer */
- uintptr_t get_sbuff() const { return sbuff_; }
- /** data size */
- size_t get_size() const { return size_; }
/** If using SMPI, the tag */
int get_tag() const { return tag_; }
};
