X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/2a15998fc166600c0a52d616a0d4c09bf873cf83..2ccf9c22b2e9dee40858cb70a44763f4084e15da:/src/mc/checker/CommunicationDeterminismChecker.cpp diff --git a/src/mc/checker/CommunicationDeterminismChecker.cpp b/src/mc/checker/CommunicationDeterminismChecker.cpp index 41d59622c3..7d112063e6 100644 --- a/src/mc/checker/CommunicationDeterminismChecker.cpp +++ b/src/mc/checker/CommunicationDeterminismChecker.cpp @@ -1,4 +1,4 @@ -/* 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. */ @@ -29,8 +29,8 @@ std::vector> incomplete_communic /********** 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; @@ -50,7 +50,7 @@ static e_mc_comm_pattern_difference_t compare_comm_pattern(simgrid::mc::PatternC } 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; @@ -95,28 +95,30 @@ static void update_comm_pattern(simgrid::mc::PatternCommunication* comm_pattern, { // HACK, type punning simgrid::mc::Remote 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) { @@ -183,26 +185,28 @@ void CommunicationDeterminismChecker::get_comm_pattern(smx_simcall_t request, e_ pattern->comm_addr = static_cast(simcall_comm_isend__getraw__result(request)); Remote temp_synchro; - mc_model_checker->process().read(temp_synchro, - remote(static_cast(pattern->comm_addr))); - kernel::activity::CommImpl* synchro = static_cast(temp_synchro.get_buffer()); + mc_model_checker->get_remote_simulation().read( + temp_synchro, remote(static_cast(pattern->comm_addr))); + const kernel::activity::CommImpl* synchro = static_cast(temp_synchro.get_buffer()); - char* remote_name = mc_model_checker->process().read(RemotePtr( + char* remote_name = mc_model_checker->get_remote_simulation().read(RemotePtr( (uint64_t)(synchro->get_mailbox() ? &synchro->get_mailbox()->name_ : &synchro->mbox_cpy->name_))); - pattern->rdv = mc_model_checker->process().read_string(RemotePtr(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(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(simcall_comm_isend__get__data(request)))); + mc_model_checker->get_remote_simulation().read( + &mpi_request, remote(static_cast(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()){ @@ -223,21 +227,23 @@ void CommunicationDeterminismChecker::get_comm_pattern(smx_simcall_t request, e_ #if HAVE_SMPI smpi::Request mpi_request; - mc_model_checker->process().read(&mpi_request, - remote(static_cast(simcall_comm_irecv__get__data(request)))); + mc_model_checker->get_remote_simulation().read( + &mpi_request, remote(static_cast(simcall_comm_irecv__get__data(request)))); pattern->tag = mpi_request.tag(); #endif Remote temp_comm; - mc_model_checker->process().read(temp_comm, remote(static_cast(pattern->comm_addr))); - kernel::activity::CommImpl* comm = temp_comm.get_buffer(); + mc_model_checker->get_remote_simulation().read( + temp_comm, remote(static_cast(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(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(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); @@ -253,7 +259,7 @@ void CommunicationDeterminismChecker::complete_comm_pattern(RemotePtr& 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!"); @@ -334,7 +340,7 @@ void CommunicationDeterminismChecker::prepare() 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()); @@ -357,7 +363,7 @@ void CommunicationDeterminismChecker::restoreState() /* 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; } @@ -379,14 +385,14 @@ void CommunicationDeterminismChecker::restoreState() 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); @@ -461,7 +467,7 @@ void CommunicationDeterminismChecker::real_run() 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()); @@ -525,7 +531,6 @@ void CommunicationDeterminismChecker::run() mc::session->initialize(); this->prepare(); - this->real_run(); }