X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/26af220e017a088b56105b2f21fadecf7d6e2a88..873fe7743b2a9f2eddc53ed3383bdd74bb3fe226:/src/mc/mc_comm_determinism.cpp diff --git a/src/mc/mc_comm_determinism.cpp b/src/mc/mc_comm_determinism.cpp index bede55833d..7e7d2b1814 100644 --- a/src/mc/mc_comm_determinism.cpp +++ b/src/mc/mc_comm_determinism.cpp @@ -1,23 +1,34 @@ -/* Copyright (c) 2008-2014. The SimGrid Team. +/* Copyright (c) 2008-2015. The SimGrid Team. * All rights reserved. */ /* This program is free software; you can redistribute it and/or modify it * under the terms of the license (GNU LGPL) which comes with this package. */ -#include "mc_state.h" -#include "mc_comm_pattern.h" -#include "mc_request.h" -#include "mc_safety.h" -#include "mc_private.h" -#include "mc_record.h" -#include "mc_smx.h" -#include "mc_client.h" +#include -extern "C" { +#include +#include +#include +#include +#include + +#include "src/mc/mc_state.h" +#include "src/mc/mc_comm_pattern.h" +#include "src/mc/mc_request.h" +#include "src/mc/mc_safety.h" +#include "src/mc/mc_private.h" +#include "src/mc/mc_record.h" +#include "src/mc/mc_smx.h" +#include "src/mc/Client.hpp" +#include "src/mc/mc_exit.h" + +using simgrid::mc::remote; XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_comm_determinism, mc, "Logging specific to MC communication determinism detection"); +extern "C" { + /********** Global variables **********/ xbt_dynar_t initial_communications_pattern; @@ -38,15 +49,14 @@ static e_mc_comm_pattern_difference_t compare_comm_pattern(mc_comm_pattern_t com return TAG_DIFF; if (comm1->data_size != comm2->data_size) return DATA_SIZE_DIFF; - if(comm1->data == NULL && comm2->data == NULL) + if(comm1->data == nullptr && comm2->data == NULL) return NONE_DIFF; - if(comm1->data != NULL && comm2->data !=NULL) { + if(comm1->data != nullptr && comm2->data !=NULL) { if (!memcmp(comm1->data, comm2->data, comm1->data_size)) return NONE_DIFF; return DATA_DIFF; - }else{ + } else return DATA_DIFF; - } return NONE_DIFF; } @@ -81,7 +91,7 @@ static char* print_determinism_result(e_mc_comm_pattern_difference_t diff, int p res = bprintf("%s\n Different data for communication #%d", type, cursor); break; default: - res = NULL; + res = nullptr; break; } @@ -91,8 +101,7 @@ static char* print_determinism_result(e_mc_comm_pattern_difference_t diff, int p static void update_comm_pattern(mc_comm_pattern_t comm_pattern, smx_synchro_t comm_addr) { s_smx_synchro_t comm; - MC_process_read_simple(&mc_model_checker->process(), - &comm, comm_addr, sizeof(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); @@ -100,14 +109,15 @@ 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 != NULL) { + if (comm_pattern->data_size == -1 && comm.comm.src_buff != nullptr) { size_t buff_size; - MC_process_read_simple(&mc_model_checker->process(), - &buff_size, comm.comm.dst_buff_size, sizeof(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); - MC_process_read_simple(&mc_model_checker->process(), - comm_pattern->data, comm.comm.src_buff, comm_pattern->data_size); + mc_model_checker->process().read_bytes( + comm_pattern->data, comm_pattern->data_size, + remote(comm.comm.src_buff)); } } @@ -125,12 +135,12 @@ static void deterministic_comm_pattern(int process, mc_comm_pattern_t comm, int if (diff != NONE_DIFF) { if (comm->type == SIMIX_COMM_SEND){ initial_global_state->send_deterministic = 0; - if(initial_global_state->send_diff != NULL) + 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); }else{ initial_global_state->recv_deterministic = 0; - if(initial_global_state->recv_diff != NULL) + 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); } @@ -140,9 +150,9 @@ static void deterministic_comm_pattern(int process, mc_comm_pattern_t comm, int XBT_INFO("*********************************************************"); XBT_INFO("%s", initial_global_state->send_diff); xbt_free(initial_global_state->send_diff); - initial_global_state->send_diff = NULL; + initial_global_state->send_diff = nullptr; MC_print_statistics(mc_stats); - xbt_abort(); + 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)) { XBT_INFO("****************************************************"); XBT_INFO("***** Non-deterministic communications pattern *****"); @@ -150,11 +160,11 @@ static void deterministic_comm_pattern(int process, mc_comm_pattern_t comm, int 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 = NULL; + initial_global_state->send_diff = nullptr; xbt_free(initial_global_state->recv_diff); - initial_global_state->recv_diff = NULL; + initial_global_state->recv_diff = nullptr; MC_print_statistics(mc_stats); - xbt_abort(); + mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM); } } } @@ -175,7 +185,7 @@ void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type mc_comm_pattern_t pattern = xbt_new0(s_mc_comm_pattern_t, 1); pattern->data_size = -1; - pattern->data = NULL; + pattern->data = nullptr; pattern->index = initial_pattern->index_comm + xbt_dynar_length(incomplete_pattern); @@ -184,30 +194,25 @@ void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type pattern->type = SIMIX_COMM_SEND; pattern->comm_addr = simcall_comm_isend__get__result(request); - s_smx_synchro_t synchro; - MC_process_read_simple(&mc_model_checker->process(), - &synchro, pattern->comm_addr, sizeof(synchro)); + s_smx_synchro_t synchro = mc_model_checker->process().read( + (std::uint64_t) pattern->comm_addr); - char* remote_name; - MC_process_read_simple(&mc_model_checker->process(), &remote_name, - synchro.comm.rdv ? &synchro.comm.rdv->name : &synchro.comm.rdv_cpy->name, - sizeof(remote_name)); - pattern->rdv = - MC_process_read_string(&mc_model_checker->process(), remote_name); + 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_host = MC_smx_process_get_host_name(issuer); - struct s_smpi_mpi_request mpi_request; - MC_process_read_simple(&mc_model_checker->process(), - &mpi_request, (MPI_Request) simcall_comm_isend__get__data(request), - sizeof(mpi_request)); + 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 != NULL){ + if(synchro.comm.src_buff != nullptr){ pattern->data_size = synchro.comm.src_buff_size; pattern->data = xbt_malloc0(pattern->data_size); - MC_process_read_simple(&mc_model_checker->process(), - pattern->data, synchro.comm.src_buff, pattern->data_size); + mc_model_checker->process().read_bytes( + pattern->data, pattern->data_size, remote(synchro.comm.src_buff)); } if(mpi_request.detached){ if (!initial_global_state->initial_communications_pattern_done) { @@ -231,26 +236,21 @@ void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type pattern->comm_addr = simcall_comm_irecv__get__result(request); struct s_smpi_mpi_request mpi_request; - MC_process_read_simple(&mc_model_checker->process(), - &mpi_request, (MPI_Request) simcall_comm_irecv__get__data(request), - sizeof(mpi_request)); + mc_model_checker->process().read( + &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_process_read_simple(&mc_model_checker->process(), - &synchro, pattern->comm_addr, sizeof(synchro)); + mc_model_checker->process().read(&synchro, remote(pattern->comm_addr)); char* remote_name; - MC_process_read_simple(&mc_model_checker->process(), &remote_name, - synchro.comm.rdv ? &synchro.comm.rdv->name : &synchro.comm.rdv_cpy->name, - sizeof(remote_name)); - pattern->rdv = - MC_process_read_string(&mc_model_checker->process(), remote_name); + 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_host = MC_smx_process_get_host_name(issuer); - } else { + } 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), @@ -266,7 +266,7 @@ void MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigne int completed = 0; /* Complete comm pattern */ - xbt_dynar_foreach(xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t), cursor, current_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) { update_comm_pattern(current_comm_pattern, comm_addr); completed = 1; @@ -276,17 +276,17 @@ void MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigne XBT_DEBUG("Remove incomplete comm pattern for process %u at cursor %u", issuer, cursor); break; } - } + 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); - if (!initial_global_state->initial_communications_pattern_done) { + if (!initial_global_state->initial_communications_pattern_done) /* Store comm pattern */ xbt_dynar_push(pattern->list, &comm_pattern); - } else { + else { /* Evaluate comm determinism */ deterministic_comm_pattern(issuer, comm_pattern, backtracking); pattern->index_comm++; @@ -296,19 +296,15 @@ void MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigne /************************ Main algorithm ************************/ -static void MC_modelcheck_comm_determinism_main(void); +static int MC_modelcheck_comm_determinism_main(void); static void MC_pre_modelcheck_comm_determinism(void) { - MC_SET_MC_HEAP; - - mc_state_t initial_state = NULL; - smx_process_t process; + mc_state_t initial_state = nullptr; int i; const int maxpid = MC_smx_get_maxpid(); - if (_sg_mc_visited > 0) - visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp); + 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); @@ -322,42 +318,33 @@ static void MC_pre_modelcheck_comm_determinism(void) // 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), NULL); + xbt_dynar_t process_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), nullptr); xbt_dynar_insert_at(incomplete_communications_pattern, i, &process_pattern); } initial_state = MC_state_new(); - MC_SET_STD_HEAP; XBT_DEBUG("********* Start communication determinism verification *********"); /* Wait for requests (schedules processes) */ - MC_wait_for_requests(); - - MC_SET_MC_HEAP; + mc_model_checker->wait_for_requests(); /* Get an enabled process and insert it in the interleave set of the initial state */ - MC_EACH_SIMIX_PROCESS(process, - if (MC_process_is_enabled(process)) { - MC_state_interleave_process(initial_state, process); - } - ); + 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); xbt_fifo_unshift(mc_stack, initial_state); - - MC_SET_STD_HEAP; - } -static void MC_modelcheck_comm_determinism_main(void) +static int MC_modelcheck_comm_determinism_main(void) { - char *req_str = NULL; + char *req_str = nullptr; int value; - mc_visited_state_t visited_state = NULL; - smx_simcall_t req = NULL; - smx_process_t process = NULL; - mc_state_t state = NULL, next_state = NULL; + std::unique_ptr visited_state = nullptr; + smx_simcall_t req = nullptr; + mc_state_t state = nullptr, next_state = NULL; while (xbt_fifo_size(mc_stack) > 0) { @@ -374,82 +361,64 @@ static void MC_modelcheck_comm_determinism_main(void) if ((xbt_fifo_size(mc_stack) <= _sg_mc_max_depth) && (req = MC_state_get_request(state, &value)) - && (visited_state == NULL)) { + && (visited_state == nullptr)) { - req_str = MC_request_to_string(req, value, MC_REQUEST_SIMIX); + req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix); XBT_DEBUG("Execute: %s", req_str); xbt_free(req_str); - if (dot_output != NULL) { - MC_SET_MC_HEAP; - req_str = MC_request_get_dot_output(req, value); - MC_SET_STD_HEAP; - } + if (dot_output != nullptr) + req_str = simgrid::mc::request_get_dot_output(req, value); MC_state_set_executed_request(state, req, value); mc_stats->executed_transitions++; /* TODO : handle test and testany simcalls */ e_mc_call_type_t call = MC_CALL_TYPE_NONE; - if (_sg_mc_comms_determinism || _sg_mc_send_determinism) { + if (_sg_mc_comms_determinism || _sg_mc_send_determinism) call = MC_get_call_type(req); - } /* Answer the request */ - MC_simcall_handle(req, value); /* After this call req is no longer useful */ + simgrid::mc::handle_simcall(req, value); /* After this call req is no longer useful */ - MC_SET_MC_HEAP; if(!initial_global_state->initial_communications_pattern_done) MC_handle_comm_pattern(call, req, value, initial_communications_pattern, 0); else - MC_handle_comm_pattern(call, req, value, NULL, 0); - MC_SET_STD_HEAP; + MC_handle_comm_pattern(call, req, value, nullptr, 0); /* Wait for requests (schedules processes) */ - MC_wait_for_requests(); + mc_model_checker->wait_for_requests(); /* Create the new expanded state */ - MC_SET_MC_HEAP; - next_state = MC_state_new(); - if ((visited_state = is_visited_state(next_state)) == NULL) { + if ((visited_state = simgrid::mc::is_visited_state(next_state)) == nullptr) { /* Get enabled processes and insert them in the interleave set of the next state */ - MC_EACH_SIMIX_PROCESS(process, - if (MC_process_is_enabled(process)) { - MC_state_interleave_process(next_state, process); - } - ); + 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); - if (dot_output != NULL) + if (dot_output != nullptr) fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str); - } else { - - if (dot_output != NULL) - fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_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); - if (dot_output != NULL) + if (dot_output != nullptr) xbt_free(req_str); - MC_SET_STD_HEAP; - } else { - if (xbt_fifo_size(mc_stack) > _sg_mc_max_depth) { + if (xbt_fifo_size(mc_stack) > _sg_mc_max_depth) XBT_WARN("/!\\ Max depth reached ! /!\\ "); - } else if (visited_state != NULL) { + 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 { + else XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack)); - } - - MC_SET_MC_HEAP; if (!initial_global_state->initial_communications_pattern_done) initial_global_state->initial_communications_pattern_done = 1; @@ -459,24 +428,19 @@ static void MC_modelcheck_comm_determinism_main(void) 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); - MC_SET_STD_HEAP; - - visited_state = NULL; + visited_state = nullptr; /* Check for deadlocks */ - if (MC_deadlock_check()) { - MC_show_deadlock(NULL); - return; + if (mc_model_checker->checkDeadlock()) { + MC_show_deadlock(nullptr); + return SIMGRID_MC_EXIT_DEADLOCK; } - MC_SET_MC_HEAP; - - while ((state = (mc_state_t) xbt_fifo_shift(mc_stack)) != NULL) { + while ((state = (mc_state_t) xbt_fifo_shift(mc_stack)) != nullptr) if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack) < _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); - MC_SET_STD_HEAP; MC_replay(mc_stack); @@ -487,52 +451,37 @@ static void MC_modelcheck_comm_determinism_main(void) 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); } - } - MC_SET_STD_HEAP; } } MC_print_statistics(mc_stats); - MC_SET_STD_HEAP; - - exit(0); + return SIMGRID_MC_EXIT_SUCCESS; } -void MC_modelcheck_comm_determinism(void) +int MC_modelcheck_comm_determinism(void) { XBT_INFO("Check communication determinism"); - mc_reduce_kind = e_mc_reduce_none; - MC_wait_for_requests(); + mc_model_checker->wait_for_requests(); - if (mc_mode == MC_MODE_CLIENT) { + if (mc_mode == MC_MODE_CLIENT) // This will move somehwere else: - MC_client_handle_messages(); - } - - xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); + simgrid::mc::Client::get()->handleMessages(); /* Create exploration stack */ mc_stack = xbt_fifo_new(); - MC_SET_STD_HEAP; - MC_pre_modelcheck_comm_determinism(); - MC_SET_MC_HEAP; initial_global_state = xbt_new0(s_mc_global_t, 1); - initial_global_state->snapshot = MC_take_snapshot(0); + 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 = NULL; - initial_global_state->send_diff = NULL; - - MC_SET_STD_HEAP; - - MC_modelcheck_comm_determinism_main(); + initial_global_state->recv_diff = nullptr; + initial_global_state->send_diff = nullptr; - mmalloc_set_current_heap(heap); + return MC_modelcheck_comm_determinism_main(); } }