From: Marion Guthmuller Date: Mon, 9 Feb 2015 18:31:41 +0000 (+0100) Subject: model-checker : communications determinism with visited state equality reduction X-Git-Tag: v3_12~760^2~14 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/00efa36e829e34b5052058bc12c9061ebaab0f90?ds=sidebyside model-checker : communications determinism with visited state equality reduction --- diff --git a/src/mc/mc_comm_determinism.c b/src/mc/mc_comm_determinism.c index 9c01b85e0e..b68e563946 100644 --- a/src/mc/mc_comm_determinism.c +++ b/src/mc/mc_comm_determinism.c @@ -18,8 +18,6 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_comm_determinism, mc, xbt_dynar_t initial_communications_pattern; xbt_dynar_t incomplete_communications_pattern; -xbt_dynar_t communications_pattern; -int nb_comm_pattern; /********** Static functions ***********/ @@ -31,120 +29,136 @@ static void comm_pattern_free(mc_comm_pattern_t p) p = NULL; } -static void comm_pattern_free_voidp(void *p) +static void list_comm_pattern_free(mc_list_comm_pattern_t l) { - comm_pattern_free((mc_comm_pattern_t) * (void **) p); -} - -static mc_comm_pattern_t get_comm_pattern_from_idx(xbt_dynar_t pattern, - unsigned int *idx, - e_smx_comm_type_t type, - unsigned long proc) -{ - mc_comm_pattern_t current_comm; - while (*idx < xbt_dynar_length(pattern)) { - current_comm = - (mc_comm_pattern_t) xbt_dynar_get_as(pattern, *idx, mc_comm_pattern_t); - if (current_comm->type == type && type == SIMIX_COMM_SEND) { - if (current_comm->src_proc == proc) - return current_comm; - } else if (current_comm->type == type && type == SIMIX_COMM_RECEIVE) { - if (current_comm->dst_proc == proc) - return current_comm; - } - (*idx)++; - } - return NULL; + xbt_dynar_free(&(l->list)); + xbt_free(l); + l = NULL; } -static int compare_comm_pattern(mc_comm_pattern_t comm1, - mc_comm_pattern_t comm2) -{ +static e_mc_comm_pattern_difference_t compare_comm_pattern(mc_comm_pattern_t comm1, mc_comm_pattern_t comm2) { + if(comm1->type != comm2->type) + return TYPE_DIFF; if (strcmp(comm1->rdv, comm2->rdv) != 0) - return 1; + return RDV_DIFF; if (comm1->src_proc != comm2->src_proc) - return 1; + return SRC_PROC_DIFF; if (comm1->dst_proc != comm2->dst_proc) - return 1; + return DST_PROC_DIFF; if (comm1->data_size != comm2->data_size) - return 1; - if (memcmp(comm1->data, comm2->data, comm1->data_size) != 0) - return 1; + return DATA_SIZE_DIFF; + if(comm1->data == NULL && comm2->data == NULL) + return 0; + /*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 deterministic_pattern(xbt_dynar_t pattern, int partial) -{ - - unsigned int cursor = 0, send_index = 0, recv_index = 0; - mc_comm_pattern_t comm1, comm2; - unsigned int current_process = 1; /* Process 0 corresponds to maestro */ - unsigned int nb_comms1, nb_comms2; - xbt_dynar_t process_comms_pattern1, process_comms_pattern2; - - while (current_process < simix_process_maxpid) { - process_comms_pattern1 = (xbt_dynar_t)xbt_dynar_get_as(initial_communications_pattern, current_process, xbt_dynar_t); - process_comms_pattern2 = (xbt_dynar_t)xbt_dynar_get_as(pattern, current_process, xbt_dynar_t); - nb_comms1 = xbt_dynar_length(process_comms_pattern1); - nb_comms2 = xbt_dynar_length(process_comms_pattern2); - if(!xbt_dynar_is_empty((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t))) - xbt_die("Damn ! Some communications from the process %u are incomplete (%lu)! That means one or several simcalls are not handle.", current_process, xbt_dynar_length((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t))); - if (!partial && (nb_comms1 != nb_comms2)) { - XBT_INFO("The total number of communications is different between the compared patterns for the process %u.\n Communication determinism verification for this process cannot be performed.", current_process); - initial_global_state->send_deterministic = -1; - initial_global_state->comm_deterministic = -1; - } else { - while (cursor < nb_comms2) { - comm1 = (mc_comm_pattern_t)xbt_dynar_get_as(process_comms_pattern1, cursor, mc_comm_pattern_t); - if (comm1->type == SIMIX_COMM_SEND) { - comm2 = get_comm_pattern_from_idx(process_comms_pattern2, &send_index, comm1->type, current_process); - if (compare_comm_pattern(comm1, comm2)) { - XBT_INFO("The communications pattern of the process %u is different! (Different communication : %u)", current_process, cursor+1); - initial_global_state->send_deterministic = 0; - initial_global_state->comm_deterministic = 0; - return; - } - send_index++; - } else if (comm1->type == SIMIX_COMM_RECEIVE) { - comm2 = get_comm_pattern_from_idx(process_comms_pattern2, &recv_index, comm1->type, current_process); - if (compare_comm_pattern(comm1, comm2)) { - initial_global_state->comm_deterministic = 0; - if (!_sg_mc_send_determinism){ - XBT_INFO("The communications pattern of the process %u is different! (Different communication : %u)", current_process, cursor+1); - return; - } - } - recv_index++; - } - cursor++; - } +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; } - current_process++; - cursor = 0; - send_index = 0; - recv_index = 0; + 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(); } } -static void print_communications_pattern(xbt_dynar_t comms_pattern) +static void print_communications_pattern() { - unsigned int cursor = 0; + unsigned int cursor = 0, cursor2 = 0; mc_comm_pattern_t current_comm; + mc_list_comm_pattern_t current_list; unsigned int current_process = 1; - xbt_dynar_t current_pattern; while (current_process < simix_process_maxpid) { - current_pattern = (xbt_dynar_t)xbt_dynar_get_as(comms_pattern, current_process, xbt_dynar_t); + 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); - xbt_dynar_foreach(current_pattern, cursor, current_comm) { + 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("[(%lu) %s -> (%lu) %s] %s ", current_comm->src_proc, + 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("[(%lu) %s <- (%lu) %s] %s ", current_comm->dst_proc, + 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 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; @@ -156,11 +170,9 @@ static void update_comm_pattern(mc_comm_pattern_t comm_pattern, smx_synchro_t co void *addr_pointed; comm_pattern->src_proc = comm->comm.src_proc->pid; comm_pattern->dst_proc = comm->comm.dst_proc->pid; - comm_pattern->src_host = - simcall_host_get_name(comm->comm.src_proc->smx_host); - comm_pattern->dst_host = - simcall_host_get_name(comm->comm.dst_proc->smx_host); - if (comm_pattern->data_size == -1) { + comm_pattern->src_host = simcall_host_get_name(comm->comm.src_proc->smx_host); + comm_pattern->dst_host = simcall_host_get_name(comm->comm.dst_proc->smx_host); + 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); addr_pointed = *(void **) comm->comm.src_buff; @@ -171,87 +183,139 @@ static void update_comm_pattern(mc_comm_pattern_t comm_pattern, smx_synchro_t co } } +static void deterministic_comm_pattern(int process, mc_comm_pattern_t comm, int backtracking) { + + 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); + e_mc_comm_pattern_difference_t diff; + + if((diff = compare_comm_pattern(initial_comm, comm)) != NONE_DIFF){ + 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); + } + } + + list_comm_pattern->index_comm++; + comm_pattern_free(comm); + +} + /********** Non Static functions ***********/ -void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, mc_call_type call_type) +void comm_pattern_free_voidp(void *p) { + comm_pattern_free((mc_comm_pattern_t) * (void **) p); +} + +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) { + mc_comm_pattern_t pattern = NULL; pattern = xbt_new0(s_mc_comm_pattern_t, 1); - pattern->num = ++nb_comm_pattern; 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; - if (call_type == MC_CALL_TYPE_SEND) { // ISEND + + if (call_type == MC_CALL_TYPE_SEND) { + /* Create comm pattern */ pattern->type = SIMIX_COMM_SEND; pattern->comm = simcall_comm_isend__get__result(request); + 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; pattern->src_host = simcall_host_get_name(request->issuer->smx_host); - 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) - memcpy(pattern->data, addr_pointed, pattern->data_size); - else - memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size); - } else if (call_type == MC_CALL_TYPE_RECV) { // IRECV + if(pattern->comm->comm.src_buff != NULL){ + 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) + memcpy(pattern->data, addr_pointed, pattern->data_size); + else + memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size); + } + } else if (call_type == MC_CALL_TYPE_RECV) { pattern->type = SIMIX_COMM_RECEIVE; pattern->comm = simcall_comm_irecv__get__result(request); + 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_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) - pattern->rdv = strdup(pattern->comm->comm.rdv->name); - else - pattern->rdv = strdup(pattern->comm->comm.rdv_cpy->name); - - xbt_dynar_push((xbt_dynar_t)xbt_dynar_get_as(list, request->issuer->pid, xbt_dynar_t), &pattern); - - xbt_dynar_push_as((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, request->issuer->pid, xbt_dynar_t), int, xbt_dynar_length((xbt_dynar_t)xbt_dynar_get_as(list, request->issuer->pid, xbt_dynar_t)) - 1); + xbt_dynar_push((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, request->issuer->pid, xbt_dynar_t), &pattern); + 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) -{ +void complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm, int backtracking) { + mc_comm_pattern_t current_comm_pattern; unsigned int cursor = 0; - int index; 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; - /* Looking for the corresponding communication in the comm pattern list of the src process */ - xbt_dynar_foreach((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, src, xbt_dynar_t), cursor, index){ - current_comm_pattern = (mc_comm_pattern_t) xbt_dynar_get_as((xbt_dynar_t)xbt_dynar_get_as(list, src, xbt_dynar_t), index, mc_comm_pattern_t); - if(current_comm_pattern->comm == comm){ + /* Complete comm pattern */ + xbt_dynar_foreach((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, src, xbt_dynar_t), cursor, current_comm_pattern) { + if (current_comm_pattern-> comm == comm) { update_comm_pattern(current_comm_pattern, comm); - xbt_dynar_remove_at((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, src, xbt_dynar_t), cursor, NULL); 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); break; } } - if(!src_completed) xbt_die("Corresponding communication for the source process not found!"); cursor = 0; - /* Looking for the corresponding communication in the comm pattern list of the dst process */ - xbt_dynar_foreach((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, dst, xbt_dynar_t), cursor, index){ - current_comm_pattern = (mc_comm_pattern_t) xbt_dynar_get_as((xbt_dynar_t)xbt_dynar_get_as(list, dst, xbt_dynar_t), index, mc_comm_pattern_t); - if(current_comm_pattern->comm == comm){ + 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); - xbt_dynar_remove_at((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, dst, xbt_dynar_t), cursor, NULL); 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 dest process not found!"); - - + 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++; + } else { + /* Evaluate comm determinism */ + deterministic_comm_pattern(src, src_comm_pattern, backtracking); + deterministic_comm_pattern(dst, dst_comm_pattern, backtracking); + } } /************************ Main algorithm ************************/ @@ -271,28 +335,22 @@ void MC_pre_modelcheck_comm_determinism(void) if (_sg_mc_visited > 0) visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp); - initial_communications_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_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 0) { /* Get current state */ - state = - (mc_state_t) - xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack)); + state = (mc_state_t) xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack)); XBT_DEBUG("**************************************************"); XBT_DEBUG("Exploration depth = %d (state = %d, interleaved processes = %d)", @@ -343,8 +398,10 @@ void MC_modelcheck_comm_determinism(void) && (req = MC_state_get_request(state, &value)) && (visited_state == NULL)) { - MC_LOG_REQUEST(mc_comm_determinism, req, value); - + req_str = MC_request_to_string(req, value); + XBT_DEBUG("Execute: %s", req_str); + xbt_free(req_str); + if (dot_output != NULL) { MC_SET_MC_HEAP; req_str = MC_request_get_dot_output(req, value); @@ -355,7 +412,7 @@ void MC_modelcheck_comm_determinism(void) mc_stats->executed_transitions++; /* TODO : handle test and testany simcalls */ - mc_call_type call = MC_CALL_TYPE_NONE; + e_mc_call_type_t call = MC_CALL_TYPE_NONE; if (_sg_mc_comms_determinism || _sg_mc_send_determinism) { call = mc_get_call_type(req); } @@ -364,8 +421,10 @@ void MC_modelcheck_comm_determinism(void) 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; - mc_update_comm_pattern(call, req, value, current_pattern); + if(!initial_global_state->initial_communications_pattern_done) + handle_comm_pattern(call, req, value, initial_communications_pattern, 0); + else + handle_comm_pattern(call, req, value, NULL, 0); MC_SET_STD_HEAP; /* Wait for requests (schedules processes) */ @@ -376,7 +435,7 @@ void MC_modelcheck_comm_determinism(void) next_state = MC_state_new(); - if ((visited_state = is_visited_state()) == NULL) { + if ((visited_state = is_visited_state(next_state)) == NULL) { /* Get enabled processes and insert them in the interleave set of the next state */ xbt_swag_foreach(process, simix_global->process_list) { @@ -386,14 +445,12 @@ void MC_modelcheck_comm_determinism(void) } if (dot_output != NULL) - fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, - next_state->num, req_str); + fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str); } else { if (dot_output != NULL) - fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, - visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str); + fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str); } @@ -416,49 +473,13 @@ void MC_modelcheck_comm_determinism(void) MC_SET_MC_HEAP; - if (initial_global_state->initial_communications_pattern_done) { - if (!visited_state) { - deterministic_pattern(communications_pattern, 0); - } else { - deterministic_pattern(communications_pattern, 1); - } - - if (_sg_mc_comms_determinism && !initial_global_state->comm_deterministic) { - XBT_INFO("****************************************************"); - XBT_INFO("***** Non-deterministic communications pattern *****"); - XBT_INFO("****************************************************"); - XBT_INFO("** Initial communications pattern (per process): **"); - print_communications_pattern(initial_communications_pattern); - XBT_INFO("** Communications pattern counter-example (per process): **"); - print_communications_pattern(communications_pattern); - MC_print_statistics(mc_stats); - MC_SET_STD_HEAP; - return; - } else if (_sg_mc_send_determinism && !initial_global_state->send_deterministic) { - XBT_INFO - ("*********************************************************"); - XBT_INFO - ("***** Non-send-deterministic communications pattern *****"); - XBT_INFO - ("*********************************************************"); - XBT_INFO("** Initial communications pattern: **"); - print_communications_pattern(initial_communications_pattern); - XBT_INFO("** Communications pattern counter-example: **"); - print_communications_pattern(communications_pattern); - MC_print_statistics(mc_stats); - MC_SET_STD_HEAP; - return; - } - - } else { + if (!initial_global_state->initial_communications_pattern_done) initial_global_state->initial_communications_pattern_done = 1; - } /* Trash the current state, no longer needed */ xbt_fifo_shift(mc_stack); - MC_state_delete(state); - XBT_DEBUG("Delete state %d at depth %d", state->num, - xbt_fifo_size(mc_stack) + 1); + 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; @@ -473,23 +494,20 @@ void MC_modelcheck_comm_determinism(void) MC_SET_MC_HEAP; while ((state = xbt_fifo_shift(mc_stack)) != NULL) { - if (MC_state_interleave_size(state) - && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) { + 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_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, -1); + MC_replay(mc_stack); + + XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack)); - XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, - xbt_fifo_size(mc_stack)); break; } else { - XBT_DEBUG("Delete state %d at depth %d", state->num, - xbt_fifo_size(mc_stack) + 1); - MC_state_delete(state); + XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1); + MC_state_delete(state, !state->in_visited_states ? 1 : 0); } } diff --git a/src/mc/mc_comm_pattern.h b/src/mc/mc_comm_pattern.h index cb45a66c87..667f24e529 100644 --- a/src/mc/mc_comm_pattern.h +++ b/src/mc/mc_comm_pattern.h @@ -27,22 +27,36 @@ typedef struct s_mc_comm_pattern{ char *rdv; ssize_t data_size; void *data; + int index; } s_mc_comm_pattern_t, *mc_comm_pattern_t; +typedef struct s_mc_list_comm_pattern{ + unsigned int index_comm; + xbt_dynar_t list; +}s_mc_list_comm_pattern_t, *mc_list_comm_pattern_t; + extern xbt_dynar_t initial_communications_pattern; -extern xbt_dynar_t communications_pattern; extern xbt_dynar_t incomplete_communications_pattern; -// Can we use the SIMIX syscall for this? -typedef enum mc_call_type { +typedef enum { MC_CALL_TYPE_NONE, MC_CALL_TYPE_SEND, MC_CALL_TYPE_RECV, MC_CALL_TYPE_WAIT, MC_CALL_TYPE_WAITANY, -} mc_call_type; +} e_mc_call_type_t; + +typedef enum { + NONE_DIFF, + TYPE_DIFF, + RDV_DIFF, + SRC_PROC_DIFF, + DST_PROC_DIFF, + DATA_SIZE_DIFF, + DATA_DIFF, +} e_mc_comm_pattern_difference_t; -static inline mc_call_type mc_get_call_type(smx_simcall_t req) +static inline e_mc_call_type_t mc_get_call_type(smx_simcall_t req) { switch(req->call) { case SIMCALL_COMM_ISEND: @@ -58,9 +72,11 @@ static inline mc_call_type mc_get_call_type(smx_simcall_t req) } } -void get_comm_pattern(xbt_dynar_t communications_pattern, smx_simcall_t request, mc_call_type call_type); -void mc_update_comm_pattern(mc_call_type call_type, smx_simcall_t request, int value, xbt_dynar_t current_pattern); -void complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm); +void get_comm_pattern(xbt_dynar_t communications_pattern, smx_simcall_t request, e_mc_call_type_t call_type); +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 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 19f84ef514..3776138b3d 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -194,9 +194,9 @@ void MC_init() /* Main MC state: */ MC_ignore_global_variable("mc_model_checker"); - MC_ignore_global_variable("communications_pattern"); MC_ignore_global_variable("initial_communications_pattern"); MC_ignore_global_variable("incomplete_communications_pattern"); + MC_ignore_global_variable("nb_comm_pattern"); /* MC __thread variables: */ MC_ignore_global_variable("mc_diff_info"); @@ -370,7 +370,8 @@ int MC_deadlock_check() return deadlock; } -void mc_update_comm_pattern(mc_call_type call_type, smx_simcall_t req, int value, xbt_dynar_t pattern) { +void handle_comm_pattern(e_mc_call_type_t call_type, smx_simcall_t req, int value, xbt_dynar_t pattern, int backtracking) { + switch(call_type) { case MC_CALL_TYPE_NONE: break; @@ -379,6 +380,7 @@ void mc_update_comm_pattern(mc_call_type call_type, smx_simcall_t req, int value get_comm_pattern(pattern, req, call_type); break; case MC_CALL_TYPE_WAIT: + case MC_CALL_TYPE_WAITANY: { smx_synchro_t current_comm = NULL; if (call_type == MC_CALL_TYPE_WAIT) @@ -387,12 +389,51 @@ void mc_update_comm_pattern(mc_call_type call_type, smx_simcall_t req, int value 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); + complete_comm_pattern(pattern, current_comm, backtracking); break; } default: xbt_die("Unexpected call type %i", (int)call_type); } + +} + +static void MC_restore_communications_pattern(mc_state_t state) { + mc_list_comm_pattern_t list_process_comm; + unsigned int cursor, cursor2; + xbt_dynar_foreach(initial_communications_pattern, cursor, list_process_comm){ + list_process_comm->index_comm = (int)xbt_dynar_get_as(state->index_comm, cursor, int); + } + mc_comm_pattern_t comm; + cursor = 0; + xbt_dynar_t initial_incomplete_process_comms, incomplete_process_comms; + for(int i=0; iincomplete_comm_pattern, i, xbt_dynar_t); + xbt_dynar_foreach(incomplete_process_comms, cursor2, comm) { + mc_comm_pattern_t copy_comm = xbt_new0(s_mc_comm_pattern_t, 1); + copy_comm->index = comm->index; + copy_comm->type = comm->type; + copy_comm->comm = comm->comm; + copy_comm->rdv = strdup(comm->rdv); + copy_comm->data_size = -1; + copy_comm->data = NULL; + if(comm->type == SIMIX_COMM_SEND){ + copy_comm->src_proc = comm->src_proc; + copy_comm->src_host = comm->src_host; + if(comm->data != NULL){ + copy_comm->data_size = comm->data_size; + copy_comm->data = xbt_malloc0(comm->data_size); + memcpy(copy_comm->data, comm->data, comm->data_size); + } + }else{ + copy_comm->dst_proc = comm->dst_proc; + copy_comm->dst_host = comm->dst_host; + } + xbt_dynar_push(initial_incomplete_process_comms, ©_comm); + } + } } /** @@ -749,11 +790,9 @@ void MC_print_statistics(mc_stats_t stats) } if (initial_global_state != NULL) { if (_sg_mc_comms_determinism) - XBT_INFO("Communication-deterministic : %s", - !initial_global_state->comm_deterministic ? "No" : "Yes"); + 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("Send-deterministic : %s", !initial_global_state->send_deterministic ? "No" : "Yes"); } mmalloc_set_current_heap(previous_heap); } diff --git a/src/mc/mc_state.c b/src/mc/mc_state.c index e9b4b04490..1f3abcec74 100644 --- a/src/mc/mc_state.c +++ b/src/mc/mc_state.c @@ -9,6 +9,52 @@ #include "mc_state.h" #include "mc_request.h" #include "mc_private.h" +#include "mc_comm_pattern.h" + +static void copy_incomplete_communications_pattern(mc_state_t state) { + int i; + xbt_dynar_t incomplete_process_comms; + mc_comm_pattern_t comm; + unsigned int cursor; + state->incomplete_comm_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp); + for (i=0; iindex = comm->index; + copy_comm->type = comm->type; + copy_comm->comm = comm->comm; + copy_comm->rdv = strdup(comm->rdv); + copy_comm->data_size = -1; + copy_comm->data = NULL; + if(comm->type == SIMIX_COMM_SEND){ + copy_comm->src_proc = comm->src_proc; + copy_comm->src_host = comm->src_host; + if (comm->data != NULL) { + copy_comm->data_size = comm->data_size; + copy_comm->data = xbt_malloc0(comm->data_size); + memcpy(copy_comm->data, comm->data, comm->data_size); + } + }else{ + copy_comm->dst_proc = comm->dst_proc; + copy_comm->dst_host = comm->dst_host; + } + xbt_dynar_push(incomplete_process_comms_copy, ©_comm); + } + xbt_dynar_insert_at(state->incomplete_comm_pattern, i, &incomplete_process_comms_copy); + } +} + +static void copy_index_communications_pattern(mc_state_t state) { + + state->index_comm = xbt_dynar_new(sizeof(unsigned int), NULL); + mc_list_comm_pattern_t list_process_comm; + unsigned int cursor; + xbt_dynar_foreach(initial_communications_pattern, cursor, list_process_comm){ + xbt_dynar_push_as(state->index_comm, unsigned int, list_process_comm->index_comm); + } +} /** * \brief Creates a state data structure used by the exploration algorithm diff --git a/src/mc/mc_visited.c b/src/mc/mc_visited.c index 8ac5d0fa73..0c3c971b78 100644 --- a/src/mc/mc_visited.c +++ b/src/mc/mc_visited.c @@ -208,20 +208,25 @@ int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max) * \brief Checks whether a given state has already been visited by the algorithm. */ -mc_visited_state_t is_visited_state() +mc_visited_state_t is_visited_state(mc_state_t graph_state) { if (_sg_mc_visited == 0) return NULL; + int partial_comm = 0; + /* If comm determinism verification, we cannot stop the exploration if some communications are not finished (at least, data are transfered). These communications - are incomplete and they cannot be analyzed and compared with the initial pattern */ + are incomplete and they cannot be analyzed and compared with the initial pattern. */ if (_sg_mc_comms_determinism || _sg_mc_send_determinism) { int current_process = 1; while (current_process < simix_process_maxpid) { - if (!xbt_dynar_is_empty((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t))) - return NULL; + if (!xbt_dynar_is_empty((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t))){ + XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited."); + partial_comm = 1; + break; + } current_process++; } }