X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/39657d7de68ca06c1c3064d52c025aacdd8a9add..30aafed5b1b68a0248307e0f2161d7d838e562e3:/src/mc/CommunicationDeterminismChecker.cpp diff --git a/src/mc/CommunicationDeterminismChecker.cpp b/src/mc/CommunicationDeterminismChecker.cpp index e5b383d922..e183c7d07c 100644 --- a/src/mc/CommunicationDeterminismChecker.cpp +++ b/src/mc/CommunicationDeterminismChecker.cpp @@ -116,7 +116,10 @@ static void update_comm_pattern(simgrid::mc::PatternCommunication* comm_pattern, } } -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*); @@ -127,37 +130,36 @@ static void deterministic_comm_pattern(int process, simgrid::mc::PatternCommunic 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); + 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{ - 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); + 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 +169,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( @@ -208,7 +210,7 @@ void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type remote(synchro.comm.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 +218,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++; @@ -253,7 +255,9 @@ 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, smx_synchro_t comm_addr, unsigned int issuer, int backtracking) +{ simgrid::mc::PatternCommunication* current_comm_pattern; unsigned int cursor = 0; std::unique_ptr comm_pattern; @@ -279,22 +283,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 +328,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", mc_stats->expanded_states); - 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("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"); + 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() @@ -376,7 +372,7 @@ 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 *********"); @@ -402,6 +398,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 +465,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 +481,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 +492,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); @@ -455,17 +502,18 @@ 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). 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(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()) @@ -492,8 +540,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", @@ -518,7 +566,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()); @@ -539,20 +587,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; }