From: Marion Guthmuller Date: Tue, 19 Mar 2013 18:27:51 +0000 (+0100) Subject: model-checker : order reached_pairs by number of processes and heap bytes used X-Git-Tag: v3_9_90~424^2~8 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/ff3607bbc694290df2b8b5b722b9a02e8834f37c?ds=sidebyside model-checker : order reached_pairs by number of processes and heap bytes used --- diff --git a/examples/msg/mc/bugged1_liveness.tesh b/examples/msg/mc/bugged1_liveness.tesh index b083c7ca67..b0f05b3e17 100644 --- a/examples/msg/mc/bugged1_liveness.tesh +++ b/examples/msg/mc/bugged1_liveness.tesh @@ -39,7 +39,6 @@ $ ${bindir:=.}/bugged1_liveness --cfg=model-check:1 --cfg=contexts/factory:ucont > [0.000000] [mc_global/INFO] [(3)client] iSend (src=client, buff=(verbose only), size=(verbose only)) > [0.000000] [mc_global/INFO] [(1)coordinator] Wait (comm=(verbose only) [(3)client -> (1)coordinator]) > [0.000000] [mc_global/INFO] [(1)coordinator] iSend (src=coordinator, buff=(verbose only), size=(verbose only)) -> [0.000000] [mc_global/INFO] Expanded states = 22 -> [0.000000] [mc_global/INFO] Visited states = 21 +> [0.000000] [mc_global/INFO] Expanded pairs = 23 +> [0.000000] [mc_global/INFO] Visited pairs = 21 > [0.000000] [mc_global/INFO] Executed transitions = 21 -> [0.000000] [mc_global/INFO] Expanded / Visited = 0.954545 diff --git a/examples/msg/mc/chord/chord_neverjoin.tesh b/examples/msg/mc/chord/chord_neverjoin.tesh index 26881288ff..b458c9c7bf 100644 --- a/examples/msg/mc/chord/chord_neverjoin.tesh +++ b/examples/msg/mc/chord/chord_neverjoin.tesh @@ -25,7 +25,6 @@ $ ${bindir:=.}/chord_liveness --cfg=model-check:1 --cfg=contexts/factory:ucontex > [0.000000] [mc_global/INFO] [(1)node] Wait (comm=(verbose only) [(3)node -> (1)node]) > [0.000000] [mc_global/INFO] [(1)node] iRecv (dst=node, buff=(verbose only), size=(verbose only)) > [0.000000] [mc_global/INFO] [(1)node] Test FALSE (comm=(verbose only)) -> [0.000000] [mc_global/INFO] Expanded states = 11 -> [0.000000] [mc_global/INFO] Visited states = 10 +> [0.000000] [mc_global/INFO] Expanded pairs = 14 +> [0.000000] [mc_global/INFO] Visited pairs = 10 > [0.000000] [mc_global/INFO] Executed transitions = 10 -> [0.000000] [mc_global/INFO] Expanded / Visited = 0.909091 diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index 970ef80e3f..947fc558f6 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -527,7 +527,7 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack) depth++; /* Update statistics */ - mc_stats->visited_states++; + mc_stats->visited_pairs++; mc_stats->executed_transitions++; item = xbt_fifo_get_prev_item(item); @@ -570,7 +570,7 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack) depth++; /* Update statistics */ - mc_stats->visited_states++; + mc_stats->visited_pairs++; mc_stats->executed_transitions++; } } @@ -692,14 +692,14 @@ void MC_dump_stack_liveness(xbt_fifo_t stack){ void MC_print_statistics(mc_stats_t stats) { - //XBT_INFO("State space size ~= %lu", stats->state_size); - XBT_INFO("Expanded states = %lu", stats->expanded_states); - XBT_INFO("Visited states = %lu", stats->visited_states); + if(stats->expanded_pairs == 0){ + XBT_INFO("Expanded states = %lu", stats->expanded_states); + XBT_INFO("Visited states = %lu", stats->visited_states); + }else{ + XBT_INFO("Expanded pairs = %lu", stats->expanded_pairs); + XBT_INFO("Visited pairs = %lu", stats->visited_pairs); + } XBT_INFO("Executed transitions = %lu", stats->executed_transitions); - XBT_INFO("Expanded / Visited = %lf", - (double) stats->visited_states / stats->expanded_states); - /*XBT_INFO("Exploration coverage = %lf", - (double)stats->expanded_states / stats->state_size); */ } void MC_assert(int prop) diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c index f19a670201..7d07e0dda2 100644 --- a/src/mc/mc_liveness.c +++ b/src/mc/mc_liveness.c @@ -19,17 +19,15 @@ xbt_dynar_t successors; /********* Static functions *********/ -static int is_reached_acceptance_pair(xbt_automaton_state_t st){ - - int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); - - MC_SET_RAW_MEM; +static mc_acceptance_pair_t acceptance_pair_new(int num, xbt_automaton_state_t as){ mc_acceptance_pair_t new_pair = NULL; new_pair = xbt_new0(s_mc_acceptance_pair_t, 1); - new_pair->num = xbt_dynar_length(acceptance_pairs) + 1; - new_pair->automaton_state = st; + new_pair->num = num; + new_pair->automaton_state = as; new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL); + new_pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap); + new_pair->nb_processes = xbt_swag_size(simix_global->process_list); new_pair->system_state = MC_take_snapshot(); /* Get values of propositional symbols */ @@ -42,105 +40,219 @@ static int is_reached_acceptance_pair(xbt_automaton_state_t st){ res = f(); xbt_dynar_push_as(new_pair->prop_ato, int, res); } - + + return new_pair; + +} + +static int is_reached_acceptance_pair(int num, xbt_automaton_state_t as){ + + int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + + MC_SET_RAW_MEM; + mc_acceptance_pair_t new_pair = acceptance_pair_new(num, as); MC_UNSET_RAW_MEM; if(xbt_dynar_is_empty(acceptance_pairs)){ MC_SET_RAW_MEM; - /* New acceptance pair */ xbt_dynar_push(acceptance_pairs, &new_pair); MC_UNSET_RAW_MEM; if(raw_mem_set) MC_SET_RAW_MEM; - - return 0; + + return -1; }else{ MC_SET_RAW_MEM; - cursor = 0; + size_t current_bytes_used = new_pair->heap_bytes_used; + int current_nb_processes = new_pair->nb_processes; + + unsigned int cursor = 0; + int previous_cursor = 0, next_cursor = 0; + int start = 0; + int end = xbt_dynar_length(acceptance_pairs) - 1; + mc_acceptance_pair_t pair_test = NULL; - - xbt_dynar_foreach(acceptance_pairs, cursor, pair_test){ - if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)) - XBT_DEBUG("****** Pair reached #%d ******", pair_test->num); - if(xbt_automaton_state_compare(pair_test->automaton_state, st) == 0){ - if(xbt_automaton_propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){ - if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){ - - if(raw_mem_set) - MC_SET_RAW_MEM; - else - MC_UNSET_RAW_MEM; - - return 1; + size_t bytes_used_test; + int nb_processes_test; + int same_processes_and_bytes_not_found = 1; + + while(start <= end && same_processes_and_bytes_not_found){ + cursor = (start + end) / 2; + pair_test = (mc_acceptance_pair_t)xbt_dynar_get_as(acceptance_pairs, cursor, mc_acceptance_pair_t); + bytes_used_test = pair_test->heap_bytes_used; + nb_processes_test = pair_test->nb_processes; + if(nb_processes_test < current_nb_processes) + start = cursor + 1; + if(nb_processes_test > current_nb_processes) + end = cursor - 1; + if(nb_processes_test == current_nb_processes){ + if(bytes_used_test < current_bytes_used) + start = cursor + 1; + if(bytes_used_test > current_bytes_used) + end = cursor - 1; + if(bytes_used_test == current_bytes_used){ + same_processes_and_bytes_not_found = 0; + if(xbt_automaton_state_compare(pair_test->automaton_state, as) == 0){ + if(xbt_automaton_propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){ + if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){ + if(raw_mem_set) + MC_SET_RAW_MEM; + else + MC_UNSET_RAW_MEM; + return pair_test->num; + } + } + } + /* Search another pair with same number of bytes used in std_heap */ + previous_cursor = cursor - 1; + while(previous_cursor >= 0){ + pair_test = (mc_acceptance_pair_t)xbt_dynar_get_as(acceptance_pairs, previous_cursor, mc_acceptance_pair_t); + bytes_used_test = pair_test->system_state->heap_bytes_used; + if(bytes_used_test != current_bytes_used) + break; + if(xbt_automaton_state_compare(pair_test->automaton_state, as) == 0){ + if(xbt_automaton_propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){ + if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){ + if(raw_mem_set) + MC_SET_RAW_MEM; + else + MC_UNSET_RAW_MEM; + return pair_test->num; + } + } + } + previous_cursor--; + } + next_cursor = cursor + 1; + while(next_cursor < xbt_dynar_length(acceptance_pairs)){ + pair_test = (mc_acceptance_pair_t)xbt_dynar_get_as(acceptance_pairs, next_cursor, mc_acceptance_pair_t); + bytes_used_test = pair_test->system_state->heap_bytes_used; + if(bytes_used_test != current_bytes_used) + break; + if(xbt_automaton_state_compare(pair_test->automaton_state, as) == 0){ + if(xbt_automaton_propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){ + if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){ + if(raw_mem_set) + MC_SET_RAW_MEM; + else + MC_UNSET_RAW_MEM; + return pair_test->num; + } + } + } + next_cursor++; } - }else{ - XBT_DEBUG("Different values of propositional symbols"); } - }else{ - XBT_DEBUG("Different automaton state"); } } - /* New acceptance pair */ - xbt_dynar_push(acceptance_pairs, &new_pair); + pair_test = (mc_acceptance_pair_t)xbt_dynar_get_as(acceptance_pairs, cursor, mc_acceptance_pair_t); + bytes_used_test = pair_test->heap_bytes_used; + + if(bytes_used_test < current_bytes_used) + xbt_dynar_insert_at(acceptance_pairs, cursor + 1, &new_pair); + else + xbt_dynar_insert_at(acceptance_pairs, cursor, &new_pair); MC_UNSET_RAW_MEM; if(raw_mem_set) MC_SET_RAW_MEM; - - compare = 0; - return 0; + return -1; } + } -static void set_acceptance_pair_reached(xbt_automaton_state_t st){ +static void set_acceptance_pair_reached(int num, xbt_automaton_state_t as){ int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); MC_SET_RAW_MEM; + mc_acceptance_pair_t new_pair = acceptance_pair_new(num, as); + MC_UNSET_RAW_MEM; - mc_acceptance_pair_t pair = NULL; - pair = xbt_new0(s_mc_acceptance_pair_t, 1); - pair->num = xbt_dynar_length(acceptance_pairs) + 1; - pair->automaton_state = st; - pair->prop_ato = xbt_dynar_new(sizeof(int), NULL); - pair->system_state = MC_take_snapshot(); + if(xbt_dynar_is_empty(acceptance_pairs)){ - /* Get values of propositional symbols */ - unsigned int cursor = 0; - xbt_automaton_propositional_symbol_t ps = NULL; - int res; - int_f_void_t f; + MC_SET_RAW_MEM; + xbt_dynar_push(acceptance_pairs, &new_pair); + MC_UNSET_RAW_MEM; - xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){ - f = (int_f_void_t)ps->function; - res = f(); - xbt_dynar_push_as(pair->prop_ato, int, res); - } + }else{ - xbt_dynar_push(acceptance_pairs, &pair); - - MC_UNSET_RAW_MEM; + MC_SET_RAW_MEM; + + size_t current_bytes_used = new_pair->heap_bytes_used; + int current_nb_processes = new_pair->nb_processes; + + unsigned int cursor = 0; + int start = 0; + int end = xbt_dynar_length(acceptance_pairs) - 1; + + mc_acceptance_pair_t pair_test = NULL; + size_t bytes_used_test; + int nb_processes_test; + + while(start <= end){ + cursor = (start + end) / 2; + pair_test = (mc_acceptance_pair_t)xbt_dynar_get_as(acceptance_pairs, cursor, mc_acceptance_pair_t); + bytes_used_test = pair_test->heap_bytes_used; + nb_processes_test = pair_test->nb_processes; + if(nb_processes_test < current_nb_processes) + start = cursor + 1; + if(nb_processes_test > current_nb_processes) + end = cursor - 1; + if(nb_processes_test == current_nb_processes){ + if(bytes_used_test < current_bytes_used) + start = cursor + 1; + if(bytes_used_test > current_bytes_used) + end = cursor - 1; + if(bytes_used_test == current_bytes_used) + break; + } + } + + if(bytes_used_test < current_bytes_used) + xbt_dynar_insert_at(acceptance_pairs, cursor + 1, &new_pair); + else + xbt_dynar_insert_at(acceptance_pairs, cursor, &new_pair); + + MC_UNSET_RAW_MEM; + + } if(raw_mem_set) MC_SET_RAW_MEM; } -static mc_visited_pair_t visited_pair_new(xbt_automaton_state_t as){ +static void remove_acceptance_pair(int num_pair){ + + unsigned int cursor = 0; + mc_acceptance_pair_t current_pair; + + xbt_dynar_foreach(acceptance_pairs, cursor, current_pair){ + if(current_pair->num == num_pair) + break; + } + + xbt_dynar_remove_at(acceptance_pairs, cursor, NULL); + +} + +static mc_visited_pair_t visited_pair_new(int num, xbt_automaton_state_t as){ mc_visited_pair_t new_pair = NULL; new_pair = xbt_new0(s_mc_visited_pair_t, 1); new_pair->automaton_state = as; + new_pair->num = num; new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL); new_pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap); new_pair->nb_processes = xbt_swag_size(simix_global->process_list); @@ -161,7 +273,7 @@ static mc_visited_pair_t visited_pair_new(xbt_automaton_state_t as){ } -static int is_visited_pair(xbt_automaton_state_t as){ +static int is_visited_pair(int num, xbt_automaton_state_t as){ if(_sg_mc_visited == 0) return -1; @@ -169,7 +281,7 @@ static int is_visited_pair(xbt_automaton_state_t as){ int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); MC_SET_RAW_MEM; - mc_visited_pair_t new_pair = visited_pair_new(as); + mc_visited_pair_t new_pair = visited_pair_new(num, as); MC_UNSET_RAW_MEM; if(xbt_dynar_is_empty(visited_pairs)){ @@ -443,7 +555,7 @@ void MC_ddfs_init(void){ xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair); MC_UNSET_RAW_MEM; - set_acceptance_pair_reached(automaton_state); + set_acceptance_pair_reached(mc_initial_pair->num, automaton_state); if(cursor != 0){ MC_restore_snapshot(initial_state_liveness->snapshot); @@ -483,7 +595,7 @@ void MC_ddfs(int search_cycle){ XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle); - mc_stats->visited_states++; + mc_stats->visited_pairs++; int value; mc_state_t next_graph_state = NULL; @@ -498,7 +610,6 @@ void MC_ddfs(int search_cycle){ mc_pair_t pair_succ; mc_pair_t pair_to_remove; - mc_acceptance_pair_t acceptance_pair_to_remove; if(xbt_fifo_size(mc_stack_liveness) < _sg_mc_max_depth){ @@ -583,7 +694,7 @@ void MC_ddfs(int search_cycle){ if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ - if(is_reached_acceptance_pair(pair_succ->automaton_state)){ + if(is_reached_acceptance_pair(pair_succ->num, pair_succ->automaton_state) != -1){ XBT_INFO("Next pair (depth = %d, %u interleave) already reached !", xbt_fifo_size(mc_stack_liveness) + 1, MC_state_interleave_size(pair_succ->graph_state)); @@ -598,7 +709,7 @@ void MC_ddfs(int search_cycle){ }else{ - if(is_visited_pair(pair_succ->automaton_state) != -1){ + if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){ XBT_DEBUG("Next pair already visited !"); break; @@ -621,7 +732,7 @@ void MC_ddfs(int search_cycle){ }else{ - if(is_visited_pair(pair_succ->automaton_state) != -1){ + if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){ XBT_DEBUG("Next pair already visited !"); break; @@ -639,7 +750,7 @@ void MC_ddfs(int search_cycle){ }else{ - if(is_visited_pair(pair_succ->automaton_state) != -1){ + if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){ XBT_DEBUG("Next pair already visited !"); break; @@ -650,7 +761,7 @@ void MC_ddfs(int search_cycle){ XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id); - set_acceptance_pair_reached(pair_succ->automaton_state); + set_acceptance_pair_reached(pair_succ->num, pair_succ->automaton_state); search_cycle = 1; @@ -734,7 +845,7 @@ void MC_ddfs(int search_cycle){ if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ - if(is_reached_acceptance_pair(pair_succ->automaton_state)){ + if(is_reached_acceptance_pair(pair_succ->num, pair_succ->automaton_state) != -1){ XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1); @@ -749,7 +860,7 @@ void MC_ddfs(int search_cycle){ }else{ - if(is_visited_pair(pair_succ->automaton_state) != -1){ + if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){ XBT_DEBUG("Next pair already visited !"); break; @@ -772,7 +883,7 @@ void MC_ddfs(int search_cycle){ }else{ - if(is_visited_pair(pair_succ->automaton_state) != -1){ + if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){ XBT_DEBUG("Next pair already visited !"); break; @@ -792,7 +903,7 @@ void MC_ddfs(int search_cycle){ }else{ - if(is_visited_pair(pair_succ->automaton_state) != -1){ + if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){ XBT_DEBUG("Next pair already visited !"); break; @@ -801,7 +912,7 @@ void MC_ddfs(int search_cycle){ if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){ - set_acceptance_pair_reached(pair_succ->automaton_state); + set_acceptance_pair_reached(pair_succ->num, pair_succ->automaton_state); search_cycle = 1; @@ -849,9 +960,7 @@ void MC_ddfs(int search_cycle){ xbt_fifo_remove(mc_stack_liveness, pair_to_remove); pair_to_remove = NULL; if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){ - acceptance_pair_to_remove = xbt_dynar_pop_as(acceptance_pairs, mc_acceptance_pair_t); - acceptance_pair_free(acceptance_pair_to_remove); - acceptance_pair_to_remove = NULL; + remove_acceptance_pair(current_pair->num); } MC_UNSET_RAW_MEM; diff --git a/src/mc/mc_pair.c b/src/mc/mc_pair.c index 9e8ff3ed88..bd686f940d 100644 --- a/src/mc/mc_pair.c +++ b/src/mc/mc_pair.c @@ -12,6 +12,7 @@ mc_pair_t MC_pair_new(mc_state_t gs, xbt_automaton_state_t as, int r){ p->graph_state = gs; p->system_state = NULL; p->requests = r; + p->num = ++mc_stats->expanded_pairs; return p; } diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index 15deac2caf..4839b41793 100644 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@ -140,7 +140,9 @@ void MC_state_remove_interleave_process(mc_state_t state, smx_process_t process) typedef struct mc_stats { unsigned long state_size; unsigned long visited_states; + unsigned long visited_pairs; unsigned long expanded_states; + unsigned long expanded_pairs; unsigned long executed_transitions; } s_mc_stats_t, *mc_stats_t; @@ -285,6 +287,7 @@ typedef struct s_mc_pair{ mc_state_t graph_state; xbt_automaton_state_t automaton_state; int requests; + int num; }s_mc_pair_t, *mc_pair_t; typedef struct s_mc_acceptance_pair{ @@ -292,6 +295,8 @@ typedef struct s_mc_acceptance_pair{ xbt_automaton_state_t automaton_state; xbt_dynar_t prop_ato; mc_snapshot_t system_state; + size_t heap_bytes_used; + int nb_processes; }s_mc_acceptance_pair_t, *mc_acceptance_pair_t; typedef struct s_mc_visited_pair{