X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/f7a4833f1a704ef0be1ef00f9de84ad8d5975426..9cc0d42f835e6aa5ea5195a346098e74b0376927:/src/mc/CommunicationDeterminismChecker.cpp diff --git a/src/mc/CommunicationDeterminismChecker.cpp b/src/mc/CommunicationDeterminismChecker.cpp index 541a00135e..4588869070 100644 --- a/src/mc/CommunicationDeterminismChecker.cpp +++ b/src/mc/CommunicationDeterminismChecker.cpp @@ -8,7 +8,6 @@ #include #include -#include #include #include @@ -36,10 +35,10 @@ 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 (strcmp(comm1->rdv, comm2->rdv) != 0) + if (comm1->rdv != comm2->rdv) return RDV_DIFF; if (comm1->src_proc != comm2->src_proc) return SRC_PROC_DIFF; @@ -47,20 +46,14 @@ static e_mc_comm_pattern_difference_t compare_comm_pattern(mc_comm_pattern_t com return DST_PROC_DIFF; if (comm1->tag != comm2->tag) return TAG_DIFF; - if (comm1->data_size != comm2->data_size) + if (comm1->data.size() != comm2->data.size()) return DATA_SIZE_DIFF; - if(comm1->data == nullptr && comm2->data == NULL) - return NONE_DIFF; - if(comm1->data != nullptr && comm2->data !=NULL) { - if (!memcmp(comm1->data, comm2->data, comm1->data_size)) - return NONE_DIFF; - return DATA_DIFF; - } else + if (comm1->data != comm2->data) return DATA_DIFF; 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) @@ -98,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)); @@ -109,28 +102,25 @@ static void update_comm_pattern(mc_comm_pattern_t comm_pattern, smx_synchro_t co 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 == -1 && comm.comm.src_buff != nullptr) { + if (comm_pattern->data.size() == 0 && comm.comm.src_buff != nullptr) { size_t buff_size; mc_model_checker->process().read( &buff_size, remote(comm.comm.dst_buff_size)); - comm_pattern->data_size = buff_size; - comm_pattern->data = xbt_malloc0(comm_pattern->data_size); + comm_pattern->data.resize(buff_size); mc_model_checker->process().read_bytes( - comm_pattern->data, comm_pattern->data_size, + comm_pattern->data.data(), comm_pattern->data.size(), remote(comm.comm.src_buff)); } } -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){ @@ -170,9 +160,6 @@ static void deterministic_comm_pattern(int process, mc_comm_pattern_t comm, int } } } - - MC_comm_pattern_free(comm); - } /********** Non Static functions ***********/ @@ -180,14 +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 = xbt_new0(s_mc_comm_pattern_t, 1); - pattern->data_size = -1; - pattern->data = nullptr; + std::unique_ptr pattern = + std::unique_ptr( + new simgrid::mc::PatternCommunication()); pattern->index = initial_pattern->index_comm + xbt_dynar_length(incomplete_pattern); @@ -211,24 +198,23 @@ void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type pattern->tag = mpi_request.tag; if(synchro.comm.src_buff != nullptr){ - pattern->data_size = synchro.comm.src_buff_size; - pattern->data = xbt_malloc0(pattern->data_size); + pattern->data.resize(synchro.comm.src_buff_size); mc_model_checker->process().read_bytes( - pattern->data, pattern->data_size, remote(synchro.comm.src_buff)); + pattern->data.data(), pattern->data.size(), + remote(synchro.comm.src_buff)); } 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; @@ -254,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 */ @@ -272,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; } @@ -282,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++; } } @@ -312,60 +301,48 @@ CommunicationDeterminismChecker::~CommunicationDeterminismChecker() } -// TODO, deduplicate with SafetyChecker RecordTrace CommunicationDeterminismChecker::getRecordTrace() // override { RecordTrace res; - for (simgrid::mc::State* state : stack_) { - int value = 0; - smx_simcall_t saved_req = MC_state_get_executed_request(state, &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 (simgrid::mc::State* state : stack_) { - int value; - smx_simcall_t req = MC_state_get_executed_request(state, &value); - if (req) { - char* req_str = simgrid::mc::request_to_string( - req, value, simgrid::mc::RequestType::executed); - trace.push_back(req_str); - xbt_free(req_str); - } + for (auto const& state : stack_) { + 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)); } return trace; } void CommunicationDeterminismChecker::prepare() { - simgrid::mc::State* initial_state = nullptr; + int i; const int maxpid = MC_smx_get_maxpid(); // Create initial_communications_pattern elements: - initial_communications_pattern = xbt_dynar_new(sizeof(mc_list_comm_pattern_t), MC_list_comm_pattern_free_voidp); + initial_communications_pattern = simgrid::xbt::newDeleteDynar(); for (i=0; i < maxpid; i++){ - mc_list_comm_pattern_t process_list_pattern = xbt_new0(s_mc_list_comm_pattern_t, 1); - process_list_pattern->list = xbt_dynar_new(sizeof(mc_comm_pattern_t), MC_comm_pattern_free_voidp); - 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); } - initial_state = MC_state_new(); + std::unique_ptr initial_state = + std::unique_ptr(MC_state_new()); XBT_DEBUG("********* Start communication determinism verification *********"); @@ -375,9 +352,9 @@ 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, &p.copy); + initial_state->interleave(&p.copy); - stack_.push_back(initial_state); + stack_.push_back(std::move(initial_state)); } static inline @@ -396,38 +373,36 @@ bool all_communications_are_finished() int CommunicationDeterminismChecker::main(void) { - - char *req_str = nullptr; - int value; std::unique_ptr visited_state = nullptr; smx_simcall_t req = nullptr; - simgrid::mc::State* next_state = nullptr; while (!stack_.empty()) { /* Get current state */ - simgrid::mc::State* state = stack_.back(); + simgrid::mc::State* state = stack_.back().get(); XBT_DEBUG("**************************************************"); - XBT_DEBUG("Exploration depth = %zi (state = %d, interleaved processes = %d)", + XBT_DEBUG("Exploration depth = %zi (state = %d, interleaved processes = %zd)", stack_.size(), state->num, - MC_state_interleave_size(state)); + state->interleaveSize()); /* Update statistics */ mc_stats->visited_states++; - if (stack_.size() <= _sg_mc_max_depth - && (req = MC_state_get_request(state, &value)) + if (stack_.size() <= (std::size_t) _sg_mc_max_depth + && (req = MC_state_get_request(state)) != nullptr && (visited_state == nullptr)) { - req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix); - XBT_DEBUG("Execute: %s", req_str); - xbt_free(req_str); + int req_num = state->req_num; + XBT_DEBUG("Execute: %s", + simgrid::mc::request_to_string( + 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 */ @@ -436,18 +411,19 @@ 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(); /* Create the new expanded state */ - next_state = MC_state_new(); + std::unique_ptr next_state = + std::unique_ptr(MC_state_new()); /* If comm determinism verification, we cannot stop the exploration if some communications are not finished (at least, data are transfered). @@ -456,28 +432,27 @@ int CommunicationDeterminismChecker::main(void) bool compare_snapshots = all_communications_are_finished() && initial_global_state->initial_communications_pattern_done; - if (_sg_mc_visited == 0 || (visited_state = visitedStates_.addVisitedState(next_state, compare_snapshots)) == nullptr) { + if (_sg_mc_visited == 0 + || (visited_state = visitedStates_.addVisitedState(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, &p.copy); + next_state->interleave(&p.copy); if (dot_output != nullptr) - fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str); + fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", + state->num, next_state->num, req_str.c_str()); } else if (dot_output != nullptr) fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", - state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str); - - stack_.push_back(next_state); + state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str.c_str()); - if (dot_output != nullptr) - xbt_free(req_str); + stack_.push_back(std::move(next_state)); } else { - if (stack_.size() > _sg_mc_max_depth) + if (stack_.size() > (std::size_t) _sg_mc_max_depth) XBT_WARN("/!\\ Max depth reached ! /!\\ "); else if (visited_state != nullptr) XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.", visited_state->other_num == -1 ? visited_state->num : visited_state->other_num); @@ -489,10 +464,9 @@ int CommunicationDeterminismChecker::main(void) initial_global_state->initial_communications_pattern_done = 1; /* Trash the current state, no longer needed */ - stack_.pop_back(); - MC_state_delete(state, !state->in_visited_states ? 1 : 0); XBT_DEBUG("Delete state %d at depth %zi", - state->num, stack_.size() + 1); + state->num, stack_.size()); + stack_.pop_back(); visited_state = nullptr; @@ -503,25 +477,24 @@ int CommunicationDeterminismChecker::main(void) } while (!stack_.empty()) { - simgrid::mc::State* state = stack_.back(); + std::unique_ptr state = std::move(stack_.back()); stack_.pop_back(); - if (MC_state_interleave_size(state) - && stack_.size() < _sg_mc_max_depth) { + if (state->interleaveSize() + && stack_.size() < (std::size_t) _sg_mc_max_depth) { /* We found a back-tracking point, let's loop */ XBT_DEBUG("Back-tracking to state %d at depth %zi", state->num, stack_.size() + 1); - stack_.push_back(state); + stack_.push_back(std::move(state)); simgrid::mc::replay(stack_); XBT_DEBUG("Back-tracking to state %d at depth %zi done", - state->num, stack_.size()); + stack_.back()->num, stack_.size()); break; } else { XBT_DEBUG("Delete state %d at depth %zi", state->num, stack_.size() + 1); - MC_state_delete(state, !state->in_visited_states ? 1 : 0); } } } @@ -536,10 +509,6 @@ int CommunicationDeterminismChecker::run() XBT_INFO("Check communication determinism"); mc_model_checker->wait_for_requests(); - if (mc_mode == MC_MODE_CLIENT) - // This will move somehwere else: - simgrid::mc::Client::get()->handleMessages(); - this->prepare(); initial_global_state = std::unique_ptr(new s_mc_global_t()); @@ -555,5 +524,10 @@ int CommunicationDeterminismChecker::run() return res; } +Checker* createCommunicationDeterminismChecker(Session& session) +{ + return new CommunicationDeterminismChecker(session); +} + } } \ No newline at end of file