> [ 3.000000] (maestro@) Oops! Deadlock detected, some activities are still around but will never complete. This usually happens when the user code is not perfectly clean.
> [ 3.000000] (maestro@) 1 actors are still running, waiting for something.
> [ 3.000000] (maestro@) Legend of the following listing: "Actor <pid> (<name>@<host>): <status>"
-> [ 3.000000] (maestro@) Actor 3 (C@Ginette): waiting for communication activity 0xdeadbeef () in state WAITING to finish
+> [ 3.000000] (maestro@) Actor 3 (C@Ginette): waiting for communication activity 0xdeadbeef () in state WAITING to finish
> [ 3.000000] (C@Ginette) I was killed!
> [ 3.000000] (C@Ginette) The backtrace would be displayed here if --log=no_loc would not have been passed
> [ 3.000000] (maestro@) Oops! Deadlock detected, some activities are still around but will never complete. This usually happens when the user code is not perfectly clean.
> [ 3.000000] (maestro@) 1 actors are still running, waiting for something.
> [ 3.000000] (maestro@) Legend of the following listing: "Actor <pid> (<name>@<host>): <status>"
-> [ 3.000000] (maestro@) Actor 3 (C@Ginette): waiting for communication activity 0xdeadbeef () in state WAITING to finish
+> [ 3.000000] (maestro@) Actor 3 (C@Ginette): waiting for communication activity 0xdeadbeef () in state WAITING to finish
> [ 3.000000] (C@Ginette) I was killed!
> [ 3.000000] (C@Ginette) The backtrace would be displayed here if --log=no_loc would not have been passed
> [ 3.000000] (maestro@) Actor C terminates now
> [ 0.000000] (0:maestro@) 1: iRecv(mbox=0)
> [ 0.000000] (0:maestro@) 3: iSend(mbox=0)
> [ 0.000000] (0:maestro@) 1: WaitComm(from 3 to 1, mbox=0, no timeout)
-> [ 0.000000] (0:maestro@) Path = 1;2;1;1;2;4;1;1;3;1
+> [ 0.000000] (0:maestro@) You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;2;1;1;2;4;1;1;3;1'
> [ 0.000000] (0:maestro@) DFS exploration ended. 22 unique states visited; 4 backtracks (56 transition replays, 30 states visited overall)
\ No newline at end of file
> [ 0.000000] (0:maestro@) 1: iRecv(mbox=0)
> [ 0.000000] (0:maestro@) 3: iSend(mbox=0)
> [ 0.000000] (0:maestro@) 1: WaitComm(from 3 to 1, mbox=0, no timeout)
-> [ 0.000000] (0:maestro@) Path = 1;3;1;3;1;3;1
+> [ 0.000000] (0:maestro@) You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;3;1;3;1;3;1'
> [ 0.000000] (0:maestro@) DFS exploration ended. 1006 unique states visited; 350 backtracks (5319 transition replays, 3963 states visited overall)
> [0.000000] [mc_ModelChecker/INFO] 1: iRecv(mbox=0)
> [0.000000] [mc_ModelChecker/INFO] 2: iSend(mbox=0)
> [0.000000] [mc_ModelChecker/INFO] 1: WaitComm(from 2 to 1, mbox=0, no timeout)
-> [0.000000] [mc_ModelChecker/INFO] Path = 1;3;1;1;2;1
+> [0.000000] [mc_ModelChecker/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;3;1;1;2;1'
> [0.000000] [mc_dfs/INFO] DFS exploration ended. 119 unique states visited; 36 backtracks (330 transition replays, 175 states visited overall)
> [ 0.000000] (0:maestro@) 1: iRecv(mbox=0)
> [ 0.000000] (0:maestro@) 2: iSend(mbox=0)
> [ 0.000000] (0:maestro@) 1: WaitComm(from 2 to 1, mbox=0, no timeout)
-> [ 0.000000] (0:maestro@) Path = 1;3;1;1;2;1
+> [ 0.000000] (0:maestro@) You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;3;1;1;2;1'
> [ 0.000000] (0:maestro@) DFS exploration ended. 18 unique states visited; 4 backtracks (36 transition replays, 14 states visited overall)
> [0.000000] [mc_global/INFO] **************************
> [0.000000] [mc_global/INFO] *** DEADLOCK DETECTED ***
> [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:2 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:3 dstbuf:2 bufsize:4)
> [0.000000] [mc_global/INFO] Counter-example execution trace:
> [0.000000] [mc_global/INFO] 1: iSend(mbox=2)
> [0.000000] [mc_global/INFO] 2: iSend(mbox=0)
-> [0.000000] [mc_global/INFO] Path = 1;2
+> [0.000000] [mc_Session/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;2'
> [0.000000] [mc_dfs/INFO] DFS exploration ended. 3 unique states visited; 1 backtracks (3 transition replays, 0 states visited overall)
> Execution failed with code 3.
> [0.000000] [mc_global/INFO] **************************
> [0.000000] [mc_global/INFO] *** DEADLOCK DETECTED ***
> [0.000000] [mc_global/INFO] **************************
+> [0.000000] [ker_engine/INFO] 3 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 (main thread@Lilibeth) simcall ActorJoin(pid:2)
+> [0.000000] [ker_engine/INFO] Actor 2 (0:1@Lilibeth) simcall MUTEX_WAIT(mutex_id: 1owner:3)
+> [0.000000] [ker_engine/INFO] Actor 3 (0:2@Lilibeth) simcall MUTEX_WAIT(mutex_id: 0owner:2)
> [0.000000] [mc_global/INFO] Counter-example execution trace:
> [0.000000] [mc_global/INFO] 2: MUTEX_ASYNC_LOCK(mutex: 0, owner:2)
> [0.000000] [mc_global/INFO] 2: MUTEX_WAIT(mutex: 0, owner:2)
> [0.000000] [mc_global/INFO] 2: MUTEX_ASYNC_LOCK(mutex: 1, owner:3)
> [0.000000] [mc_global/INFO] 3: MUTEX_WAIT(mutex: 1, owner:3)
> [0.000000] [mc_global/INFO] 3: MUTEX_ASYNC_LOCK(mutex: 0, owner:2)
-> [0.000000] [mc_global/INFO] Path = 2;2;3;2;3;3
+> [0.000000] [mc_Session/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'2;2;3;2;3;3'
> [0.000000] [mc_dfs/INFO] DFS exploration ended. 19 unique states visited; 2 backtracks (22 transition replays, 2 states visited overall)
#include <dlfcn.h>
#endif /* _WIN32 */
+extern int xbt_log_no_loc;
+
#if SIMGRID_HAVE_MC
#include "src/mc/remote/AppSide.hpp"
#endif
if (boost::dynamic_pointer_cast<kernel::activity::IoImpl>(actor->waiting_synchro_) != nullptr)
synchro_description = "I/O";
- XBT_INFO("Actor %ld (%s@%s): waiting for %s activity %#zx (%s) in state %s to finish", actor->get_pid(),
+ XBT_INFO("Actor %ld (%s@%s): waiting for %s activity %#zx (%s) in state %s to finish %s", actor->get_pid(),
actor->get_cname(), actor->get_host()->get_cname(), synchro_description,
(xbt_log_no_loc ? (size_t)0xDEADBEEF : (size_t)actor->waiting_synchro_.get()),
- actor->waiting_synchro_->get_cname(), actor->waiting_synchro_->get_state_str());
+ actor->waiting_synchro_->get_cname(), actor->waiting_synchro_->get_state_str(),
+ (actor->simcall_.observer_ != nullptr && not xbt_log_no_loc
+ ? actor->simcall_.observer_->to_string().c_str()
+ : ""));
} else {
XBT_INFO("Actor %ld (%s@%s) simcall %s", actor->get_pid(), actor->get_cname(), actor->get_host()->get_cname(),
- actor->simcall_.get_cname());
+ (actor->simcall_.observer_ != nullptr ? actor->simcall_.observer_->to_string().c_str()
+ : actor->simcall_.get_cname()));
}
}
}
/* This program is free software; you can redistribute it and/or modify it
* under the terms of the license (GNU LGPL) which comes with this package. */
+#include "src/mc/mc_replay.hpp"
#include <simgrid/Exception.hpp>
#include <simgrid/s4u/Actor.hpp>
#include <simgrid/s4u/Host.hpp>
if (not wannadie())
smpi_switch_data_segment(get_iface());
#endif
+ if (simgrid_mc_replay_show_backtraces)
+ xbt_backtrace_display_current();
}
/** This actor will be terminated automatically when the last non-daemon actor finishes */
stream << (short)mc::Transition::Type::UNKNOWN;
}
}
+template <typename A> static std::string ptr_to_id(A* ptr)
+{
+ static std::unordered_map<A*, std::string> map;
+ if (map.find(ptr) == map.end())
+ map.insert(std::make_pair(ptr, std::to_string(map.size() + 1)));
+ return map[ptr];
+}
+static std::string to_string_activity_test(const activity::ActivityImpl* act)
+{
+ if (auto* comm = dynamic_cast<activity::CommImpl const*>(act)) {
+ return std::string("CommTest(comm_id:") + ptr_to_id<activity::CommImpl const>(comm) +
+ " 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:" + ptr_to_id<unsigned char>(comm->src_buff_) +
+ " dstbuf:" + ptr_to_id<unsigned char>(comm->dst_buff_) + " bufsize:" + std::to_string(comm->src_buff_size_);
+ } else {
+ return "TestUnknownType()";
+ }
+}
void ActivityTestanySimcall::serialize(std::stringstream& stream) const
{
stream << (short)mc::Transition::Type::TESTANY << ' ' << activities_.size() << ' ';
stream << ' ';
}
}
+std::string ActivityTestanySimcall::to_string() const
+{
+ std::stringstream buffer("TestAny(");
+ for (auto const& act : activities_) {
+ buffer << to_string_activity_test(act);
+ }
+ return buffer.str();
+}
+
void ActivityTestSimcall::serialize(std::stringstream& stream) const
{
serialize_activity_test(activity_, stream);
}
+std::string ActivityTestSimcall::to_string() const
+{
+ return to_string_activity_test(activity_);
+}
static void serialize_activity_wait(const activity::ActivityImpl* act, bool timeout, std::stringstream& stream)
{
if (auto* comm = dynamic_cast<activity::CommImpl const*>(act)) {
stream << (short)mc::Transition::Type::UNKNOWN;
}
}
+static std::string to_string_activity_wait(const activity::ActivityImpl* act)
+{
+ if (auto* comm = dynamic_cast<activity::CommImpl const*>(act)) {
+ return std::string("CommWait(comm_id:") + ptr_to_id<activity::CommImpl const>(comm) +
+ " 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::string(comm->get_mailbox() == nullptr ? xbt::string("-") : comm->get_mailbox()->get_name()) +
+ "(id:" + std::to_string(comm->get_mailbox_id()) + ") srcbuf:" + ptr_to_id<unsigned char>(comm->src_buff_) +
+ " dstbuf:" + ptr_to_id<unsigned char>(comm->dst_buff_) + " bufsize:" + std::to_string(comm->src_buff_size_) +
+ ")";
+ } else {
+ return "WaitUnknownType()";
+ }
+}
void ActivityWaitSimcall::serialize(std::stringstream& stream) const
{
stream << ' ';
}
}
+std::string ActivityWaitSimcall::to_string() const
+{
+ return to_string_activity_wait(activity_);
+}
+std::string ActivityWaitanySimcall::to_string() const
+{
+ std::stringstream buffer("WaitAny(");
+ for (auto const& act : activities_) {
+ buffer << to_string_activity_wait(act);
+ }
+ return buffer.str();
+}
ActivityWaitanySimcall::ActivityWaitanySimcall(ActorImpl* actor, const std::vector<activity::ActivityImpl*>& activities,
double timeout)
: ResultingSimcall(actor, -1), activities_(activities), timeout_(timeout)
XBT_DEBUG("SendObserver comm:%p mbox:%u buff:%p size:%zu tag:%d", comm_, mbox_->get_id(), src_buff_, src_buff_size_,
tag_);
}
+std::string CommIsendSimcall::to_string() const
+{
+ return std::string("CommAsyncSend(comm_id: ") + std::to_string((uintptr_t)comm_) +
+ " 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_) + ")";
+}
void CommIrecvSimcall::serialize(std::stringstream& stream) const
{
stream << (uintptr_t)comm_ << ' ' << 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_);
}
+std::string CommIrecvSimcall::to_string() const
+{
+ return std::string("CommAsyncRecv(comm_id: ") + ptr_to_id<activity::CommImpl const>(comm_) +
+ " mbox:" + std::to_string(mbox_->get_id()) + " dstbuf:" + ptr_to_id<unsigned char>(dst_buff_) +
+ " tag: " + std::to_string(tag_) + ")";
+}
} // namespace simgrid::kernel::actor
bool is_visible() const override { return true; }
activity::ActivityImpl* get_activity() const { return activity_; }
void serialize(std::stringstream& stream) const override;
+ std::string to_string() const override;
};
class ActivityTestanySimcall final : public ResultingSimcall<ssize_t> {
bool is_visible() const override { return true; }
bool is_enabled() override { return true; /* can return -1 if no activity is ready */ }
void serialize(std::stringstream& stream) const override;
+ std::string to_string() const override;
int get_max_consider() const override;
void prepare(int times_considered) override;
const std::vector<activity::ActivityImpl*>& get_activities() const { return activities_; }
{
}
void serialize(std::stringstream& stream) const override;
+ std::string to_string() const override;
bool is_visible() const override { return true; }
bool is_enabled() override;
activity::ActivityImpl* get_activity() const { return activity_; }
ActivityWaitanySimcall(ActorImpl* actor, const std::vector<activity::ActivityImpl*>& activities, double timeout);
bool is_enabled() override;
void serialize(std::stringstream& stream) const override;
+ std::string to_string() const override;
bool is_visible() const override { return true; }
void prepare(int times_considered) override;
int get_max_consider() const override;
{
}
void serialize(std::stringstream& stream) const override;
+ std::string to_string() const override;
bool is_visible() const override { return true; }
activity::MailboxImpl* get_mailbox() const { return mbox_; }
double get_payload_size() const { return payload_size_; }
{
}
void serialize(std::stringstream& stream) const override;
+ std::string to_string() const override;
bool is_visible() const override { return true; }
activity::MailboxImpl* get_mailbox() const { return mbox_; }
double get_rate() const { return rate_; }
*/
void ActorImpl::simcall_handle(int times_considered)
{
- XBT_DEBUG("Handling simcall %p: %s", &simcall_, simcall_.get_cname());
+ XBT_DEBUG("Handling simcall %p: %s(%ld) %s", &simcall_, simcall_.issuer_->get_cname(), simcall_.issuer_->get_pid(),
+ (simcall_.observer_ != nullptr ? simcall_.observer_->to_string().c_str() : simcall_.get_cname()));
if (simcall_.observer_ != nullptr)
simcall_.observer_->prepare(times_considered);
if (wannadie())
stream << (short)mc::Transition::Type::RANDOM << ' ';
stream << min_ << ' ' << max_;
}
+std::string RandomSimcall::to_string() const
+{
+ return std::string("Random(min:") + std::to_string(min_) + " max:" + std::to_string(max_) + ")";
+}
void RandomSimcall::prepare(int times_considered)
{
{
THROW_UNIMPLEMENTED;
}
+std::string ConditionWaitSimcall::to_string() const
+{
+ THROW_UNIMPLEMENTED;
+}
ActorJoinSimcall::ActorJoinSimcall(ActorImpl* actor, ActorImpl* other, double timeout)
: SimcallObserver(actor), other_(s4u::ActorPtr(other->get_iface())), timeout_(timeout)
stream << (short)mc::Transition::Type::ACTOR_JOIN << ' ';
stream << other_->get_pid() << ' ' << (timeout_ > 0);
}
+std::string ActorJoinSimcall::to_string() const
+{
+ return std::string("ActorJoin(pid:") + std::to_string(other_->get_pid()) + ")";
+}
} // namespace simgrid::kernel::actor
{ /* Nothing to do by default */
}
- /** Serialize to the given string buffer */
+ /** Serialize to the given string buffer, to send over the network */
virtual void serialize(std::stringstream& stream) const = 0;
+ /** Used to debug (to display the simcall on which each actor is blocked when displaying it */
+ virtual std::string to_string() const = 0;
+
/** Whether the MC should see this simcall.
* Simcall that don't have an observer (ie, most of them) are not visible from the MC, but if there is an observer,
* they are observable by default. */
xbt_assert(min < max);
}
void serialize(std::stringstream& stream) const override;
+ std::string to_string() const override;
int get_max_consider() const override;
void prepare(int times_considered) override;
int get_value() const { return next_value_; }
{
}
void serialize(std::stringstream& stream) const override;
+ std::string to_string() const override;
bool is_enabled() override;
activity::ConditionVariableImpl* get_cond() const { return cond_; }
activity::MutexImpl* get_mutex() const { return mutex_; }
public:
ActorJoinSimcall(ActorImpl* actor, ActorImpl* other, double timeout = -1.0);
void serialize(std::stringstream& stream) const override;
+ std::string to_string() const override;
bool is_enabled() override;
s4u::ActorPtr get_other_actor() const { return other_; }
const auto* owner = get_mutex()->get_owner();
stream << (short)type_ << ' ' << get_mutex()->get_id() << ' ' << (owner != nullptr ? owner->get_pid() : -1);
}
+std::string MutexObserver::to_string() const
+{
+ return std::string(mc::Transition::to_c_str(type_)) + "(mutex_id: " + std::to_string(get_mutex()->get_id()) +
+ "owner:" + std::to_string(get_mutex()->get_owner()->get_pid()) + ")";
+}
bool MutexObserver::is_enabled()
{
{
stream << (short)type_ << ' ' << get_sem()->get_id() << ' ' << false /* Granted is ignored for LOCK/UNLOCK */;
}
+std::string SemaphoreObserver::to_string() const
+{
+ return std::string(mc::Transition::to_c_str(type_)) + "(sem_id: " + std::to_string(get_sem()->get_id()) + ")";
+}
SemaphoreAcquisitionObserver::SemaphoreAcquisitionObserver(ActorImpl* actor, mc::Transition::Type type,
activity::SemAcquisitionImpl* acqui, double timeout)
{
stream << (short)type_ << ' ' << acquisition_->semaphore_->get_id() << ' ' << acquisition_->granted_;
}
+std::string SemaphoreAcquisitionObserver::to_string() const
+{
+ return std::string(mc::Transition::to_c_str(type_)) +
+ "(sem_id: " + std::to_string(acquisition_->semaphore_->get_id()) + ' ' +
+ (acquisition_->granted_ ? "granted)" : "not granted)");
+}
BarrierObserver::BarrierObserver(ActorImpl* actor, mc::Transition::Type type, activity::BarrierImpl* bar)
: ResultingSimcall(actor, false), type_(type), barrier_(bar), timeout_(-1)
xbt_assert(barrier_ != nullptr || (acquisition_ != nullptr && acquisition_->barrier_ != nullptr));
stream << (short)type_ << ' ' << (barrier_ != nullptr ? barrier_->get_id() : acquisition_->barrier_->get_id());
}
+std::string BarrierObserver::to_string() const
+{
+ return std::string(mc::Transition::to_c_str(type_)) +
+ "(barrier_id: " + std::to_string(barrier_ != nullptr ? barrier_->get_id() : acquisition_->barrier_->get_id()) +
+ ")";
+}
bool BarrierObserver::is_enabled()
{
return type_ == mc::Transition::Type::BARRIER_ASYNC_LOCK ||
MutexObserver(ActorImpl* actor, mc::Transition::Type type, activity::MutexImpl* mutex);
void serialize(std::stringstream& stream) const override;
+ std::string to_string() const override;
bool is_enabled() override;
activity::MutexImpl* get_mutex() const { return mutex_; }
SemaphoreObserver(ActorImpl* actor, mc::Transition::Type type, activity::SemaphoreImpl* sem);
void serialize(std::stringstream& stream) const override;
+ std::string to_string() const override;
activity::SemaphoreImpl* get_sem() const { return sem_; }
};
double timeout = -1.0);
void serialize(std::stringstream& stream) const override;
+ std::string to_string() const override;
bool is_enabled() override;
double get_timeout() const { return timeout_; }
};
-/* This observer is ued for BARRIER_LOCK and BARRIER_WAIT. WAIT is returning and needs the acquisition */
+/* This observer is used for BARRIER_LOCK and BARRIER_WAIT. WAIT is returning and needs the acquisition */
class BarrierObserver final : public ResultingSimcall<bool> {
mc::Transition::Type type_;
activity::BarrierImpl* const barrier_ = nullptr;
double timeout = -1.0);
void serialize(std::stringstream& stream) const override;
+ std::string to_string() const override;
bool is_enabled() override;
double get_timeout() const { return timeout_; }
XBT_INFO("Counter-example execution trace:");
for (auto const& s : explorer->get_textual_trace())
XBT_INFO(" %s", s.c_str());
- XBT_INFO("Path = %s", explorer->get_record_trace().to_string().c_str());
+ XBT_INFO("You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with "
+ "--cfg=model-check/replay:'%s'",
+ explorer->get_record_trace().to_string().c_str());
explorer->log_state();
if (xbt_log_no_loc) {
XBT_INFO("Stack trace not displayed because you passed --log=no_loc");
XBT_INFO("Counter-example execution trace:");
for (auto const& s : get_exploration()->get_textual_trace())
XBT_INFO(" %s", s.c_str());
- XBT_INFO("Path = %s", get_exploration()->get_record_trace().to_string().c_str());
+ XBT_INFO("You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with "
+ "--cfg=model-check/replay:'%s'",
+ get_exploration()->get_record_trace().to_string().c_str());
exploration_->log_state();
this->exit(SIMGRID_MC_EXIT_SAFETY);
(int)sizeof(message));
if (message.value != 0) {
- XBT_CINFO(mc_global, "**************************");
- XBT_CINFO(mc_global, "*** DEADLOCK DETECTED ***");
- XBT_CINFO(mc_global, "**************************");
XBT_CINFO(mc_global, "Counter-example execution trace:");
for (auto const& frame : model_checker_->get_exploration()->get_textual_trace())
XBT_CINFO(mc_global, " %s", frame.c_str());
- XBT_CINFO(mc_global, "Path = %s", model_checker_->get_exploration()->get_record_trace().to_string().c_str());
+ XBT_INFO("You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with "
+ "--cfg=model-check/replay:'%s'",
+ model_checker_->get_exploration()->get_record_trace().to_string().c_str());
model_checker_->get_exploration()->log_state();
throw DeadlockError();
}
XBT_INFO("Counter-example execution trace:");
for (auto const& s : get_textual_trace())
XBT_INFO(" %s", s.c_str());
- XBT_INFO("Path = %s", get_record_trace().to_string().c_str());
+ XBT_INFO("You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with "
+ "--cfg=model-check/replay:'%s'",
+ get_record_trace().to_string().c_str());
log_state();
throw TerminationError();
State* state = stack_.back().get();
XBT_DEBUG("**************************************************");
- XBT_DEBUG("Exploration depth=%zu (state:%ld; %zu interleaves)", stack_.size(), state->get_num(),
+ XBT_DEBUG("Exploration depth=%zu (state:#%ld; %zu interleaves todo)", stack_.size(), state->get_num(),
state->count_todo());
mc_model_checker->inc_visited_states();
XBT_INFO("Counter-example that violates formula:");
for (auto const& s : this->get_textual_trace())
XBT_INFO(" %s", s.c_str());
- XBT_INFO("Path = %s", get_record_trace().to_string().c_str());
+ XBT_INFO("You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with "
+ "--cfg=model-check/replay:'%s'",
+ get_record_trace().to_string().c_str());
log_state();
XBT_INFO("Counter-example depth: %zu", depth);
}
#endif
XBT_LOG_NEW_DEFAULT_CATEGORY(mc, "All MC categories");
+bool simgrid_mc_replay_show_backtraces = false;
namespace simgrid::mc {
{
auto* engine = kernel::EngineImpl::get_instance();
+ XBT_DEBUG("execute_actors: %lu of %zu to run (%s)", engine->get_actor_to_run_count(), engine->get_actor_count(),
+ (MC_record_replay_is_active() ? "replay active" : "no replay"));
while (engine->has_actors_to_run()) {
engine->run_all_actors();
for (auto const& actor : engine->get_actors_that_ran()) {
* transition for ever.
* This is controlled in the is_enabled() method of the corresponding observers.
*/
-// Called from both MCer and MCed:
bool actor_is_enabled(kernel::actor::ActorImpl* actor)
{
#if SIMGRID_HAVE_MC
#if SIMGRID_HAVE_MC
xbt_assert(mc_model_checker == nullptr, "This should be called from the client side");
#endif
- if (req->observer_ != nullptr)
- return req->observer_->is_visible();
- else
+ if (req->observer_ == nullptr)
return false;
+ return req->observer_->is_visible();
}
} // namespace simgrid::mc
void RecordTrace::replay() const
{
simgrid::mc::execute_actors();
+ auto* engine = kernel::EngineImpl::get_instance();
- for (const simgrid::mc::Transition* transition : transitions_) {
- XBT_DEBUG("Executing %ld$%i", transition->aid_, transition->times_considered_);
+ int frame_count = 1;
+ if (xbt_log_no_loc)
+ XBT_INFO("The backtrace of each transition will not be shown because of --log=no_loc");
+ else
+ simgrid_mc_replay_show_backtraces = 1;
- // Choose a request:
- kernel::actor::ActorImpl* actor = kernel::EngineImpl::get_instance()->get_actor_by_pid(transition->aid_);
+ for (const simgrid::mc::Transition* transition : transitions_) {
+ kernel::actor::ActorImpl* actor = engine->get_actor_by_pid(transition->aid_);
xbt_assert(actor != nullptr, "Unexpected actor (id:%ld).", transition->aid_);
const kernel::actor::Simcall* simcall = &(actor->simcall_);
- xbt_assert(simcall->call_ != kernel::actor::Simcall::Type::NONE, "No simcall for process %ld.", transition->aid_);
- xbt_assert(simgrid::mc::request_is_visible(simcall) && simgrid::mc::actor_is_enabled(actor), "Unexpected simcall.");
+ xbt_assert(simgrid::mc::request_is_visible(simcall), "Simcall %s of actor %s is not visible.", simcall->get_cname(),
+ actor->get_cname());
+
+ XBT_INFO("***********************************************************************************");
+ XBT_INFO("* Path chunk #%d '%ld/%i' Actor %s(pid:%ld): %s", frame_count++, transition->aid_,
+ transition->times_considered_, simcall->issuer_->get_cname(), simcall->issuer_->get_pid(),
+ simcall->observer_->to_string().c_str());
+ XBT_INFO("***********************************************************************************");
+ if (not mc::actor_is_enabled(actor))
+ simgrid::kernel::EngineImpl::get_instance()->display_all_actor_status();
+
+ xbt_assert(simgrid::mc::actor_is_enabled(actor), "Actor %s (simcall %s) is not enabled.", actor->get_cname(),
+ simcall->get_cname());
// Execute the request:
simcall->issuer_->simcall_handle(transition->times_considered_);
simgrid::mc::execute_actors();
}
+
+ const auto& actor_list = engine->get_actor_list();
+ if (actor_list.empty()) {
+ XBT_INFO("The replay of the trace is complete. The application is terminating.");
+ } else if (std::none_of(begin(actor_list), end(actor_list),
+ [](const auto& kv) { return mc::actor_is_enabled(kv.second); })) {
+ XBT_INFO("The replay of the trace is complete. DEADLOCK detected.");
+ engine->display_all_actor_status();
+ } else {
+ XBT_INFO("The replay of the trace is complete. The application could run further.");
+ }
}
void simgrid::mc::RecordTrace::replay(const std::string& path_string)
const char* current = data;
while (*current) {
long aid;
- int times_considered;
+ int times_considered = 0;
if (int count = sscanf(current, "%ld/%d", &aid, ×_considered); count != 2 && count != 1)
throw std::invalid_argument("Could not parse record path");
return not MC_record_path().empty();
}
+/** Whether we should display extra information during this MC replay */
+extern bool simgrid_mc_replay_show_backtraces;
+
#endif
#include <sys/types.h>
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_client, mc, "MC client logic");
+XBT_LOG_EXTERNAL_CATEGORY(mc_global);
namespace simgrid::mc {
void AppSide::handle_deadlock_check(const s_mc_message_t*) const
{
- const auto& actor_list = kernel::EngineImpl::get_instance()->get_actor_list();
+ auto* engine = kernel::EngineImpl::get_instance();
+ const auto& actor_list = engine->get_actor_list();
bool deadlock = not actor_list.empty() && std::none_of(begin(actor_list), end(actor_list), [](const auto& kv) {
return mc::actor_is_enabled(kv.second);
});
+ if (deadlock) {
+ XBT_CINFO(mc_global, "**************************");
+ XBT_CINFO(mc_global, "*** DEADLOCK DETECTED ***");
+ XBT_CINFO(mc_global, "**************************");
+ engine->display_all_actor_status();
+ }
// Send result:
s_mc_message_int_t answer{MessageType::DEADLOCK_CHECK_REPLY, deadlock};
xbt_assert(channel_.send(answer) == 0, "Could not send response");
#include "smpi_host.hpp"
#include "src/kernel/EngineImpl.hpp"
#include "src/kernel/activity/CommImpl.hpp"
+#include "src/mc/mc_replay.hpp"
#include "src/smpi/include/smpi_actor.hpp"
#include "xbt/config.hpp"
#include "xbt/file.hpp"
smpi_init_fortran_types();
if(_smpi_init_sleep > 0)
simgrid::s4u::this_actor::sleep_for(_smpi_init_sleep);
- if (not MC_is_active()) {
+ if (not MC_is_active() && not MC_record_replay_is_active()) {
smpi_deployment_startup_barrier(smpi_process()->get_instance_id());
}
}
if (frame_name.rfind("simgrid::xbt::MainFunction", 0) == 0 ||
frame_name.rfind("simgrid::kernel::context::Context::operator()()", 0) == 0)
break;
- ss << " -> " << frame_count++ << "# " << frame << "\n";
+ if (xbt_log_no_loc) { // Don't display file source and line if so
+ if (frame.name().empty())
+ ss << " -> #" << frame_count++ << " (debug info not found and log:no_loc activated)\n";
+ else
+ ss << " -> #" << frame_count++ << " " << frame.name() << "\n";
+ } else
+ ss << " -> #" << frame_count++ << " " << frame << "\n";
+ // If we are displaying the user side of a simcall, remove the crude details of context switching
+ if (frame_name.find("simgrid::kernel::actor::simcall_answered") != std::string::npos ||
+ frame_name.find("simgrid::kernel::actor::simcall_blocking") != std::string::npos ||
+ frame_name.find("simcall_run_answered") != std::string::npos ||
+ frame_name.find("simcall_run_blocking") != std::string::npos) {
+ frame_count = 0;
+ ss.str(std::string()); // This is how you clear a stringstream in C++. clear() is something else :'(
+ }
if (frame_name == "main")
break;
} else {
void Backtrace::display() const
{
std::string backtrace = resolve();
- std::fprintf(stderr, "Backtrace (displayed in actor %s):\n%s\n", xbt_procname(),
+ std::fprintf(stderr, "Backtrace (displayed in actor %s%s):\n%s\n", xbt_procname(),
+ (xbt_log_no_loc ? " -- short trace because of --log=no_loc" : ""),
backtrace.empty() ? "(backtrace not set -- did you install Boost.Stacktrace?)" : backtrace.c_str());
}
target_link_libraries(${x} simgrid)
set_target_properties(${x} PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}/${x})
set_property(TARGET ${x} APPEND PROPERTY INCLUDE_DIRECTORIES "${INTERNAL_INCLUDES}")
+ target_compile_options(${x} PRIVATE ${CMAKE_C_DEBUG_FLAGS})
add_dependencies(tests-mc ${x})
endif()
#!/usr/bin/env tesh
-$ ${bindir:=.}/random-bug printf ${platfdir}/small_platform.xml --log=xbt_cfg.thresh:warning "--log=root.fmt:[%10.6r]%e(%i:%a@%h)%e%m%n" "--cfg=model-check/replay:1/3;1/4"
+$ ${bindir:=.}/random-bug printf ${platfdir}/small_platform.xml --log=xbt_cfg.thresh:warning "--log=root.fmt:[%10.6r]%e(%i:%a@%h)%e%m%n" "--cfg=model-check/replay:1/3;1/4" --log=no_loc
> [ 0.000000] (0:maestro@) Behavior: printf
> [ 0.000000] (0:maestro@) path=1/3;1/4
+> [ 0.000000] (0:maestro@) The backtrace of each transition will not be shown because of --log=no_loc
+> [ 0.000000] (0:maestro@) ***********************************************************************************
+> [ 0.000000] (0:maestro@) * Path chunk #1 '1/3' Actor app(pid:1): Random(min:0 max:5)
+> [ 0.000000] (0:maestro@) ***********************************************************************************
+> [ 0.000000] (0:maestro@) ***********************************************************************************
+> [ 0.000000] (0:maestro@) * Path chunk #2 '1/4' Actor app(pid:1): Random(min:0 max:5)
+> [ 0.000000] (0:maestro@) ***********************************************************************************
> [ 0.000000] (1:app@Fafard) Error reached
+> [ 0.000000] (0:maestro@) The replay of the trace is complete. The application is terminating.
# Behavior: assert does not have the same output within and without MC, so don't test it here. That's already covered with the other ones
! expect signal SIGIOT
-$ $VALGRIND_NO_LEAK_CHECK ${bindir:=.}/random-bug abort ${platfdir}/small_platform.xml --log=xbt_cfg.thresh:warning "--log=root.fmt:[%10.6r]%e(%i:%a@%h)%e%m%n" "--cfg=model-check/replay:1/3;1/4"
+$ $VALGRIND_NO_LEAK_CHECK ${bindir:=.}/random-bug abort ${platfdir}/small_platform.xml --log=xbt_cfg.thresh:warning "--log=root.fmt:[%10.6r]%e(%i:%a@%h)%e%m%n" "--cfg=model-check/replay:1/3;1/4" --log=no_loc
> [ 0.000000] (0:maestro@) Behavior: abort
> [ 0.000000] (0:maestro@) path=1/3;1/4
+> [ 0.000000] (0:maestro@) The backtrace of each transition will not be shown because of --log=no_loc
+> [ 0.000000] (0:maestro@) ***********************************************************************************
+> [ 0.000000] (0:maestro@) * Path chunk #1 '1/3' Actor app(pid:1): Random(min:0 max:5)
+> [ 0.000000] (0:maestro@) ***********************************************************************************
+> [ 0.000000] (0:maestro@) ***********************************************************************************
+> [ 0.000000] (0:maestro@) * Path chunk #2 '1/4' Actor app(pid:1): Random(min:0 max:5)
+> [ 0.000000] (0:maestro@) ***********************************************************************************
> [ 0.000000] (0:maestro@) Counter-example execution trace:
> [ 0.000000] (0:maestro@) 1: Random([0;5] ~> 3)
> [ 0.000000] (0:maestro@) 1: Random([0;5] ~> 4)
-> [ 0.000000] (0:maestro@) Path = 1/3;1/4
+> [ 0.000000] (0:maestro@) You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1/3;1/4'
> [ 0.000000] (0:maestro@) DFS exploration ended. 27 unique states visited; 22 backtracks (68 transition replays, 19 states visited overall)
! expect return 6
> [ 0.000000] (0:maestro@) Counter-example execution trace:
> [ 0.000000] (0:maestro@) 1: Random([0;5] ~> 3)
> [ 0.000000] (0:maestro@) 1: Random([0;5] ~> 4)
-> [ 0.000000] (0:maestro@) Path = 1/3;1/4
+> [ 0.000000] (0:maestro@) You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1/3;1/4'
> [ 0.000000] (0:maestro@) DFS exploration ended. 27 unique states visited; 22 backtracks (68 transition replays, 19 states visited overall)
> [ 0.000000] (0:maestro@) Stack trace not displayed because you passed --log=no_loc
> [ 0.000000] (0:maestro@) Counter-example execution trace:
> [ 0.000000] (0:maestro@) 1: Random([0;5] ~> 3)
> [ 0.000000] (0:maestro@) 1: Random([0;5] ~> 4)
-> [ 0.000000] (0:maestro@) Path = 1/3;1/4
+> [ 0.000000] (0:maestro@) You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1/3;1/4'
> [ 0.000000] (0:maestro@) DFS exploration ended. 27 unique states visited; 22 backtracks (68 transition replays, 19 states visited overall)
> [ 0.000000] (0:maestro@) Stack trace not displayed because you passed --log=no_loc
if res_category != "TRUE_NEG" and res_category != "TRUE_POS":
print("XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX\n")
- print(f"SimGrid gave the wrong result on {binary} ({outcome} instead of {test['expect']}).")
+ print(f"SimGrid gave the wrong result on {binary} ({outcome} instead of {test['detail']}).\nExpected diagnostic: {test['diagnostic']}")
sys.exit(1)
if detail not in possible_details:
raise ValueError(
f"\n{filename}:{line_num}: MBI parse error: Detailled outcome {detail} is not one of the allowed ones.")
- test = {'filename': filename, 'id': test_num, 'cmd': cmd, 'expect': expect, 'detail': detail}
+
+ nextline = next(input_file)
+ m = re.match('[ |]*(.*)', nextline)
+ if not m:
+ raise ValueError(f"\n{filename}:{line_num}: MBI parse error: Expected diagnostic of the test not found.\n")
+ diagnostic = m.group(1)
+
+ test = {'filename': filename, 'id': test_num, 'cmd': cmd, 'expect': expect, 'detail': detail, 'diagnostic': diagnostic}
res.append(test.copy())
test_num += 1
line_num += 1
