namespace kernel {
namespace activity {
+unsigned MailboxImpl::next_id_ = 0;
+
/** @brief set the receiver of the mailbox to allow eager sends
* @param actor The receiving dude
*/
friend s4u::Mailbox* s4u::Mailbox::by_name(const std::string& name);
friend mc::CommunicationDeterminismChecker;
- explicit MailboxImpl(const std::string& name) : piface_(this), name_(name) {}
+ static unsigned next_id_; // Next ID to be given
+ unsigned id_;
+ explicit MailboxImpl(const std::string& name) : piface_(this), name_(name), id_(next_id_++) {}
public:
/** @brief Public interface */
+ unsigned get_id() { return id_; }
+
const s4u::Mailbox* get_iface() const { return &piface_; }
s4u::Mailbox* get_iface() { return &piface_; }
#include "src/kernel/actor/SimcallObserver.hpp"
#include "simgrid/s4u/Host.hpp"
#include "src/kernel/activity/CommImpl.hpp"
+#include "src/kernel/activity/MailboxImpl.hpp"
#include "src/kernel/activity/MutexImpl.hpp"
#include "src/kernel/actor/ActorImpl.hpp"
#include "src/mc/mc_config.hpp"
+#include <sstream>
+
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_observer, mc, "Logging specific to MC simcall observation");
namespace simgrid {
return true; // Depend on things we don't know for sure that they are independent
}
-std::string SimcallObserver::to_string(int /*times_considered*/) const
+/*
+std::string SimcallObserver::to_string(int) const
{
return simgrid::xbt::string_printf("[(%ld)%s (%s)] ", issuer_->get_pid(), issuer_->get_host()->get_cname(),
issuer_->get_cname());
-}
+}*/
std::string SimcallObserver::dot_label(int /*times_considered*/) const
{
return xbt::string_printf("[(%ld)] ", issuer_->get_pid());
}
-std::string RandomSimcall::to_string(int times_considered) const
-{
- return SimcallObserver::to_string(times_considered) + "MC_RANDOM(" + std::to_string(times_considered) + ")";
-}
-
std::string RandomSimcall::dot_label(int times_considered) const
{
return SimcallObserver::dot_label(times_considered) + "MC_RANDOM(" + std::to_string(next_value_) + ")";
return max_ - min_ + 1;
}
-std::string MutexUnlockSimcall::to_string(int times_considered) const
-{
- return SimcallObserver::to_string(times_considered) + "Mutex UNLOCK";
-}
-
std::string MutexUnlockSimcall::dot_label(int times_considered) const
{
return SimcallObserver::dot_label(times_considered) + "Mutex UNLOCK";
}
+/*
std::string MutexLockSimcall::to_string(int times_considered) const
{
auto mutex = get_mutex();
res += ", owner = " + std::to_string(mutex->get_owner() ? mutex->get_owner()->get_pid() : -1);
res += ", sleeping = n/a)";
return res;
-}
+}*/
std::string MutexLockSimcall::dot_label(int times_considered) const
{
return not blocking_ || get_mutex()->get_owner() == nullptr || get_mutex()->get_owner() == get_issuer();
}
-std::string ConditionWaitSimcall::to_string(int times_considered) const
-{
- std::string res = SimcallObserver::to_string(times_considered) + "Condition WAIT";
- res += "(" + (timeout_ == -1.0 ? "" : std::to_string(timeout_)) + ")";
- return res;
-}
-
std::string ConditionWaitSimcall::dot_label(int times_considered) const
{
return SimcallObserver::dot_label(times_considered) + "Condition WAIT";
return true;
}
-std::string SemAcquireSimcall::to_string(int times_considered) const
-{
- std::string res = SimcallObserver::to_string(times_considered) + "Sem ACQUIRE";
- res += "(" + (timeout_ == -1.0 ? "" : std::to_string(timeout_)) + ")";
- return res;
-}
-
std::string SemAcquireSimcall::dot_label(int times_considered) const
{
return SimcallObserver::dot_label(times_considered) + "Sem ACQUIRE";
next_value_ = times_considered;
}
+/*
std::string ActivityTestanySimcall::to_string(int times_considered) const
{
std::string res = SimcallObserver::to_string(times_considered);
}
return res;
-}
+}*/
std::string ActivityTestanySimcall::dot_label(int times_considered) const
{
return true;
}
+void ActivityWaitSimcall::serialize(Simcall& type, char* buffer)
+{
+ std::stringstream stream;
+ if (auto* comm = dynamic_cast<activity::CommImpl*>(activity_)) {
+ type = Simcall::COMM_WAIT;
+ stream << timeout_ << ' ' << comm;
+ 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() != nullptr ? comm->get_mailbox()->get_id() : 666);
+ stream << ' ' << (void*)comm->src_buff_ << ' ' << (void*)comm->dst_buff_ << ' ' << comm->src_buff_size_;
+ strcpy(buffer, stream.str().c_str());
+ } else {
+ type = Simcall::UNKNOWN;
+ strcpy(buffer, stream.str().c_str());
+ }
+}
+/*
std::string ActivityTestSimcall::to_string(int times_considered) const
{
std::string res = SimcallObserver::to_string(times_considered) + "Test ";
} else
xbt_die("Only Comms are supported here for now");
return res;
-}
+}*/
std::string ActivityTestSimcall::dot_label(int times_considered) const
{
return true;
}
-std::string ActivityWaitSimcall::to_string(int times_considered) const
-{
- std::string res = SimcallObserver::to_string(times_considered);
- auto* comm = dynamic_cast<activity::CommImpl*>(activity_);
- if (comm == nullptr) {
- res += "ActivityWait on non-Comm (FIXME)"; // FIXME
- return res;
- }
-
- if (times_considered == -1) {
- res += "WaitTimeout(comm=" + (XBT_LOG_ISENABLED(mc_observer, xbt_log_priority_verbose)
- ? xbt::string_printf("%p)", comm)
- : "(verbose only))");
- } else {
- res += "Wait(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());
- }
- return res;
-}
-
std::string ActivityWaitSimcall::dot_label(int times_considered) const
{
std::string res = SimcallObserver::dot_label(times_considered);
next_value_ = times_considered;
}
-std::string ActivityWaitanySimcall::to_string(int times_considered) const
-{
- std::string res = SimcallObserver::to_string(times_considered) + "WaitAny(";
- size_t count = activities_.size();
- if (count > 0) {
- if (auto* comm = dynamic_cast<kernel::activity::CommImpl*>(activities_[times_considered]))
- res += "comm=" +
- (XBT_LOG_ISENABLED(mc_observer, xbt_log_priority_verbose) ? xbt::string_printf("%p", comm)
- : "(verbose only)") +
- xbt::string_printf("(%d of %zu))", times_considered + 1, count);
- else
- xbt_die("Only Comms are supported here for now");
- } else
- res += "comm at idx " + std::to_string(times_considered) + ")";
- return res;
-}
-
bool CommIsendSimcall::depends(SimcallObserver* other)
{
if (get_issuer() == other->get_issuer())
return true;
}
+void CommIsendSimcall::serialize(Simcall& type, char* buffer)
+{
+ type = Simcall::ISEND;
+ std::stringstream stream;
+ stream << mbox_->get_id() << ' ' << (void*)src_buff_ << ' ' << src_buff_size_;
+ strcpy(buffer, stream.str().c_str());
+}
-std::string CommIsendSimcall::to_string(int times_considered) const
+void CommIrecvSimcall::serialize(Simcall& type, char* buffer)
{
- std::string res = SimcallObserver::to_string(times_considered) + "iSend(";
- res += xbt::string_printf("src=(%ld)%s (%s)", get_issuer()->get_pid(), get_issuer()->get_host()->get_cname(),
- get_issuer()->get_cname());
- res += ", buff=" + (XBT_LOG_ISENABLED(mc_observer, xbt_log_priority_verbose) ? xbt::string_printf("%p", src_buff_)
- : "(verbose only)");
- res += ", size=" +
- (XBT_LOG_ISENABLED(mc_observer, xbt_log_priority_verbose) ? std::to_string(src_buff_size_) : "(verbose only)");
- res += ")";
- return res;
+ type = Simcall::IRECV;
+ std::stringstream stream;
+ stream << mbox_->get_id() << dst_buff_;
+ strcpy(buffer, stream.str().c_str());
}
bool CommIrecvSimcall::depends(SimcallObserver* other)
return true;
}
+/*
std::string CommIrecvSimcall::to_string(int times_considered) const
{
std::string res = SimcallObserver::to_string(times_considered) + "iRecv(";
res += ")";
return res;
}
+*/
} // namespace actor
} // namespace kernel
#include "simgrid/forward.h"
#include "xbt/asserts.h"
+#include "xbt/utility.hpp"
#include <string>
ActorImpl* const issuer_;
public:
+ XBT_DECLARE_ENUM_CLASS(Simcall, UNKNOWN, RANDOM, ISEND, IRECV, COMM_WAIT, COMM_TEST);
+
+ SimcallObserver() = default;
explicit SimcallObserver(ActorImpl* issuer) : issuer_(issuer) {}
ActorImpl* get_issuer() const { return issuer_; }
/** Whether this transition can currently be taken without blocking.
/** Computes the dependency relation */
virtual bool depends(SimcallObserver* other);
+ /** Serialize to the given buffer */
+ virtual void serialize(Simcall& type, char* buffer) { type = Simcall::UNKNOWN; }
+
/** Some simcalls may only be observable under some conditions.
* Most simcalls are not visible from the MC because they don't have an observer at all. */
virtual bool is_visible() const { return true; }
- virtual std::string to_string(int times_considered) const = 0;
virtual std::string dot_label(int times_considered) const = 0;
};
T result_;
public:
+ ResultingSimcall() = default;
ResultingSimcall(ActorImpl* actor, T default_result) : SimcallObserver(actor), result_(default_result) {}
void set_result(T res) { result_ = res; }
T get_result() const { return result_; }
res->next_value_ = next_value_;
return res;
}
+ void serialize(Simcall& type, char* buffer) override { type = Simcall::RANDOM; }
int get_max_consider() const override;
void prepare(int times_considered) override;
- std::string to_string(int times_considered) const override;
std::string dot_label(int times_considered) const override;
int get_value() const { return next_value_; }
bool depends(SimcallObserver* other) override;
public:
SimcallObserver* clone() override { return new MutexUnlockSimcall(get_issuer(), get_mutex()); }
- std::string to_string(int times_considered) const override;
std::string dot_label(int times_considered) const override;
};
}
SimcallObserver* clone() override { return new MutexLockSimcall(get_issuer(), get_mutex(), blocking_); }
bool is_enabled() const override;
- std::string to_string(int times_considered) const override;
std::string dot_label(int times_considered) const override;
};
SimcallObserver* clone() override { return new ConditionWaitSimcall(get_issuer(), cond_, mutex_, timeout_); }
bool is_enabled() const override;
bool is_visible() const override { return false; }
- std::string to_string(int times_considered) const override;
std::string dot_label(int times_considered) const override;
activity::ConditionVariableImpl* get_cond() const { return cond_; }
activity::MutexImpl* get_mutex() const { return mutex_; }
SimcallObserver* clone() override { return new SemAcquireSimcall(get_issuer(), sem_, timeout_); }
bool is_enabled() const override;
bool is_visible() const override { return false; }
- std::string to_string(int times_considered) const override;
std::string dot_label(int times_considered) const override;
activity::SemaphoreImpl* get_sem() const { return sem_; }
double get_timeout() const { return timeout_; }
SimcallObserver* clone() override { return new ActivityTestSimcall(get_issuer(), activity_); }
bool is_visible() const override { return true; }
bool depends(SimcallObserver* other) override;
- std::string to_string(int times_considered) const override;
std::string dot_label(int times_considered) const override;
activity::ActivityImpl* get_activity() const { return activity_; }
};
bool is_visible() const override { return true; }
int get_max_consider() const override;
void prepare(int times_considered) override;
- std::string to_string(int times_considered) const override;
std::string dot_label(int times_considered) const override;
const std::vector<activity::ActivityImpl*>& get_activities() const { return activities_; }
int get_value() const { return next_value_; }
{
}
SimcallObserver* clone() override { return new ActivityWaitSimcall(get_issuer(), activity_, timeout_); }
+ void serialize(Simcall& type, char* buffer);
bool is_visible() const override { return true; }
bool is_enabled() const override;
bool depends(SimcallObserver* other) override;
- std::string to_string(int times_considered) const override;
std::string dot_label(int times_considered) const override;
activity::ActivityImpl* get_activity() const { return activity_; }
void set_activity(activity::ActivityImpl* activity) { activity_ = activity; }
bool is_visible() const override { return true; }
void prepare(int times_considered) override;
int get_max_consider() const override;
- std::string to_string(int times_considered) const override;
std::string dot_label(int times_considered) const override;
const std::vector<activity::ActivityImpl*>& get_activities() const { return activities_; }
double get_timeout() const { return timeout_; }
, copy_data_fun_(copy_data_fun)
{
}
+ void serialize(Simcall& type, char* buffer) override;
CommIsendSimcall* clone() override
{
return new CommIsendSimcall(get_issuer(), mbox_, payload_size_, rate_, src_buff_, src_buff_size_, match_fun_,
}
bool is_visible() const override { return true; }
bool depends(SimcallObserver* other) override;
- std::string to_string(int times_considered) const override;
std::string dot_label(int times_considered) const override
{
return SimcallObserver::dot_label(times_considered) + "iSend";
return new CommIrecvSimcall(get_issuer(), mbox_, dst_buff_, dst_buff_size_, match_fun_, copy_data_fun_, payload_,
rate_);
}
+ void serialize(Simcall& type, char* buffer) override;
bool is_visible() const override { return true; }
bool depends(SimcallObserver* other) override;
- std::string to_string(int times_considered) const override;
std::string dot_label(int times_considered) const override
{
return SimcallObserver::dot_label(times_considered) + "iRecv";
checker_side_.dispatch();
}
-RemotePtr<simgrid::kernel::actor::SimcallObserver> ModelChecker::handle_simcall(Transition const& transition)
+Transition* ModelChecker::handle_simcall(Transition const& transition, bool new_transition)
{
s_mc_message_simcall_execute_t m;
memset(&m, 0, sizeof(m));
if (this->remote_process_->running())
checker_side_.dispatch(); // The app may send messages while processing the transition
- return remote(answer.observer);
+ if (new_transition)
+ return recv_transition(transition.aid_, transition.times_considered_, answer.simcall, answer.buffer);
+ else
+ return nullptr;
}
bool ModelChecker::simcall_is_visible(aid_t aid)
{
return answer.value;
}
-bool ModelChecker::requests_are_dependent(RemotePtr<kernel::actor::SimcallObserver> obs1,
- RemotePtr<kernel::actor::SimcallObserver> obs2) const
-{
- xbt_assert(mc_model_checker != nullptr, "This should be called from the checker side");
-
- s_mc_message_simcalls_dependent_t m;
- memset(&m, 0, sizeof(m));
- m.type = MessageType::SIMCALLS_DEPENDENT;
- m.obs1 = obs1.local();
- m.obs2 = obs2.local();
-
- if (m.obs1 == nullptr || m.obs2 == nullptr)
- return true;
- checker_side_.get_channel().send(m);
-
- s_mc_message_simcalls_dependent_answer_t answer;
- ssize_t s = checker_side_.get_channel().receive(answer);
- xbt_assert(s != -1, "Could not receive message");
- xbt_assert(s == sizeof(answer) && answer.type == MessageType::SIMCALLS_DEPENDENT_ANSWER,
- "Received unexpected message %s (%i, size=%i) "
- "expected MessageType::SIMCALLS_DEPENDENT_ANSWER (%i, size=%i)",
- to_c_str(answer.type), (int)answer.type, (int)s, (int)MessageType::SIMCALLS_DEPENDENT_ANSWER,
- (int)sizeof(answer));
-
- return answer.value;
-}
-
-std::string ModelChecker::simcall_to_string(MessageType type, aid_t aid, int times_considered)
+std::string ModelChecker::simcall_dot_label(aid_t aid, int times_considered)
{
xbt_assert(mc_model_checker != nullptr, "This should be called from the checker side");
s_mc_message_simcall_to_string_t m;
memset(&m, 0, sizeof(m));
- m.type = type;
+ m.type = MessageType::SIMCALL_DOT_LABEL;
m.aid = aid;
m.time_considered = times_considered;
checker_side_.get_channel().send(m);
s_mc_message_simcall_to_string_answer_t answer;
ssize_t s = checker_side_.get_channel().receive(answer);
xbt_assert(s != -1, "Could not receive message");
- xbt_assert(s == sizeof(answer) && answer.type == MessageType::SIMCALL_TO_STRING_ANSWER,
+ xbt_assert(s == sizeof(answer) && answer.type == MessageType::SIMCALL_DOT_LABEL_ANSWER,
"Received unexpected message %s (%i, size=%i) "
"expected MessageType::SIMCALL_TO_STRING_ANSWER (%i, size=%i)",
- to_c_str(answer.type), (int)answer.type, (int)s, (int)MessageType::SIMCALL_TO_STRING_ANSWER,
+ to_c_str(answer.type), (int)answer.type, (int)s, (int)MessageType::SIMCALL_DOT_LABEL_ANSWER,
(int)sizeof(answer));
- return std::string(answer.value);
-}
-
-std::string ModelChecker::simcall_to_string(aid_t aid, int times_considered)
-{
- std::string answer = simcall_to_string(MessageType::SIMCALL_TO_STRING, aid, times_considered);
- XBT_DEBUG("to_string(%ld) is returning %s", aid, answer.c_str());
- return answer;
-}
-
-std::string ModelChecker::simcall_dot_label(aid_t aid, int times_considered)
-{
- std::string answer = simcall_to_string(MessageType::SIMCALL_DOT_LABEL, aid, times_considered);
- XBT_DEBUG("dot_label(%ld) is returning %s", aid, answer.c_str());
- return answer;
+ XBT_DEBUG("dot_label(%ld) is returning %s", aid, answer.value);
+ return answer.value;
}
void ModelChecker::finalize_app(bool terminate_asap)
void shutdown();
void resume();
void wait_for_requests();
- RemotePtr<simgrid::kernel::actor::SimcallObserver> handle_simcall(Transition const& transition);
+ Transition* handle_simcall(Transition const& transition, bool new_transition);
/* Interactions with the simcall observer */
bool simcall_is_visible(aid_t aid);
- bool requests_are_dependent(RemotePtr<kernel::actor::SimcallObserver> obs1,
- RemotePtr<kernel::actor::SimcallObserver> obs2) const;
- std::string simcall_to_string(aid_t aid, int times_considered);
std::string simcall_dot_label(aid_t aid, int times_considered);
XBT_ATTRIB_NORETURN void exit(int status);
#include "src/mc/remote/RemoteProcess.hpp"
#include "xbt/asserts.h"
+#include <sstream>
+
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_transition, mc, "Logging specific to MC transitions");
namespace simgrid {
namespace mc {
unsigned long Transition::executed_transitions_ = 0;
+unsigned long Transition::replayed_transitions_ = 0;
-std::string Transition::to_string() const
+std::string Transition::to_string(bool verbose)
{
xbt_assert(mc_model_checker != nullptr, "Must be called from MCer");
return textual_;
}
-const char* Transition::to_cstring() const
+const char* Transition::to_cstring(bool verbose)
{
xbt_assert(mc_model_checker != nullptr, "Must be called from MCer");
+ to_string();
return textual_.c_str();
}
void Transition::init(aid_t aid, int times_considered)
{
aid_ = aid;
times_considered_ = times_considered;
- textual_ = mc_model_checker->simcall_to_string(aid_, times_considered_);
}
-RemotePtr<simgrid::kernel::actor::SimcallObserver> Transition::replay() const
+void Transition::replay() const
{
- executed_transitions_++;
+ replayed_transitions_++;
- simgrid::mc::RemotePtr<simgrid::kernel::actor::SimcallObserver> res = mc_model_checker->handle_simcall(*this);
+ mc_model_checker->handle_simcall(*this, false);
mc_model_checker->wait_for_requests();
+}
+
+CommWaitTransition::CommWaitTransition(aid_t issuer, int times_considered, char* buffer)
+ : Transition(issuer, times_considered)
+{
+ std::stringstream stream(buffer);
+ stream >> timeout_ >> comm_ >> sender_ >> receiver_ >> mbox_ >> src_buff_ >> dst_buff_ >> size_;
+}
+std::string CommWaitTransition::to_string(bool verbose)
+{
+ textual_ = Transition::to_string(verbose);
+ textual_ += xbt::string_printf("[src=%ld -> dst=%ld, mbox=%u, tout=%f", sender_, receiver_, mbox_, timeout_);
+ if (verbose) {
+ textual_ += ", src_buff=" + xbt::string_printf("%p", src_buff_) + ", size=" + std::to_string(size_);
+ textual_ += ", dst_buff=" + xbt::string_printf("%p", dst_buff_);
+ }
+ textual_ += "]";
+ return textual_;
+}
+
+CommRecvTransition::CommRecvTransition(aid_t issuer, int times_considered, char* buffer)
+ : Transition(issuer, times_considered)
+{
+ std::stringstream stream(buffer);
+ stream >> mbox_ >> dst_buff_;
+}
+std::string CommRecvTransition::to_string(bool verbose)
+{
+ textual_ = xbt::string_printf("iRecv(recver=%ld mbox=%u", aid_, mbox_);
+ if (verbose)
+ textual_ += ", buff=" + xbt::string_printf("%p", dst_buff_);
+ textual_ += ")";
+ return textual_;
+}
+CommSendTransition::CommSendTransition(aid_t issuer, int times_considered, char* buffer)
+ : Transition(issuer, times_considered)
+{
+ std::stringstream stream(buffer);
+ stream >> mbox_ >> src_buff_ >> size_;
+}
+std::string CommSendTransition::to_string(bool verbose = false)
+{
+ textual_ = xbt::string_printf("iSend(sender=%ld mbox=%u", aid_, mbox_);
+ if (verbose)
+ textual_ += ", buff=" + xbt::string_printf("%p", src_buff_) + ", size=" + std::to_string(size_);
+ textual_ += ")";
+ return textual_;
+}
- return res;
+Transition* recv_transition(aid_t issuer, int times_considered, kernel::actor::SimcallObserver::Simcall simcall,
+ char* buffer)
+{
+ switch (simcall) {
+ case kernel::actor::SimcallObserver::Simcall::COMM_WAIT:
+ return new CommWaitTransition(issuer, times_considered, buffer);
+ case kernel::actor::SimcallObserver::Simcall::IRECV:
+ return new CommRecvTransition(issuer, times_considered, buffer);
+ case kernel::actor::SimcallObserver::Simcall::ISEND:
+ return new CommSendTransition(issuer, times_considered, buffer);
+ case kernel::actor::SimcallObserver::Simcall::UNKNOWN:
+ return new Transition(issuer, times_considered);
+ default:
+ xbt_die("recv_transition of type %s unimplemented", kernel::actor::SimcallObserver::to_c_str(simcall));
+ }
}
} // namespace mc
#define SIMGRID_MC_TRANSITION_HPP
#include "simgrid/forward.h" // aid_t
+#include "src/kernel/actor/SimcallObserver.hpp"
#include "src/mc/remote/RemotePtr.hpp"
#include <string>
*/
class Transition {
/* Textual representation of the transition, to display backtraces */
- std::string textual_ = "";
static unsigned long executed_transitions_;
+ static unsigned long replayed_transitions_;
+
+ friend State; // FIXME remove this once we have a proper class to handle the statistics
+
+protected:
+ std::string textual_ = "";
public:
aid_t aid_ = 0;
*/
int times_considered_ = 0;
+ Transition() = default;
+ Transition(aid_t issuer, int times_considered) : aid_(issuer), times_considered_(times_considered) {}
+
void init(aid_t aid, int times_considered);
- std::string to_string() const;
- const char* to_cstring() const;
+ virtual std::string to_string(bool verbose = false);
+ const char* to_cstring(bool verbose = false);
/* Moves the application toward a path that was already explored, but don't change the current transition */
- RemotePtr<simgrid::kernel::actor::SimcallObserver> replay() const;
+ void replay() const;
+
+ virtual bool depends(Transition* other) { return true; }
/* Returns the total amount of transitions executed so far (for statistics) */
static unsigned long get_executed_transitions() { return executed_transitions_; }
+ /* Returns the total amount of transitions replayed so far while backtracing (for statistics) */
+ static unsigned long get_replayed_transitions() { return replayed_transitions_; }
+};
+
+class CommWaitTransition : public Transition {
+ double timeout_;
+ uintptr_t comm_;
+ aid_t sender_;
+ aid_t receiver_;
+ unsigned mbox_;
+ unsigned char* src_buff_;
+ unsigned char* dst_buff_;
+ size_t size_;
+
+public:
+ CommWaitTransition(aid_t issuer, int times_considered, char* buffer);
+ std::string to_string(bool verbose) override;
};
+class CommRecvTransition : public Transition {
+ unsigned mbox_;
+ void* dst_buff_;
+
+public:
+ CommRecvTransition(aid_t issuer, int times_considered, char* buffer);
+ std::string to_string(bool verbose) override;
+};
+
+class CommSendTransition : public Transition {
+ unsigned mbox_;
+ void* src_buff_;
+ size_t size_;
+
+public:
+ CommSendTransition(aid_t issuer, int times_considered, char* buffer);
+ std::string to_string(bool verbose) override;
+};
+
+/** Make a new transition from serialized description */
+Transition* recv_transition(aid_t issuer, int times_considered, kernel::actor::SimcallObserver::Simcall simcall,
+ char* buffer);
+
} // namespace mc
} // namespace simgrid
return process_info;
}
-bool Api::requests_are_dependent(RemotePtr<kernel::actor::SimcallObserver> obs1,
- RemotePtr<kernel::actor::SimcallObserver> obs2) const
-{
- xbt_assert(mc_model_checker != nullptr, "Must be called from MCer");
-
- return mc_model_checker->requests_are_dependent(obs1, obs2);
-}
-
xbt::string const& Api::get_actor_host_name(smx_actor_t actor) const
{
if (mc_model_checker == nullptr)
void dump_record_path() const;
// SIMCALL APIs
- bool requests_are_dependent(RemotePtr<kernel::actor::SimcallObserver> obs1,
- RemotePtr<kernel::actor::SimcallObserver> obs2) const;
std::string request_get_dot_output(aid_t aid, int value) const;
smx_actor_t simcall_get_issuer(s_smx_simcall const* req) const;
RemotePtr<kernel::activity::MailboxImpl> get_mbox_remote_addr(smx_simcall_t const req) const;
}
/* Actually answer the request: let execute the selected request (MCed does one step) */
- auto remote_observer = state->execute_next(next);
+ state->set_transition(state->execute_next(next));
// If there are processes to interleave and the maximum depth has not been
// reached then perform one step of the exploration algorithm.
/* Create the new expanded state (copy the state of MCed into our MCer data) */
auto next_state = std::make_unique<State>();
- next_state->remote_observer_ = remote_observer;
if (_sg_mc_termination)
this->check_non_termination(next_state.get());
XBT_DEBUG("Simcall >>%s<< and >>%s<< with same issuer %ld", state->get_transition()->to_cstring(),
prev_state->get_transition()->to_cstring(), issuer_id);
break;
- } else if (api::get().requests_are_dependent(prev_state->remote_observer_, state->remote_observer_)) {
+ } else if (prev_state->get_transition()->depends(state->get_transition())) {
if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
XBT_DEBUG("Dependent Transitions:");
XBT_DEBUG(" %s (state=%ld)", prev_state->get_transition()->to_cstring(), prev_state->num_);
const char* current = data;
while (*current) {
- simgrid::mc::Transition item;
- int count = sscanf(current, "%ld/%d", &item.aid_, &item.times_considered_);
+ long aid;
+ int times_considered;
+ int count = sscanf(current, "%ld/%d", &aid, ×_considered);
+ simgrid::mc::Transition item(aid, times_considered);
if(count != 2 && count != 1)
throw std::invalid_argument("Could not parse record path");
{
const unsigned long maxpid = api::get().get_maxpid();
actor_states_.resize(maxpid);
+ transition_.reset(new Transition());
/* Stateful model checking */
if ((_sg_mc_checkpoint > 0 && (num_ % _sg_mc_checkpoint == 0)) || _sg_mc_termination) {
auto snapshot_ptr = api::get().take_snapshot(num_);
Transition* State::get_transition() const
{
- return const_cast<Transition*>(&this->transition_);
+ return transition_.get();
}
int State::next_transition() const
}
return -1;
}
-RemotePtr<simgrid::kernel::actor::SimcallObserver> State::execute_next(int next)
+Transition* State::execute_next(int next)
{
std::vector<ActorInformation>& actors = mc_model_checker->get_remote_process().actors();
actor_state->set_done();
}
- transition_.init(aid, times_considered);
+ transition_->init(aid, times_considered);
executed_req_ = actor->simcall_;
- XBT_DEBUG("Let's run actor %ld, going for transition %s", aid, transition_.to_cstring());
+ XBT_DEBUG("Let's run actor %ld, going for transition %s", aid, transition_->to_cstring());
- return transition_.replay();
+ Transition::executed_transitions_++;
+
+ Transition* res = mc_model_checker->handle_simcall(*transition_, true);
+ mc_model_checker->wait_for_requests();
+
+ return res;
}
void State::copy_incomplete_comm_pattern()
static long expended_states_; /* Count total amount of states, for stats */
/* Outgoing transition: what was the last transition that we took to leave this state? Useful for replay */
- Transition transition_;
+ std::unique_ptr<Transition> transition_;
public:
explicit State();
/** The simcall which was executed, going out of that state */
s_smx_simcall executed_req_;
- /** Observer of the transition leading to that sate */
- RemotePtr<kernel::actor::SimcallObserver> remote_observer_;
-
/** Snapshot of system state (if needed) */
std::shared_ptr<simgrid::mc::Snapshot> system_state_;
int next_transition() const;
/* Explore a new path */
- RemotePtr<simgrid::kernel::actor::SimcallObserver> execute_next(int next);
+ Transition* execute_next(int next);
std::size_t count_todo() const;
void mark_todo(aid_t actor) { this->actor_states_[actor].mark_todo(); }
Transition* get_transition() const;
+ void set_transition(Transition* t) { transition_.reset(t); }
/* Returns the total amount of states created so far (for statistics) */
static long get_expanded_states() { return expended_states_; }
actor->observer_stack_.push_back(observer);
}
// Finish the RPC from the server: we need to return a pointer to the observer, saved in a stable storage
- s_mc_message_simcall_execute_answer_t answer{MessageType::SIMCALL_EXECUTE_ANSWER, observer};
- XBT_DEBUG("send SIMCALL_EXECUTE_ANSWER(%p)", observer);
+ s_mc_message_simcall_execute_answer_t answer;
+ memset(&answer, 0, sizeof(answer));
+ answer.type = MessageType::SIMCALL_EXECUTE_ANSWER;
+ if (observer != nullptr)
+ observer->serialize(answer.simcall, answer.buffer);
+ XBT_DEBUG("send SIMCALL_EXECUTE_ANSWER(%s) ~> %s '%s'", actor->get_cname(),
+ simgrid::kernel::actor::SimcallObserver::to_c_str(answer.simcall), answer.buffer);
xbt_assert(channel_.send(answer) == 0, "Could not send response");
// The client may send some messages to the server while processing the transition
break;
}
- case MessageType::SIMCALL_TO_STRING: {
- assert_msg_size("SIMCALL_TO_STRING", s_mc_message_simcall_to_string_t);
- auto msg_simcall = (s_mc_message_simcall_to_string_t*)message_buffer.data();
- const kernel::actor::ActorImpl* actor = kernel::actor::ActorImpl::by_pid(msg_simcall->aid);
- xbt_assert(actor != nullptr, "Invalid pid %ld", msg_simcall->aid);
- xbt_assert(actor->simcall_.observer_, "The transition of %s has no observer", actor->get_cname());
- std::string value = "";
- if (actor->simcall_.observer_ != nullptr)
- value = actor->simcall_.observer_->to_string(msg_simcall->time_considered);
- else
- value = "[(" + std::to_string(actor->get_pid()) + ")" + actor->get_host()->get_cname() + " (" +
- actor->get_cname() + ")] " + SIMIX_simcall_name(actor->simcall_) + "(unknown?)";
-
- // Send result:
- s_mc_message_simcall_to_string_answer_t answer{MessageType::SIMCALL_TO_STRING_ANSWER, {0}};
- value.copy(answer.value, (sizeof answer.value) - 1); // last byte was set to '\0' by initialization above
- xbt_assert(channel_.send(answer) == 0, "Could not send response");
- break;
- }
-
case MessageType::SIMCALL_DOT_LABEL: {
assert_msg_size("SIMCALL_DOT_LABEL", s_mc_message_simcall_to_string_t);
auto msg_simcall = (s_mc_message_simcall_to_string_t*)message_buffer.data();
value = "UNIMPLEMENTED";
// Send result:
- s_mc_message_simcall_to_string_answer_t answer{MessageType::SIMCALL_TO_STRING_ANSWER, {0}};
+ s_mc_message_simcall_to_string_answer_t answer{MessageType::SIMCALL_DOT_LABEL_ANSWER, {0}};
value.copy(answer.value, (sizeof answer.value) - 1); // last byte was set to '\0' by initialization above
xbt_assert(channel_.send(answer) == 0, "Could not send response");
break;
}
- case MessageType::SIMCALLS_DEPENDENT: {
- assert_msg_size("SIMCALLS_DEPENDENT", s_mc_message_simcalls_dependent_t);
- auto msg_simcalls = (s_mc_message_simcalls_dependent_t*)message_buffer.data();
- auto* obs1 = msg_simcalls->obs1;
- auto* obs2 = msg_simcalls->obs2;
- bool res = true;
-
- if (obs1 != nullptr && obs2 != nullptr) {
- res = obs1->depends(obs2);
-
- XBT_DEBUG("return SIMCALLS_DEPENDENT(%s, %s) = %s", obs1->to_string(0).c_str(), obs2->to_string(0).c_str(),
- (res ? "true" : "false"));
- }
-
- // Send result:
- s_mc_message_simcalls_dependent_answer_t answer{MessageType::SIMCALLS_DEPENDENT_ANSWER, 0};
- answer.value = res;
- xbt_assert(channel_.send(answer) == 0, "Could not send response");
- break;
- }
-
case MessageType::ACTOR_ENABLED:
assert_msg_size("ACTOR_ENABLED", s_mc_message_actor_enabled_t);
handle_actor_enabled((s_mc_message_actor_enabled_t*)message_buffer.data());
#ifdef __cplusplus
+#include "src/kernel/actor/SimcallObserver.hpp"
+
#include "mc/datatypes.h"
#include "simgrid/forward.h" // aid_t
#include <array>
XBT_DECLARE_ENUM_CLASS(MessageType, NONE, INITIAL_ADDRESSES, CONTINUE, IGNORE_HEAP, UNIGNORE_HEAP, IGNORE_MEMORY,
STACK_REGION, REGISTER_SYMBOL, DEADLOCK_CHECK, DEADLOCK_CHECK_REPLY, WAITING, SIMCALL_EXECUTE,
- SIMCALL_EXECUTE_ANSWER, SIMCALL_IS_VISIBLE, SIMCALL_IS_VISIBLE_ANSWER, SIMCALL_TO_STRING,
- SIMCALL_TO_STRING_ANSWER, SIMCALLS_DEPENDENT, SIMCALLS_DEPENDENT_ANSWER, SIMCALL_DOT_LABEL,
- ASSERTION_FAILED, ACTOR_ENABLED, ACTOR_ENABLED_REPLY, FINALIZE);
+ SIMCALL_EXECUTE_ANSWER, SIMCALL_IS_VISIBLE, SIMCALL_IS_VISIBLE_ANSWER, SIMCALL_DOT_LABEL,
+ SIMCALL_DOT_LABEL_ANSWER, ASSERTION_FAILED, ACTOR_ENABLED, ACTOR_ENABLED_REPLY, FINALIZE);
} // namespace mc
} // namespace simgrid
};
struct s_mc_message_simcall_execute_answer_t {
simgrid::mc::MessageType type;
- simgrid::kernel::actor::SimcallObserver* observer;
+ simgrid::kernel::actor::SimcallObserver::Simcall simcall;
+ char buffer[2048];
};
struct s_mc_message_restore_t {
bool value;
};
-struct s_mc_message_simcall_to_string_t { // MessageType::SIMCALL_TO_STRING or MessageType::SIMCALL_DOT_LABEL
+struct s_mc_message_simcall_to_string_t { // MessageType::SIMCALL_DOT_LABEL
simgrid::mc::MessageType type;
aid_t aid;
int time_considered;
};
-struct s_mc_message_simcall_to_string_answer_t { // MessageType::SIMCALL_TO_STRING_ANSWER
+struct s_mc_message_simcall_to_string_answer_t { // MessageType::SIMCALL_DOT_LABEL_ANSWER
simgrid::mc::MessageType type;
char value[1024];
};
-struct s_mc_message_simcalls_dependent_t { // MessageType::SIMCALLS_DEPENDENT
- simgrid::mc::MessageType type;
- simgrid::kernel::actor::SimcallObserver* obs1;
- simgrid::kernel::actor::SimcallObserver* obs2;
-};
-struct s_mc_message_simcalls_dependent_answer_t { // MessageType::SIMCALLS_DEPENDENT_ANSWER
- simgrid::mc::MessageType type;
- bool value;
-};
-
#endif // __cplusplus
#endif
