From: Marion Guthmuller Date: Thu, 26 Jun 2014 15:49:25 +0000 (+0200) Subject: model-checker : visited states reduction available with comm determinism verification X-Git-Tag: v3_12~956^2~4 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/83a2c3a9dd2104f4db2f42a483b212f07aa39f6b?hp=c3d9e19f326834612b2acff8b8352ecf9108ac01 model-checker : visited states reduction available with comm determinism verification --- diff --git a/src/mc/mc_comm_determinism.c b/src/mc/mc_comm_determinism.c index 37a6f9054f..ff049896a7 100644 --- a/src/mc/mc_comm_determinism.c +++ b/src/mc/mc_comm_determinism.c @@ -68,53 +68,56 @@ static int compare_comm_pattern(mc_comm_pattern_t comm1, return 0; } -static void deterministic_pattern(xbt_dynar_t initial_pattern, - xbt_dynar_t pattern) +static void deterministic_pattern(xbt_dynar_t pattern, int partial) { - if (!xbt_dynar_is_empty(incomplete_communications_pattern)) - xbt_die - ("Damn ! Some communications are incomplete that means one or several simcalls are not handle ... "); - unsigned int cursor = 0, send_index = 0, recv_index = 0; mc_comm_pattern_t comm1, comm2; - int comm_comparison = 0; - int current_process = 0; + 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) { - while (cursor < xbt_dynar_length(initial_pattern)) { - comm1 = - (mc_comm_pattern_t) xbt_dynar_get_as(initial_pattern, cursor, - mc_comm_pattern_t); - if (comm1->type == SIMIX_COMM_SEND && comm1->src_proc == current_process) { - comm2 = - get_comm_pattern_from_idx(pattern, &send_index, comm1->type, - current_process); - comm_comparison = compare_comm_pattern(comm1, comm2); - if (comm_comparison == 1) { - initial_global_state->send_deterministic = 0; - initial_global_state->comm_deterministic = 0; - return; - } - send_index++; - } else if (comm1->type == SIMIX_COMM_RECEIVE - && comm1->dst_proc == current_process) { - comm2 = - get_comm_pattern_from_idx(pattern, &recv_index, comm1->type, - current_process); - comm_comparison = compare_comm_pattern(comm1, comm2); - if (comm_comparison == 1) { - initial_global_state->comm_deterministic = 0; - if (!_sg_mc_send_determinism) + 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 && comm1->src_proc == current_process) { + 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!", current_process); + initial_global_state->send_deterministic = 0; + initial_global_state->comm_deterministic = 0; return; + } + send_index++; + } else if (comm1->type == SIMIX_COMM_RECEIVE && comm1->dst_proc == current_process) { + 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!", current_process); + return; + } + } + recv_index++; } - recv_index++; + cursor++; } - cursor++; } + current_process++; cursor = 0; send_index = 0; recv_index = 0; - current_process++; } } @@ -122,18 +125,46 @@ static void print_communications_pattern(xbt_dynar_t comms_pattern) { unsigned int cursor = 0; mc_comm_pattern_t current_comm; - xbt_dynar_foreach(comms_pattern, cursor, current_comm) { - if (current_comm->type == SIMIX_COMM_SEND) - XBT_INFO("[(%lu) %s -> (%lu) %s] %s ", 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, - current_comm->dst_host, current_comm->src_proc, - current_comm->src_host, "iRecv"); + 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); + XBT_INFO("Communications from the process %u:", current_process); + xbt_dynar_foreach(current_pattern, cursor, current_comm) { + if (current_comm->type == SIMIX_COMM_SEND) { + XBT_INFO("[(%lu) %s -> (%lu) %s] %s ", 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, + current_comm->dst_host, current_comm->src_proc, + current_comm->src_host, "iRecv"); + } + } + current_process++; + cursor = 0; } } +static void update_comm_pattern(mc_comm_pattern_t comm_pattern, smx_action_t comm) +{ + 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->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 > std_heap && addr_pointed < ((xbt_mheap_t) std_heap)->breakval) + memcpy(comm_pattern->data, addr_pointed, comm_pattern->data_size); + else + memcpy(comm_pattern->data, comm->comm.src_buff, comm_pattern->data_size); + } +} /********** Non Static functions ***********/ @@ -145,8 +176,8 @@ void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, int call) pattern->data_size = -1; void *addr_pointed; if (call == 1) { // ISEND - pattern->comm = simcall_comm_isend__get__result(request); pattern->type = SIMIX_COMM_SEND; + pattern->comm = simcall_comm_isend__get__result(request); 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; @@ -158,11 +189,10 @@ void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, int call) else memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size); } else { // IRECV - pattern->comm = simcall_comm_irecv__get__result(request); 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(pattern->comm->comm.dst_proc->smx_host); + pattern->dst_host = simcall_host_get_name(request->issuer->smx_host); } if (pattern->comm->comm.rdv != NULL) @@ -170,49 +200,52 @@ void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, int call) else pattern->rdv = strdup(pattern->comm->comm.rdv_cpy->name); - xbt_dynar_push(list, &pattern); + xbt_dynar_push((xbt_dynar_t)xbt_dynar_get_as(list, request->issuer->pid, xbt_dynar_t), &pattern); - xbt_dynar_push_as(incomplete_communications_pattern, int, - xbt_dynar_length(list) - 1); + 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); } void complete_comm_pattern(xbt_dynar_t list, smx_action_t comm) { - mc_comm_pattern_t current_pattern; + mc_comm_pattern_t current_comm_pattern; unsigned int cursor = 0; int index; - int completed = 0; - void *addr_pointed; - 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 == comm) { - current_pattern->src_proc = comm->comm.src_proc->pid; - current_pattern->dst_proc = comm->comm.dst_proc->pid; - current_pattern->src_host = - simcall_host_get_name(comm->comm.src_proc->smx_host); - current_pattern->dst_host = - simcall_host_get_name(comm->comm.dst_proc->smx_host); - if (current_pattern->data_size == -1) { - current_pattern->data_size = *(comm->comm.dst_buff_size); - current_pattern->data = xbt_malloc0(current_pattern->data_size); - addr_pointed = *(void **) comm->comm.src_buff; - if (addr_pointed > std_heap - && addr_pointed < ((xbt_mheap_t) std_heap)->breakval) - memcpy(current_pattern->data, addr_pointed, - current_pattern->data_size); - else - memcpy(current_pattern->data, comm->comm.src_buff, - current_pattern->data_size); - } - xbt_dynar_remove_at(incomplete_communications_pattern, cursor, NULL); - completed++; - if (completed == 2) - return; - cursor--; + unsigned int src = comm->comm.src_proc->pid; + unsigned int dst = comm->comm.dst_proc->pid; + 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){ + 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; + 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){ + 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; + break; } } + + if(!dst_completed) + xbt_die("Corresponding communication for the dest process not found!"); + + } /************************ Main algorithm ************************/ @@ -224,19 +257,30 @@ void MC_pre_modelcheck_comm_determinism(void) 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); - - 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); + 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; i 0) { @@ -291,7 +336,7 @@ void MC_modelcheck_comm_determinism(void) if ((xbt_fifo_size(mc_stack) <= _sg_mc_max_depth) && (req = MC_state_get_request(state, &value)) - && (visited_state == -1)) { + && (visited_state == NULL)) { /* Debug information */ if (XBT_LOG_ISENABLED(mc_comm_determinism, xbt_log_priority_debug)) { @@ -311,46 +356,36 @@ void MC_modelcheck_comm_determinism(void) /* TODO : handle test and testany simcalls */ if (_sg_mc_comms_determinism || _sg_mc_send_determinism) { if (req->call == SIMCALL_COMM_ISEND) - comm_pattern = 1; + call = 1; else if (req->call == SIMCALL_COMM_IRECV) - comm_pattern = 2; + call = 2; else if (req->call == SIMCALL_COMM_WAIT) - comm_pattern = 3; + call = 3; else if (req->call == SIMCALL_COMM_WAITANY) - comm_pattern = 4; + call = 4; } /* Answer the request */ SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */ MC_SET_MC_HEAP; - if (comm_pattern == 1 || comm_pattern == 2) { - if (!initial_global_state->initial_communications_pattern_done) - get_comm_pattern(initial_communications_pattern, req, comm_pattern); - else - get_comm_pattern(communications_pattern, req, comm_pattern); - } else if (comm_pattern == 3) { + 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 */ - if (!initial_global_state->initial_communications_pattern_done) - complete_comm_pattern(initial_communications_pattern, current_comm); - else - complete_comm_pattern(communications_pattern, current_comm); - } - } else if (comm_pattern == 4) { - 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 */ - if (!initial_global_state->initial_communications_pattern_done) - complete_comm_pattern(initial_communications_pattern, current_comm); - else - complete_comm_pattern(communications_pattern, current_comm); - } + 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_SET_STD_HEAP; - comm_pattern = 0; + call = 0; /* Wait for requests (schedules processes) */ MC_wait_for_requests(); @@ -360,9 +395,9 @@ void MC_modelcheck_comm_determinism(void) next_state = MC_state_new(); - if ((visited_state = is_visited_state()) == -1) { + if ((visited_state = is_visited_state()) == NULL) { - /* Get an enabled process and insert it in the interleave set of the next state */ + /* Get enabled processes and insert them in the interleave set of the next state */ xbt_swag_foreach(process, simix_global->process_list) { if (MC_process_is_enabled(process)) { MC_state_interleave_process(next_state, process); @@ -377,7 +412,7 @@ void MC_modelcheck_comm_determinism(void) if (dot_output != NULL) fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, - visited_state, req_str); + visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str); } @@ -392,50 +427,48 @@ void MC_modelcheck_comm_determinism(void) if (xbt_fifo_size(mc_stack) > _sg_mc_max_depth) { XBT_WARN("/!\\ Max depth reached ! /!\\ "); - } else if (visited_state != -1) { - XBT_DEBUG("State already visited, exploration stopped on this path."); + } else if (visited_state != NULL) { + XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.", visited_state->other_num == -1 ? visited_state->num : visited_state->other_num); } else { - XBT_DEBUG("There are no more processes to interleave. (depth %d)", - xbt_fifo_size(mc_stack) + 1); + XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack)); } MC_SET_MC_HEAP; if (initial_global_state->initial_communications_pattern_done) { - if (visited_state == -1) { - deterministic_pattern(initial_communications_pattern, - communications_pattern); - if (initial_global_state->comm_deterministic == 0 - && _sg_mc_comms_determinism) { + 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:"); + XBT_INFO("** Initial communications pattern (per process): **"); print_communications_pattern(initial_communications_pattern); - XBT_INFO("Communications pattern counter-example:"); + 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 (initial_global_state->send_deterministic == 0 - && _sg_mc_send_determinism) { + } 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:"); + XBT_INFO("** Initial communications pattern: **"); print_communications_pattern(initial_communications_pattern); - XBT_INFO("Communications pattern counter-example:"); + XBT_INFO("** Communications pattern counter-example: **"); print_communications_pattern(communications_pattern); MC_print_statistics(mc_stats); MC_SET_STD_HEAP; return; - } - } else { - } + } else { initial_global_state->initial_communications_pattern_done = 1; } @@ -448,7 +481,7 @@ void MC_modelcheck_comm_determinism(void) MC_SET_STD_HEAP; - visited_state = -1; + visited_state = NULL; /* Check for deadlocks */ if (MC_deadlock_check()) { diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index a3de319ea1..fe8508bb6b 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -129,6 +129,7 @@ void _mc_cfg_cb_comms_determinism(const char *name, int pos) ("You are specifying a value to enable/disable the detection of determinism in the communications schemes after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry."); } _sg_mc_comms_determinism = xbt_cfg_get_boolean(_sg_cfg_set, name); + mc_reduce_kind = e_mc_reduce_none; } void _mc_cfg_cb_send_determinism(const char *name, int pos) @@ -138,6 +139,7 @@ void _mc_cfg_cb_send_determinism(const char *name, int pos) ("You are specifying a value to enable/disable the detection of send-determinism in the communications schemes after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry."); } _sg_mc_send_determinism = xbt_cfg_get_boolean(_sg_cfg_set, name); + mc_reduce_kind = e_mc_reduce_none; } /* MC global data structures */ @@ -276,6 +278,9 @@ void MC_init() MC_ignore_global_variable("maestro_stack_start"); MC_ignore_global_variable("maestro_stack_end"); MC_ignore_global_variable("smx_total_comms"); + MC_ignore_global_variable("communications_pattern"); + MC_ignore_global_variable("initial_communications_pattern"); + MC_ignore_global_variable("incomplete_communications_pattern"); MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double)); @@ -478,13 +483,12 @@ void MC_replay(xbt_fifo_t stack, int start) { int raw_mem = (mmalloc_get_current_heap() == mc_heap); - int value, i = 1, count = 1; + int value, i = 1, count = 1, call = 0, j; char *req_str; smx_simcall_t req = NULL, saved_req = NULL; xbt_fifo_item_t item, start_item; mc_state_t state; smx_process_t process = NULL; - int comm_pattern = 0; smx_action_t current_comm; XBT_DEBUG("**** Begin Replay ****"); @@ -507,7 +511,7 @@ void MC_replay(xbt_fifo_t stack, int start) MC_SET_MC_HEAP; - if ((mc_reduce_kind == e_mc_reduce_dpor) && !_sg_mc_comms_determinism && !_sg_mc_send_determinism) { + 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)) { @@ -520,8 +524,12 @@ void MC_replay(xbt_fifo_t stack, int start) } if (_sg_mc_comms_determinism || _sg_mc_send_determinism) { - xbt_dynar_reset(communications_pattern); - xbt_dynar_reset(incomplete_communications_pattern); + for (j=0; jissuer->pid); xbt_dict_remove(first_enabled_state, key); @@ -558,36 +566,34 @@ void MC_replay(xbt_fifo_t stack, int start) /* TODO : handle test and testany simcalls */ if (_sg_mc_comms_determinism || _sg_mc_send_determinism) { if (req->call == SIMCALL_COMM_ISEND) - comm_pattern = 1; + call = 1; else if (req->call == SIMCALL_COMM_IRECV) - comm_pattern = 2; + call = 2; else if (req->call == SIMCALL_COMM_WAIT) - comm_pattern = 3; + call = 3; else if (req->call == SIMCALL_COMM_WAITANY) - comm_pattern = 4; + call = 4; } SIMIX_simcall_pre(req, value); if (_sg_mc_comms_determinism || _sg_mc_send_determinism) { MC_SET_MC_HEAP; - if (comm_pattern == 1 || comm_pattern == 2) { - get_comm_pattern(communications_pattern, req, comm_pattern); - } else if (comm_pattern == 3 /* || comm_pattern == 4 */ ) { + if (call == 1) { /* Send */ + get_comm_pattern(communications_pattern, req, call); + } else if (call == 2) { /* Recv */ + get_comm_pattern(communications_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 */ + if (current_comm->comm.refcount == 1) /* First wait only must be considered */ complete_comm_pattern(communications_pattern, current_comm); - } - } else if (comm_pattern == 4 /* || comm_pattern == 4 */ ) { - 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 */ + } 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(communications_pattern, current_comm); - } } MC_SET_STD_HEAP; - comm_pattern = 0; + call = 0; } @@ -595,7 +601,7 @@ void MC_replay(xbt_fifo_t stack, int start) count++; - if ((mc_reduce_kind == e_mc_reduce_dpor) && !_sg_mc_comms_determinism && !_sg_mc_send_determinism) { + if (mc_reduce_kind == e_mc_reduce_dpor) { MC_SET_MC_HEAP; /* Insert in dict all enabled processes */ xbt_swag_foreach(process, simix_global->process_list) { diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index dd30b53972..5395a1d80a 100644 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@ -342,7 +342,7 @@ typedef struct s_mc_visited_state{ }s_mc_visited_state_t, *mc_visited_state_t; extern xbt_dynar_t visited_states; -int is_visited_state(void); +mc_visited_state_t is_visited_state(void); void visited_state_free(mc_visited_state_t state); void visited_state_free_voidp(void *s); @@ -592,6 +592,7 @@ typedef struct s_mc_comm_pattern{ void *data; }s_mc_comm_pattern_t, *mc_comm_pattern_t; +extern xbt_dynar_t initial_communications_pattern; extern xbt_dynar_t communications_pattern; extern xbt_dynar_t incomplete_communications_pattern; diff --git a/src/mc/mc_safety.c b/src/mc/mc_safety.c index a77883fdcc..6f671f2bdf 100644 --- a/src/mc/mc_safety.c +++ b/src/mc/mc_safety.c @@ -93,7 +93,7 @@ void MC_modelcheck_safety(void) xbt_fifo_item_t item = NULL; mc_state_t state_test = NULL; int pos; - int visited_state = -1; + mc_visited_state_t visited_state = NULL; int enabled = 0; while (xbt_fifo_size(mc_stack) > 0) { @@ -115,7 +115,7 @@ void MC_modelcheck_safety(void) /* If there are processes to interleave and the maximum depth has not been reached then perform one step of the exploration algorithm */ if (xbt_fifo_size(mc_stack) <= _sg_mc_max_depth && !user_max_depth_reached - && (req = MC_state_get_request(state, &value)) && visited_state == -1) { + && (req = MC_state_get_request(state, &value)) && visited_state == NULL) { /* Debug information */ if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) { @@ -151,7 +151,7 @@ void MC_modelcheck_safety(void) next_state = MC_state_new(); - if ((visited_state = is_visited_state()) == -1) { + if ((visited_state = is_visited_state()) == NULL) { /* Get an enabled process and insert it in the interleave set of the next state */ xbt_swag_foreach(process, simix_global->process_list) { @@ -175,7 +175,7 @@ void MC_modelcheck_safety(void) if (dot_output != NULL) fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, - visited_state, req_str); + visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str); } @@ -206,14 +206,14 @@ void MC_modelcheck_safety(void) } else { if ((xbt_fifo_size(mc_stack) > _sg_mc_max_depth) || user_max_depth_reached - || visited_state != -1) { + || visited_state != NULL) { - if (user_max_depth_reached && visited_state == -1) + if (user_max_depth_reached && visited_state == NULL) XBT_DEBUG("User max depth reached !"); - else if (visited_state == -1) + else if (visited_state == NULL) XBT_WARN("/!\\ Max depth reached ! /!\\ "); else - XBT_DEBUG("State already visited, exploration stopped on this path."); + XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.", visited_state->other_num == -1 ? visited_state->num : visited_state->other_num); if (mc_reduce_kind == e_mc_reduce_dpor) { /* Interleave enabled processes in the state in which they have been enabled for the first time */ @@ -257,7 +257,7 @@ void MC_modelcheck_safety(void) MC_SET_STD_HEAP; - visited_state = -1; + visited_state = NULL; /* Check for deadlocks */ if (MC_deadlock_check()) { diff --git a/src/mc/mc_visited.c b/src/mc/mc_visited.c index 0cd160042b..1767124df9 100644 --- a/src/mc/mc_visited.c +++ b/src/mc/mc_visited.c @@ -104,12 +104,12 @@ int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max) int nb_processes, heap_bytes_used, nb_processes_test, heap_bytes_used_test; void *ref_test; - if (_sg_mc_safety) { - nb_processes = ((mc_visited_state_t) ref)->nb_processes; - heap_bytes_used = ((mc_visited_state_t) ref)->heap_bytes_used; - } else if (_sg_mc_liveness) { + if (_sg_mc_liveness) { nb_processes = ((mc_visited_pair_t) ref)->nb_processes; heap_bytes_used = ((mc_visited_pair_t) ref)->heap_bytes_used; + } else { + nb_processes = ((mc_visited_state_t) ref)->nb_processes; + heap_bytes_used = ((mc_visited_state_t) ref)->heap_bytes_used; } int start = 0; @@ -117,17 +117,17 @@ int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max) while (start <= end) { cursor = (start + end) / 2; - if (_sg_mc_safety) { - ref_test = - (mc_visited_state_t) xbt_dynar_get_as(list, cursor, - mc_visited_state_t); - nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes; - heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used; - } else if (_sg_mc_liveness) { + if (_sg_mc_liveness) { ref_test = - (mc_visited_pair_t) xbt_dynar_get_as(list, cursor, mc_visited_pair_t); + (mc_visited_pair_t) xbt_dynar_get_as(list, cursor, mc_visited_pair_t); nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes; heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used; + } else { + ref_test = + (mc_visited_state_t) xbt_dynar_get_as(list, cursor, + mc_visited_state_t); + nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes; + heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used; } if (nb_processes_test < nb_processes) { start = cursor + 1; @@ -142,20 +142,20 @@ int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max) *min = *max = cursor; previous_cursor = cursor - 1; while (previous_cursor >= 0) { - if (_sg_mc_safety) { + if (_sg_mc_liveness) { + ref_test = + (mc_visited_pair_t) xbt_dynar_get_as(list, previous_cursor, + mc_visited_pair_t); + nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes; + heap_bytes_used_test = + ((mc_visited_pair_t) ref_test)->heap_bytes_used; + } else { ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, previous_cursor, mc_visited_state_t); nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes; heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used; - } else if (_sg_mc_liveness) { - ref_test = - (mc_visited_pair_t) xbt_dynar_get_as(list, previous_cursor, - mc_visited_pair_t); - nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes; - heap_bytes_used_test = - ((mc_visited_pair_t) ref_test)->heap_bytes_used; } if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used) @@ -165,20 +165,20 @@ int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max) } next_cursor = cursor + 1; while (next_cursor < xbt_dynar_length(list)) { - if (_sg_mc_safety) { - ref_test = - (mc_visited_state_t) xbt_dynar_get_as(list, next_cursor, - mc_visited_state_t); - nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes; - heap_bytes_used_test = - ((mc_visited_state_t) ref_test)->heap_bytes_used; - } else if (_sg_mc_liveness) { + if (_sg_mc_liveness) { ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, next_cursor, mc_visited_pair_t); nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes; heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used; + } else { + ref_test = + (mc_visited_state_t) xbt_dynar_get_as(list, next_cursor, + mc_visited_state_t); + nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes; + heap_bytes_used_test = + ((mc_visited_state_t) ref_test)->heap_bytes_used; } if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used) @@ -203,11 +203,24 @@ 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. */ -int is_visited_state() + +mc_visited_state_t is_visited_state() { if (_sg_mc_visited == 0) - return -1; + return NULL; + + /* 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 */ + 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; + current_process++; + } + } int mc_mem_set = (mmalloc_get_current_heap() == mc_heap); @@ -222,7 +235,7 @@ int is_visited_state() if (!mc_mem_set) MC_SET_STD_HEAP; - return -1; + return NULL; } else { @@ -282,7 +295,7 @@ int is_visited_state() if (!mc_mem_set) MC_SET_STD_HEAP; - return new_state->other_num; + return state_test; } cursor++; } @@ -328,7 +341,7 @@ int is_visited_state() if (!mc_mem_set) MC_SET_STD_HEAP; - return -1; + return NULL; } }