X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/1930bee57857b8ccfbdaa457ea6748a49fc8d4f8..872d65264714799b25eb231609c3f05bae3d03dc:/src/mc/CommunicationDeterminismChecker.cpp diff --git a/src/mc/CommunicationDeterminismChecker.cpp b/src/mc/CommunicationDeterminismChecker.cpp index 0e29e9a0c4..dc3ac5f7ad 100644 --- a/src/mc/CommunicationDeterminismChecker.cpp +++ b/src/mc/CommunicationDeterminismChecker.cpp @@ -36,7 +36,8 @@ xbt_dynar_t incomplete_communications_pattern; /********** Static functions ***********/ -static e_mc_comm_pattern_difference_t compare_comm_pattern(simgrid::mc::PatternCommunication* comm1, simgrid::mc::PatternCommunication* comm2) { +static e_mc_comm_pattern_difference_t compare_comm_pattern(simgrid::mc::PatternCommunication* comm1, simgrid::mc::PatternCommunication* comm2) +{ if(comm1->type != comm2->type) return TYPE_DIFF; if (comm1->rdv != comm2->rdv) @@ -57,7 +58,7 @@ static e_mc_comm_pattern_difference_t compare_comm_pattern(simgrid::mc::PatternC static char* print_determinism_result(e_mc_comm_pattern_difference_t diff, int process, simgrid::mc::PatternCommunication* comm, unsigned int cursor) { char *type, *res; - if(comm->type == SIMIX_COMM_SEND) + if (comm->type == simgrid::mc::PatternCommunicationType::send) type = bprintf("The send communications pattern of the process %d is different!", process - 1); else type = bprintf("The recv communications pattern of the process %d is different!", process - 1); @@ -92,32 +93,41 @@ static char* print_determinism_result(e_mc_comm_pattern_difference_t diff, int p return res; } -static void update_comm_pattern(simgrid::mc::PatternCommunication* comm_pattern, smx_synchro_t comm_addr) +static void update_comm_pattern( + simgrid::mc::PatternCommunication* comm_pattern, + simgrid::mc::RemotePtr comm_addr) { - s_smx_synchro_t comm; - mc_model_checker->process().read(&comm, remote(comm_addr)); + // HACK, type punning + simgrid::mc::Remote temp_comm; + mc_model_checker->process().read(temp_comm, comm_addr); + simgrid::simix::Comm* comm = + static_cast(temp_comm.data()); smx_process_t src_proc = mc_model_checker->process().resolveProcess( - simgrid::mc::remote(comm.comm.src_proc)); + simgrid::mc::remote(comm->src_proc)); smx_process_t dst_proc = mc_model_checker->process().resolveProcess( - simgrid::mc::remote(comm.comm.dst_proc)); + simgrid::mc::remote(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); comm_pattern->dst_host = MC_smx_process_get_host_name(dst_proc); - if (comm_pattern->data.size() == 0 && comm.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.comm.dst_buff_size)); + &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.comm.src_buff)); + remote(comm->src_buff)); } } -static void deterministic_comm_pattern(int process, simgrid::mc::PatternCommunication* comm, int backtracking) { +namespace simgrid { +namespace mc { +void CommunicationDeterminismChecker::deterministic_comm_pattern( + int process, simgrid::mc::PatternCommunication* comm, int backtracking) +{ simgrid::mc::PatternCommunicationList* list = xbt_dynar_get_as(initial_communications_pattern, process, simgrid::mc::PatternCommunicationList*); @@ -126,38 +136,37 @@ static void deterministic_comm_pattern(int process, simgrid::mc::PatternCommunic compare_comm_pattern(list->list[list->index_comm].get(), comm); if (diff != NONE_DIFF) { - if (comm->type == SIMIX_COMM_SEND){ - simgrid::mc::initial_global_state->send_deterministic = 0; - if(simgrid::mc::initial_global_state->send_diff != nullptr) - xbt_free(simgrid::mc::initial_global_state->send_diff); - simgrid::mc::initial_global_state->send_diff = print_determinism_result(diff, process, comm, list->index_comm + 1); - }else{ - simgrid::mc::initial_global_state->recv_deterministic = 0; - if(simgrid::mc::initial_global_state->recv_diff != nullptr) - xbt_free(simgrid::mc::initial_global_state->recv_diff); - simgrid::mc::initial_global_state->recv_diff = print_determinism_result(diff, process, comm, list->index_comm + 1); + if (comm->type == simgrid::mc::PatternCommunicationType::send) { + this->send_deterministic = 0; + if (this->send_diff != nullptr) + xbt_free(this->send_diff); + this->send_diff = print_determinism_result(diff, process, comm, list->index_comm + 1); + } else { + this->recv_deterministic = 0; + if (this->recv_diff != nullptr) + xbt_free(this->recv_diff); + this->recv_diff = print_determinism_result(diff, process, comm, list->index_comm + 1); } - if(_sg_mc_send_determinism && !simgrid::mc::initial_global_state->send_deterministic){ + if(_sg_mc_send_determinism && !this->send_deterministic){ XBT_INFO("*********************************************************"); XBT_INFO("***** Non-send-deterministic communications pattern *****"); XBT_INFO("*********************************************************"); - 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; + XBT_INFO("%s", this->send_diff); + xbt_free(this->send_diff); + this->send_diff = nullptr; 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 - && !simgrid::mc::initial_global_state->recv_deterministic)) { + && (!this->send_deterministic && !this->recv_deterministic)) { XBT_INFO("****************************************************"); XBT_INFO("***** Non-deterministic communications pattern *****"); XBT_INFO("****************************************************"); - XBT_INFO("%s", simgrid::mc::initial_global_state->send_diff); - XBT_INFO("%s", simgrid::mc::initial_global_state->recv_diff); - xbt_free(simgrid::mc::initial_global_state->send_diff); - 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; + XBT_INFO("%s", this->send_diff); + XBT_INFO("%s", this->recv_diff); + xbt_free(this->send_diff); + this->send_diff = nullptr; + xbt_free(this->recv_diff); + this->recv_diff = nullptr; simgrid::mc::session->logState(); mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM); } @@ -167,7 +176,7 @@ static void deterministic_comm_pattern(int process, simgrid::mc::PatternCommunic /********** Non Static functions ***********/ -void MC_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(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking) { const smx_process_t issuer = MC_smx_simcall_get_issuer(request); simgrid::mc::PatternCommunicationList* initial_pattern = xbt_dynar_get_as( @@ -183,17 +192,20 @@ void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type if (call_type == MC_CALL_TYPE_SEND) { /* Create comm pattern */ - pattern->type = SIMIX_COMM_SEND; + pattern->type = simgrid::mc::PatternCommunicationType::send; pattern->comm_addr = simcall_comm_isend__get__result(request); - s_smx_synchro_t synchro = mc_model_checker->process().read( - (std::uint64_t) pattern->comm_addr); + simgrid::mc::Remote temp_synchro; + mc_model_checker->process().read(temp_synchro, remote( + static_cast(pattern->comm_addr))); + simgrid::simix::Comm* synchro = + static_cast(temp_synchro.data()); char* remote_name = mc_model_checker->process().read( - (std::uint64_t)(synchro.comm.rdv ? &synchro.comm.rdv->name : &synchro.comm.rdv_cpy->name)); + (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().resolveProcess( - simgrid::mc::remote(synchro.comm.src_proc))->pid; + simgrid::mc::remote(synchro->src_proc))->pid; pattern->src_host = MC_smx_process_get_host_name(issuer); struct s_smpi_mpi_request mpi_request = @@ -201,14 +213,14 @@ void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type (std::uint64_t) simcall_comm_isend__get__data(request)); pattern->tag = mpi_request.tag; - if(synchro.comm.src_buff != nullptr){ - pattern->data.resize(synchro.comm.src_buff_size); + 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.comm.src_buff)); + remote(synchro->src_buff)); } if(mpi_request.detached){ - if (!simgrid::mc::initial_global_state->initial_communications_pattern_done) { + if (!this->initial_communications_pattern_done) { /* Store comm pattern */ simgrid::mc::PatternCommunicationList* list = xbt_dynar_get_as( initial_communications_pattern, pattern->src_proc, @@ -216,7 +228,7 @@ void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type list->list.push_back(std::move(pattern)); } else { /* Evaluate comm determinism */ - deterministic_comm_pattern(pattern->src_proc, pattern.get(), backtracking); + this->deterministic_comm_pattern(pattern->src_proc, pattern.get(), backtracking); xbt_dynar_get_as( initial_communications_pattern, pattern->src_proc, simgrid::mc::PatternCommunicationList* )->index_comm++; @@ -224,7 +236,7 @@ void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type return; } } else if (call_type == MC_CALL_TYPE_RECV) { - pattern->type = SIMIX_COMM_RECEIVE; + pattern->type = simgrid::mc::PatternCommunicationType::receive; pattern->comm_addr = simcall_comm_irecv__get__result(request); struct s_smpi_mpi_request mpi_request; @@ -232,15 +244,18 @@ void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type &mpi_request, remote((struct s_smpi_mpi_request*)simcall_comm_irecv__get__data(request))); pattern->tag = mpi_request.tag; - s_smx_synchro_t synchro; - mc_model_checker->process().read(&synchro, remote(pattern->comm_addr)); + simgrid::mc::Remote temp_comm; + mc_model_checker->process().read(temp_comm, remote( + static_cast(pattern->comm_addr))); + simgrid::simix::Comm* comm = + static_cast(temp_comm.data()); char* remote_name; mc_model_checker->process().read(&remote_name, - remote(synchro.comm.rdv ? &synchro.comm.rdv->name : &synchro.comm.rdv_cpy->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().resolveProcess( - simgrid::mc::remote(synchro.comm.dst_proc))->pid; + simgrid::mc::remote(comm->dst_proc))->pid; pattern->dst_host = MC_smx_process_get_host_name(issuer); } else xbt_die("Unexpected call_type %i", (int) call_type); @@ -253,7 +268,11 @@ void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type xbt_dynar_push(dynar, &pattern2); } -void MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigned int issuer, int backtracking) { + +void CommunicationDeterminismChecker::complete_comm_pattern( + xbt_dynar_t list, simgrid::mc::RemotePtr comm_addr, + unsigned int issuer, int backtracking) +{ simgrid::mc::PatternCommunication* current_comm_pattern; unsigned int cursor = 0; std::unique_ptr comm_pattern; @@ -261,7 +280,7 @@ void MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigne /* Complete comm pattern */ xbt_dynar_foreach(xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t), cursor, current_comm_pattern) - if (current_comm_pattern->comm_addr == comm_addr) { + if (remote(current_comm_pattern->comm_addr) == comm_addr) { update_comm_pattern(current_comm_pattern, comm_addr); completed = 1; simgrid::mc::PatternCommunication* temp; @@ -279,22 +298,16 @@ void MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigne simgrid::mc::PatternCommunicationList* pattern = xbt_dynar_get_as( initial_communications_pattern, issuer, simgrid::mc::PatternCommunicationList*); - if (!simgrid::mc::initial_global_state->initial_communications_pattern_done) + if (!this->initial_communications_pattern_done) /* Store comm pattern */ pattern->list.push_back(std::move(comm_pattern)); else { /* Evaluate comm determinism */ - deterministic_comm_pattern(issuer, comm_pattern.get(), backtracking); + this->deterministic_comm_pattern(issuer, comm_pattern.get(), backtracking); pattern->index_comm++; } } - -/************************ Main algorithm ************************/ - -namespace simgrid { -namespace mc { - CommunicationDeterminismChecker::CommunicationDeterminismChecker(Session& session) : Checker(session) { @@ -330,29 +343,27 @@ 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) { + !this->recv_deterministic && + this->send_deterministic) { XBT_INFO("******************************************************"); XBT_INFO("**** Only-send-deterministic communication pattern ****"); XBT_INFO("******************************************************"); - XBT_INFO("%s", simgrid::mc::initial_global_state->recv_diff); + XBT_INFO("%s", this->recv_diff); } else if(_sg_mc_comms_determinism && - !simgrid::mc::initial_global_state->send_deterministic && - simgrid::mc::initial_global_state->recv_deterministic) { + !this->send_deterministic && + this->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("%s", this->send_diff); } XBT_INFO("Expanded states = %lu", expandedStatesCount_); - XBT_INFO("Visited states = %lu", mc_stats->visited_states); - XBT_INFO("Executed transitions = %lu", mc_stats->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("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"); + if (_sg_mc_comms_determinism) XBT_INFO("Recv-deterministic : %s", - !simgrid::mc::initial_global_state->recv_deterministic ? "No" : "Yes"); + !this->recv_deterministic ? "No" : "Yes"); } void CommunicationDeterminismChecker::prepare() @@ -402,6 +413,57 @@ bool all_communications_are_finished() return true; } +void CommunicationDeterminismChecker::restoreState() +{ + /* Intermediate backtracking */ + { + simgrid::mc::State* state = stack_.back().get(); + if (state->system_state) { + simgrid::mc::restore_snapshot(state->system_state); + MC_restore_communications_pattern(state); + return; + } + } + + /* 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)); + for (unsigned j=0; j < n ; j++) { + xbt_dynar_reset((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, j, xbt_dynar_t)); + xbt_dynar_get_as(initial_communications_pattern, j, simgrid::mc::PatternCommunicationList*)->index_comm = 0; + } + + /* Traverse the stack from the state at position start and re-execute the transitions */ + for (std::unique_ptr const& state : stack_) { + if (state == stack_.back()) + break; + + int req_num = state->transition.argument; + smx_simcall_t saved_req = &state->executed_req; + xbt_assert(saved_req); + + /* because we got a copy of the executed request, we have to fetch the + real one, pointed by the request field of the issuer process */ + + const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req); + smx_simcall_t req = &issuer->simcall; + + /* 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_model_checker->wait_for_requests(); + + /* Update statistics */ + mc_model_checker->visited_states++; + mc_model_checker->executed_transitions++; + } +} + int CommunicationDeterminismChecker::main(void) { std::unique_ptr visited_state = nullptr; @@ -418,7 +480,7 @@ 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 @@ -434,7 +496,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; @@ -445,7 +507,7 @@ int CommunicationDeterminismChecker::main(void) mc_model_checker->handle_simcall(state->transition); /* After this call req is no longer useful */ - if(!initial_global_state->initial_communications_pattern_done) + if (!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); @@ -462,7 +524,7 @@ int CommunicationDeterminismChecker::main(void) These communications are incomplete and they cannot be analyzed and compared with the initial pattern. */ bool compare_snapshots = all_communications_are_finished() - && initial_global_state->initial_communications_pattern_done; + && this->initial_communications_pattern_done; if (_sg_mc_visited == 0 || (visited_state = visitedStates_.addVisitedState( @@ -493,8 +555,8 @@ int CommunicationDeterminismChecker::main(void) XBT_DEBUG("There are no more processes to interleave. (depth %zi)", stack_.size()); - if (!initial_global_state->initial_communications_pattern_done) - initial_global_state->initial_communications_pattern_done = 1; + if (!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", @@ -519,7 +581,7 @@ int CommunicationDeterminismChecker::main(void) state->num, stack_.size() + 1); stack_.push_back(std::move(state)); - simgrid::mc::replay(stack_); + this->restoreState(); XBT_DEBUG("Back-tracking to state %d at depth %zi done", stack_.back()->num, stack_.size()); @@ -540,20 +602,17 @@ int CommunicationDeterminismChecker::main(void) int CommunicationDeterminismChecker::run() { XBT_INFO("Check communication determinism"); - mc_model_checker->wait_for_requests(); + simgrid::mc::session->initialize(); this->prepare(); - initial_global_state = std::unique_ptr(new s_mc_global_t()); - initial_global_state->snapshot = simgrid::mc::take_snapshot(0); - initial_global_state->initial_communications_pattern_done = 0; - initial_global_state->recv_deterministic = 1; - initial_global_state->send_deterministic = 1; - initial_global_state->recv_diff = nullptr; - initial_global_state->send_diff = nullptr; + this->initial_communications_pattern_done = 0; + this->recv_deterministic = 1; + this->send_deterministic = 1; + this->recv_diff = nullptr; + this->send_diff = nullptr; int res = this->main(); - initial_global_state = nullptr; return res; } @@ -563,4 +622,4 @@ Checker* createCommunicationDeterminismChecker(Session& session) } } -} \ No newline at end of file +}