X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/9cc0d42f835e6aa5ea5195a346098e74b0376927..cf64c8ceb2027a65be8789e5fb36902e9274be4c:/src/mc/CommunicationDeterminismChecker.cpp diff --git a/src/mc/CommunicationDeterminismChecker.cpp b/src/mc/CommunicationDeterminismChecker.cpp index 4588869070..0677f95aff 100644 --- a/src/mc/CommunicationDeterminismChecker.cpp +++ b/src/mc/CommunicationDeterminismChecker.cpp @@ -22,6 +22,7 @@ #include "src/mc/CommunicationDeterminismChecker.hpp" #include "src/mc/mc_exit.h" #include "src/mc/VisitedState.hpp" +#include "src/mc/Transition.hpp" using simgrid::mc::remote; @@ -96,8 +97,10 @@ static void update_comm_pattern(simgrid::mc::PatternCommunication* comm_pattern, s_smx_synchro_t comm; mc_model_checker->process().read(&comm, remote(comm_addr)); - smx_process_t src_proc = MC_smx_resolve_process(comm.comm.src_proc); - smx_process_t dst_proc = MC_smx_resolve_process(comm.comm.dst_proc); + smx_process_t src_proc = mc_model_checker->process().resolveProcess( + simgrid::mc::remote(comm.comm.src_proc)); + smx_process_t dst_proc = mc_model_checker->process().resolveProcess( + simgrid::mc::remote(comm.comm.dst_proc)); comm_pattern->src_proc = src_proc->pid; comm_pattern->dst_proc = dst_proc->pid; comm_pattern->src_host = MC_smx_process_get_host_name(src_proc); @@ -141,7 +144,7 @@ static void deterministic_comm_pattern(int process, simgrid::mc::PatternCommunic XBT_INFO("%s", simgrid::mc::initial_global_state->send_diff); xbt_free(simgrid::mc::initial_global_state->send_diff); simgrid::mc::initial_global_state->send_diff = nullptr; - MC_print_statistics(mc_stats); + simgrid::mc::session->logState(); mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM); }else if(_sg_mc_comms_determinism && (!simgrid::mc::initial_global_state->send_deterministic @@ -155,7 +158,7 @@ static void deterministic_comm_pattern(int process, simgrid::mc::PatternCommunic simgrid::mc::initial_global_state->send_diff = nullptr; xbt_free(simgrid::mc::initial_global_state->recv_diff); simgrid::mc::initial_global_state->recv_diff = nullptr; - MC_print_statistics(mc_stats); + simgrid::mc::session->logState(); mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM); } } @@ -189,7 +192,8 @@ void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type char* remote_name = mc_model_checker->process().read( (std::uint64_t)(synchro.comm.rdv ? &synchro.comm.rdv->name : &synchro.comm.rdv_cpy->name)); pattern->rdv = mc_model_checker->process().read_string(remote_name); - pattern->src_proc = MC_smx_resolve_process(synchro.comm.src_proc)->pid; + pattern->src_proc = mc_model_checker->process().resolveProcess( + simgrid::mc::remote(synchro.comm.src_proc))->pid; pattern->src_host = MC_smx_process_get_host_name(issuer); struct s_smpi_mpi_request mpi_request = @@ -235,7 +239,8 @@ void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type mc_model_checker->process().read(&remote_name, remote(synchro.comm.rdv ? &synchro.comm.rdv->name : &synchro.comm.rdv_cpy->name)); pattern->rdv = mc_model_checker->process().read_string(remote_name); - pattern->dst_proc = MC_smx_resolve_process(synchro.comm.dst_proc)->pid; + pattern->dst_proc = mc_model_checker->process().resolveProcess( + simgrid::mc::remote(synchro.comm.dst_proc))->pid; pattern->dst_host = MC_smx_process_get_host_name(issuer); } else xbt_die("Unexpected call_type %i", (int) call_type); @@ -305,7 +310,7 @@ RecordTrace CommunicationDeterminismChecker::getRecordTrace() // override { RecordTrace res; for (auto const& state : stack_) - res.push_back(state->getRecordElement()); + res.push_back(state->getTransition()); return res; } @@ -316,11 +321,40 @@ std::vector CommunicationDeterminismChecker::getTextualTrace() // o smx_simcall_t req = &state->executed_req; if (req) trace.push_back(simgrid::mc::request_to_string( - req, state->req_num, simgrid::mc::RequestType::executed)); + req, state->transition.argument, simgrid::mc::RequestType::executed)); } return trace; } +void CommunicationDeterminismChecker::logState() // override +{ + Checker::logState(); + if (_sg_mc_comms_determinism && + !simgrid::mc::initial_global_state->recv_deterministic && + simgrid::mc::initial_global_state->send_deterministic) { + XBT_INFO("******************************************************"); + XBT_INFO("**** Only-send-deterministic communication pattern ****"); + XBT_INFO("******************************************************"); + XBT_INFO("%s", simgrid::mc::initial_global_state->recv_diff); + } else if(_sg_mc_comms_determinism && + !simgrid::mc::initial_global_state->send_deterministic && + simgrid::mc::initial_global_state->recv_deterministic) { + XBT_INFO("******************************************************"); + XBT_INFO("**** Only-recv-deterministic communication pattern ****"); + XBT_INFO("******************************************************"); + XBT_INFO("%s", simgrid::mc::initial_global_state->send_diff); + } + 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); + if (simgrid::mc::initial_global_state != nullptr) + XBT_INFO("Send-deterministic : %s", + !simgrid::mc::initial_global_state->send_deterministic ? "No" : "Yes"); + if (simgrid::mc::initial_global_state != nullptr && _sg_mc_comms_determinism) + XBT_INFO("Recv-deterministic : %s", + !simgrid::mc::initial_global_state->recv_deterministic ? "No" : "Yes"); +} + void CommunicationDeterminismChecker::prepare() { @@ -342,13 +376,10 @@ void CommunicationDeterminismChecker::prepare() } std::unique_ptr initial_state = - std::unique_ptr(MC_state_new()); + std::unique_ptr(MC_state_new(++expandedStatesCount_)); XBT_DEBUG("********* Start communication determinism verification *********"); - /* Wait for requests (schedules processes) */ - mc_model_checker->wait_for_requests(); - /* Get an enabled process and insert it in the interleave set of the initial state */ for (auto& p : mc_model_checker->process().simix_processes()) if (simgrid::mc::process_is_enabled(&p.copy)) @@ -387,13 +418,13 @@ int CommunicationDeterminismChecker::main(void) state->interleaveSize()); /* Update statistics */ - mc_stats->visited_states++; + 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)) { - int req_num = state->req_num; + int req_num = state->transition.argument; XBT_DEBUG("Execute: %s", simgrid::mc::request_to_string( @@ -403,7 +434,7 @@ int CommunicationDeterminismChecker::main(void) if (dot_output != nullptr) req_str = simgrid::mc::request_get_dot_output(req, req_num); - mc_stats->executed_transitions++; + mc_model_checker->executed_transitions++; /* TODO : handle test and testany simcalls */ e_mc_call_type_t call = MC_CALL_TYPE_NONE; @@ -411,7 +442,8 @@ int CommunicationDeterminismChecker::main(void) call = MC_get_call_type(req); /* Answer the request */ - simgrid::mc::handle_simcall(req, req_num); /* After this call req is no longer useful */ + mc_model_checker->handle_simcall(state->transition); + /* After this call req is no longer useful */ if(!initial_global_state->initial_communications_pattern_done) MC_handle_comm_pattern(call, req, req_num, initial_communications_pattern, 0); @@ -423,7 +455,7 @@ int CommunicationDeterminismChecker::main(void) /* Create the new expanded state */ std::unique_ptr next_state = - std::unique_ptr(MC_state_new()); + std::unique_ptr(MC_state_new(++expandedStatesCount_)); /* If comm determinism verification, we cannot stop the exploration if some communications are not finished (at least, data are transfered). @@ -433,7 +465,8 @@ int CommunicationDeterminismChecker::main(void) && initial_global_state->initial_communications_pattern_done; if (_sg_mc_visited == 0 - || (visited_state = visitedStates_.addVisitedState(next_state.get(), compare_snapshots)) == nullptr) { + || (visited_state = visitedStates_.addVisitedState( + expandedStatesCount_, next_state.get(), compare_snapshots)) == nullptr) { /* Get enabled processes and insert them in the interleave set of the next state */ for (auto& p : mc_model_checker->process().simix_processes()) @@ -500,7 +533,7 @@ int CommunicationDeterminismChecker::main(void) } } - MC_print_statistics(mc_stats); + simgrid::mc::session->logState(); return SIMGRID_MC_EXIT_SUCCESS; }