#include "src/kernel/activity/MailboxImpl.hpp"
#include "src/kernel/activity/MutexImpl.hpp"
#include "src/mc/Session.hpp"
-#include "src/mc/checker/SimcallInspector.hpp"
+#include "src/mc/checker/SimcallObserver.hpp"
#include "src/mc/mc_comm_pattern.hpp"
+#include "src/mc/mc_exit.hpp"
#include "src/mc/mc_pattern.hpp"
#include "src/mc/mc_private.hpp"
-#include "src/mc/mc_smx.hpp"
-
#include "src/mc/remote/RemoteSimulation.hpp"
+
#include <xbt/asserts.h>
#include <xbt/log.h>
#include "simgrid/s4u/Host.hpp"
return nullptr; // Not executable in the application
smx_simcall_t req = nullptr;
- if (actor->simcall_.inspector_ != nullptr) {
+ if (actor->simcall_.observer_ != nullptr) {
state->transition_.times_considered_ = procstate->times_considered;
procstate->times_considered++;
if (actor->simcall_.mc_max_consider_ <= procstate->times_considered)
req = &actor->simcall_;
break;
- case Simcall::COMM_TESTANY: {
- unsigned start_count = procstate->times_considered;
+ case Simcall::COMM_TESTANY:
state->transition_.times_considered_ = -1;
while (procstate->times_considered < simcall_comm_testany__get__count(&actor->simcall_)) {
if (simgrid::mc::request_is_enabled_by_idx(&actor->simcall_, procstate->times_considered)) {
if (procstate->times_considered >= simcall_comm_testany__get__count(&actor->simcall_))
procstate->set_done();
-
- if (state->transition_.times_considered_ != -1 || start_count == 0)
+ if (state->transition_.times_considered_ != -1)
req = &actor->simcall_;
-
break;
- }
case Simcall::COMM_WAIT: {
simgrid::mc::RemotePtr<simgrid::kernel::activity::CommImpl> remote_act =
state->executed_req_ = *req;
// Fetch the data of the request and translate it:
state->internal_req_ = *req;
+ simgrid::kernel::activity::CommImpl* chosen_comm;
+ simgrid::mc::Remote<simgrid::kernel::activity::CommImpl> remote_comm;
/* The waitany and testany request are transformed into a wait or test request over the corresponding communication
* action so it can be treated later by the dependence function. */
switch (req->call_) {
- case Simcall::COMM_WAITANY: {
+ case Simcall::COMM_WAITANY:
state->internal_req_.call_ = Simcall::COMM_WAIT;
- simgrid::kernel::activity::CommImpl* remote_comm;
- remote_comm = mc_model_checker->get_remote_simulation().read(
+ chosen_comm = mc_model_checker->get_remote_simulation().read(
remote(simcall_comm_waitany__get__comms(req) + state->transition_.times_considered_));
- mc_model_checker->get_remote_simulation().read(state->internal_comm_, remote(remote_comm));
- simcall_comm_wait__set__comm(&state->internal_req_, state->internal_comm_.get_buffer());
+
+ mc_model_checker->get_remote_simulation().read(remote_comm, remote(chosen_comm));
+ simcall_comm_wait__set__comm(&state->internal_req_, remote_comm.get_buffer());
simcall_comm_wait__set__timeout(&state->internal_req_, 0);
break;
- }
case Simcall::COMM_TESTANY:
state->internal_req_.call_ = Simcall::COMM_TEST;
+ chosen_comm = mc_model_checker->get_remote_simulation().read(
+ remote(simcall_comm_testany__get__comms(req) + state->transition_.times_considered_));
- if (state->transition_.times_considered_ > 0) {
- simgrid::kernel::activity::CommImpl* remote_comm = mc_model_checker->get_remote_simulation().read(
- remote(simcall_comm_testany__get__comms(req) + state->transition_.times_considered_));
- mc_model_checker->get_remote_simulation().read(state->internal_comm_, remote(remote_comm));
- }
-
- simcall_comm_test__set__comm(&state->internal_req_, state->internal_comm_.get_buffer());
+ mc_model_checker->get_remote_simulation().read(remote_comm, remote(chosen_comm));
+ simcall_comm_test__set__comm(&state->internal_req_, remote_comm.get_buffer());
simcall_comm_test__set__result(&state->internal_req_, state->transition_.times_considered_);
break;
case Simcall::COMM_WAIT:
- mc_model_checker->get_remote_simulation().read_bytes(&state->internal_comm_, sizeof(state->internal_comm_),
- remote(simcall_comm_wait__getraw__comm(req)));
- simcall_comm_wait__set__comm(&state->executed_req_, state->internal_comm_.get_buffer());
+ chosen_comm = simcall_comm_wait__getraw__comm(req);
+ mc_model_checker->get_remote_simulation().read(state->internal_comm_, remote(chosen_comm));
simcall_comm_wait__set__comm(&state->internal_req_, state->internal_comm_.get_buffer());
break;
case Simcall::COMM_TEST:
- mc_model_checker->get_remote_simulation().read_bytes(&state->internal_comm_, sizeof(state->internal_comm_),
- remote(simcall_comm_test__getraw__comm(req)));
- simcall_comm_test__set__comm(&state->executed_req_, state->internal_comm_.get_buffer());
- simcall_comm_test__set__comm(&state->internal_req_, state->internal_comm_.get_buffer());
+ chosen_comm = simcall_comm_test__getraw__comm(req);
+ mc_model_checker->get_remote_simulation().read(remote_comm, remote(chosen_comm));
+ simcall_comm_test__set__comm(&state->internal_req_, remote_comm.get_buffer());
break;
default:
}
std::string Api::get_actor_string(smx_actor_t actor) const
-{
- std::string res = "(" + std::to_string(actor->get_pid()) + ")";
- if (actor->get_host())
- res += get_actor_host_name(actor);
- return res;
-}
-
-std::string Api::get_actor_string2(smx_actor_t actor) const
{
std::string res;
if (actor) {
return res;
}
+std::string Api::get_actor_dot_label(smx_actor_t actor) const
+{
+ std::string res = "(" + std::to_string(actor->get_pid()) + ")";
+ if (actor->get_host())
+ res += get_actor_host_name(actor);
+ return res;
+}
+
void Api::initialize(char** argv) const
{
simgrid::mc::session = new simgrid::mc::Session([argv] {
unsigned long Api::get_maxpid() const
{
- return MC_smx_get_maxpid();
+ static const char* name = nullptr;
+ if (not name) {
+ name = "simgrid::kernel::actor::maxpid";
+ if (mc_model_checker->get_remote_simulation().find_variable(name) == nullptr)
+ name = "maxpid"; // We seem to miss the namespaces when compiling with GCC
+ }
+ unsigned long maxpid;
+ mc_model_checker->get_remote_simulation().read_variable(name, &maxpid, sizeof(maxpid));
+ return maxpid;
}
int Api::get_actors_size() const
return mc_model_checker->executed_transitions;
}
-bool Api::mc_check_deadlock() const
-{
- return mc_model_checker->checkDeadlock();
-}
-
-void Api::mc_show_deadlock() const
+void Api::mc_check_deadlock() const
{
- MC_show_deadlock();
+ if (mc_model_checker->checkDeadlock()) {
+ MC_show_deadlock();
+ throw DeadlockError();
+ }
}
/** Get the issuer of a simcall (`req->issuer`)
return nullptr;
}
-std::list<transition_detail_t> Api::get_enabled_transitions(simgrid::mc::State* state)
+std::list<transition_detail_t> Api::get_enabled_transitions(simgrid::mc::State* state) const
{
std::list<transition_detail_t> tr_list{};
if (not simgrid::mc::actor_is_enabled(actor_impl))
continue;
- transition_detail_t transition = std::unique_ptr<s_transition_detail>(new s_transition_detail());
- Simcall simcall_call = actor_impl->simcall_.call_;
- smx_simcall_t simcall = &actor_impl->simcall_;
- transition->call_ = simcall_call;
+ auto transition = std::make_unique<s_transition_detail>();
+ Simcall simcall_call = actor_impl->simcall_.call_;
+ smx_simcall_t simcall = &actor_impl->simcall_;
+ transition->call_ = simcall_call;
switch (simcall_call) {
case Simcall::COMM_ISEND:
case Simcall::COMM_IRECV:
}
}
-std::string Api::request_to_string(smx_simcall_t req, int value, RequestType request_type) const
+std::string Api::request_to_string(smx_simcall_t req, int value) const
{
xbt_assert(mc_model_checker != nullptr, "Must be called from MCer");
- bool use_remote_comm = true;
- switch (request_type) {
- case simgrid::mc::RequestType::simix:
- use_remote_comm = true;
- break;
- case simgrid::mc::RequestType::executed:
- case simgrid::mc::RequestType::internal:
- use_remote_comm = false;
- break;
- default:
- THROW_IMPOSSIBLE;
- }
-
std::string type;
std::string args;
smx_actor_t issuer = simcall_get_issuer(req);
- if (issuer->simcall_.inspector_ != nullptr)
+ if (issuer->simcall_.observer_ != nullptr)
return mc_model_checker->simcall_to_string(issuer->get_pid(), value);
switch (req->call_) {
case Simcall::COMM_ISEND:
type = "iSend";
- args = "src=" + get_actor_string2(issuer);
+ args = "src=" + get_actor_string(issuer);
args += ", buff=" + pointer_to_string(simcall_comm_isend__get__src_buff(req));
args += ", size=" + buff_size_to_string(simcall_comm_isend__get__src_buff_size(req));
break;
mc_model_checker->get_remote_simulation().read_bytes(&size, sizeof(size), remote(remote_size));
type = "iRecv";
- args = "dst=" + get_actor_string2(issuer);
+ args = "dst=" + get_actor_string(issuer);
args += ", buff=" + pointer_to_string(simcall_comm_irecv__get__dst_buff(req));
args += ", size=" + buff_size_to_string(size);
break;
simgrid::mc::Remote<simgrid::kernel::activity::CommImpl> temp_synchro;
const simgrid::kernel::activity::CommImpl* act;
- if (use_remote_comm) {
- mc_model_checker->get_remote_simulation().read(temp_synchro, remote(remote_act));
- act = temp_synchro.get_buffer();
- } else
- act = remote_act;
+ mc_model_checker->get_remote_simulation().read(temp_synchro, remote(remote_act));
+ act = temp_synchro.get_buffer();
smx_actor_t src_proc =
mc_model_checker->get_remote_simulation().resolve_actor(simgrid::mc::remote(act->src_actor_.get()));
smx_actor_t dst_proc =
mc_model_checker->get_remote_simulation().resolve_actor(simgrid::mc::remote(act->dst_actor_.get()));
args = "comm=" + pointer_to_string(remote_act);
- args += " [" + get_actor_string2(src_proc) + "-> " + get_actor_string2(dst_proc) + "]";
+ args += " [" + get_actor_string(src_proc) + "-> " + get_actor_string(dst_proc) + "]";
}
break;
}
simgrid::kernel::activity::CommImpl* remote_act = simcall_comm_test__getraw__comm(req);
simgrid::mc::Remote<simgrid::kernel::activity::CommImpl> temp_synchro;
const simgrid::kernel::activity::CommImpl* act;
- if (use_remote_comm) {
- mc_model_checker->get_remote_simulation().read(temp_synchro, remote(remote_act));
- act = temp_synchro.get_buffer();
- } else
- act = remote_act;
+ mc_model_checker->get_remote_simulation().read(temp_synchro, remote(remote_act));
+ act = temp_synchro.get_buffer();
if (act->src_actor_.get() == nullptr || act->dst_actor_.get() == nullptr) {
type = "Test FALSE";
smx_actor_t dst_proc =
mc_model_checker->get_remote_simulation().resolve_actor(simgrid::mc::remote(act->dst_actor_.get()));
args = "comm=" + pointer_to_string(remote_act);
- args += " [" + get_actor_string2(src_proc) + " -> " + get_actor_string2(dst_proc) + "]";
+ args += " [" + get_actor_string(src_proc) + " -> " + get_actor_string(dst_proc) + "]";
}
break;
}
}
break;
- case Simcall::MUTEX_TRYLOCK:
case Simcall::MUTEX_LOCK: {
- if (req->call_ == Simcall::MUTEX_LOCK)
- type = "Mutex LOCK";
- else
- type = "Mutex TRYLOCK";
-
+ type = "Mutex LOCK";
simgrid::mc::Remote<simgrid::kernel::activity::MutexImpl> mutex;
mc_model_checker->get_remote_simulation().read_bytes(mutex.get_buffer(), sizeof(mutex),
- remote(req->call_ == Simcall::MUTEX_LOCK
- ? simcall_mutex_lock__get__mutex(req)
- : simcall_mutex_trylock__get__mutex(req)));
+ remote(simcall_mutex_lock__get__mutex(req)));
args = "locked = " + std::to_string(mutex.get_buffer()->is_locked()) + ", owner = ";
if (mutex.get_buffer()->get_owner() != nullptr)
args += std::to_string(mc_model_checker->get_remote_simulation()
break;
}
- return "[" + get_actor_string2(issuer) + "] " + type + "(" + args + ")";
+ return "[" + get_actor_string(issuer) + "] " + type + "(" + args + ")";
}
std::string Api::request_get_dot_output(smx_simcall_t req, int value) const
std::string label;
- if (req->inspector_ != nullptr) {
+ if (req->observer_ != nullptr) {
label = mc_model_checker->simcall_dot_label(issuer->get_pid(), value);
} else
switch (req->call_) {
case Simcall::COMM_ISEND:
- label = "[" + get_actor_string(issuer) + "] iSend";
+ label = "[" + get_actor_dot_label(issuer) + "] iSend";
break;
case Simcall::COMM_IRECV:
- label = "[" + get_actor_string(issuer) + "] iRecv";
+ label = "[" + get_actor_dot_label(issuer) + "] iRecv";
break;
case Simcall::COMM_WAIT:
if (value == -1) {
- label = "[" + get_actor_string(issuer) + "] WaitTimeout";
+ label = "[" + get_actor_dot_label(issuer) + "] WaitTimeout";
} else {
kernel::activity::ActivityImpl* remote_act = simcall_comm_wait__getraw__comm(req);
Remote<kernel::activity::CommImpl> temp_comm;
mc_model_checker->get_remote_simulation().resolve_actor(mc::remote(comm->src_actor_.get()));
const kernel::actor::ActorImpl* dst_proc =
mc_model_checker->get_remote_simulation().resolve_actor(mc::remote(comm->dst_actor_.get()));
- label = "[" + get_actor_string(issuer) + "] Wait";
+ label = "[" + get_actor_dot_label(issuer) + "] Wait";
label += " [(" + std::to_string(src_proc ? src_proc->get_pid() : 0) + ")";
label += "->(" + std::to_string(dst_proc ? dst_proc->get_pid() : 0) + ")]";
}
remote(static_cast<kernel::activity::CommImpl*>(remote_act)));
const kernel::activity::CommImpl* comm = temp_comm.get_buffer();
if (comm->src_actor_.get() == nullptr || comm->dst_actor_.get() == nullptr) {
- label = "[" + get_actor_string(issuer) + "] Test FALSE";
+ label = "[" + get_actor_dot_label(issuer) + "] Test FALSE";
} else {
- label = "[" + get_actor_string(issuer) + "] Test TRUE";
+ label = "[" + get_actor_dot_label(issuer) + "] Test TRUE";
}
break;
}
case Simcall::COMM_WAITANY:
- label = "[" + get_actor_string(issuer) + "] WaitAny";
+ label = "[" + get_actor_dot_label(issuer) + "] WaitAny";
label += xbt::string_printf(" [%d of %zu]", value + 1, simcall_comm_waitany__get__count(req));
break;
case Simcall::COMM_TESTANY:
if (value == -1) {
- label = "[" + get_actor_string(issuer) + "] TestAny FALSE";
+ label = "[" + get_actor_dot_label(issuer) + "] TestAny FALSE";
} else {
- label = "[" + get_actor_string(issuer) + "] TestAny TRUE";
+ label = "[" + get_actor_dot_label(issuer) + "] TestAny TRUE";
label += xbt::string_printf(" [%d of %zu]", value + 1, simcall_comm_testany__get__count(req));
}
break;
- case Simcall::MUTEX_TRYLOCK:
- label = "[" + get_actor_string(issuer) + "] Mutex TRYLOCK";
- break;
-
case Simcall::MUTEX_LOCK:
- label = "[" + get_actor_string(issuer) + "] Mutex LOCK";
+ label = "[" + get_actor_dot_label(issuer) + "] Mutex LOCK";
break;
default:
void Api::execute(Transition& transition, smx_simcall_t simcall) const
{
/* FIXME: once all simcalls have observers, kill the simcall parameter and use mc_model_checker->simcall_to_string() */
- transition.textual = request_to_string(simcall, transition.times_considered_, RequestType::executed);
+ transition.textual = request_to_string(simcall, transition.times_considered_);
session->execute(transition);
}
