X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/166ad11130482e81d2c3e860ab6c61e972a4cdf6..8468bc54da69c09b898b86e37bd5515edc7fdb3f:/src/mc/checker/CommunicationDeterminismChecker.cpp diff --git a/src/mc/checker/CommunicationDeterminismChecker.cpp b/src/mc/checker/CommunicationDeterminismChecker.cpp index cb723fb60e..0b3c59ae89 100644 --- a/src/mc/checker/CommunicationDeterminismChecker.cpp +++ b/src/mc/checker/CommunicationDeterminismChecker.cpp @@ -1,27 +1,24 @@ -/* 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/mc/mc_exit.h" -#include "src/mc/mc_private.h" -#include "src/mc/mc_record.h" -#include "src/mc/mc_request.h" -#include "src/mc/mc_smx.h" -#include "src/mc/mc_state.h" +#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" +#include "src/mc/mc_request.hpp" +#include "src/mc/mc_smx.hpp" +#include "src/mc/mc_state.hpp" #include "src/mc/remote/Client.hpp" -#include "src/smpi/smpi_request.hpp" +#if HAVE_SMPI +#include "smpi_request.hpp" +#endif + +#include using simgrid::mc::remote; @@ -67,25 +64,25 @@ static char* print_determinism_result(e_mc_comm_pattern_difference_t diff, int p switch(diff) { case TYPE_DIFF: - res = bprintf("%s Different type for communication #%d", type, cursor); + res = bprintf("%s Different type for communication #%u", type, cursor); break; case RDV_DIFF: - res = bprintf("%s Different rdv for communication #%d", type, cursor); + res = bprintf("%s Different rdv for communication #%u", type, cursor); break; case TAG_DIFF: - res = bprintf("%s Different tag for communication #%d", type, cursor); + res = bprintf("%s Different tag for communication #%u", type, cursor); break; case SRC_PROC_DIFF: - res = bprintf("%s Different source for communication #%d", type, cursor); + res = bprintf("%s Different source for communication #%u", type, cursor); break; case DST_PROC_DIFF: - res = bprintf("%s Different destination for communication #%d", type, cursor); + res = bprintf("%s Different destination for communication #%u", type, cursor); break; case DATA_SIZE_DIFF: - res = bprintf("%s\n Different data size for communication #%d", type, cursor); + res = bprintf("%s\n Different data size for communication #%u", type, cursor); break; case DATA_DIFF: - res = bprintf("%s\n Different data for communication #%d", type, cursor); + res = bprintf("%s\n Different data for communication #%u", type, cursor); break; default: res = nullptr; @@ -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_)); } } @@ -170,13 +167,13 @@ void CommunicationDeterminismChecker::deterministic_comm_pattern(int process, si /********** Non Static functions ***********/ -void CommunicationDeterminismChecker::get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, - e_mc_call_type_t call_type, int backtracking) +void CommunicationDeterminismChecker::get_comm_pattern(smx_simcall_t request, e_mc_call_type_t call_type, + int backtracking) { 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, @@ -236,22 +240,24 @@ void CommunicationDeterminismChecker::get_comm_pattern(xbt_dynar_t list, smx_sim simgrid::kernel::activity::CommImpl* comm = temp_comm.getBuffer(); char* remote_name; - mc_model_checker->process().read(&remote_name, remote(comm->mbox ? &comm->mbox->name_ : &comm->mbox_cpy->name_)); - 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; + 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(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); } void CommunicationDeterminismChecker::complete_comm_pattern( - xbt_dynar_t list, simgrid::mc::RemotePtr comm_addr, unsigned int issuer, - int backtracking) + simgrid::mc::RemotePtr comm_addr, unsigned int issuer, int backtracking) { simgrid::mc::PatternCommunication* current_comm_pattern; unsigned int cursor = 0; @@ -314,7 +320,6 @@ std::vector CommunicationDeterminismChecker::getTextualTrace() // o void CommunicationDeterminismChecker::logState() // override { - Checker::logState(); if (_sg_mc_comms_determinism && not this->recv_deterministic && this->send_deterministic) { XBT_INFO("******************************************************"); XBT_INFO("**** Only-send-deterministic communication pattern ****"); @@ -390,7 +395,6 @@ void CommunicationDeterminismChecker::restoreState() /* Restore the initial state */ simgrid::mc::session->restoreInitialState(); - // int n = xbt_dynar_length(incomplete_communications_pattern); unsigned n = MC_smx_get_maxpid(); assert(n == xbt_dynar_length(incomplete_communications_pattern)); assert(n == xbt_dynar_length(initial_communications_pattern)); @@ -417,7 +421,7 @@ void CommunicationDeterminismChecker::restoreState() /* TODO : handle test and testany simcalls */ e_mc_call_type_t call = MC_get_call_type(req); mc_model_checker->handle_simcall(state->transition); - MC_handle_comm_pattern(call, req, req_num, nullptr, 1); + MC_handle_comm_pattern(call, req, req_num, 1); mc_model_checker->wait_for_requests(); /* Update statistics */ @@ -426,7 +430,7 @@ void CommunicationDeterminismChecker::restoreState() } } -void CommunicationDeterminismChecker::main() +void CommunicationDeterminismChecker::real_run() { std::unique_ptr visited_state = nullptr; smx_simcall_t req = nullptr; @@ -436,14 +440,18 @@ void CommunicationDeterminismChecker::main() simgrid::mc::State* state = stack_.back().get(); XBT_DEBUG("**************************************************"); - XBT_DEBUG("Exploration depth = %zi (state = %d, interleaved processes = %zd)", stack_.size(), state->num, + XBT_DEBUG("Exploration depth = %zu (state = %d, interleaved processes = %zu)", stack_.size(), state->num, state->interleaveSize()); /* Update statistics */ mc_model_checker->visited_states++; - if (stack_.size() <= (std::size_t)_sg_mc_max_depth && (req = MC_state_get_request(state)) != nullptr && - (visited_state == nullptr)) { + if (stack_.size() <= (std::size_t)_sg_mc_max_depth) + req = MC_state_get_request(state); + else + req = nullptr; + + if (req != nullptr && visited_state == nullptr) { int req_num = state->transition.argument; @@ -464,10 +472,7 @@ void CommunicationDeterminismChecker::main() mc_model_checker->handle_simcall(state->transition); /* After this call req is no longer useful */ - if (not this->initial_communications_pattern_done) - MC_handle_comm_pattern(call, req, req_num, initial_communications_pattern, 0); - else - MC_handle_comm_pattern(call, req, req_num, nullptr, 0); + MC_handle_comm_pattern(call, req, req_num, 0); /* Wait for requests (schedules processes) */ mc_model_checker->wait_for_requests(); @@ -481,9 +486,12 @@ void CommunicationDeterminismChecker::main() * with the initial pattern. */ bool compare_snapshots = all_communications_are_finished() && this->initial_communications_pattern_done; - if (_sg_mc_max_visited_states == 0 || - (visited_state = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), compare_snapshots)) == - nullptr) { + if (_sg_mc_max_visited_states != 0) + visited_state = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), compare_snapshots); + else + visited_state = nullptr; + + 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()) @@ -508,13 +516,13 @@ void CommunicationDeterminismChecker::main() XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.", visited_state->original_num == -1 ? visited_state->num : visited_state->original_num); else - XBT_DEBUG("There are no more processes to interleave. (depth %zi)", stack_.size()); + XBT_DEBUG("There are no more processes to interleave. (depth %zu)", stack_.size()); if (not this->initial_communications_pattern_done) this->initial_communications_pattern_done = 1; /* Trash the current state, no longer needed */ - XBT_DEBUG("Delete state %d at depth %zi", state->num, stack_.size()); + XBT_DEBUG("Delete state %d at depth %zu", state->num, stack_.size()); stack_.pop_back(); visited_state = nullptr; @@ -522,7 +530,7 @@ void CommunicationDeterminismChecker::main() /* Check for deadlocks */ if (mc_model_checker->checkDeadlock()) { MC_show_deadlock(); - throw new simgrid::mc::DeadlockError(); + throw simgrid::mc::DeadlockError(); } while (not stack_.empty()) { @@ -530,16 +538,16 @@ void CommunicationDeterminismChecker::main() stack_.pop_back(); if (state->interleaveSize() && stack_.size() < (std::size_t)_sg_mc_max_depth) { /* We found a back-tracking point, let's loop */ - XBT_DEBUG("Back-tracking to state %d at depth %zi", state->num, stack_.size() + 1); + XBT_DEBUG("Back-tracking to state %d at depth %zu", state->num, stack_.size() + 1); stack_.push_back(std::move(state)); this->restoreState(); - XBT_DEBUG("Back-tracking to state %d at depth %zi done", stack_.back()->num, stack_.size()); + XBT_DEBUG("Back-tracking to state %d at depth %zu done", stack_.back()->num, stack_.size()); break; } else { - XBT_DEBUG("Delete state %d at depth %zi", state->num, stack_.size() + 1); + XBT_DEBUG("Delete state %d at depth %zu", state->num, stack_.size() + 1); } } } @@ -555,7 +563,7 @@ void CommunicationDeterminismChecker::run() this->prepare(); - this->main(); + this->real_run(); } Checker* createCommunicationDeterminismChecker(Session& session)