X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/76fcd6c75256746e4292484155108ab63f364ab5..251bbe5068a2a7b23a23a4df11fc1b785dce6ff4:/src/mc/mc_visited.c diff --git a/src/mc/mc_visited.c b/src/mc/mc_visited.c index d2dec58673..ac7c56b3c4 100644 --- a/src/mc/mc_visited.c +++ b/src/mc/mc_visited.c @@ -104,14 +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 { - xbt_die("Both liveness and safety are disabled."); + nb_processes = ((mc_visited_state_t) ref)->nb_processes; + heap_bytes_used = ((mc_visited_state_t) ref)->heap_bytes_used; } int start = 0; @@ -119,21 +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) { + if (_sg_mc_liveness) { 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) { - 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 { - nb_processes_test = 0; - heap_bytes_used_test = 0; - xbt_die("Both liveness and safety are disabled."); + 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; @@ -148,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) @@ -171,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) @@ -209,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); @@ -228,7 +235,7 @@ int is_visited_state() if (!mc_mem_set) MC_SET_STD_HEAP; - return -1; + return NULL; } else { @@ -280,18 +287,20 @@ int is_visited_state() ("State %d already visited ! (equal to state %d (state %d in dot_output))", new_state->num, state_test->num, new_state->other_num); - // Replace the old state with the new one (why?): + /* Replace the old state with the new one (with a bigger num) + (when the max number of visited states is reached, the oldest + one is removed according to its number (= with the min number) */ xbt_dynar_remove_at(visited_states, cursor, NULL); xbt_dynar_insert_at(visited_states, cursor, &new_state); if (!mc_mem_set) MC_SET_STD_HEAP; - return new_state->other_num; + return state_test; } cursor++; } - // The state has not been visited, add it to the list: + // The state has not been visited: insert the state in the dynamic array. xbt_dynar_insert_at(visited_states, min, &new_state); } else { @@ -314,7 +323,7 @@ int is_visited_state() // We have reached the maximum number of stored states; if (xbt_dynar_length(visited_states) > _sg_mc_visited) { - // Find the (index of the) older state: + // Find the (index of the) older state (with the smallest num): int min2 = mc_stats->expanded_states; unsigned int cursor2 = 0; unsigned int index2 = 0; @@ -332,7 +341,7 @@ int is_visited_state() if (!mc_mem_set) MC_SET_STD_HEAP; - return -1; + return NULL; } } @@ -407,7 +416,6 @@ int is_visited_pair(mc_visited_pair_t pair, int pair_num, pair_test = (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, cursor, mc_visited_pair_t); - //if(pair_test->acceptance_pair == 0){ /* Acceptance pair have been already checked before */ if (xbt_automaton_state_compare (pair_test->automaton_state, new_pair->automaton_state) == 0) { if (xbt_automaton_propositional_symbols_compare_value @@ -439,7 +447,6 @@ int is_visited_pair(mc_visited_pair_t pair, int pair_num, return new_pair->other_num; } } - //} } cursor++; }