X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/7e096d5d713b2a0704d0eed9fedea477c12d35a8..9cc0d42f835e6aa5ea5195a346098e74b0376927:/src/mc/CommunicationDeterminismChecker.cpp diff --git a/src/mc/CommunicationDeterminismChecker.cpp b/src/mc/CommunicationDeterminismChecker.cpp index 1fec4ed1d5..4588869070 100644 --- a/src/mc/CommunicationDeterminismChecker.cpp +++ b/src/mc/CommunicationDeterminismChecker.cpp @@ -35,7 +35,7 @@ xbt_dynar_t incomplete_communications_pattern; /********** Static functions ***********/ -static e_mc_comm_pattern_difference_t compare_comm_pattern(mc_comm_pattern_t comm1, mc_comm_pattern_t 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) @@ -53,7 +53,7 @@ static e_mc_comm_pattern_difference_t compare_comm_pattern(mc_comm_pattern_t com return NONE_DIFF; } -static char* print_determinism_result(e_mc_comm_pattern_difference_t diff, int process, mc_comm_pattern_t comm, unsigned int cursor) { +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) @@ -91,7 +91,7 @@ static char* print_determinism_result(e_mc_comm_pattern_difference_t diff, int p return res; } -static void update_comm_pattern(mc_comm_pattern_t comm_pattern, smx_synchro_t comm_addr) +static void update_comm_pattern(simgrid::mc::PatternCommunication* comm_pattern, smx_synchro_t comm_addr) { s_smx_synchro_t comm; mc_model_checker->process().read(&comm, remote(comm_addr)); @@ -113,16 +113,14 @@ static void update_comm_pattern(mc_comm_pattern_t comm_pattern, smx_synchro_t co } } -static void deterministic_comm_pattern(int process, mc_comm_pattern_t comm, int backtracking) { +static void deterministic_comm_pattern(int process, simgrid::mc::PatternCommunication* comm, int backtracking) { - mc_list_comm_pattern_t list = - xbt_dynar_get_as(initial_communications_pattern, process, mc_list_comm_pattern_t); + simgrid::mc::PatternCommunicationList* list = + xbt_dynar_get_as(initial_communications_pattern, process, simgrid::mc::PatternCommunicationList*); if(!backtracking){ - mc_comm_pattern_t initial_comm = - xbt_dynar_get_as(list->list, list->index_comm, mc_comm_pattern_t); e_mc_comm_pattern_difference_t diff = - compare_comm_pattern(initial_comm, comm); + compare_comm_pattern(list->list[list->index_comm].get(), comm); if (diff != NONE_DIFF) { if (comm->type == SIMIX_COMM_SEND){ @@ -162,9 +160,6 @@ static void deterministic_comm_pattern(int process, mc_comm_pattern_t comm, int } } } - - delete comm; - } /********** Non Static functions ***********/ @@ -172,12 +167,14 @@ static void deterministic_comm_pattern(int process, mc_comm_pattern_t comm, int void MC_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); - mc_list_comm_pattern_t initial_pattern = xbt_dynar_get_as( - initial_communications_pattern, issuer->pid, mc_list_comm_pattern_t); + simgrid::mc::PatternCommunicationList* initial_pattern = xbt_dynar_get_as( + initial_communications_pattern, issuer->pid, simgrid::mc::PatternCommunicationList*); xbt_dynar_t incomplete_pattern = xbt_dynar_get_as( incomplete_communications_pattern, issuer->pid, xbt_dynar_t); - mc_comm_pattern_t pattern = new s_mc_comm_pattern_t(); + std::unique_ptr pattern = + std::unique_ptr( + new simgrid::mc::PatternCommunication()); pattern->index = initial_pattern->index_comm + xbt_dynar_length(incomplete_pattern); @@ -209,16 +206,15 @@ void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type if(mpi_request.detached){ if (!simgrid::mc::initial_global_state->initial_communications_pattern_done) { /* Store comm pattern */ - xbt_dynar_push( - xbt_dynar_get_as( - initial_communications_pattern, pattern->src_proc, mc_list_comm_pattern_t - )->list, - &pattern); + simgrid::mc::PatternCommunicationList* list = xbt_dynar_get_as( + initial_communications_pattern, pattern->src_proc, + simgrid::mc::PatternCommunicationList*); + list->list.push_back(std::move(pattern)); } else { /* Evaluate comm determinism */ - deterministic_comm_pattern(pattern->src_proc, pattern, backtracking); + deterministic_comm_pattern(pattern->src_proc, pattern.get(), backtracking); xbt_dynar_get_as( - initial_communications_pattern, pattern->src_proc, mc_list_comm_pattern_t + initial_communications_pattern, pattern->src_proc, simgrid::mc::PatternCommunicationList* )->index_comm++; } return; @@ -244,17 +240,18 @@ void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type } else xbt_die("Unexpected call_type %i", (int) call_type); - xbt_dynar_push( - xbt_dynar_get_as(incomplete_communications_pattern, issuer->pid, xbt_dynar_t), - &pattern); - - XBT_DEBUG("Insert incomplete comm pattern %p for process %lu", pattern, issuer->pid); + XBT_DEBUG("Insert incomplete comm pattern %p for process %lu", + pattern.get(), issuer->pid); + xbt_dynar_t dynar = + xbt_dynar_get_as(incomplete_communications_pattern, issuer->pid, xbt_dynar_t); + simgrid::mc::PatternCommunication* pattern2 = pattern.release(); + xbt_dynar_push(dynar, &pattern2); } void MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigned int issuer, int backtracking) { - mc_comm_pattern_t current_comm_pattern; + simgrid::mc::PatternCommunication* current_comm_pattern; unsigned int cursor = 0; - mc_comm_pattern_t comm_pattern; + std::unique_ptr comm_pattern; int completed = 0; /* Complete comm pattern */ @@ -262,9 +259,11 @@ void MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigne if (current_comm_pattern->comm_addr == comm_addr) { update_comm_pattern(current_comm_pattern, comm_addr); completed = 1; + simgrid::mc::PatternCommunication* temp; xbt_dynar_remove_at( xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t), - cursor, &comm_pattern); + cursor, &temp); + comm_pattern = std::unique_ptr(temp); XBT_DEBUG("Remove incomplete comm pattern for process %u at cursor %u", issuer, cursor); break; } @@ -272,15 +271,15 @@ void MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigne if(!completed) xbt_die("Corresponding communication not found!"); - mc_list_comm_pattern_t pattern = xbt_dynar_get_as( - initial_communications_pattern, issuer, mc_list_comm_pattern_t); + 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) /* Store comm pattern */ - xbt_dynar_push(pattern->list, &comm_pattern); + pattern->list.push_back(std::move(comm_pattern)); else { /* Evaluate comm determinism */ - deterministic_comm_pattern(issuer, comm_pattern, backtracking); + deterministic_comm_pattern(issuer, comm_pattern.get(), backtracking); pattern->index_comm++; } } @@ -302,30 +301,22 @@ 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->getRecordElement()); 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->req_num, simgrid::mc::RequestType::executed)); } return trace; } @@ -337,18 +328,16 @@ void CommunicationDeterminismChecker::prepare() const int maxpid = MC_smx_get_maxpid(); // Create initial_communications_pattern elements: - initial_communications_pattern = simgrid::xbt::newDeleteDynar(); + initial_communications_pattern = simgrid::xbt::newDeleteDynar(); for (i=0; i < maxpid; i++){ - mc_list_comm_pattern_t process_list_pattern = new s_mc_list_comm_pattern_t(); - process_list_pattern->list = simgrid::xbt::newDeleteDynar(); - process_list_pattern->index_comm = 0; + simgrid::mc::PatternCommunicationList* process_list_pattern = new simgrid::mc::PatternCommunicationList(); xbt_dynar_insert_at(initial_communications_pattern, i, &process_list_pattern); } // Create incomplete_communications_pattern elements: incomplete_communications_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp); for (i=0; i < maxpid; i++){ - xbt_dynar_t process_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), nullptr); + xbt_dynar_t process_pattern = xbt_dynar_new(sizeof(simgrid::mc::PatternCommunication*), nullptr); xbt_dynar_insert_at(incomplete_communications_pattern, i, &process_pattern); } @@ -363,7 +352,7 @@ void CommunicationDeterminismChecker::prepare() /* 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)); } @@ -384,7 +373,6 @@ bool all_communications_are_finished() int CommunicationDeterminismChecker::main(void) { - int value; std::unique_ptr visited_state = nullptr; smx_simcall_t req = nullptr; @@ -402,18 +390,19 @@ int CommunicationDeterminismChecker::main(void) mc_stats->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->req_num; + 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++; /* TODO : handle test and testany simcalls */ @@ -422,12 +411,12 @@ 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 */ + simgrid::mc::handle_simcall(req, req_num); /* 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(); @@ -449,7 +438,7 @@ int CommunicationDeterminismChecker::main(void) /* 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",