X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/e47b3e4c9b5ea0bd18d8c088320844200e4ff07e..923896223efc203372ce0a7435cbdb7b539149f6:/src/mc/mc_comm_determinism.c diff --git a/src/mc/mc_comm_determinism.c b/src/mc/mc_comm_determinism.c index ed68099c96..1017b33579 100644 --- a/src/mc/mc_comm_determinism.c +++ b/src/mc/mc_comm_determinism.c @@ -46,124 +46,58 @@ static e_mc_comm_pattern_difference_t compare_comm_pattern(mc_comm_pattern_t com return SRC_PROC_DIFF; if (comm1->dst_proc != comm2->dst_proc) return DST_PROC_DIFF; + if (comm1->tag != comm2->tag) + return TAG_DIFF; if (comm1->data_size != comm2->data_size) return DATA_SIZE_DIFF; if(comm1->data == NULL && comm2->data == NULL) return 0; - /*if(comm1->data != NULL && comm2->data !=NULL) { + if(comm1->data != NULL && comm2->data !=NULL) { if (!memcmp(comm1->data, comm2->data, comm1->data_size)) return 0; return DATA_DIFF; }else{ return DATA_DIFF; - }*/ - return 0; -} - -static void print_determinism_result(e_mc_comm_pattern_difference_t diff, int process, mc_comm_pattern_t comm, unsigned int cursor) { - if (_sg_mc_comms_determinism && !initial_global_state->comm_deterministic) { - XBT_INFO("****************************************************"); - XBT_INFO("***** Non-deterministic communications pattern *****"); - XBT_INFO("****************************************************"); - XBT_INFO("The communications pattern of the process %d is different!", process); - switch(diff) { - case TYPE_DIFF: - XBT_INFO("Different communication type for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor); - break; - case RDV_DIFF: - XBT_INFO("Different communication rdv for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor); - break; - case SRC_PROC_DIFF: - XBT_INFO("Different communication source process for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor); - break; - case DST_PROC_DIFF: - XBT_INFO("Different communication destination process for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor); - break; - case DATA_SIZE_DIFF: - XBT_INFO("Different communication data size for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor); - break; - case DATA_DIFF: - XBT_INFO("Different communication data for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor); - break; - default: - break; - } - MC_print_statistics(mc_stats); - xbt_abort(); - } else if (_sg_mc_send_determinism && !initial_global_state->send_deterministic) { - XBT_INFO("*********************************************************"); - XBT_INFO("***** Non-send-deterministic communications pattern *****"); - XBT_INFO("*********************************************************"); - XBT_INFO("The communications pattern of the process %d is different!", process); - switch(diff) { - case TYPE_DIFF: - XBT_INFO("Different communication type for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor); - break; - case RDV_DIFF: - XBT_INFO("Different communication rdv for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor); - break; - case SRC_PROC_DIFF: - XBT_INFO("Different communication source process for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor); - break; - case DST_PROC_DIFF: - XBT_INFO("Different communication destination process for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor); - break; - case DATA_SIZE_DIFF: - XBT_INFO("Different communication data size for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor); - break; - case DATA_DIFF: - XBT_INFO("Different communication data for communication %s at index %d", comm->type == SIMIX_COMM_SEND ? "Send" : "Recv", cursor); - break; - default: - break; - } - MC_print_statistics(mc_stats); - xbt_abort(); } + return 0; } -static void print_communications_pattern() -{ - unsigned int cursor = 0, cursor2 = 0; - mc_comm_pattern_t current_comm; - mc_list_comm_pattern_t current_list; - unsigned int current_process = 1; - while (current_process < simix_process_maxpid) { - current_list = (mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, current_process, mc_list_comm_pattern_t); - XBT_INFO("Communications from the process %u:", current_process); - while(cursor2 < current_list->index_comm){ - current_comm = (mc_comm_pattern_t)xbt_dynar_get_as(current_list->list, cursor2, mc_comm_pattern_t); - if (current_comm->type == SIMIX_COMM_SEND) { - XBT_INFO("(%u) [(%lu) %s -> (%lu) %s] %s ", cursor,current_comm->src_proc, - current_comm->src_host, current_comm->dst_proc, - current_comm->dst_host, "iSend"); - } else { - XBT_INFO("(%u) [(%lu) %s <- (%lu) %s] %s ", cursor, current_comm->dst_proc, - current_comm->dst_host, current_comm->src_proc, - current_comm->src_host, "iRecv"); - } - cursor2++; - } - current_process++; - cursor = 0; - cursor2 = 0; +static char* print_determinism_result(e_mc_comm_pattern_difference_t diff, int process, mc_comm_pattern_t comm, unsigned int cursor) { + char *type, *res; + + if(comm->type == SIMIX_COMM_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); + + switch(diff) { + case TYPE_DIFF: + res = bprintf("%s Different type for communication #%d", type, cursor); + break; + case RDV_DIFF: + res = bprintf("%s Different rdv for communication #%d", type, cursor); + break; + case TAG_DIFF: + res = bprintf("%s Different tag for communication #%d", type, cursor); + break; + case SRC_PROC_DIFF: + res = bprintf("%s Different source for communication #%d", type, cursor); + break; + case DST_PROC_DIFF: + res = bprintf("%s Different destination for communication #%d", type, cursor); + break; + case DATA_SIZE_DIFF: + res = bprintf("%s\n Different data size for communication #%d", type, cursor); + break; + case DATA_DIFF: + res = bprintf("%s\n Different data for communication #%d", type, cursor); + break; + default: + res = NULL; + break; } -} -static void print_incomplete_communications_pattern(){ - unsigned int cursor = 0; - unsigned int current_process = 1; - xbt_dynar_t current_pattern; - mc_comm_pattern_t comm; - while (current_process < simix_process_maxpid) { - current_pattern = (xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t); - XBT_INFO("Incomplete communications from the process %u:", current_process); - xbt_dynar_foreach(current_pattern, cursor, comm) { - XBT_DEBUG("(%u) Communication %p", cursor, comm); - } - current_process++; - cursor = 0; - } + return res; } // FIXME, remote comm @@ -171,11 +105,13 @@ static void update_comm_pattern(mc_comm_pattern_t comm_pattern, smx_synchro_t co { 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; + 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); + comm_pattern->src_proc = src_proc->pid; + comm_pattern->dst_proc = dst_proc->pid; // TODO, resolve host name - comm_pattern->src_host = MC_smx_process_get_host_name(MC_smx_resolve_process(comm->comm.src_proc)); - comm_pattern->dst_host = MC_smx_process_get_host_name(MC_smx_resolve_process(comm->comm.dst_proc)); + 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) { comm_pattern->data_size = *(comm->comm.dst_buff_size); comm_pattern->data = xbt_malloc0(comm_pattern->data_size); @@ -193,18 +129,46 @@ static void deterministic_comm_pattern(int process, mc_comm_pattern_t comm, int mc_list_comm_pattern_t list_comm_pattern = (mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, process, mc_list_comm_pattern_t); if(!backtracking){ - mc_comm_pattern_t initial_comm = xbt_dynar_get_as(list_comm_pattern->list, comm->index, mc_comm_pattern_t); + mc_comm_pattern_t initial_comm = xbt_dynar_get_as(list_comm_pattern->list, list_comm_pattern->index_comm, mc_comm_pattern_t); e_mc_comm_pattern_difference_t diff; if((diff = compare_comm_pattern(initial_comm, comm)) != NONE_DIFF){ - if (comm->type == SIMIX_COMM_SEND) + if (comm->type == SIMIX_COMM_SEND){ initial_global_state->send_deterministic = 0; - initial_global_state->comm_deterministic = 0; - print_determinism_result(diff, process, comm, list_comm_pattern->index_comm + 1); + if(initial_global_state->send_diff != NULL) + xbt_free(initial_global_state->send_diff); + initial_global_state->send_diff = print_determinism_result(diff, process, comm, list_comm_pattern->index_comm + 1); + }else{ + initial_global_state->recv_deterministic = 0; + if(initial_global_state->recv_diff != NULL) + xbt_free(initial_global_state->recv_diff); + initial_global_state->recv_diff = print_determinism_result(diff, process, comm, list_comm_pattern->index_comm + 1); + } + if(_sg_mc_send_determinism && !initial_global_state->send_deterministic){ + XBT_INFO("*********************************************************"); + XBT_INFO("***** Non-send-deterministic communications pattern *****"); + XBT_INFO("*********************************************************"); + XBT_INFO("%s", initial_global_state->send_diff); + xbt_free(initial_global_state->send_diff); + initial_global_state->send_diff = NULL; + MC_print_statistics(mc_stats); + xbt_abort(); + }else if(_sg_mc_comms_determinism && (!initial_global_state->send_deterministic && !initial_global_state->recv_deterministic)) { + XBT_INFO("****************************************************"); + XBT_INFO("***** Non-deterministic communications pattern *****"); + XBT_INFO("****************************************************"); + 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; + xbt_free(initial_global_state->recv_diff); + initial_global_state->recv_diff = NULL; + MC_print_statistics(mc_stats); + xbt_abort(); + } } } - list_comm_pattern->index_comm++; comm_pattern_free(comm); } @@ -219,7 +183,7 @@ void list_comm_pattern_free_voidp(void *p) { list_comm_pattern_free((mc_list_comm_pattern_t) * (void **) p); } -void get_comm_pattern(const xbt_dynar_t list, const smx_simcall_t request, const e_mc_call_type_t call_type) +void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking) { mc_process_t process = &mc_model_checker->process; mc_comm_pattern_t pattern = NULL; @@ -241,10 +205,11 @@ void get_comm_pattern(const xbt_dynar_t list, const smx_simcall_t request, const /* Create comm pattern */ pattern->type = SIMIX_COMM_SEND; pattern->comm = simcall_comm_isend__get__result(request); + // FIXME, remote access to rdv->name pattern->rdv = (pattern->comm->comm.rdv != NULL) ? strdup(pattern->comm->comm.rdv->name) : strdup(pattern->comm->comm.rdv_cpy->name); - pattern->src_proc = pattern->comm->comm.src_proc->pid; - // FIXME, get remote host name + pattern->src_proc = MC_smx_resolve_process(pattern->comm->comm.src_proc)->pid; pattern->src_host = MC_smx_process_get_host_name(issuer); + pattern->tag = ((MPI_Request)simcall_comm_isend__get__data(request))->tag; if(pattern->comm->comm.src_buff != NULL){ pattern->data_size = pattern->comm->comm.src_buff_size; pattern->data = xbt_malloc0(pattern->data_size); @@ -255,11 +220,24 @@ void get_comm_pattern(const xbt_dynar_t list, const smx_simcall_t request, const else memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size); } + if(((MPI_Request)simcall_comm_isend__get__data(request))->detached){ + if (!initial_global_state->initial_communications_pattern_done) { + /* Store comm pattern */ + xbt_dynar_push(((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, pattern->src_proc, mc_list_comm_pattern_t))->list, &pattern); + } else { + /* Evaluate comm determinism */ + deterministic_comm_pattern(pattern->src_proc, pattern, backtracking); + ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, pattern->src_proc, mc_list_comm_pattern_t))->index_comm++; + } + return; + } } else if (call_type == MC_CALL_TYPE_RECV) { pattern->type = SIMIX_COMM_RECEIVE; pattern->comm = simcall_comm_irecv__get__result(request); + // TODO, remote access + pattern->tag = ((MPI_Request)simcall_comm_irecv__get__data(request))->tag; pattern->rdv = (pattern->comm->comm.rdv != NULL) ? strdup(pattern->comm->comm.rdv->name) : strdup(pattern->comm->comm.rdv_cpy->name); - pattern->dst_proc = pattern->comm->comm.dst_proc->pid; + pattern->dst_proc = MC_smx_resolve_process(pattern->comm->comm.dst_proc)->pid; // FIXME, remote process access pattern->dst_host = MC_smx_process_get_host_name(issuer); } else { @@ -271,67 +249,36 @@ void get_comm_pattern(const xbt_dynar_t list, const smx_simcall_t request, const XBT_DEBUG("Insert incomplete comm pattern %p for process %lu", pattern, issuer->pid); } -void complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm, int backtracking) { - +void complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm, unsigned int issuer, int backtracking) { mc_comm_pattern_t current_comm_pattern; unsigned int cursor = 0; - unsigned int src = comm->comm.src_proc->pid; - unsigned int dst = comm->comm.dst_proc->pid; - mc_comm_pattern_t src_comm_pattern; - mc_comm_pattern_t dst_comm_pattern; - int src_completed = 0, dst_completed = 0; + mc_comm_pattern_t comm_pattern; + int completed = 0; /* Complete comm pattern */ - xbt_dynar_foreach((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, src, xbt_dynar_t), cursor, current_comm_pattern) { + xbt_dynar_foreach((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t), cursor, current_comm_pattern) { if (current_comm_pattern-> comm == comm) { update_comm_pattern(current_comm_pattern, comm); - src_completed = 1; - xbt_dynar_remove_at((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, src, xbt_dynar_t), cursor, &src_comm_pattern); - XBT_DEBUG("Remove incomplete comm pattern for process %u at cursor %u", src, cursor); + completed = 1; + xbt_dynar_remove_at((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t), cursor, &comm_pattern); + XBT_DEBUG("Remove incomplete comm pattern for process %u at cursor %u", issuer, cursor); break; } } - if(!src_completed) - xbt_die("Corresponding communication for the source process not found!"); - - cursor = 0; + if(!completed) + xbt_die("Corresponding communication not found!"); - xbt_dynar_foreach((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, dst, xbt_dynar_t), cursor, current_comm_pattern) { - if (current_comm_pattern-> comm == comm) { - update_comm_pattern(current_comm_pattern, comm); - dst_completed = 1; - xbt_dynar_remove_at((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, dst, xbt_dynar_t), cursor, &dst_comm_pattern); - XBT_DEBUG("Remove incomplete comm pattern for process %u at cursor %u", dst, cursor); - break; - } - } - if(!dst_completed) - xbt_die("Corresponding communication for the destination process not found!"); - if (!initial_global_state->initial_communications_pattern_done) { /* Store comm pattern */ - if(src_comm_pattern->index < xbt_dynar_length(((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, src, mc_list_comm_pattern_t))->list)){ - xbt_dynar_set(((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, src, mc_list_comm_pattern_t))->list, src_comm_pattern->index, &src_comm_pattern); - ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, src, mc_list_comm_pattern_t))->list->used++; - } else { - xbt_dynar_insert_at(((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, src, mc_list_comm_pattern_t))->list, src_comm_pattern->index, &src_comm_pattern); - } - - if(dst_comm_pattern->index < xbt_dynar_length(((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, dst, mc_list_comm_pattern_t))->list)) { - xbt_dynar_set(((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, dst, mc_list_comm_pattern_t))->list, dst_comm_pattern->index, &dst_comm_pattern); - ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, dst, mc_list_comm_pattern_t))->list->used++; - } else { - xbt_dynar_insert_at(((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, dst, mc_list_comm_pattern_t))->list, dst_comm_pattern->index, &dst_comm_pattern); - } - ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, src, mc_list_comm_pattern_t))->index_comm++; - ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, dst, mc_list_comm_pattern_t))->index_comm++; + xbt_dynar_push(((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, issuer, mc_list_comm_pattern_t))->list, &comm_pattern); } else { /* Evaluate comm determinism */ - deterministic_comm_pattern(src, src_comm_pattern, backtracking); - deterministic_comm_pattern(dst, dst_comm_pattern, backtracking); + deterministic_comm_pattern(issuer, comm_pattern, backtracking); + ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, issuer, mc_list_comm_pattern_t))->index_comm++; } } + /************************ Main algorithm ************************/ void MC_pre_modelcheck_comm_determinism(void) @@ -346,14 +293,14 @@ void MC_pre_modelcheck_comm_determinism(void) visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp); initial_communications_pattern = xbt_dynar_new(sizeof(mc_list_comm_pattern_t), list_comm_pattern_free_voidp); - for (i=0; ilist = xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp); process_list_pattern->index_comm = 0; xbt_dynar_insert_at(initial_communications_pattern, i, &process_list_pattern); } incomplete_communications_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp); - for (i=0; i