-/* 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. */
/********** Static functions ***********/
-static e_mc_comm_pattern_difference_t compare_comm_pattern(simgrid::mc::PatternCommunication* comm1,
- simgrid::mc::PatternCommunication* comm2)
+static e_mc_comm_pattern_difference_t compare_comm_pattern(const simgrid::mc::PatternCommunication* comm1,
+ const simgrid::mc::PatternCommunication* comm2)
{
if(comm1->type != comm2->type)
return TYPE_DIFF;
}
static char* print_determinism_result(e_mc_comm_pattern_difference_t diff, int process,
- simgrid::mc::PatternCommunication* comm, unsigned int cursor)
+ const simgrid::mc::PatternCommunication* comm, unsigned int cursor)
{
char* type;
char* res;
{
// HACK, type punning
simgrid::mc::Remote<simgrid::kernel::activity::CommImpl> temp_comm;
- mc_model_checker->process().read(temp_comm, comm_addr);
- simgrid::kernel::activity::CommImpl* comm = temp_comm.get_buffer();
+ 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_));
}
}
namespace simgrid {
namespace mc {
-void CommunicationDeterminismChecker::deterministic_comm_pattern(int process, PatternCommunication* comm,
+void CommunicationDeterminismChecker::deterministic_comm_pattern(int process, const PatternCommunication* comm,
int backtracking)
{
if (not backtracking) {
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)));
- kernel::activity::CommImpl* synchro = static_cast<kernel::activity::CommImpl*>(temp_synchro.get_buffer());
+ 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)));
- kernel::activity::CommImpl* comm = temp_comm.get_buffer();
+ 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);
std::vector<PatternCommunication*>& incomplete_pattern = incomplete_communications_pattern[issuer];
auto current_comm_pattern =
std::find_if(begin(incomplete_pattern), end(incomplete_pattern),
- [&comm_addr](PatternCommunication* comm) { return remote(comm->comm_addr) == comm_addr; });
+ [&comm_addr](const PatternCommunication* comm) { return remote(comm->comm_addr) == comm_addr; });
if (current_comm_pattern == std::end(incomplete_pattern))
xbt_die("Corresponding communication not found!");
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;
}
break;
int req_num = state->transition_.argument_;
- smx_simcall_t saved_req = &state->executed_req_;
+ const s_smx_simcall* saved_req = &state->executed_req_;
xbt_assert(saved_req);
/* because we got a copy of the executed request, we have to fetch the
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();
}
