X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/b83ad9c88af4715987015ddc91ac93ad749df428..ae68749ec3d90fc5e403e8a4950d30b832a9629f:/src/mc/checker/CommunicationDeterminismChecker.cpp diff --git a/src/mc/checker/CommunicationDeterminismChecker.cpp b/src/mc/checker/CommunicationDeterminismChecker.cpp index 3bdf2a4805..2410b9d1dc 100644 --- a/src/mc/checker/CommunicationDeterminismChecker.cpp +++ b/src/mc/checker/CommunicationDeterminismChecker.cpp @@ -17,7 +17,6 @@ #include "src/mc/mc_private.h" #include "src/mc/mc_record.h" #include "src/mc/mc_request.h" -#include "src/mc/mc_safety.h" #include "src/mc/mc_smx.h" #include "src/mc/mc_state.h" #include "src/mc/remote/Client.hpp" @@ -97,12 +96,12 @@ static char* print_determinism_result(e_mc_comm_pattern_difference_t diff, int p } static void update_comm_pattern(simgrid::mc::PatternCommunication* comm_pattern, - simgrid::mc::RemotePtr comm_addr) + simgrid::mc::RemotePtr comm_addr) { // HACK, type punning - simgrid::mc::Remote temp_comm; + simgrid::mc::Remote temp_comm; mc_model_checker->process().read(temp_comm, comm_addr); - simgrid::kernel::activity::Comm* comm = temp_comm.getBuffer(); + 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)); @@ -128,7 +127,7 @@ void CommunicationDeterminismChecker::deterministic_comm_pattern(int process, si simgrid::mc::PatternCommunicationList* list = xbt_dynar_get_as(initial_communications_pattern, process, simgrid::mc::PatternCommunicationList*); - if(!backtracking){ + if (not backtracking) { e_mc_comm_pattern_difference_t diff = compare_comm_pattern(list->list[list->index_comm].get(), comm); if (diff != NONE_DIFF) { @@ -143,7 +142,7 @@ void CommunicationDeterminismChecker::deterministic_comm_pattern(int process, si xbt_free(this->recv_diff); this->recv_diff = print_determinism_result(diff, process, comm, list->index_comm + 1); } - if(_sg_mc_send_determinism && !this->send_deterministic){ + if (_sg_mc_send_determinism && not this->send_deterministic) { XBT_INFO("*********************************************************"); XBT_INFO("***** Non-send-deterministic communications pattern *****"); XBT_INFO("*********************************************************"); @@ -152,8 +151,7 @@ void CommunicationDeterminismChecker::deterministic_comm_pattern(int process, si this->send_diff = nullptr; simgrid::mc::session->logState(); mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM); - }else if(_sg_mc_comms_determinism - && (!this->send_deterministic && !this->recv_deterministic)) { + } else if (_sg_mc_comms_determinism && (not this->send_deterministic && not this->recv_deterministic)) { XBT_INFO("****************************************************"); XBT_INFO("***** Non-deterministic communications pattern *****"); XBT_INFO("****************************************************"); @@ -189,10 +187,11 @@ void CommunicationDeterminismChecker::get_comm_pattern(xbt_dynar_t list, smx_sim pattern->type = simgrid::mc::PatternCommunicationType::send; pattern->comm_addr = simcall_comm_isend__get__result(request); - simgrid::mc::Remote temp_synchro; + simgrid::mc::Remote temp_synchro; mc_model_checker->process().read(temp_synchro, - remote(static_cast(pattern->comm_addr))); - simgrid::kernel::activity::Comm* synchro = static_cast(temp_synchro.getBuffer()); + remote(static_cast(pattern->comm_addr))); + simgrid::kernel::activity::CommImpl* synchro = + 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_)); @@ -209,7 +208,7 @@ void CommunicationDeterminismChecker::get_comm_pattern(xbt_dynar_t list, smx_sim mc_model_checker->process().read_bytes(pattern->data.data(), pattern->data.size(), remote(synchro->src_buff)); } if(mpi_request.detached()){ - if (!this->initial_communications_pattern_done) { + if (not this->initial_communications_pattern_done) { /* Store comm pattern */ simgrid::mc::PatternCommunicationList* list = xbt_dynar_get_as(initial_communications_pattern, pattern->src_proc, simgrid::mc::PatternCommunicationList*); @@ -231,10 +230,10 @@ void CommunicationDeterminismChecker::get_comm_pattern(xbt_dynar_t list, smx_sim remote((simgrid::smpi::Request*)simcall_comm_irecv__get__data(request))); pattern->tag = mpi_request.tag(); - simgrid::mc::Remote temp_comm; + simgrid::mc::Remote temp_comm; mc_model_checker->process().read(temp_comm, - remote(static_cast(pattern->comm_addr))); - simgrid::kernel::activity::Comm* comm = temp_comm.getBuffer(); + remote(static_cast(pattern->comm_addr))); + 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_)); @@ -251,7 +250,7 @@ void CommunicationDeterminismChecker::get_comm_pattern(xbt_dynar_t list, smx_sim } void CommunicationDeterminismChecker::complete_comm_pattern( - xbt_dynar_t list, simgrid::mc::RemotePtr comm_addr, unsigned int issuer, + xbt_dynar_t list, simgrid::mc::RemotePtr comm_addr, unsigned int issuer, int backtracking) { simgrid::mc::PatternCommunication* current_comm_pattern; @@ -271,13 +270,13 @@ void CommunicationDeterminismChecker::complete_comm_pattern( break; } - if(!completed) + if (not completed) xbt_die("Corresponding communication not found!"); simgrid::mc::PatternCommunicationList* pattern = xbt_dynar_get_as(initial_communications_pattern, issuer, simgrid::mc::PatternCommunicationList*); - if (!this->initial_communications_pattern_done) + if (not this->initial_communications_pattern_done) /* Store comm pattern */ pattern->list.push_back(std::move(comm_pattern)); else { @@ -316,12 +315,12 @@ std::vector CommunicationDeterminismChecker::getTextualTrace() // o void CommunicationDeterminismChecker::logState() // override { Checker::logState(); - if (_sg_mc_comms_determinism && !this->recv_deterministic && this->send_deterministic) { + if (_sg_mc_comms_determinism && not this->recv_deterministic && this->send_deterministic) { XBT_INFO("******************************************************"); XBT_INFO("**** Only-send-deterministic communication pattern ****"); XBT_INFO("******************************************************"); XBT_INFO("%s", this->recv_diff); - } else if (_sg_mc_comms_determinism && !this->send_deterministic && this->recv_deterministic) { + } else if (_sg_mc_comms_determinism && not this->send_deterministic && this->recv_deterministic) { XBT_INFO("******************************************************"); XBT_INFO("**** Only-recv-deterministic communication pattern ****"); XBT_INFO("******************************************************"); @@ -330,9 +329,9 @@ void CommunicationDeterminismChecker::logState() // override XBT_INFO("Expanded states = %lu", expandedStatesCount_); XBT_INFO("Visited states = %lu", mc_model_checker->visited_states); XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions); - XBT_INFO("Send-deterministic : %s", !this->send_deterministic ? "No" : "Yes"); + XBT_INFO("Send-deterministic : %s", not this->send_deterministic ? "No" : "Yes"); if (_sg_mc_comms_determinism) - XBT_INFO("Recv-deterministic : %s", !this->recv_deterministic ? "No" : "Yes"); + XBT_INFO("Recv-deterministic : %s", not this->recv_deterministic ? "No" : "Yes"); } void CommunicationDeterminismChecker::prepare() @@ -361,7 +360,7 @@ void CommunicationDeterminismChecker::prepare() /* Get an enabled actor and insert it in the interleave set of the initial state */ for (auto& actor : mc_model_checker->process().actors()) if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer())) - initial_state->interleave(actor.copy.getBuffer()); + initial_state->addInterleavingSet(actor.copy.getBuffer()); stack_.push_back(std::move(initial_state)); } @@ -370,8 +369,8 @@ static inline bool all_communications_are_finished() { for (size_t current_actor = 1; current_actor < MC_smx_get_maxpid(); current_actor++) { xbt_dynar_t pattern = xbt_dynar_get_as(incomplete_communications_pattern, current_actor, xbt_dynar_t); - if (!xbt_dynar_is_empty(pattern)) { - XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited."); + if (not xbt_dynar_is_empty(pattern)) { + XBT_DEBUG("Some communications are not finished, cannot stop the exploration! State not visited."); return false; } } @@ -427,12 +426,12 @@ void CommunicationDeterminismChecker::restoreState() } } -void CommunicationDeterminismChecker::main(void) +void CommunicationDeterminismChecker::main() { std::unique_ptr visited_state = nullptr; smx_simcall_t req = nullptr; - while (!stack_.empty()) { + while (not stack_.empty()) { /* Get current state */ simgrid::mc::State* state = stack_.back().get(); @@ -465,7 +464,7 @@ void CommunicationDeterminismChecker::main(void) mc_model_checker->handle_simcall(state->transition); /* After this call req is no longer useful */ - if (!this->initial_communications_pattern_done) + 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); @@ -489,7 +488,7 @@ void CommunicationDeterminismChecker::main(void) /* Get enabled actors and insert them in the interleave set of the next state */ for (auto& actor : mc_model_checker->process().actors()) if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer())) - next_state->interleave(actor.copy.getBuffer()); + next_state->addInterleavingSet(actor.copy.getBuffer()); if (dot_output != nullptr) fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", @@ -504,14 +503,14 @@ void CommunicationDeterminismChecker::main(void) } else { if (stack_.size() > (std::size_t) _sg_mc_max_depth) - XBT_WARN("/!\\ Max depth reached ! /!\\ "); + XBT_WARN("/!\\ Max depth reached! /!\\ "); else if (visited_state != nullptr) 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()); - if (!this->initial_communications_pattern_done) + if (not this->initial_communications_pattern_done) this->initial_communications_pattern_done = 1; /* Trash the current state, no longer needed */ @@ -526,7 +525,7 @@ void CommunicationDeterminismChecker::main(void) throw new simgrid::mc::DeadlockError(); } - while (!stack_.empty()) { + while (not stack_.empty()) { std::unique_ptr state = std::move(stack_.back()); stack_.pop_back(); if (state->interleaveSize() && stack_.size() < (std::size_t)_sg_mc_max_depth) {