X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/22e6546d2c6f14864cc93c4ed1470d8e8c1e2d95..2cf13759ba1696d88f5ff86afee5324f30ccdbfc:/src/mc/checker/CommunicationDeterminismChecker.cpp diff --git a/src/mc/checker/CommunicationDeterminismChecker.cpp b/src/mc/checker/CommunicationDeterminismChecker.cpp index 955a2f2cf1..f9e5fb1853 100644 --- a/src/mc/checker/CommunicationDeterminismChecker.cpp +++ b/src/mc/checker/CommunicationDeterminismChecker.cpp @@ -1,18 +1,11 @@ -/* Copyright (c) 2008-2017. The SimGrid Team. All rights reserved. */ +/* Copyright (c) 2008-2019. 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. */ -#include - -#include -#include -#include -#include - -#include "src/mc/Transition.hpp" -#include "src/mc/VisitedState.hpp" #include "src/mc/checker/CommunicationDeterminismChecker.hpp" +#include "src/kernel/activity/MailboxImpl.hpp" +#include "src/mc/VisitedState.hpp" #include "src/mc/mc_exit.hpp" #include "src/mc/mc_private.hpp" #include "src/mc/mc_record.hpp" @@ -21,7 +14,11 @@ #include "src/mc/mc_state.hpp" #include "src/mc/remote/Client.hpp" +#if HAVE_SMPI #include "smpi_request.hpp" +#endif + +#include using simgrid::mc::remote; @@ -103,18 +100,18 @@ static void update_comm_pattern(simgrid::mc::PatternCommunication* comm_pattern, mc_model_checker->process().read(temp_comm, comm_addr); simgrid::kernel::activity::CommImpl* comm = temp_comm.getBuffer(); - smx_actor_t src_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(comm->src_proc)); - smx_actor_t dst_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(comm->dst_proc)); - comm_pattern->src_proc = src_proc->pid; - comm_pattern->dst_proc = dst_proc->pid; + smx_actor_t src_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(comm->src_actor_.get())); + smx_actor_t dst_proc = mc_model_checker->process().resolveActor(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) { + 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->process().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)); + remote(comm->src_buff_)); } } @@ -175,8 +172,8 @@ void CommunicationDeterminismChecker::get_comm_pattern(xbt_dynar_t list, smx_sim { const smx_actor_t issuer = MC_smx_simcall_get_issuer(request); simgrid::mc::PatternCommunicationList* initial_pattern = - xbt_dynar_get_as(initial_communications_pattern, issuer->pid, simgrid::mc::PatternCommunicationList*); - xbt_dynar_t incomplete_pattern = xbt_dynar_get_as(incomplete_communications_pattern, issuer->pid, xbt_dynar_t); + xbt_dynar_get_as(initial_communications_pattern, issuer->get_pid(), simgrid::mc::PatternCommunicationList*); + xbt_dynar_t incomplete_pattern = xbt_dynar_get_as(incomplete_communications_pattern, issuer->get_pid(), xbt_dynar_t); std::unique_ptr pattern = std::unique_ptr(new simgrid::mc::PatternCommunication()); @@ -194,19 +191,23 @@ void CommunicationDeterminismChecker::get_comm_pattern(xbt_dynar_t list, smx_sim static_cast(temp_synchro.getBuffer()); char* remote_name = mc_model_checker->process().read( - (std::uint64_t)(synchro->mbox ? &synchro->mbox->name_ : &synchro->mbox_cpy->name_)); - pattern->rdv = mc_model_checker->process().read_string(remote_name); - pattern->src_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(synchro->src_proc))->pid; + RemotePtr((uint64_t)(synchro->mbox ? &synchro->mbox->name_ : &synchro->mbox_cpy->name_))); + pattern->rdv = mc_model_checker->process().read_string(RemotePtr(remote_name)); + pattern->src_proc = + mc_model_checker->process().resolveActor(simgrid::mc::remote(synchro->src_actor_.get()))->get_pid(); pattern->src_host = MC_smx_actor_get_host_name(issuer); - simgrid::smpi::Request mpi_request = - mc_model_checker->process().read((std::uint64_t)simcall_comm_isend__get__data(request)); +#if HAVE_SMPI + simgrid::smpi::Request mpi_request = mc_model_checker->process().read( + RemotePtr((std::uint64_t)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)); + 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_)); } +#if HAVE_SMPI if(mpi_request.detached()){ if (not this->initial_communications_pattern_done) { /* Store comm pattern */ @@ -221,14 +222,17 @@ void CommunicationDeterminismChecker::get_comm_pattern(xbt_dynar_t list, smx_sim } return; } +#endif } else if (call_type == MC_CALL_TYPE_RECV) { pattern->type = simgrid::mc::PatternCommunicationType::receive; pattern->comm_addr = static_cast(simcall_comm_irecv__getraw__result(request)); +#if HAVE_SMPI simgrid::smpi::Request mpi_request; mc_model_checker->process().read(&mpi_request, remote((simgrid::smpi::Request*)simcall_comm_irecv__get__data(request))); pattern->tag = mpi_request.tag(); +#endif simgrid::mc::Remote temp_comm; mc_model_checker->process().read(temp_comm, @@ -239,14 +243,15 @@ void CommunicationDeterminismChecker::get_comm_pattern(xbt_dynar_t list, smx_sim mc_model_checker->process().read( &remote_name, remote(comm->mbox ? &simgrid::xbt::string::to_string_data(comm->mbox->name_).data : &simgrid::xbt::string::to_string_data(comm->mbox_cpy->name_).data)); - pattern->rdv = mc_model_checker->process().read_string(remote_name); - pattern->dst_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(comm->dst_proc))->pid; + pattern->rdv = mc_model_checker->process().read_string(RemotePtr(remote_name)); + pattern->dst_proc = + mc_model_checker->process().resolveActor(simgrid::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("Insert incomplete comm pattern %p for process %lu", pattern.get(), issuer->pid); - xbt_dynar_t dynar = xbt_dynar_get_as(incomplete_communications_pattern, issuer->pid, xbt_dynar_t); + XBT_DEBUG("Insert incomplete comm pattern %p for process %ld", pattern.get(), issuer->get_pid()); + xbt_dynar_t dynar = xbt_dynar_get_as(incomplete_communications_pattern, issuer->get_pid(), xbt_dynar_t); simgrid::mc::PatternCommunication* pattern2 = pattern.release(); xbt_dynar_push(dynar, &pattern2); } @@ -426,7 +431,7 @@ void CommunicationDeterminismChecker::restoreState() } } -void CommunicationDeterminismChecker::main() +void CommunicationDeterminismChecker::real_run() { std::unique_ptr visited_state = nullptr; smx_simcall_t req = nullptr; @@ -562,7 +567,7 @@ void CommunicationDeterminismChecker::run() this->prepare(); - this->main(); + this->real_run(); } Checker* createCommunicationDeterminismChecker(Session& session)