X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/ccb2167210583f3eb1249db10916cfd7389cb0df..30aafed5b1b68a0248307e0f2161d7d838e562e3:/src/mc/CommunicationDeterminismChecker.cpp diff --git a/src/mc/CommunicationDeterminismChecker.cpp b/src/mc/CommunicationDeterminismChecker.cpp index 9f7c2a2e18..e183c7d07c 100644 --- a/src/mc/CommunicationDeterminismChecker.cpp +++ b/src/mc/CommunicationDeterminismChecker.cpp @@ -8,7 +8,6 @@ #include #include -#include #include #include @@ -22,6 +21,8 @@ #include "src/mc/Client.hpp" #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; @@ -35,10 +36,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; @@ -46,20 +47,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) @@ -97,94 +92,94 @@ 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)); - 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); 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) { +namespace simgrid { +namespace mc { + +void CommunicationDeterminismChecker::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){ - initial_global_state->send_deterministic = 0; - if(initial_global_state->send_diff != nullptr) - xbt_free(initial_global_state->send_diff); - 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{ - initial_global_state->recv_deterministic = 0; - if(initial_global_state->recv_diff != nullptr) - xbt_free(initial_global_state->recv_diff); - 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 && !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", initial_global_state->send_diff); - xbt_free(initial_global_state->send_diff); - initial_global_state->send_diff = nullptr; - MC_print_statistics(mc_stats); + 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 && (!initial_global_state->send_deterministic && !initial_global_state->recv_deterministic)) { + }else if(_sg_mc_comms_determinism + && (!this->send_deterministic && !this->recv_deterministic)) { XBT_INFO("****************************************************"); XBT_INFO("***** Non-deterministic communications pattern *****"); XBT_INFO("****************************************************"); - XBT_INFO("%s", initial_global_state->send_diff); - XBT_INFO("%s", initial_global_state->recv_diff); - xbt_free(initial_global_state->send_diff); - initial_global_state->send_diff = nullptr; - xbt_free(initial_global_state->recv_diff); - initial_global_state->recv_diff = nullptr; - MC_print_statistics(mc_stats); + 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); } } } - - MC_comm_pattern_free(comm); - } /********** 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); - 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); @@ -199,7 +194,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 = @@ -208,24 +204,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 (!initial_global_state->initial_communications_pattern_done) { + if (!this->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); + this->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; @@ -246,22 +241,26 @@ 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); - 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; + +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; - mc_comm_pattern_t comm_pattern; + std::unique_ptr comm_pattern; int completed = 0; /* Complete comm pattern */ @@ -269,9 +268,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; } @@ -279,25 +280,19 @@ 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 (!initial_global_state->initial_communications_pattern_done) + if (!this->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); + this->deterministic_comm_pattern(issuer, comm_pattern.get(), backtracking); pattern->index_comm++; } } - -/************************ Main algorithm ************************/ - -namespace simgrid { -namespace mc { - CommunicationDeterminismChecker::CommunicationDeterminismChecker(Session& session) : Checker(session) { @@ -309,83 +304,84 @@ CommunicationDeterminismChecker::~CommunicationDeterminismChecker() } -// TODO, deduplicate with SafetyChecker RecordTrace CommunicationDeterminismChecker::getRecordTrace() // override { RecordTrace res; + for (auto const& state : stack_) + res.push_back(state->getTransition()); + return res; +} - xbt_fifo_item_t start = xbt_fifo_get_last_item(mc_stack); - for (xbt_fifo_item_t item = start; item; item = xbt_fifo_get_prev_item(item)) { - - // Find (pid, value): - simgrid::mc::State* state = (simgrid::mc::State*) xbt_fifo_get_item_content(item); - 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)); +std::vector CommunicationDeterminismChecker::getTextualTrace() // override +{ + std::vector trace; + for (auto const& state : stack_) { + smx_simcall_t req = &state->executed_req; + if (req) + trace.push_back(simgrid::mc::request_to_string( + req, state->transition.argument, simgrid::mc::RequestType::executed)); } - - return std::move(res); + return trace; } -// TODO, deduplicate with SafetyChecker -std::vector CommunicationDeterminismChecker::getTextualTrace() // override +void CommunicationDeterminismChecker::logState() // override { - std::vector res; - for (xbt_fifo_item_t item = xbt_fifo_get_last_item(mc_stack); - item; item = xbt_fifo_get_prev_item(item)) { - simgrid::mc::State* state = (simgrid::mc::State*)xbt_fifo_get_item_content(item); - 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); - res.push_back(req_str); - xbt_free(req_str); - } + Checker::logState(); + if (_sg_mc_comms_determinism && + !this->recv_deterministic && + this->send_deterministic) { + XBT_INFO("******************************************************"); + XBT_INFO("**** Only-send-deterministic communication pattern ****"); + XBT_INFO("******************************************************"); + XBT_INFO("%s", this->recv_diff); + } else if(_sg_mc_comms_determinism && + !this->send_deterministic && + this->recv_deterministic) { + XBT_INFO("******************************************************"); + XBT_INFO("**** Only-recv-deterministic communication pattern ****"); + XBT_INFO("******************************************************"); + XBT_INFO("%s", this->send_diff); } - return std::move(res); + 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", + !this->recv_deterministic ? "No" : "Yes"); } void CommunicationDeterminismChecker::prepare() { - simgrid::mc::State* initial_state = nullptr; + int i; const int maxpid = MC_smx_get_maxpid(); - simgrid::mc::visited_states.clear(); - // 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(++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, &p.copy); + initial_state->interleave(&p.copy); - xbt_fifo_unshift(mc_stack, initial_state); + stack_.push_back(std::move(initial_state)); } static inline @@ -402,42 +398,90 @@ bool all_communications_are_finished() return true; } -int CommunicationDeterminismChecker::main(void) +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); - char *req_str = nullptr; - int value; + /* 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; smx_simcall_t req = nullptr; - simgrid::mc::State* state = nullptr; - simgrid::mc::State* next_state = nullptr; - while (xbt_fifo_size(mc_stack) > 0) { + while (!stack_.empty()) { /* Get current state */ - state = (simgrid::mc::State*) xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack)); + simgrid::mc::State* state = stack_.back().get(); XBT_DEBUG("**************************************************"); - XBT_DEBUG("Exploration depth = %d (state = %d, interleaved processes = %d)", - xbt_fifo_size(mc_stack), state->num, - MC_state_interleave_size(state)); + XBT_DEBUG("Exploration depth = %zi (state = %d, interleaved processes = %zd)", + stack_.size(), state->num, + state->interleaveSize()); /* Update statistics */ - mc_stats->visited_states++; + mc_model_checker->visited_states++; - if ((xbt_fifo_size(mc_stack) <= _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->transition.argument; + + 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++; + mc_model_checker->executed_transitions++; /* TODO : handle test and testany simcalls */ e_mc_call_type_t call = MC_CALL_TYPE_NONE; @@ -445,61 +489,64 @@ 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); + 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, 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(++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 = simgrid::mc::is_visited_state(next_state, compare_snapshots)) == nullptr) { + if (_sg_mc_visited == 0 + || (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, &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); + state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str.c_str()); - xbt_fifo_unshift(mc_stack, next_state); - - if (dot_output != nullptr) - xbt_free(req_str); + stack_.push_back(std::move(next_state)); } else { - if (xbt_fifo_size(mc_stack) > _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); else - XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack)); + 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_fifo_shift(mc_stack); - MC_state_delete(state, !state->in_visited_states ? 1 : 0); - XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1); + XBT_DEBUG("Delete state %d at depth %zi", + state->num, stack_.size()); + stack_.pop_back(); visited_state = nullptr; @@ -509,52 +556,54 @@ int CommunicationDeterminismChecker::main(void) return SIMGRID_MC_EXIT_DEADLOCK; } - while ((state = (simgrid::mc::State*) xbt_fifo_shift(mc_stack)) != nullptr) - if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) { + while (!stack_.empty()) { + std::unique_ptr state = std::move(stack_.back()); + stack_.pop_back(); + 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 %d", state->num, xbt_fifo_size(mc_stack) + 1); - xbt_fifo_unshift(mc_stack, state); + XBT_DEBUG("Back-tracking to state %d at depth %zi", + state->num, stack_.size() + 1); + stack_.push_back(std::move(state)); - MC_replay(mc_stack); + this->restoreState(); - XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack)); + XBT_DEBUG("Back-tracking to state %d at depth %zi done", + stack_.back()->num, stack_.size()); break; } else { - XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1); - MC_state_delete(state, !state->in_visited_states ? 1 : 0); + XBT_DEBUG("Delete state %d at depth %zi", + state->num, stack_.size() + 1); } - + } } } - MC_print_statistics(mc_stats); + simgrid::mc::session->logState(); return SIMGRID_MC_EXIT_SUCCESS; } 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(); - - /* Create exploration stack */ - mc_stack = xbt_fifo_new(); + simgrid::mc::session->initialize(); this->prepare(); - initial_global_state = xbt_new0(s_mc_global_t, 1); - 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; - return this->main(); + int res = this->main(); + return res; +} + +Checker* createCommunicationDeterminismChecker(Session& session) +{ + return new CommunicationDeterminismChecker(session); } }