mc_model_checker->get_remote_simulation().read(temp_synchro, remote(pattern->comm_addr));
const kernel::activity::CommImpl* synchro = temp_synchro.get_buffer();
- char* remote_name = mc_model_checker->get_remote_simulation().read<char*>(RemotePtr<char*>(
- (uint64_t)(synchro->get_mailbox() ? &synchro->get_mailbox()->name_ : &synchro->mbox_cpy->name_)));
+ // char* remote_name = mc_model_checker->get_remote_simulation().read<char*>(RemotePtr<char*>(
+ // (uint64_t)(synchro->get_mailbox() ? &synchro->get_mailbox()->name_ : &synchro->mbox_cpy->name_)));
pattern->rdv = mcapi::get().get_pattern_comm_rdv(pattern->comm_addr);
pattern->src_proc = mcapi::get().get_pattern_comm_src_proc(pattern->comm_addr);
pattern->src_host = mc_api::get().get_actor_host_name(issuer);
std::vector<std::string> trace;
for (auto const& state : stack_) {
smx_simcall_t req = &state->executed_req_;
- trace.push_back(request_to_string(req, state->transition_.argument_, RequestType::executed));
+ trace.push_back(mcapi::get().request_to_string(req, state->transition_.argument_, RequestType::executed));
}
return trace;
}
/* TODO : handle test and testany simcalls */
CallType call = MC_get_call_type(req);
- mc_model_checker->handle_simcall(state->transition_);
+ mcapi::get().handle_simcall(state->transition_);
MC_handle_comm_pattern(call, req, req_num, 1);
mcapi::get().mc_wait_for_requests();
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_api, mc, "Logging specific to MC Fasade APIs ");
+using Simcall = simgrid::simix::Simcall;
+
namespace simgrid {
namespace mc {
simgrid::mc::ActorState* procstate = &state->actor_states_[actor->get_pid()];
state->transition_.pid_ = -1;
state->transition_.argument_ = -1;
- state->executed_req_.call_ = SIMCALL_NONE;
+ state->executed_req_.call_ = Simcall::NONE;
if (not simgrid::mc::actor_is_enabled(actor))
return nullptr; // Not executable in the application
smx_simcall_t req = nullptr;
switch (actor->simcall_.call_) {
- case SIMCALL_COMM_WAITANY:
+ case Simcall::COMM_WAITANY:
state->transition_.argument_ = -1;
while (procstate->times_considered < simcall_comm_waitany__get__count(&actor->simcall_)) {
if (simgrid::mc::request_is_enabled_by_idx(&actor->simcall_, procstate->times_considered)) {
req = &actor->simcall_;
break;
- case SIMCALL_COMM_TESTANY: {
+ case Simcall::COMM_TESTANY: {
unsigned start_count = procstate->times_considered;
state->transition_.argument_ = -1;
while (procstate->times_considered < simcall_comm_testany__get__count(&actor->simcall_)) {
break;
}
- case SIMCALL_COMM_WAIT: {
+ case Simcall::COMM_WAIT: {
simgrid::mc::RemotePtr<simgrid::kernel::activity::CommImpl> remote_act =
remote(simcall_comm_wait__getraw__comm(&actor->simcall_));
simgrid::mc::Remote<simgrid::kernel::activity::CommImpl> temp_act;
break;
}
- case SIMCALL_MC_RANDOM: {
+ case Simcall::MC_RANDOM: {
int min_value = simcall_mc_random__get__min(&actor->simcall_);
state->transition_.argument_ = procstate->times_considered + min_value;
procstate->times_considered++;
/* 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: {
- state->internal_req_.call_ = SIMCALL_COMM_WAIT;
+ 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(
remote(simcall_comm_waitany__get__comms(req) + state->transition_.argument_));
break;
}
- case SIMCALL_COMM_TESTANY:
- state->internal_req_.call_ = SIMCALL_COMM_TEST;
+ case Simcall::COMM_TESTANY:
+ state->internal_req_.call_ = Simcall::COMM_TEST;
if (state->transition_.argument_ > 0) {
simgrid::kernel::activity::CommImpl* remote_comm = mc_model_checker->get_remote_simulation().read(
simcall_comm_test__set__result(&state->internal_req_, state->transition_.argument_);
break;
- case SIMCALL_COMM_WAIT:
+ 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());
simcall_comm_wait__set__comm(&state->internal_req_, state->internal_comm_.get_buffer());
break;
- case SIMCALL_COMM_TEST:
+ 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());
return simgrid::mc::request_get_dot_output(req, value);
}
-const char* mc_api::simix_simcall_name(e_smx_simcall_t kind) const
+const char* mc_api::simix_simcall_name(simgrid::simix::Simcall kind) const
{
return SIMIX_simcall_name(kind);
}
}
}
-
-/* Search an enabled transition for the given process.
- *
- * This can be seen as an iterator returning the next transition of the process.
- *
- * We only consider the processes that are both
- * - marked "to be interleaved" in their ActorState (controlled by the checker algorithm).
- * - which simcall can currently be executed (like a comm where the other partner is already known)
- * Once we returned the last enabled transition of a process, it is marked done.
- *
- * Things can get muddled with the WAITANY and TESTANY simcalls, that are rewritten on the fly to a bunch of WAIT
- * (resp TEST) transitions using the transition.argument field to remember what was the last returned sub-transition.
- */
-static inline smx_simcall_t MC_state_choose_request_for_process(simgrid::mc::State* state, smx_actor_t actor)
-{
- using simgrid::simix::Simcall;
-
- /* reset the outgoing transition */
- simgrid::mc::ActorState* procstate = &state->actor_states_[actor->get_pid()];
- state->transition_.pid_ = -1;
- state->transition_.argument_ = -1;
- state->executed_req_.call_ = Simcall::NONE;
-
- if (not simgrid::mc::actor_is_enabled(actor))
- return nullptr; // Not executable in the application
-
- smx_simcall_t req = nullptr;
- switch (actor->simcall_.call_) {
- case Simcall::COMM_WAITANY:
- state->transition_.argument_ = -1;
- while (procstate->times_considered < simcall_comm_waitany__get__count(&actor->simcall_)) {
- if (simgrid::mc::request_is_enabled_by_idx(&actor->simcall_, procstate->times_considered)) {
- state->transition_.argument_ = procstate->times_considered;
- ++procstate->times_considered;
- break;
- }
- ++procstate->times_considered;
- }
-
- if (procstate->times_considered >= simcall_comm_waitany__get__count(&actor->simcall_))
- procstate->set_done();
- if (state->transition_.argument_ != -1)
- req = &actor->simcall_;
- break;
-
- case Simcall::COMM_TESTANY: {
- unsigned start_count = procstate->times_considered;
- state->transition_.argument_ = -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)) {
- state->transition_.argument_ = procstate->times_considered;
- ++procstate->times_considered;
- break;
- }
- ++procstate->times_considered;
- }
-
- if (procstate->times_considered >= simcall_comm_testany__get__count(&actor->simcall_))
- procstate->set_done();
-
- if (state->transition_.argument_ != -1 || start_count == 0)
- req = &actor->simcall_;
-
- break;
- }
-
- case Simcall::COMM_WAIT: {
- simgrid::mc::RemotePtr<simgrid::kernel::activity::CommImpl> remote_act =
- remote(simcall_comm_wait__getraw__comm(&actor->simcall_));
- simgrid::mc::Remote<simgrid::kernel::activity::CommImpl> temp_act;
- mc_model_checker->get_remote_simulation().read(temp_act, remote_act);
- const simgrid::kernel::activity::CommImpl* act = temp_act.get_buffer();
- if (act->src_actor_.get() && act->dst_actor_.get())
- state->transition_.argument_ = 0; // OK
- else if (act->src_actor_.get() == nullptr && act->type_ == simgrid::kernel::activity::CommImpl::Type::READY &&
- act->detached())
- state->transition_.argument_ = 0; // OK
- else
- state->transition_.argument_ = -1; // timeout
- procstate->set_done();
- req = &actor->simcall_;
- break;
- }
-
- case Simcall::MC_RANDOM: {
- int min_value = simcall_mc_random__get__min(&actor->simcall_);
- state->transition_.argument_ = procstate->times_considered + min_value;
- procstate->times_considered++;
- if (state->transition_.argument_ == simcall_mc_random__get__max(&actor->simcall_))
- procstate->set_done();
- req = &actor->simcall_;
- break;
- }
-
- default:
- procstate->set_done();
- state->transition_.argument_ = 0;
- req = &actor->simcall_;
- break;
- }
- if (not req)
- return nullptr;
-
- state->transition_.pid_ = actor->get_pid();
- state->executed_req_ = *req;
- // Fetch the data of the request and translate it:
- state->internal_req_ = *req;
-
- /* 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: {
- state->internal_req_.call_ = Simcall::COMM_WAIT;
- simgrid::kernel::activity::CommImpl* remote_comm;
- remote_comm = mc_model_checker->get_remote_simulation().read(
- remote(simcall_comm_waitany__get__comms(req) + state->transition_.argument_));
- 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());
- simcall_comm_wait__set__timeout(&state->internal_req_, 0);
- break;
- }
-
- case Simcall::COMM_TESTANY:
- state->internal_req_.call_ = Simcall::COMM_TEST;
-
- if (state->transition_.argument_ > 0) {
- simgrid::kernel::activity::CommImpl* remote_comm = mc_model_checker->get_remote_simulation().read(
- remote(simcall_comm_testany__get__comms(req) + state->transition_.argument_));
- 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());
- simcall_comm_test__set__result(&state->internal_req_, state->transition_.argument_);
- 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());
- 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());
- break;
-
- default:
- /* No translation needed */
- break;
- }
-
- return req;
-}
-
-smx_simcall_t MC_state_choose_request(simgrid::mc::State* state)
-{
- for (auto& actor : mc_model_checker->get_remote_simulation().actors()) {
- /* Only consider the actors that were marked as interleaving by the checker algorithm */
- if (not state->actor_states_[actor.copy.get_buffer()->get_pid()].is_todo())
- continue;
-
- smx_simcall_t res = MC_state_choose_request_for_process(state, actor.copy.get_buffer());
- if (res)
- return res;
- }
- return nullptr;
-}
