X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/ea9cce21b6d3f37823143217f1ca183bb2f0c9ac..a6cfbb1f3aefdb686ce955601ddf20391fa0fe45:/src/mc/mc_comm_determinism.cpp?ds=sidebyside diff --git a/src/mc/mc_comm_determinism.cpp b/src/mc/mc_comm_determinism.cpp index ab30d5c14d..a30cd61b02 100644 --- a/src/mc/mc_comm_determinism.cpp +++ b/src/mc/mc_comm_determinism.cpp @@ -12,6 +12,9 @@ #include "mc_record.h" #include "mc_smx.h" #include "mc_client.h" +#include "mc_exit.h" + +using simgrid::mc::remote; extern "C" { @@ -91,8 +94,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); @@ -102,12 +104,13 @@ static void update_comm_pattern(mc_comm_pattern_t comm_pattern, smx_synchro_t co comm_pattern->dst_host = MC_smx_process_get_host_name(dst_proc); if (comm_pattern->data_size == -1 && comm.comm.src_buff != NULL) { 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)); } } @@ -142,7 +145,7 @@ static void deterministic_comm_pattern(int process, mc_comm_pattern_t comm, int xbt_free(initial_global_state->send_diff); initial_global_state->send_diff = NULL; MC_print_statistics(mc_stats); - xbt_abort(); + exit(SIMGRID_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 *****"); @@ -154,7 +157,7 @@ static void deterministic_comm_pattern(int process, mc_comm_pattern_t comm, int xbt_free(initial_global_state->recv_diff); initial_global_state->recv_diff = NULL; MC_print_statistics(mc_stats); - xbt_abort(); + exit(SIMGRID_EXIT_NON_DETERMINISM); } } } @@ -184,30 +187,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){ 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,21 +229,17 @@ 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 { @@ -300,8 +294,6 @@ static void 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; int i; @@ -327,15 +319,12 @@ static void MC_pre_modelcheck_comm_determinism(void) } 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; - /* 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)) { @@ -344,9 +333,6 @@ static void MC_pre_modelcheck_comm_determinism(void) ); xbt_fifo_unshift(mc_stack, initial_state); - - MC_SET_STD_HEAP; - } static void MC_modelcheck_comm_determinism_main(void) @@ -381,9 +367,7 @@ static void MC_modelcheck_comm_determinism_main(void) 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; } MC_state_set_executed_request(state, req, value); @@ -398,19 +382,15 @@ static void MC_modelcheck_comm_determinism_main(void) /* Answer the request */ MC_simcall_handle(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; /* Wait for requests (schedules processes) */ MC_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) { @@ -437,8 +417,6 @@ static void MC_modelcheck_comm_determinism_main(void) if (dot_output != NULL) xbt_free(req_str); - MC_SET_STD_HEAP; - } else { if (xbt_fifo_size(mc_stack) > _sg_mc_max_depth) { @@ -449,8 +427,6 @@ static void MC_modelcheck_comm_determinism_main(void) 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,8 +435,6 @@ 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; /* Check for deadlocks */ @@ -469,14 +443,11 @@ static void MC_modelcheck_comm_determinism_main(void) return; } - MC_SET_MC_HEAP; - while ((state = (mc_state_t) xbt_fifo_shift(mc_stack)) != NULL) { 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); @@ -488,34 +459,29 @@ static void MC_modelcheck_comm_determinism_main(void) 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); } void MC_modelcheck_comm_determinism(void) { + XBT_INFO("Check communication determinism"); + mc_reduce_kind = e_mc_reduce_none; + MC_wait_for_requests(); + 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); - /* 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->initial_communications_pattern_done = 0; @@ -524,11 +490,7 @@ void MC_modelcheck_comm_determinism(void) initial_global_state->recv_diff = NULL; initial_global_state->send_diff = NULL; - MC_SET_STD_HEAP; - MC_modelcheck_comm_determinism_main(); - - mmalloc_set_current_heap(heap); } }