From 276b87ef25a4bce97dfec6020bc7e6d5a0ec837c Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Tue, 29 Apr 2014 17:03:09 +0200 Subject: [PATCH] model-checker : fix the detection of determinism --- src/mc/mc_dpor.c | 44 +++++++++++++++++++++++++++++--------------- src/mc/mc_global.c | 17 ++++++++++++----- src/mc/mc_private.h | 3 ++- 3 files changed, 43 insertions(+), 21 deletions(-) diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c index 5ab8aed15e..cf407ad649 100644 --- a/src/mc/mc_dpor.c +++ b/src/mc/mc_dpor.c @@ -14,6 +14,7 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dpor, mc, xbt_dynar_t visited_states; xbt_dict_t first_enabled_state; xbt_dynar_t initial_communications_pattern; +xbt_dynar_t incomplete_communications_pattern; xbt_dynar_t communications_pattern; int nb_comm_pattern; @@ -82,6 +83,8 @@ static void deterministic_pattern(xbt_dynar_t initial_pattern, xbt_dynar_t patte comm_comparison = compare_comm_pattern(comm1, comm2); if(comm_comparison == 1){ initial_state_safety->comm_deterministic = 0; + if(!_sg_mc_send_determinism) + return; } recv_index++; } @@ -97,20 +100,23 @@ static void deterministic_pattern(xbt_dynar_t initial_pattern, xbt_dynar_t patte static int complete_comm_pattern(xbt_dynar_t list, mc_comm_pattern_t pattern){ mc_comm_pattern_t current_pattern; unsigned int cursor = 0; - xbt_dynar_foreach(list, cursor, current_pattern){ + int index; + xbt_dynar_foreach(incomplete_communications_pattern, cursor, index){ + current_pattern = (mc_comm_pattern_t)xbt_dynar_get_as(list, index, mc_comm_pattern_t); if(current_pattern->comm == pattern->comm){ - if(!current_pattern->completed){ - current_pattern->src_proc = pattern->comm->comm.src_proc->pid; - current_pattern->src_host = simcall_host_get_name(pattern->comm->comm.src_proc->smx_host); - current_pattern->dst_proc = pattern->comm->comm.dst_proc->pid; - current_pattern->dst_host = simcall_host_get_name(pattern->comm->comm.dst_proc->smx_host); + current_pattern->src_proc = pattern->comm->comm.src_proc->pid; + current_pattern->dst_proc = pattern->comm->comm.dst_proc->pid; + current_pattern->src_host = simcall_host_get_name(pattern->comm->comm.src_proc->smx_host); + current_pattern->dst_host = simcall_host_get_name(pattern->comm->comm.dst_proc->smx_host); + if(current_pattern->data_size == -1){ current_pattern->data_size = pattern->comm->comm.src_buff_size; current_pattern->data = xbt_malloc0(current_pattern->data_size); - current_pattern->matched_comm = pattern->num; memcpy(current_pattern->data, current_pattern->comm->comm.src_buff, current_pattern->data_size); - current_pattern->completed = 1; - return current_pattern->num; } + current_pattern->matched_comm = pattern->num; + current_pattern->completed = 1; + xbt_dynar_remove_at(incomplete_communications_pattern, cursor, NULL); + return current_pattern->num; } } return -1; @@ -121,14 +127,15 @@ void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, int call){ pattern = xbt_new0(s_mc_comm_pattern_t, 1); pattern->num = ++nb_comm_pattern; pattern->completed = 0; + pattern->data_size = -1; if(call == 1){ // ISEND pattern->comm = simcall_comm_isend__get__result(request); pattern->type = SIMIX_COMM_SEND; if(pattern->comm->comm.dst_proc != NULL){ pattern->matched_comm = complete_comm_pattern(list, pattern); pattern->dst_proc = pattern->comm->comm.dst_proc->pid; - pattern->completed = 1; pattern->dst_host = simcall_host_get_name(pattern->comm->comm.dst_proc->smx_host); + pattern->completed = 1; } pattern->src_proc = pattern->comm->comm.src_proc->pid; pattern->src_host = simcall_host_get_name(request->issuer->smx_host); @@ -141,20 +148,26 @@ void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, int call){ if(pattern->comm->comm.src_proc != NULL){ pattern->matched_comm = complete_comm_pattern(list, pattern); pattern->src_proc = pattern->comm->comm.src_proc->pid; - pattern->src_host = simcall_host_get_name(pattern->comm->comm.src_proc->smx_host); + pattern->src_host = simcall_host_get_name(request->issuer->smx_host); pattern->completed = 1; pattern->data_size = pattern->comm->comm.src_buff_size; pattern->data=xbt_malloc0(pattern->data_size); memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size); } pattern->dst_proc = pattern->comm->comm.dst_proc->pid; - pattern->dst_host = simcall_host_get_name(request->issuer->smx_host); + pattern->dst_host = simcall_host_get_name(pattern->comm->comm.dst_proc->smx_host); } + if(pattern->comm->comm.rdv != NULL) pattern->rdv = strdup(pattern->comm->comm.rdv->name); else pattern->rdv = strdup(pattern->comm->comm.rdv_cpy->name); + xbt_dynar_push(list, &pattern); + + if(!pattern->completed) + xbt_dynar_push_as(incomplete_communications_pattern, int, xbt_dynar_length(list) - 1); + } static void print_communications_pattern(xbt_dynar_t comms_pattern){ @@ -414,6 +427,7 @@ void MC_dpor_init() initial_communications_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp); communications_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp); + incomplete_communications_pattern = xbt_dynar_new(sizeof(int), NULL); nb_comm_pattern = 0; initial_state = MC_state_new(); @@ -764,13 +778,13 @@ void MC_dpor(void) XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack_safety)); break; } else { - req = MC_state_get_internal_request(state); - if(_sg_mc_comms_determinism){ + /*req = MC_state_get_internal_request(state); + if(_sg_mc_comms_determinism || _sg_mc_send_determinism){ if(req->call == SIMCALL_COMM_ISEND || req->call == SIMCALL_COMM_IRECV){ if(!xbt_dynar_is_empty(communications_pattern)) xbt_dynar_remove_at(communications_pattern, xbt_dynar_length(communications_pattern) - 1, NULL); } - } + }*/ XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1); MC_state_delete(state); } diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index acbc818593..124e885250 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -1115,17 +1115,24 @@ void MC_replay(xbt_fifo_t stack, int start) } MC_SET_RAW_MEM; - xbt_dict_reset(first_enabled_state); - xbt_swag_foreach(process, simix_global->process_list){ - if(MC_process_is_enabled(process)){ + + if(mc_reduce_kind == e_mc_reduce_dpor){ + xbt_dict_reset(first_enabled_state); + xbt_swag_foreach(process, simix_global->process_list){ + if(MC_process_is_enabled(process)){ char *key = bprintf("%lu", process->pid); char *data = bprintf("%d", count); xbt_dict_set(first_enabled_state, key, data, NULL); xbt_free(key); + } } } - if(_sg_mc_comms_determinism || _sg_mc_send_determinism) + + if(_sg_mc_comms_determinism || _sg_mc_send_determinism){ xbt_dynar_reset(communications_pattern); + xbt_dynar_reset(incomplete_communications_pattern); + } + MC_UNSET_RAW_MEM; @@ -1160,7 +1167,7 @@ void MC_replay(xbt_fifo_t stack, int start) if(req->call == SIMCALL_COMM_ISEND) comm_pattern = 1; else if(req->call == SIMCALL_COMM_IRECV) - comm_pattern = 2; + comm_pattern = 2; } SIMIX_simcall_pre(req, value); diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index 0de75609ec..0d45e7484b 100644 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@ -562,12 +562,13 @@ typedef struct s_mc_comm_pattern{ const char *src_host; const char *dst_host; char *rdv; - size_t data_size; + ssize_t data_size; void *data; int matched_comm; }s_mc_comm_pattern_t, *mc_comm_pattern_t; extern xbt_dynar_t communications_pattern; +extern xbt_dynar_t incomplete_communications_pattern; void get_comm_pattern(xbt_dynar_t communications_pattern, smx_simcall_t request, int call); -- 2.20.1