From: Marion Guthmuller Date: Tue, 24 Feb 2015 16:25:36 +0000 (+0100) Subject: model-checker : extend comm determinism verification X-Git-Tag: v3_12~749 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/a883120fb94a2ec473ac6ecfba41a69ff1846426 model-checker : extend comm determinism verification --- diff --git a/src/mc/mc_comm_determinism.c b/src/mc/mc_comm_determinism.c index 1b11b1830b..1755a6ae6a 100644 --- a/src/mc/mc_comm_determinism.c +++ b/src/mc/mc_comm_determinism.c @@ -45,9 +45,9 @@ 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) + if (comm1->tag != comm2->tag) return TAG_DIFF; - /*if (comm1->data_size != comm2->data_size) + if (comm1->data_size != comm2->data_size) return DATA_SIZE_DIFF; if(comm1->data == NULL && comm2->data == NULL) return 0; @@ -57,76 +57,45 @@ static e_mc_comm_pattern_difference_t compare_comm_pattern(mc_comm_pattern_t com 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 TAG_DIFF: - XBT_INFO("Different communication tag 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 TAG_DIFF: - XBT_INFO("Different communication tag 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(); +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: + break; } + + return res; } static void update_comm_pattern(mc_comm_pattern_t comm_pattern, smx_synchro_t comm) @@ -152,18 +121,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); } @@ -178,15 +175,13 @@ void list_comm_pattern_free_voidp(void *p) { list_comm_pattern_free((mc_list_comm_pattern_t) * (void **) p); } -void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, 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_comm_pattern_t pattern = NULL; pattern = xbt_new0(s_mc_comm_pattern_t, 1); pattern->data_size = -1; pattern->data = NULL; - - pattern->index = ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, request->issuer->pid, mc_list_comm_pattern_t))->index_comm + xbt_dynar_length((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, request->issuer->pid, xbt_dynar_t)); void *addr_pointed; @@ -207,6 +202,17 @@ void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t 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); @@ -223,67 +229,37 @@ void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t XBT_DEBUG("Insert incomplete comm pattern %p for process %lu", pattern, request->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) diff --git a/src/mc/mc_comm_pattern.h b/src/mc/mc_comm_pattern.h index e3cd1af92f..2bb40d2540 100644 --- a/src/mc/mc_comm_pattern.h +++ b/src/mc/mc_comm_pattern.h @@ -76,11 +76,11 @@ static inline e_mc_call_type_t mc_get_call_type(smx_simcall_t req) } } -void get_comm_pattern(xbt_dynar_t communications_pattern, smx_simcall_t request, e_mc_call_type_t call_type); +void get_comm_pattern(xbt_dynar_t communications_pattern, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking); void handle_comm_pattern(e_mc_call_type_t call_type, smx_simcall_t request, int value, xbt_dynar_t current_pattern, int backtracking); void comm_pattern_free_voidp(void *p); void list_comm_pattern_free_voidp(void *p); -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); void MC_pre_modelcheck_comm_determinism(void); void MC_modelcheck_comm_determinism(void); diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index 59425b305f..ca66d7bdb0 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -249,8 +249,11 @@ static void MC_modelcheck_comm_determinism_init(void) 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; - initial_global_state->comm_deterministic = 1; + 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(); @@ -331,12 +334,13 @@ void MC_do_the_modelcheck_for_real() XBT_INFO("Check communication determinism"); MC_modelcheck_comm_determinism_init(); } else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0') { - if (mc_reduce_kind == e_mc_reduce_unset) - mc_reduce_kind = e_mc_reduce_dpor; - if(_sg_mc_termination) + if(_sg_mc_termination){ XBT_INFO("Check non progressive cycles"); - else + mc_reduce_kind = e_mc_reduce_none; + }else{ XBT_INFO("Check a safety property"); + mc_reduce_kind = e_mc_reduce_dpor; + } MC_modelcheck_safety_init(); } else { if (mc_reduce_kind == e_mc_reduce_unset) @@ -379,7 +383,7 @@ void handle_comm_pattern(e_mc_call_type_t call_type, smx_simcall_t req, int valu break; case MC_CALL_TYPE_SEND: case MC_CALL_TYPE_RECV: - get_comm_pattern(pattern, req, call_type); + get_comm_pattern(pattern, req, call_type, backtracking); break; case MC_CALL_TYPE_WAIT: case MC_CALL_TYPE_WAITANY: @@ -389,10 +393,7 @@ void handle_comm_pattern(e_mc_call_type_t call_type, smx_simcall_t req, int valu current_comm = simcall_comm_wait__get__comm(req); else current_comm = xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value, smx_synchro_t); - // First wait only must be considered: - if (current_comm->comm.refcount == 1) - complete_comm_pattern(pattern, current_comm, backtracking); - break; + complete_comm_pattern(pattern, current_comm, req->issuer->pid, backtracking); } default: xbt_die("Unexpected call type %i", (int)call_type); @@ -457,7 +458,7 @@ void MC_replay(xbt_fifo_t stack) XBT_DEBUG("**** Begin Replay ****"); /* Intermediate backtracking */ - if(_sg_mc_checkpoint > 0) { + if(_sg_mc_checkpoint > 0 || _sg_mc_termination || _sg_mc_visited > 0) { start_item = xbt_fifo_get_first_item(stack); state = (mc_state_t)xbt_fifo_get_item_content(start_item); if(state->system_state){ @@ -741,11 +742,23 @@ void MC_dump_stack_liveness(xbt_fifo_t stack) } - void MC_print_statistics(mc_stats_t stats) { xbt_mheap_t previous_heap = mmalloc_get_current_heap(); + if(_sg_mc_comms_determinism) { + if (!initial_global_state->recv_deterministic && initial_global_state->send_deterministic){ + XBT_INFO("******************************************************"); + XBT_INFO("**** Only-send-deterministic communication pattern ****"); + XBT_INFO("******************************************************"); + XBT_INFO("%s", initial_global_state->recv_diff); + }else if(!initial_global_state->send_deterministic && initial_global_state->recv_deterministic) { + XBT_INFO("******************************************************"); + XBT_INFO("**** Only-recv-deterministic communication pattern ****"); + XBT_INFO("******************************************************"); + XBT_INFO("%s", initial_global_state->send_diff); + } + } if (stats->expanded_pairs == 0) { XBT_INFO("Expanded states = %lu", stats->expanded_states); XBT_INFO("Visited states = %lu", stats->visited_states); @@ -759,11 +772,10 @@ void MC_print_statistics(mc_stats_t stats) fprintf(dot_output, "}\n"); fclose(dot_output); } - if (initial_global_state != NULL) { + if (initial_global_state != NULL && (_sg_mc_comms_determinism || _sg_mc_send_determinism)) { + XBT_INFO("Send-deterministic : %s", !initial_global_state->send_deterministic ? "No" : "Yes"); if (_sg_mc_comms_determinism) - XBT_INFO("Communication-deterministic : %s", !initial_global_state->comm_deterministic ? "No" : "Yes"); - if (_sg_mc_send_determinism) - XBT_INFO("Send-deterministic : %s", !initial_global_state->send_deterministic ? "No" : "Yes"); + XBT_INFO("Recv-deterministic : %s", !initial_global_state->recv_deterministic ? "No" : "Yes"); } mmalloc_set_current_heap(previous_heap); } diff --git a/src/mc/mc_snapshot.h b/src/mc/mc_snapshot.h index 1d0f9b0937..d393116e2d 100644 --- a/src/mc/mc_snapshot.h +++ b/src/mc/mc_snapshot.h @@ -213,8 +213,10 @@ typedef struct s_mc_global_t{ int prev_pair; char *prev_req; int initial_communications_pattern_done; - int comm_deterministic; + int recv_deterministic; int send_deterministic; + char *send_diff; + char *recv_diff; }s_mc_global_t, *mc_global_t; typedef struct s_mc_checkpoint_ignore_region{