X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/ab8e2fe95944fb998edd6e95d1022a05175c4f92..cf64c8ceb2027a65be8789e5fb36902e9274be4c:/src/mc/CommunicationDeterminismChecker.cpp diff --git a/src/mc/CommunicationDeterminismChecker.cpp b/src/mc/CommunicationDeterminismChecker.cpp index f983945862..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); @@ -301,34 +306,55 @@ CommunicationDeterminismChecker::~CommunicationDeterminismChecker() } -// TODO, deduplicate with SafetyChecker RecordTrace CommunicationDeterminismChecker::getRecordTrace() // override { RecordTrace res; - for (auto const& state : stack_) { - int value = 0; - smx_simcall_t saved_req = MC_state_get_executed_request(state.get(), &value); - const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req); - const int pid = issuer->pid; - res.push_back(RecordTraceElement(pid, value)); - } + for (auto const& state : stack_) + res.push_back(state->getTransition()); return res; } -// TODO, deduplicate with SafetyChecker std::vector CommunicationDeterminismChecker::getTextualTrace() // override { std::vector trace; for (auto const& state : stack_) { - int value; - smx_simcall_t req = MC_state_get_executed_request(state.get(), &value); + smx_simcall_t req = &state->executed_req; if (req) trace.push_back(simgrid::mc::request_to_string( - req, value, 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() { @@ -350,17 +376,14 @@ 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)) - MC_state_interleave_process(initial_state.get(), &p.copy); + initial_state->interleave(&p.copy); stack_.push_back(std::move(initial_state)); } @@ -381,7 +404,6 @@ bool all_communications_are_finished() int CommunicationDeterminismChecker::main(void) { - int value; std::unique_ptr visited_state = nullptr; smx_simcall_t req = nullptr; @@ -396,22 +418,23 @@ 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, &value)) + && (req = MC_state_get_request(state)) != nullptr && (visited_state == nullptr)) { + int req_num = state->transition.argument; + XBT_DEBUG("Execute: %s", simgrid::mc::request_to_string( - req, value, simgrid::mc::RequestType::simix).c_str()); + req, req_num, simgrid::mc::RequestType::simix).c_str()); std::string req_str; if (dot_output != nullptr) - req_str = simgrid::mc::request_get_dot_output(req, value); + req_str = simgrid::mc::request_get_dot_output(req, req_num); - MC_state_set_executed_request(state, req, value); - 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; @@ -419,19 +442,20 @@ int CommunicationDeterminismChecker::main(void) call = MC_get_call_type(req); /* Answer the request */ - simgrid::mc::handle_simcall(req, value); /* 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, value, initial_communications_pattern, 0); + MC_handle_comm_pattern(call, req, req_num, initial_communications_pattern, 0); else - MC_handle_comm_pattern(call, req, value, nullptr, 0); + MC_handle_comm_pattern(call, req, req_num, nullptr, 0); /* Wait for requests (schedules processes) */ mc_model_checker->wait_for_requests(); /* 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). @@ -441,12 +465,13 @@ 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()) if (simgrid::mc::process_is_enabled(&p.copy)) - MC_state_interleave_process(next_state.get(), &p.copy); + next_state->interleave(&p.copy); if (dot_output != nullptr) fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", @@ -508,7 +533,7 @@ int CommunicationDeterminismChecker::main(void) } } - MC_print_statistics(mc_stats); + simgrid::mc::session->logState(); return SIMGRID_MC_EXIT_SUCCESS; }