X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/2fff26ec917956fb24c8b686efbb8a151f928d55..eb261664cc90426f7dede99a570454748801a357:/src/mc/mc_comm_determinism.c diff --git a/src/mc/mc_comm_determinism.c b/src/mc/mc_comm_determinism.c index cfbf3f32bb..fc4e1bd772 100644 --- a/src/mc/mc_comm_determinism.c +++ b/src/mc/mc_comm_determinism.c @@ -4,7 +4,12 @@ /* 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" XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_comm_determinism, mc, "Logging specific to MC communication determinism detection"); @@ -146,8 +151,9 @@ static void print_communications_pattern(xbt_dynar_t comms_pattern) } } -static void update_comm_pattern(mc_comm_pattern_t comm_pattern, smx_action_t comm) +static void update_comm_pattern(mc_comm_pattern_t comm_pattern, smx_synchro_t comm) { + mc_process_t process = &mc_model_checker->process; void *addr_pointed; comm_pattern->src_proc = comm->comm.src_proc->pid; comm_pattern->dst_proc = comm->comm.dst_proc->pid; @@ -159,7 +165,8 @@ static void update_comm_pattern(mc_comm_pattern_t comm_pattern, smx_action_t com comm_pattern->data_size = *(comm->comm.dst_buff_size); comm_pattern->data = xbt_malloc0(comm_pattern->data_size); addr_pointed = *(void **) comm->comm.src_buff; - if (addr_pointed > (void*) std_heap && addr_pointed < std_heap->breakval) + if (addr_pointed > (void*) process->heap_address + && addr_pointed < MC_process_get_heap(process)->breakval) memcpy(comm_pattern->data, addr_pointed, comm_pattern->data_size); else memcpy(comm_pattern->data, comm->comm.src_buff, comm_pattern->data_size); @@ -168,14 +175,15 @@ static void update_comm_pattern(mc_comm_pattern_t comm_pattern, smx_action_t com /********** Non Static functions ***********/ -void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, int call) +void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, mc_call_type call_type) { + mc_process_t process = &mc_model_checker->process; mc_comm_pattern_t pattern = NULL; pattern = xbt_new0(s_mc_comm_pattern_t, 1); pattern->num = ++nb_comm_pattern; pattern->data_size = -1; void *addr_pointed; - if (call == 1) { // ISEND + if (call_type == MC_CALL_TYPE_SEND) { // ISEND pattern->type = SIMIX_COMM_SEND; pattern->comm = simcall_comm_isend__get__result(request); pattern->src_proc = pattern->comm->comm.src_proc->pid; @@ -183,15 +191,18 @@ void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, int call) pattern->data_size = pattern->comm->comm.src_buff_size; pattern->data = xbt_malloc0(pattern->data_size); addr_pointed = *(void **) pattern->comm->comm.src_buff; - if (addr_pointed > (void*) std_heap && addr_pointed < std_heap->breakval) + if (addr_pointed > (void*) process->heap_address + && addr_pointed < MC_process_get_heap(process)->breakval) memcpy(pattern->data, addr_pointed, pattern->data_size); else memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size); - } else { // IRECV + } else if (call_type == MC_CALL_TYPE_RECV) { // IRECV pattern->type = SIMIX_COMM_RECEIVE; pattern->comm = simcall_comm_irecv__get__result(request); pattern->dst_proc = pattern->comm->comm.dst_proc->pid; pattern->dst_host = simcall_host_get_name(request->issuer->smx_host); + } else { + xbt_die("Unexpected call_type %i", (int) call_type); } if (pattern->comm->comm.rdv != NULL) @@ -205,7 +216,7 @@ void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, int call) } -void complete_comm_pattern(xbt_dynar_t list, smx_action_t comm) +void complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm) { mc_comm_pattern_t current_comm_pattern; unsigned int cursor = 0; @@ -251,16 +262,12 @@ void complete_comm_pattern(xbt_dynar_t list, smx_action_t comm) void MC_pre_modelcheck_comm_determinism(void) { - - int mc_mem_set = (mmalloc_get_current_heap() == mc_heap); + MC_SET_MC_HEAP; mc_state_t initial_state = NULL; smx_process_t process; int i; - if (!mc_mem_set) - MC_SET_MC_HEAP; - if (_sg_mc_visited > 0) visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp); @@ -310,12 +317,11 @@ void MC_modelcheck_comm_determinism(void) { char *req_str = NULL; - int value, call = 0; + 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; - smx_action_t current_comm; xbt_dynar_t current_pattern; while (xbt_fifo_size(mc_stack) > 0) { @@ -337,55 +343,31 @@ void MC_modelcheck_comm_determinism(void) && (req = MC_state_get_request(state, &value)) && (visited_state == NULL)) { - /* Debug information */ - if (XBT_LOG_ISENABLED(mc_comm_determinism, xbt_log_priority_debug)) { - req_str = MC_request_to_string(req, value); - XBT_DEBUG("Execute: %s", req_str); - xbt_free(req_str); - } + MC_LOG_REQUEST(mc_comm_determinism, req, value); - MC_SET_MC_HEAP; - if (dot_output != NULL) + if (dot_output != NULL) { + MC_SET_MC_HEAP; req_str = MC_request_get_dot_output(req, value); - MC_SET_STD_HEAP; + MC_SET_STD_HEAP; + } MC_state_set_executed_request(state, req, value); mc_stats->executed_transitions++; /* TODO : handle test and testany simcalls */ + mc_call_type call = MC_CALL_TYPE_NONE; if (_sg_mc_comms_determinism || _sg_mc_send_determinism) { - if (req->call == SIMCALL_COMM_ISEND) - call = 1; - else if (req->call == SIMCALL_COMM_IRECV) - call = 2; - else if (req->call == SIMCALL_COMM_WAIT) - call = 3; - else if (req->call == SIMCALL_COMM_WAITANY) - call = 4; + call = mc_get_call_type(req); } /* Answer the request */ - SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */ + SIMIX_simcall_handle(req, value); /* After this call req is no longer useful */ MC_SET_MC_HEAP; current_pattern = !initial_global_state->initial_communications_pattern_done ? initial_communications_pattern : communications_pattern; - if (call == 1) { /* Send */ - get_comm_pattern(current_pattern, req, call); - } else if (call == 2) { /* Recv */ - get_comm_pattern(current_pattern, req, call); - } else if (call == 3) { /* Wait */ - current_comm = simcall_comm_wait__get__comm(req); - if (current_comm->comm.refcount == 1) /* First wait only must be considered */ - complete_comm_pattern(current_pattern, current_comm); - } else if (call == 4) { /* WaitAny */ - current_comm = xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value, smx_action_t); - if (current_comm->comm.refcount == 1) /* First wait only must be considered */ - complete_comm_pattern(current_pattern, current_comm); - } + mc_update_comm_pattern(call, req, value, current_pattern); MC_SET_STD_HEAP; - call = 0; - /* Wait for requests (schedules processes) */ MC_wait_for_requests();