-/* Copyright (c) 2008-2019. The SimGrid Team. All rights reserved. */
+/* Copyright (c) 2008-2020. The SimGrid Team. All rights reserved. */
/* 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. */
{
// HACK, type punning
simgrid::mc::Remote<simgrid::kernel::activity::CommImpl> temp_comm;
- mc_model_checker->process().read(temp_comm, comm_addr);
+ mc_model_checker->get_remote_simulation().read(temp_comm, comm_addr);
const simgrid::kernel::activity::CommImpl* comm = temp_comm.get_buffer();
- smx_actor_t src_proc = mc_model_checker->process().resolve_actor(simgrid::mc::remote(comm->src_actor_.get()));
- smx_actor_t dst_proc = mc_model_checker->process().resolve_actor(simgrid::mc::remote(comm->dst_actor_.get()));
+ smx_actor_t src_proc =
+ mc_model_checker->get_remote_simulation().resolve_actor(simgrid::mc::remote(comm->src_actor_.get()));
+ smx_actor_t dst_proc =
+ mc_model_checker->get_remote_simulation().resolve_actor(simgrid::mc::remote(comm->dst_actor_.get()));
comm_pattern->src_proc = src_proc->get_pid();
comm_pattern->dst_proc = dst_proc->get_pid();
comm_pattern->src_host = MC_smx_actor_get_host_name(src_proc);
comm_pattern->dst_host = MC_smx_actor_get_host_name(dst_proc);
if (comm_pattern->data.size() == 0 && comm->src_buff_ != nullptr) {
size_t buff_size;
- mc_model_checker->process().read(&buff_size, remote(comm->dst_buff_size_));
+ mc_model_checker->get_remote_simulation().read(&buff_size, remote(comm->dst_buff_size_));
comm_pattern->data.resize(buff_size);
- mc_model_checker->process().read_bytes(comm_pattern->data.data(), comm_pattern->data.size(),
- remote(comm->src_buff_));
+ mc_model_checker->get_remote_simulation().read_bytes(comm_pattern->data.data(), comm_pattern->data.size(),
+ remote(comm->src_buff_));
}
}
pattern->comm_addr = static_cast<kernel::activity::CommImpl*>(simcall_comm_isend__getraw__result(request));
Remote<kernel::activity::CommImpl> temp_synchro;
- mc_model_checker->process().read(temp_synchro,
- remote(static_cast<kernel::activity::CommImpl*>(pattern->comm_addr)));
+ mc_model_checker->get_remote_simulation().read(
+ temp_synchro, remote(static_cast<kernel::activity::CommImpl*>(pattern->comm_addr)));
const kernel::activity::CommImpl* synchro = static_cast<kernel::activity::CommImpl*>(temp_synchro.get_buffer());
- char* remote_name = mc_model_checker->process().read<char*>(RemotePtr<char*>(
+ 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 = mc_model_checker->process().read_string(RemotePtr<char>(remote_name));
- pattern->src_proc = mc_model_checker->process().resolve_actor(mc::remote(synchro->src_actor_.get()))->get_pid();
+ pattern->rdv = mc_model_checker->get_remote_simulation().read_string(RemotePtr<char>(remote_name));
+ pattern->src_proc =
+ mc_model_checker->get_remote_simulation().resolve_actor(mc::remote(synchro->src_actor_.get()))->get_pid();
pattern->src_host = MC_smx_actor_get_host_name(issuer);
#if HAVE_SMPI
simgrid::smpi::Request mpi_request;
- mc_model_checker->process().read(&mpi_request,
- remote(static_cast<smpi::Request*>(simcall_comm_isend__get__data(request))));
+ mc_model_checker->get_remote_simulation().read(
+ &mpi_request, remote(static_cast<smpi::Request*>(simcall_comm_isend__get__data(request))));
pattern->tag = mpi_request.tag();
#endif
if (synchro->src_buff_ != nullptr) {
pattern->data.resize(synchro->src_buff_size_);
- mc_model_checker->process().read_bytes(pattern->data.data(), pattern->data.size(), remote(synchro->src_buff_));
+ mc_model_checker->get_remote_simulation().read_bytes(pattern->data.data(), pattern->data.size(),
+ remote(synchro->src_buff_));
}
#if HAVE_SMPI
if(mpi_request.detached()){
#if HAVE_SMPI
smpi::Request mpi_request;
- mc_model_checker->process().read(&mpi_request,
- remote(static_cast<smpi::Request*>(simcall_comm_irecv__get__data(request))));
+ mc_model_checker->get_remote_simulation().read(
+ &mpi_request, remote(static_cast<smpi::Request*>(simcall_comm_irecv__get__data(request))));
pattern->tag = mpi_request.tag();
#endif
Remote<kernel::activity::CommImpl> temp_comm;
- mc_model_checker->process().read(temp_comm, remote(static_cast<kernel::activity::CommImpl*>(pattern->comm_addr)));
+ mc_model_checker->get_remote_simulation().read(
+ temp_comm, remote(static_cast<kernel::activity::CommImpl*>(pattern->comm_addr)));
const kernel::activity::CommImpl* comm = temp_comm.get_buffer();
char* remote_name;
- mc_model_checker->process().read(
+ mc_model_checker->get_remote_simulation().read(
&remote_name, remote(comm->get_mailbox() ? &xbt::string::to_string_data(comm->get_mailbox()->name_).data
: &xbt::string::to_string_data(comm->mbox_cpy->name_).data));
- pattern->rdv = mc_model_checker->process().read_string(RemotePtr<char>(remote_name));
- pattern->dst_proc = mc_model_checker->process().resolve_actor(mc::remote(comm->dst_actor_.get()))->get_pid();
+ pattern->rdv = mc_model_checker->get_remote_simulation().read_string(RemotePtr<char>(remote_name));
+ pattern->dst_proc =
+ mc_model_checker->get_remote_simulation().resolve_actor(mc::remote(comm->dst_actor_.get()))->get_pid();
pattern->dst_host = MC_smx_actor_get_host_name(issuer);
} else
xbt_die("Unexpected call_type %i", (int) call_type);
XBT_DEBUG("********* Start communication determinism verification *********");
/* Get an enabled actor and insert it in the interleave set of the initial state */
- for (auto& actor : mc_model_checker->process().actors())
+ for (auto& actor : mc_model_checker->get_remote_simulation().actors())
if (mc::actor_is_enabled(actor.copy.get_buffer()))
initial_state->add_interleaving_set(actor.copy.get_buffer());
/* Intermediate backtracking */
State* last_state = stack_.back().get();
if (last_state->system_state_) {
- last_state->system_state_->restore(&mc_model_checker->process());
+ last_state->system_state_->restore(&mc_model_checker->get_remote_simulation());
MC_restore_communications_pattern(last_state);
return;
}
real one, pointed by the request field of the issuer process */
const smx_actor_t issuer = MC_smx_simcall_get_issuer(saved_req);
- smx_simcall_t req = &issuer->simcall;
+ smx_simcall_t req = &issuer->simcall_;
/* TODO : handle test and testany simcalls */
e_mc_call_type_t call = MC_get_call_type(req);
if (visited_state == nullptr) {
/* Get enabled actors and insert them in the interleave set of the next state */
- for (auto& actor : mc_model_checker->process().actors())
+ for (auto& actor : mc_model_checker->get_remote_simulation().actors())
if (simgrid::mc::actor_is_enabled(actor.copy.get_buffer()))
next_state->add_interleaving_set(actor.copy.get_buffer());
mc::session->initialize();
this->prepare();
-
this->real_run();
}