X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/4241b524e565e4fb4a3f1a4fa24d1d05106ee7cb..1c74d5445a84d41600a92559db3e1a4b16e7bc57:/src/mc/CommunicationDeterminismChecker.cpp diff --git a/src/mc/CommunicationDeterminismChecker.cpp b/src/mc/CommunicationDeterminismChecker.cpp index b30b312d48..2449b6cdda 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,11 @@ 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,23 +48,17 @@ 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) + 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); @@ -97,143 +93,146 @@ 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, + 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::kernel::activity::Comm* comm = temp_comm.getBuffer(); - 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_actor_t src_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(comm->src_proc)); + smx_actor_t dst_proc = mc_model_checker->process().resolveActor(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 == -1 && comm.comm.src_buff != nullptr) { + comm_pattern->src_host = MC_smx_actor_get_host_name(src_proc); + comm_pattern->dst_host = MC_smx_actor_get_host_name(dst_proc); + 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)); - comm_pattern->data_size = buff_size; - comm_pattern->data = xbt_malloc0(comm_pattern->data_size); + &buff_size, remote(comm->dst_buff_size)); + comm_pattern->data.resize(buff_size); mc_model_checker->process().read_bytes( - comm_pattern->data, comm_pattern->data_size, - remote(comm.comm.src_buff)); + comm_pattern->data.data(), comm_pattern->data.size(), + remote(comm->src_buff)); } } -static void deterministic_comm_pattern(int process, mc_comm_pattern_t comm, int backtracking) { +namespace simgrid { +namespace mc { - mc_list_comm_pattern_t list = - xbt_dynar_get_as(initial_communications_pattern, process, mc_list_comm_pattern_t); +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*); 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){ - 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; - 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 - && (!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; - 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); + const smx_actor_t issuer = MC_smx_simcall_get_issuer(request); + 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); 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::kernel::activity::Comm* synchro = + static_cast(temp_synchro.getBuffer()); 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_smx_resolve_process(synchro.comm.src_proc)->pid; - pattern->src_host = MC_smx_process_get_host_name(issuer); + pattern->src_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(synchro->src_proc))->pid; + pattern->src_host = MC_smx_actor_get_host_name(issuer); struct s_smpi_mpi_request mpi_request = mc_model_checker->process().read( (std::uint64_t) simcall_comm_isend__get__data(request)); 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); + if (synchro->src_buff != nullptr){ + pattern->data.resize(synchro->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->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 */ - 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; } } 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; @@ -241,39 +240,48 @@ 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::kernel::activity::Comm* comm = temp_comm.getBuffer(); 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_smx_resolve_process(synchro.comm.dst_proc)->pid; - pattern->dst_host = MC_smx_process_get_host_name(issuer); + pattern->dst_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(comm->dst_proc))->pid; + pattern->dst_host = MC_smx_actor_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, simgrid::mc::RemotePtr 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 */ 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; 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; } @@ -281,25 +289,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 (!simgrid::mc::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) { @@ -311,91 +313,91 @@ CommunicationDeterminismChecker::~CommunicationDeterminismChecker() } -// TODO, deduplicate with SafetyChecker RecordTrace CommunicationDeterminismChecker::getRecordTrace() // override { RecordTrace 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)); - } - + for (auto const& state : stack_) + res.push_back(state->getTransition()); return res; } -// TODO, deduplicate with SafetyChecker std::vector CommunicationDeterminismChecker::getTextualTrace() // 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); - } + 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 res; + return trace; +} + +void CommunicationDeterminismChecker::logState() // override +{ + 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); + } + 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(new simgrid::mc::State(++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); + /* Get an enabled actor and insert it in the interleave set of the initial state */ + for (auto& actor : mc_model_checker->process().actors()) + if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer())) + initial_state->interleave(actor.copy.getBuffer()); - xbt_fifo_unshift(mc_stack, initial_state); + stack_.push_back(std::move(initial_state)); } static inline bool all_communications_are_finished() { - for (size_t current_process = 1; current_process < MC_smx_get_maxpid(); current_process++) { - xbt_dynar_t pattern = xbt_dynar_get_as( - incomplete_communications_pattern, current_process, xbt_dynar_t); + for (size_t current_actor = 1; current_actor < MC_smx_get_maxpid(); current_actor++) { + xbt_dynar_t pattern = xbt_dynar_get_as(incomplete_communications_pattern, current_actor, xbt_dynar_t); if (!xbt_dynar_is_empty(pattern)) { XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited."); return false; @@ -404,42 +406,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); + + /* 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_actor_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++; + } +} - char *req_str = nullptr; - int value; +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; @@ -447,61 +497,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(new simgrid::mc::State(++expandedStatesCount_)); /* If comm determinism verification, we cannot stop the exploration if - some communications are not finished (at least, data are transfered). + some communications are not finished (at least, data are transferred). 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); + /* Get enabled actors and insert them in the interleave set of the next state */ + for (auto& actor : mc_model_checker->process().actors()) + if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer())) + next_state->interleave(actor.copy.getBuffer()); 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); - - xbt_fifo_unshift(mc_stack, 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 (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; @@ -511,55 +564,55 @@ 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 = 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; } +Checker* createCommunicationDeterminismChecker(Session& session) +{ + return new CommunicationDeterminismChecker(session); +} + +} } -} \ No newline at end of file