X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/e5149b6787696e0041d192b0573dd0882a296c73..923896223efc203372ce0a7435cbdb7b539149f6:/src/mc/mc_visited.c diff --git a/src/mc/mc_visited.c b/src/mc/mc_visited.c index 8ac5d0fa73..941a780abd 100644 --- a/src/mc/mc_visited.c +++ b/src/mc/mc_visited.c @@ -18,10 +18,24 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_visited, mc, xbt_dynar_t visited_pairs; xbt_dynar_t visited_states; +static int is_exploration_stack_state(mc_visited_state_t state){ + xbt_fifo_item_t item = xbt_fifo_get_first_item(mc_stack); + while (item) { + if (((mc_state_t)xbt_fifo_get_item_content(item))->num == state->num){ + ((mc_state_t)xbt_fifo_get_item_content(item))->in_visited_states = 0; + return 1; + } + item = xbt_fifo_get_next_item(item); + } + return 0; +} + void visited_state_free(mc_visited_state_t state) { if (state) { - MC_free_snapshot(state->system_state); + if(!is_exploration_stack_state(state)){ + MC_free_snapshot(state->system_state); + } xbt_free(state); } } @@ -37,9 +51,12 @@ void visited_state_free_voidp(void *s) */ static mc_visited_state_t visited_state_new() { + mc_process_t process = &(mc_model_checker->process); mc_visited_state_t new_state = NULL; new_state = xbt_new0(s_mc_visited_state_t, 1); - new_state->heap_bytes_used = mmalloc_get_bytes_used(std_heap); + new_state->heap_bytes_used = mmalloc_get_bytes_used_remote( + MC_process_get_heap(process)->heaplimit, + MC_process_get_malloc_info(process)); new_state->nb_processes = xbt_swag_size(simix_global->process_list); new_state->system_state = MC_take_snapshot(mc_stats->expanded_states); new_state->num = mc_stats->expanded_states; @@ -47,16 +64,17 @@ static mc_visited_state_t visited_state_new() return new_state; } - -mc_visited_pair_t MC_visited_pair_new(int pair_num, - xbt_automaton_state_t automaton_state, - xbt_dynar_t atomic_propositions) +mc_visited_pair_t MC_visited_pair_new(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, mc_state_t graph_state) { + mc_process_t process = &(mc_model_checker->process); mc_visited_pair_t pair = NULL; pair = xbt_new0(s_mc_visited_pair_t, 1); - pair->graph_state = MC_state_new(); - pair->graph_state->system_state = MC_take_snapshot(pair_num); - pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap); + pair->graph_state = graph_state; + if(pair->graph_state->system_state == NULL) + pair->graph_state->system_state = MC_take_snapshot(pair_num); + pair->heap_bytes_used = mmalloc_get_bytes_used_remote( + MC_process_get_heap(process)->heaplimit, + MC_process_get_malloc_info(process)); pair->nb_processes = xbt_swag_size(simix_global->process_list); pair->automaton_state = automaton_state; pair->num = pair_num; @@ -72,10 +90,23 @@ mc_visited_pair_t MC_visited_pair_new(int pair_num, return pair; } +static int is_exploration_stack_pair(mc_visited_pair_t pair){ + xbt_fifo_item_t item = xbt_fifo_get_first_item(mc_stack); + while (item) { + if (((mc_pair_t)xbt_fifo_get_item_content(item))->num == pair->num){ + ((mc_pair_t)xbt_fifo_get_item_content(item))->visited_pair_removed = 1; + return 1; + } + item = xbt_fifo_get_next_item(item); + } + return 0; +} + void MC_visited_pair_delete(mc_visited_pair_t p) { p->automaton_state = NULL; - MC_state_delete(p->graph_state); + if( !is_exploration_stack_pair(p)) + MC_state_delete(p->graph_state, 1); xbt_dynar_free(&(p->atomic_propositions)); xbt_free(p); p = NULL; @@ -100,9 +131,7 @@ void MC_visited_pair_delete(mc_visited_pair_t p) int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max) { - int mc_mem_set = (mmalloc_get_current_heap() == mc_heap); - - MC_SET_MC_HEAP; + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); int cursor = 0, previous_cursor, next_cursor; int nb_processes, heap_bytes_used, nb_processes_test, heap_bytes_used_test; @@ -122,14 +151,11 @@ int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max) while (start <= end) { cursor = (start + end) / 2; if (_sg_mc_liveness) { - ref_test = - (mc_visited_pair_t) xbt_dynar_get_as(list, cursor, mc_visited_pair_t); + ref_test = (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); + 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; } @@ -147,22 +173,15 @@ int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max) previous_cursor = cursor - 1; while (previous_cursor >= 0) { if (_sg_mc_liveness) { - ref_test = - (mc_visited_pair_t) xbt_dynar_get_as(list, previous_cursor, - mc_visited_pair_t); + 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; + 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); + 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; + 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) + if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used) break; *min = previous_cursor; previous_cursor--; @@ -170,36 +189,26 @@ 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_liveness) { - ref_test = - (mc_visited_pair_t) xbt_dynar_get_as(list, next_cursor, - mc_visited_pair_t); + 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; + 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); + 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; + 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) + if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used) break; *max = next_cursor; next_cursor++; } - if (!mc_mem_set) - MC_SET_STD_HEAP; + mmalloc_set_current_heap(heap); return -1; } } } - if (!mc_mem_set) - MC_SET_STD_HEAP; - + mmalloc_set_current_heap(heap); return cursor; } @@ -208,37 +217,40 @@ 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; + while (current_process < MC_smx_get_maxpid()) { + 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++; } } - int mc_mem_set = (mmalloc_get_current_heap() == mc_heap); - - MC_SET_MC_HEAP; + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); mc_visited_state_t new_state = visited_state_new(); + graph_state->system_state = new_state->system_state; + graph_state->in_visited_states = 1; + XBT_DEBUG("Snapshot %p of visited state %d (exploration stack state %d)", new_state->system_state, new_state->num, graph_state->num); if (xbt_dynar_is_empty(visited_states)) { xbt_dynar_push(visited_states, &new_state); - - if (!mc_mem_set) - MC_SET_STD_HEAP; - + mmalloc_set_current_heap(heap); return NULL; } else { @@ -271,48 +283,44 @@ mc_visited_state_t is_visited_state() return new_state->other_num; } */ - cursor = min; - while (cursor <= max) { - state_test = - (mc_visited_state_t) xbt_dynar_get_as(visited_states, cursor, - mc_visited_state_t); - if (snapshot_compare(state_test, new_state) == 0) { - // The state has been visited: - - if (state_test->other_num == -1) - new_state->other_num = state_test->num; - else - new_state->other_num = state_test->other_num; - if (dot_output == NULL) - XBT_DEBUG("State %d already visited ! (equal to state %d)", - new_state->num, state_test->num); - else - XBT_DEBUG - ("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 (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 state_test; + if(!partial_comm && initial_global_state->initial_communications_pattern_done){ + + cursor = min; + while (cursor <= max) { + state_test = (mc_visited_state_t) xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t); + if (snapshot_compare(state_test, new_state) == 0) { + // The state has been visited: + + if (state_test->other_num == -1) + new_state->other_num = state_test->num; + else + new_state->other_num = state_test->other_num; + if (dot_output == NULL) + XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num); + else + XBT_DEBUG("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 (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); + XBT_DEBUG("Replace visited state %d with the new visited state %d", state_test->num, new_state->num); + + mmalloc_set_current_heap(heap); + return state_test; + } + cursor++; } - cursor++; } - - // The state has not been visited: insert the state in the dynamic array. + xbt_dynar_insert_at(visited_states, min, &new_state); - + XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, xbt_dynar_length(visited_states)); + } else { // The state has not been visited: insert the state in the dynamic array. - state_test = - (mc_visited_state_t) xbt_dynar_get_as(visited_states, index, - mc_visited_state_t); + state_test = (mc_visited_state_t) xbt_dynar_get_as(visited_states, index, mc_visited_state_t); if (state_test->nb_processes < new_state->nb_processes) { xbt_dynar_insert_at(visited_states, index + 1, &new_state); } else { @@ -322,11 +330,15 @@ mc_visited_state_t is_visited_state() xbt_dynar_insert_at(visited_states, index, &new_state); } + XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, xbt_dynar_length(visited_states)); + } // We have reached the maximum number of stored states; if (xbt_dynar_length(visited_states) > _sg_mc_visited) { + XBT_DEBUG("Try to remove visited state (maximum number of stored states reached)"); + // Find the (index of the) older state (with the smallest num): int min2 = mc_stats->expanded_states; unsigned int cursor2 = 0; @@ -340,43 +352,35 @@ mc_visited_state_t is_visited_state() // and drop it: xbt_dynar_remove_at(visited_states, index2, NULL); + XBT_DEBUG("Remove visited state (maximum number of stored states reached)"); } - if (!mc_mem_set) - MC_SET_STD_HEAP; - + mmalloc_set_current_heap(heap); return NULL; - } } /** * \brief Checks whether a given pair has already been visited by the algorithm. */ -int is_visited_pair(mc_visited_pair_t pair, int pair_num, - xbt_automaton_state_t automaton_state, - xbt_dynar_t atomic_propositions) -{ +int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair) { if (_sg_mc_visited == 0) return -1; - int mc_mem_set = (mmalloc_get_current_heap() == mc_heap); - - MC_SET_MC_HEAP; + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); - mc_visited_pair_t new_pair = NULL; + mc_visited_pair_t new_visited_pair = NULL; - if (pair == NULL) { - new_pair = - MC_visited_pair_new(pair_num, automaton_state, atomic_propositions); + if (visited_pair == NULL) { + new_visited_pair = MC_visited_pair_new(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state); } else { - new_pair = pair; + new_visited_pair = visited_pair; } if (xbt_dynar_is_empty(visited_pairs)) { - xbt_dynar_push(visited_pairs, &new_pair); + xbt_dynar_push(visited_pairs, &new_visited_pair); } else { @@ -385,7 +389,7 @@ int is_visited_pair(mc_visited_pair_t pair, int pair_num, mc_visited_pair_t pair_test; int cursor; - index = get_search_interval(visited_pairs, new_pair, &min, &max); + index = get_search_interval(visited_pairs, new_visited_pair, &min, &max); if (min != -1 && max != -1) { // Visited pair with same number of processes and same heap bytes used exists /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_pairs, min), (max-min)+1, pair); @@ -417,28 +421,20 @@ int is_visited_pair(mc_visited_pair_t pair, int pair_num, } */ cursor = min; while (cursor <= max) { - pair_test = - (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, cursor, - mc_visited_pair_t); - if (xbt_automaton_state_compare - (pair_test->automaton_state, new_pair->automaton_state) == 0) { - if (xbt_automaton_propositional_symbols_compare_value - (pair_test->atomic_propositions, - new_pair->atomic_propositions) == 0) { - if (snapshot_compare(pair_test, new_pair) == 0) { + pair_test = (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, cursor, mc_visited_pair_t); + if (xbt_automaton_state_compare(pair_test->automaton_state, new_visited_pair->automaton_state) == 0) { + if (xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, new_visited_pair->atomic_propositions) == 0) { + if (snapshot_compare(pair_test, new_visited_pair) == 0) { if (pair_test->other_num == -1) - new_pair->other_num = pair_test->num; + new_visited_pair->other_num = pair_test->num; else - new_pair->other_num = pair_test->other_num; + new_visited_pair->other_num = pair_test->other_num; if (dot_output == NULL) - XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", - new_pair->num, pair_test->num); + XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_visited_pair->num, pair_test->num); else - XBT_DEBUG - ("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", - new_pair->num, pair_test->num, new_pair->other_num); - xbt_dynar_remove_at(visited_pairs, cursor, NULL); - xbt_dynar_insert_at(visited_pairs, cursor, &new_pair); + XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", new_visited_pair->num, pair_test->num, new_visited_pair->other_num); + xbt_dynar_remove_at(visited_pairs, cursor, &pair_test); + xbt_dynar_insert_at(visited_pairs, cursor, &new_visited_pair); pair_test->visited_removed = 1; if (pair_test->acceptance_pair) { if (pair_test->acceptance_removed == 1) @@ -446,26 +442,23 @@ int is_visited_pair(mc_visited_pair_t pair, int pair_num, } else { MC_visited_pair_delete(pair_test); } - if (!mc_mem_set) - MC_SET_STD_HEAP; - return new_pair->other_num; + mmalloc_set_current_heap(heap); + return new_visited_pair->other_num; } } } cursor++; } - xbt_dynar_insert_at(visited_pairs, min, &new_pair); + xbt_dynar_insert_at(visited_pairs, min, &new_visited_pair); } else { - pair_test = - (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, index, - mc_visited_pair_t); - if (pair_test->nb_processes < new_pair->nb_processes) { - xbt_dynar_insert_at(visited_pairs, index + 1, &new_pair); + pair_test = (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, index, mc_visited_pair_t); + if (pair_test->nb_processes < new_visited_pair->nb_processes) { + xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair); } else { - if (pair_test->heap_bytes_used < new_pair->heap_bytes_used) - xbt_dynar_insert_at(visited_pairs, index + 1, &new_pair); + if (pair_test->heap_bytes_used < new_visited_pair->heap_bytes_used) + xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair); else - xbt_dynar_insert_at(visited_pairs, index, &new_pair); + xbt_dynar_insert_at(visited_pairs, index, &new_visited_pair); } } @@ -491,8 +484,6 @@ int is_visited_pair(mc_visited_pair_t pair, int pair_num, } - if (!mc_mem_set) - MC_SET_STD_HEAP; - + mmalloc_set_current_heap(heap); return -1; }