#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"
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:
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
}
}
-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;
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()));
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";
}
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;
- case Simcall::MUTEX_TRYLOCK:
- label = "[" + get_actor_dot_label(issuer) + "] Mutex TRYLOCK";
- break;
-
case Simcall::MUTEX_LOCK:
label = "[" + get_actor_dot_label(issuer) + "] Mutex LOCK";
break;
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);
}
