From 9788cd051f72b982ec571c96e84577e9749188b1 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Tue, 1 Oct 2013 10:46:58 +0200 Subject: [PATCH] model-checker : parallel system state comparison for safety MC --- src/mc/mc_compare.c | 42 +++++--- src/mc/mc_dpor.c | 231 ++++++++++++++++++++------------------------ src/mc/mc_private.h | 2 +- 3 files changed, 132 insertions(+), 143 deletions(-) diff --git a/src/mc/mc_compare.c b/src/mc/mc_compare.c index 3cb30bfd81..b58023327b 100644 --- a/src/mc/mc_compare.c +++ b/src/mc/mc_compare.c @@ -330,10 +330,22 @@ static int compare_local_variables(mc_snapshot_stack_t stack1, mc_snapshot_stack } } -int snapshot_compare(void *p1, void *p2){ +int snapshot_compare(void *state1, void *state2){ - mc_snapshot_t s1 = ((mc_pair_t)p1)->graph_state->system_state; - mc_snapshot_t s2 = ((mc_pair_t)p2)->graph_state->system_state; + mc_snapshot_t s1, s2; + int num1, num2; + + if(_sg_mc_property_file && _sg_mc_property_file[0] != '\0'){ /* Liveness MC */ + s1 = ((mc_pair_t)state1)->graph_state->system_state; + s2 = ((mc_pair_t)state2)->graph_state->system_state; + num1 = ((mc_pair_t)state1)->num; + num2 = ((mc_pair_t)state2)->num; + }else{ /* Safety MC */ + s1 = ((mc_visited_state_t)state1)->system_state; + s2 = ((mc_visited_state_t)state2)->system_state; + num1 = ((mc_visited_state_t)state1)->num; + num2 = ((mc_visited_state_t)state2)->num; + } int errors = 0; int res_init; @@ -360,12 +372,12 @@ int snapshot_compare(void *p1, void *p2){ xbt_os_walltimer_stop(timer); mc_comp_times->stacks_sizes_comparison_time = xbt_os_timer_elapsed(timer); } - XBT_DEBUG("(%d - %d) Different size used in stacks : %zu - %zu", ((mc_pair_t)p1)->num, ((mc_pair_t)p2)->num, size_used1, size_used2); + XBT_DEBUG("(%d - %d) Different size used in stacks : %zu - %zu", num1, num2, size_used1, size_used2); errors++; is_diff = 1; #else #ifdef MC_VERBOSE - XBT_VERB("(%d - %d) Different size used in stacks : %zu - %zu", ((mc_pair_t)p1)->num, ((mc_pair_t)p2)->num, size_used1, size_used2); + XBT_VERB("(%d - %d) Different size used in stacks : %zu - %zu", num1, num2, size_used1, size_used2); #endif xbt_os_walltimer_stop(timer); @@ -446,11 +458,11 @@ int snapshot_compare(void *p1, void *p2){ res_init = init_heap_information((xbt_mheap_t)s1->regions[0]->data, (xbt_mheap_t)s2->regions[0]->data, s1->to_ignore, s2->to_ignore); if(res_init == -1){ #ifdef MC_DEBUG - XBT_DEBUG("(%d - %d) Different heap information", ((mc_pair_t)p1)->num, ((mc_pair_t)p2)->num); + XBT_DEBUG("(%d - %d) Different heap information", num1, num2); errors++; #else #ifdef MC_VERBOSE - XBT_VERB("(%d - %d) Different heap information", ((mc_pair_t)p1)->num, ((mc_pair_t)p2)->num); + XBT_VERB("(%d - %d) Different heap information", num1, num2); #endif xbt_os_walltimer_stop(global_timer); @@ -481,13 +493,13 @@ int snapshot_compare(void *p1, void *p2){ xbt_os_walltimer_stop(timer); mc_comp_times->stacks_comparison_time = xbt_os_timer_elapsed(timer); } - XBT_DEBUG("(%d - %d) Different local variables between stacks %d", ((mc_pair_t)p1)->num, ((mc_pair_t)p2)->num, cursor + 1); + XBT_DEBUG("(%d - %d) Different local variables between stacks %d", num1, num2, cursor + 1); errors++; is_diff = 1; #else #ifdef MC_VERBOSE - XBT_VERB("(%d - %d) Different local variables between stacks %d", ((mc_pair_t)p1)->num, ((mc_pair_t)p2)->num, cursor + 1); + XBT_VERB("(%d - %d) Different local variables between stacks %d", num1, num2, cursor + 1); #endif reset_heap_information(); @@ -515,11 +527,11 @@ int snapshot_compare(void *p1, void *p2){ #ifdef MC_DEBUG xbt_os_walltimer_stop(timer); mc_comp_times->binary_global_variables_comparison_time = xbt_os_timer_elapsed(timer); - XBT_DEBUG("(%d - %d) Different global variables in binary", ((mc_pair_t)p1)->num, ((mc_pair_t)p2)->num); + XBT_DEBUG("(%d - %d) Different global variables in binary", num1, num2); errors++; #else #ifdef MC_VERBOSE - XBT_VERB("(%d - %d) Different global variables in binary", ((mc_pair_t)p1)->num, ((mc_pair_t)p2)->num); + XBT_VERB("(%d - %d) Different global variables in binary", num1, num2); #endif reset_heap_information(); @@ -545,11 +557,11 @@ int snapshot_compare(void *p1, void *p2){ #ifdef MC_DEBUG xbt_os_walltimer_stop(timer); mc_comp_times->libsimgrid_global_variables_comparison_time = xbt_os_timer_elapsed(timer); - XBT_DEBUG("(%d - %d) Different global variables in libsimgrid", ((mc_pair_t)p1)->num, ((mc_pair_t)p2)->num); + XBT_DEBUG("(%d - %d) Different global variables in libsimgrid", num1, num2); errors++; #else #ifdef MC_VERBOSE - XBT_VERB("(%d - %d) Different global variables in libsimgrid", ((mc_pair_t)p1)->num, ((mc_pair_t)p2)->num); + XBT_VERB("(%d - %d) Different global variables in libsimgrid", num1, num2); #endif reset_heap_information(); @@ -573,12 +585,12 @@ int snapshot_compare(void *p1, void *p2){ #ifdef MC_DEBUG xbt_os_walltimer_stop(timer); mc_comp_times->heap_comparison_time = xbt_os_timer_elapsed(timer); - XBT_DEBUG("(%d - %d) Different heap (mmalloc_compare)", ((mc_pair_t)p1)->num, ((mc_pair_t)p2)->num); + XBT_DEBUG("(%d - %d) Different heap (mmalloc_compare)", num1, num2); errors++; #else #ifdef MC_VERBOSE - XBT_VERB("(%d - %d) Different heap (mmalloc_compare)", ((mc_pair_t)p1)->num, ((mc_pair_t)p2)->num); + XBT_VERB("(%d - %d) Different heap (mmalloc_compare)", num1, num2); #endif reset_heap_information(); diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c index 7df33bdd73..4209fac184 100644 --- a/src/mc/mc_dpor.c +++ b/src/mc/mc_dpor.c @@ -9,9 +9,13 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dpor, mc, "Logging specific to MC DPOR exploration"); +/********** Global variables **********/ + xbt_dynar_t visited_states; xbt_dict_t first_enabled_state; +/********** Static functions ***********/ + static void visited_state_free(mc_visited_state_t state){ if(state){ MC_free_snapshot(state->system_state); @@ -37,8 +41,59 @@ static mc_visited_state_t visited_state_new(){ } -/* Dichotomic search in visited_states dynar. - * States are ordered by the number of processes then the number of bytes used in std_heap */ +static int get_search_interval(xbt_dynar_t all_states, mc_visited_state_t state, int *min, int *max){ + + int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + + MC_SET_RAW_MEM; + + int cursor = 0, previous_cursor, next_cursor; + mc_visited_state_t state_test; + int start = 0; + int end = xbt_dynar_length(all_states) - 1; + + while(start <= end){ + cursor = (start + end) / 2; + state_test = (mc_visited_state_t)xbt_dynar_get_as(all_states, cursor, mc_visited_state_t); + if(state_test->nb_processes < state->nb_processes){ + start = cursor + 1; + }else if(state_test->nb_processes > state->nb_processes){ + end = cursor - 1; + }else{ + if(state_test->heap_bytes_used < state->heap_bytes_used){ + start = cursor +1; + }else if(state_test->heap_bytes_used > state->heap_bytes_used){ + end = cursor - 1; + }else{ + *min = *max = cursor; + previous_cursor = cursor - 1; + while(previous_cursor >= 0){ + state_test = (mc_visited_state_t)xbt_dynar_get_as(all_states, previous_cursor, mc_visited_state_t); + if(state_test->nb_processes != state->nb_processes || state_test->heap_bytes_used != state->heap_bytes_used) + break; + *min = previous_cursor; + previous_cursor--; + } + next_cursor = cursor + 1; + while(next_cursor < xbt_dynar_length(all_states)){ + state_test = (mc_visited_state_t)xbt_dynar_get_as(all_states, next_cursor, mc_visited_state_t); + if(state_test->nb_processes != state->nb_processes || state_test->heap_bytes_used != state->heap_bytes_used) + break; + *max = next_cursor; + next_cursor++; + } + if(!raw_mem_set) + MC_UNSET_RAW_MEM; + return -1; + } + } + } + + if(!raw_mem_set) + MC_UNSET_RAW_MEM; + + return cursor; +} static int is_visited_state(){ @@ -48,151 +103,72 @@ static int is_visited_state(){ int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); MC_SET_RAW_MEM; + mc_visited_state_t new_state = visited_state_new(); - MC_UNSET_RAW_MEM; if(xbt_dynar_is_empty(visited_states)){ - MC_SET_RAW_MEM; xbt_dynar_push(visited_states, &new_state); - MC_UNSET_RAW_MEM; - if(raw_mem_set) - MC_SET_RAW_MEM; + if(!raw_mem_set) + MC_UNSET_RAW_MEM; return -1; }else{ - MC_SET_RAW_MEM; - - size_t current_bytes_used = new_state->heap_bytes_used; - int current_nb_processes = new_state->nb_processes; - - unsigned int cursor = 0; - int previous_cursor = 0, next_cursor = 0; - int start = 0; - int end = xbt_dynar_length(visited_states) - 1; - - mc_visited_state_t state_test = NULL; - 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; - state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t); - bytes_used_test = state_test->heap_bytes_used; - nb_processes_test = state_test->nb_processes; - if(nb_processes_test < current_nb_processes){ - start = cursor + 1; - }else if(nb_processes_test > current_nb_processes){ - end = cursor - 1; - }else 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(snapshot_compare(new_state->system_state, state_test->system_state) == 0){ - 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("Next state %d already visited ! (equal to state %d)", new_state->num, state_test->num); - else - XBT_DEBUG("Next state %d already visited ! (equal to state %d (state %d in dot_output))", new_state->num, state_test->num, new_state->other_num); - xbt_dynar_remove_at(visited_states, cursor, NULL); - xbt_dynar_insert_at(visited_states, cursor, &new_state); - if(raw_mem_set) - MC_SET_RAW_MEM; - else - MC_UNSET_RAW_MEM; - return new_state->other_num; - }else{ - /* Search another state with same number of bytes used in std_heap */ - previous_cursor = cursor - 1; - while(previous_cursor >= 0){ - state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, previous_cursor, mc_visited_state_t); - bytes_used_test = state_test->system_state->heap_bytes_used; - if(bytes_used_test != current_bytes_used) - break; - if(snapshot_compare(new_state->system_state, state_test->system_state) == 0){ - 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("Next state %d already visited ! (equal to state %d)", new_state->num, state_test->num); - else - XBT_DEBUG("Next state %d already visited ! (equal to state %d (state %d in dot_output))", new_state->num, state_test->num, new_state->other_num); - xbt_dynar_remove_at(visited_states, previous_cursor, NULL); - xbt_dynar_insert_at(visited_states, cursor, &new_state); - if(raw_mem_set) - MC_SET_RAW_MEM; - else - MC_UNSET_RAW_MEM; - return new_state->other_num; - } - previous_cursor--; - } - next_cursor = cursor + 1; - while(next_cursor < xbt_dynar_length(visited_states)){ - state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, next_cursor, mc_visited_state_t); - bytes_used_test = state_test->system_state->heap_bytes_used; - if(bytes_used_test != current_bytes_used) - break; - if(snapshot_compare(new_state->system_state, state_test->system_state) == 0){ - 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("Next state %d already visited ! (equal to state %d)", new_state->num, state_test->num); - else - XBT_DEBUG("Next state %d already visited ! (equal to state %d (state %d in dot_output))", new_state->num, state_test->num, new_state->other_num); - xbt_dynar_remove_at(visited_states, next_cursor, NULL); - xbt_dynar_insert_at(visited_states, next_cursor, &new_state); - if(raw_mem_set) - MC_SET_RAW_MEM; - else - MC_UNSET_RAW_MEM; - return new_state->other_num; - } - next_cursor++; - } - } - } + int min = -1, max = -1, index; + int res; + mc_visited_state_t state_test; + + index = get_search_interval(visited_states, new_state, &min, &max); + + if(min != -1 && max != -1){ + res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_states, min), (max-min)+1, new_state); + if(res != -1){ + state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, (min+res)-1, mc_visited_state_t); + 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); + xbt_dynar_remove_at(visited_states, (min + res) - 1, NULL); + xbt_dynar_insert_at(visited_states, (min+res) - 1, &new_state); + if(!raw_mem_set) + MC_UNSET_RAW_MEM; + return new_state->other_num; + } + xbt_dynar_insert_at(visited_states, min, &new_state); + }else{ + 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{ + if(state_test->heap_bytes_used < new_state->heap_bytes_used) + xbt_dynar_insert_at(visited_states, index + 1, &new_state); + else + xbt_dynar_insert_at(visited_states, index, &new_state); } } - state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t); - bytes_used_test = state_test->heap_bytes_used; - - if(bytes_used_test < current_bytes_used) - xbt_dynar_insert_at(visited_states, cursor + 1, &new_state); - else - xbt_dynar_insert_at(visited_states, cursor, &new_state); - if(xbt_dynar_length(visited_states) > _sg_mc_visited){ - int min = mc_stats->expanded_states; + int min2 = mc_stats->expanded_states; unsigned int cursor2 = 0; - unsigned int index = 0; + unsigned int index2 = 0; xbt_dynar_foreach(visited_states, cursor2, state_test){ - if(state_test->num < min){ - index = cursor2; - min = state_test->num; + if(state_test->num < min2){ + index2 = cursor2; + min2 = state_test->num; } } - xbt_dynar_remove_at(visited_states, index, NULL); + xbt_dynar_remove_at(visited_states, index2, NULL); } - - MC_UNSET_RAW_MEM; - if(raw_mem_set) - MC_SET_RAW_MEM; + if(!raw_mem_set) + MC_UNSET_RAW_MEM; return -1; @@ -214,7 +190,8 @@ void MC_dpor_init() MC_SET_RAW_MEM; initial_state = MC_state_new(); - visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp); + if(_sg_mc_visited > 0) + visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp); first_enabled_state = xbt_dict_new_homogeneous(&xbt_free_f); diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index 2bef415552..f112c7e3e9 100644 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@ -255,7 +255,7 @@ typedef struct s_mc_comparison_times{ extern __thread mc_comparison_times_t mc_comp_times; extern __thread double mc_snapshot_comparison_time; -int snapshot_compare(void *p1, void *p2); +int snapshot_compare(void *state1, void *state2); int SIMIX_pre_mc_compare_snapshots(smx_simcall_t simcall, mc_snapshot_t s1, mc_snapshot_t s2); void print_comparison_times(void); -- 2.20.1