From: Marion Guthmuller Date: Mon, 14 Jan 2013 11:17:10 +0000 (+0100) Subject: model-checker : use a global timer for snapshot comparison times, define macros inste... X-Git-Tag: v3_9_rc1~86^2~13 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/ee64b03734cc22f81bd0f067f9be724b46f36e9e model-checker : use a global timer for snapshot comparison times, define macros instead of if(XBT_LOG_ISENABLED) and add informations used for comparison (regions types, stacks sizes) in snapshot structure --- diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c index d9522fd5dd..70cdb6ef78 100644 --- a/src/mc/mc_checkpoint.c +++ b/src/mc/mc_checkpoint.c @@ -32,7 +32,7 @@ static void MC_region_destroy(mc_mem_region_t reg); static void MC_snapshot_add_region(mc_snapshot_t snapshot, int type, void *start_addr, size_t size); static void add_value(xbt_dynar_t *list, const char *type, unsigned long int val); -static xbt_dynar_t take_snapshot_stacks(void *heap); +static xbt_dynar_t take_snapshot_stacks(mc_snapshot_t *s, void *heap); static xbt_strbuff_t get_local_variables_values(void *stack_context, void *heap); static void print_local_variables_values(xbt_dynar_t all_variables); static void *get_stack_pointer(void *stack_context, void *heap); @@ -74,6 +74,7 @@ static void MC_snapshot_add_region(mc_snapshot_t snapshot, int type, void *start mc_mem_region_t new_reg = MC_region_new(type, start_addr, size); snapshot->regions = xbt_realloc(snapshot->regions, (snapshot->num_reg + 1) * sizeof(mc_mem_region_t)); snapshot->regions[snapshot->num_reg] = new_reg; + snapshot->region_type[snapshot->num_reg] = type; snapshot->num_reg++; return; } @@ -204,7 +205,7 @@ mc_snapshot_t MC_take_snapshot() } if(_sg_mc_visited > 0 || strcmp(_sg_mc_property_file,"")) - snapshot->stacks = take_snapshot_stacks(heap); + snapshot->stacks = take_snapshot_stacks(&snapshot, heap); free_memory_map(maps); @@ -377,19 +378,20 @@ static void add_value(xbt_dynar_t *list, const char *type, unsigned long int val xbt_dynar_push(*list, &value); } -static xbt_dynar_t take_snapshot_stacks(void *heap){ +static xbt_dynar_t take_snapshot_stacks(mc_snapshot_t *snapshot, void *heap){ xbt_dynar_t res = xbt_dynar_new(sizeof(s_mc_snapshot_stack_t), snapshot_stack_free_voidp); - unsigned int cursor1 = 0; + unsigned int cursor = 0; stack_region_t current_stack; - xbt_dynar_foreach(stacks_areas, cursor1, current_stack){ + xbt_dynar_foreach(stacks_areas, cursor, current_stack){ mc_snapshot_stack_t st = xbt_new(s_mc_snapshot_stack_t, 1); st->local_variables = get_local_variables_values(current_stack->context, heap); st->stack_pointer = get_stack_pointer(current_stack->context, heap); - st->size_used = current_stack->size - ((char *)st->stack_pointer - (char *)((char *)heap + ((char *)current_stack->address - (char *)std_heap))); xbt_dynar_push(res, &st); + (*snapshot)->stack_sizes = xbt_realloc((*snapshot)->stack_sizes, (cursor + 1) * sizeof(size_t)); + (*snapshot)->stack_sizes[cursor] = current_stack->size - ((char *)st->stack_pointer - (char *)((char *)heap + ((char *)current_stack->address - (char *)std_heap))); } return res; diff --git a/src/mc/mc_compare.c b/src/mc/mc_compare.c index d0c54f16e0..abb7b8171d 100644 --- a/src/mc/mc_compare.c +++ b/src/mc/mc_compare.c @@ -144,7 +144,7 @@ void heap_equality_free_voidp(void *e){ int SIMIX_pre_mc_compare_snapshots(smx_simcall_t simcall, mc_snapshot_t s1, mc_snapshot_t s2){ - return snapshot_compare(s1, s2, NULL, NULL); + return snapshot_compare(s1, s2); } int get_heap_region_index(mc_snapshot_t s){ @@ -162,146 +162,126 @@ int get_heap_region_index(mc_snapshot_t s){ return -1; } -int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t ct1, mc_comparison_times_t ct2){ +int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){ int raw_mem = (mmalloc_get_current_heap() == raw_heap); MC_SET_RAW_MEM; - int errors = 0, i = 0; - - if(ct1 != NULL) - ct1->nb_comparisons++; - if(ct2 != NULL) - ct2->nb_comparisons++; + int errors = 0; xbt_os_timer_t global_timer = xbt_os_timer_new(); xbt_os_timer_t timer = xbt_os_timer_new(); xbt_os_timer_start(global_timer); - if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)) + #ifdef MC_DEBUG xbt_os_timer_start(timer); + #endif /* Compare number of processes */ if(s1->nb_processes != s2->nb_processes){ - if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){ - xbt_os_timer_stop(timer); - if(ct1 != NULL) - xbt_dynar_push_as(ct1->chunks_used_comparison_times, double, xbt_os_timer_elapsed(timer)); - if(ct2 != NULL) - xbt_dynar_push_as(ct2->chunks_used_comparison_times, double, xbt_os_timer_elapsed(timer)); - XBT_DEBUG("Different number of processes : %d - %d", s1->nb_processes, s2->nb_processes); - errors++; - }else{ - if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_verbose)) - XBT_VERB("Different number of processes : %d - %d", s1->nb_processes, s2->nb_processes); + #ifdef MC_DEBUG + xbt_os_timer_stop(timer); + mc_comp_times->nb_processes_comparison_time = xbt_os_timer_elapsed(timer); + XBT_DEBUG("Different number of processes : %d - %d", s1->nb_processes, s2->nb_processes); + errors++; + #else + #ifdef MC_VERBOSE + XBT_VERB("Different number of processes : %d - %d", s1->nb_processes, s2->nb_processes); + #endif - xbt_os_timer_free(timer); - xbt_os_timer_stop(global_timer); - if(ct1 != NULL) - xbt_dynar_push_as(ct1->snapshot_comparison_times, double, xbt_os_timer_elapsed(global_timer)); - if(ct2 != NULL) - xbt_dynar_push_as(ct2->snapshot_comparison_times, double, xbt_os_timer_elapsed(global_timer)); - xbt_os_timer_free(global_timer); + xbt_os_timer_free(timer); + xbt_os_timer_stop(global_timer); + mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer); + xbt_os_timer_free(global_timer); - if(!raw_mem) - MC_UNSET_RAW_MEM; + if(!raw_mem) + MC_UNSET_RAW_MEM; - return 1; - } + return 1; + #endif } /* Compare number of blocks/fragments used in each heap */ - if(s1->heap_chunks_used != s2->heap_chunks_used){ - - if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){ + #ifdef MC_DEBUG xbt_os_timer_stop(timer); - if(ct1 != NULL) - xbt_dynar_push_as(ct1->chunks_used_comparison_times, double, xbt_os_timer_elapsed(timer)); - if(ct2 != NULL) - xbt_dynar_push_as(ct2->chunks_used_comparison_times, double, xbt_os_timer_elapsed(timer)); + mc_comp_times->chunks_used_comparison_time = xbt_os_timer_elapsed(timer); XBT_DEBUG("Different number of chunks used in each heap : %zu - %zu", s1->heap_chunks_used, s2->heap_chunks_used); errors++; - }else{ - if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_verbose)) + #else + #ifdef MC_VERBOSE XBT_VERB("Different number of chunks used in each heap : %zu - %zu", s1->heap_chunks_used, s2->heap_chunks_used); - + #endif + xbt_os_timer_free(timer); xbt_os_timer_stop(global_timer); - if(ct1 != NULL) - xbt_dynar_push_as(ct1->snapshot_comparison_times, double, xbt_os_timer_elapsed(global_timer)); - if(ct2 != NULL) - xbt_dynar_push_as(ct2->snapshot_comparison_times, double, xbt_os_timer_elapsed(global_timer)); + mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer); xbt_os_timer_free(global_timer); if(!raw_mem) MC_UNSET_RAW_MEM; return 1; - } + #endif }else{ - - if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)) + #ifdef MC_DEBUG xbt_os_timer_stop(timer); + #endif } - if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)) + #ifdef MC_DEBUG xbt_os_timer_start(timer); + #endif /* Compare size of stacks */ - - unsigned int cursor = 0; + int i = 0; size_t size_used1, size_used2; int is_diff = 0; - while(cursor < xbt_dynar_length(stacks_areas)){ - size_used1 = ((mc_snapshot_stack_t)xbt_dynar_get_as(s1->stacks, cursor, mc_snapshot_stack_t))->size_used; - size_used2 = ((mc_snapshot_stack_t)xbt_dynar_get_as(s2->stacks, cursor, mc_snapshot_stack_t))->size_used; + while(i < xbt_dynar_length(s1->stacks)){ + size_used1 = s1->stack_sizes[i]; + size_used2 = s2->stack_sizes[i]; if(size_used1 != size_used2){ - if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){ - if(is_diff == 0){ - xbt_os_timer_stop(timer); - if(ct1 != NULL) - xbt_dynar_push_as(ct1->stacks_sizes_comparison_times, double, xbt_os_timer_elapsed(timer)); - if(ct2 != NULL) - xbt_dynar_push_as(ct2->stacks_sizes_comparison_times, double, xbt_os_timer_elapsed(timer)); - } - XBT_DEBUG("Different size used in stacks : %zu - %zu", size_used1, size_used2); - errors++; - is_diff = 1; - }else{ - if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_verbose)) - XBT_VERB("Different size used in stacks : %zu - %zu", size_used1, size_used2); + #ifdef MC_DEBUG + if(is_diff == 0){ + xbt_os_timer_stop(timer); + mc_comp_times->stacks_sizes_comparison_time = xbt_os_timer_elapsed(timer); + } + XBT_DEBUG("Different size used in stacks : %zu - %zu", size_used1, size_used2); + errors++; + is_diff = 1; + #else + #ifdef MC_VERBOSE + XBT_VERB("Different size used in stacks : %zu - %zu", size_used1, size_used2); + #endif - xbt_os_timer_free(timer); - xbt_os_timer_stop(global_timer); - if(ct1 != NULL) - xbt_dynar_push_as(ct1->snapshot_comparison_times, double, xbt_os_timer_elapsed(global_timer)); - if(ct2 != NULL) - xbt_dynar_push_as(ct2->snapshot_comparison_times, double, xbt_os_timer_elapsed(global_timer)); - xbt_os_timer_free(global_timer); + xbt_os_timer_free(timer); + xbt_os_timer_stop(global_timer); + mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer); + xbt_os_timer_free(global_timer); - if(!raw_mem) - MC_UNSET_RAW_MEM; + if(!raw_mem) + MC_UNSET_RAW_MEM; - return 1; - } + return 1; + #endif } - cursor++; + i++; } - if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){ + #ifdef MC_DEBUG if(is_diff == 0) xbt_os_timer_stop(timer); xbt_os_timer_start(timer); - } + #endif int heap_index = 0, data_libsimgrid_index = 0, data_program_index = 0; + i = 0; /* Get index of regions */ while(i < s1->num_reg){ - switch(s1->regions[i]->type){ + switch(s1->region_type[i]){ case 0: heap_index = i; i++; @@ -309,94 +289,81 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t c case 1: data_libsimgrid_index = i; i++; - while( i < s1->num_reg && s1->regions[i]->type == 1) + while( i < s1->num_reg && s1->region_type[i] == 1) i++; break; case 2: data_program_index = i; i++; - while( i < s1->num_reg && s1->regions[i]->type == 2) + while( i < s1->num_reg && s1->region_type[i] == 2) i++; break; } } /* Compare binary global variables */ - - is_diff = compare_global_variables(s1->regions[data_program_index]->type, s1->regions[data_program_index]->data, s2->regions[data_program_index]->data); + is_diff = compare_global_variables(s1->region_type[data_program_index], s1->regions[data_program_index]->data, s2->regions[data_program_index]->data); if(is_diff != 0){ - if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){ + #ifdef MC_DEBUG xbt_os_timer_stop(timer); - if(ct1 != NULL) - xbt_dynar_push_as(ct1->binary_global_variables_comparison_times, double, xbt_os_timer_elapsed(timer)); - if(ct2 != NULL) - xbt_dynar_push_as(ct2->binary_global_variables_comparison_times, double, xbt_os_timer_elapsed(timer)); + mc_comp_times->binary_global_variables_comparison_time = xbt_os_timer_elapsed(timer); XBT_DEBUG("Different global variables in binary"); errors++; - }else{ - if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_verbose)) + #else + #ifdef MC_VERBOSE XBT_VERB("Different global variables in binary"); + #endif xbt_os_timer_free(timer); xbt_os_timer_stop(global_timer); - if(ct1 != NULL) - xbt_dynar_push_as(ct1->snapshot_comparison_times, double, xbt_os_timer_elapsed(global_timer)); - if(ct2 != NULL) - xbt_dynar_push_as(ct2->snapshot_comparison_times, double, xbt_os_timer_elapsed(global_timer)); + mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer); xbt_os_timer_free(global_timer); if(!raw_mem) MC_UNSET_RAW_MEM; return 1; - } + #endif } - if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){ + #ifdef MC_VERBOSE if(is_diff == 0) xbt_os_timer_stop(timer); xbt_os_timer_start(timer); - } + #endif /* Compare libsimgrid global variables */ - - is_diff = compare_global_variables(s1->regions[data_libsimgrid_index]->type, s1->regions[data_libsimgrid_index]->data, s2->regions[data_libsimgrid_index]->data); + is_diff = compare_global_variables(s1->region_type[data_libsimgrid_index], s1->regions[data_libsimgrid_index]->data, s2->regions[data_libsimgrid_index]->data); if(is_diff != 0){ - if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){ + #ifdef MC_DEBUG xbt_os_timer_stop(timer); - if(ct1 != NULL) - xbt_dynar_push_as(ct1->libsimgrid_global_variables_comparison_times, double, xbt_os_timer_elapsed(timer)); - if(ct2 != NULL) - xbt_dynar_push_as(ct2->libsimgrid_global_variables_comparison_times, double, xbt_os_timer_elapsed(timer)); + mc_comp_times->libsimgrid_global_variables_comparison_time = xbt_os_timer_elapsed(timer); XBT_DEBUG("Different global variables in libsimgrid"); errors++; - }else{ - if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_verbose)) + #else + #ifdef MC_VERBOSE XBT_VERB("Different global variables in libsimgrid"); + #endif xbt_os_timer_free(timer); xbt_os_timer_stop(global_timer); - if(ct1 != NULL) - xbt_dynar_push_as(ct1->snapshot_comparison_times, double, xbt_os_timer_elapsed(global_timer)); - if(ct2 != NULL) - xbt_dynar_push_as(ct2->snapshot_comparison_times, double, xbt_os_timer_elapsed(global_timer)); + mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer); xbt_os_timer_free(global_timer); if(!raw_mem) MC_UNSET_RAW_MEM; return 1; - } + #endif } - if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){ + #ifdef MC_DEBUG if(is_diff == 0) xbt_os_timer_stop(timer); xbt_os_timer_start(timer); - } + #endif /* Compare heap */ - xbt_dynar_t stacks1 = xbt_dynar_new(sizeof(stack_region_t), stack_region_free_voidp); xbt_dynar_t stacks2 = xbt_dynar_new(sizeof(stack_region_t), stack_region_free_voidp); xbt_dynar_t equals = xbt_dynar_new(sizeof(heap_equality_t), heap_equality_free_voidp); @@ -405,47 +372,43 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t c if(mmalloc_compare_heap((xbt_mheap_t)s1->regions[heap_index]->data, (xbt_mheap_t)s2->regions[heap_index]->data, &stacks1, &stacks2, &equals)){ - if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){ + #ifdef MC_DEBUG xbt_os_timer_stop(timer); - if(ct1 != NULL) - xbt_dynar_push_as(ct1->heap_comparison_times, double, xbt_os_timer_elapsed(timer)); - if(ct2 != NULL) - xbt_dynar_push_as(ct2->heap_comparison_times, double, xbt_os_timer_elapsed(timer)); + mc_comp_times->heap_comparison_time = xbt_os_timer_elapsed(timer); XBT_DEBUG("Different heap (mmalloc_compare)"); errors++; - }else{ + #else xbt_os_timer_free(timer); xbt_dynar_free(&stacks1); xbt_dynar_free(&stacks2); xbt_dynar_free(&equals); - if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_verbose)) + #ifdef MC_VERBOSE XBT_VERB("Different heap (mmalloc_compare)"); + #endif xbt_os_timer_stop(global_timer); - if(ct1 != NULL) - xbt_dynar_push_as(ct1->snapshot_comparison_times, double, xbt_os_timer_elapsed(global_timer)); - if(ct2 != NULL) - xbt_dynar_push_as(ct2->snapshot_comparison_times, double, xbt_os_timer_elapsed(global_timer)); + mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer); xbt_os_timer_free(global_timer); if(!raw_mem) MC_UNSET_RAW_MEM; return 1; - } + #endif }else{ - if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)) + #ifdef MC_DEBUG xbt_os_timer_stop(timer); + #endif } - if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)) + #ifdef MC_DEBUG xbt_os_timer_start(timer); + #endif /* Stacks comparison */ - - cursor = 0; + unsigned int cursor = 0; stack_region_t stack_region1, stack_region2; int diff = 0, diff_local = 0; void *sp1, *sp2; @@ -461,38 +424,33 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t c if(diff > 0){ /* Differences may be due to padding */ diff_local = compare_local_variables(((mc_snapshot_stack_t)xbt_dynar_get_as(s1->stacks, cursor, mc_snapshot_stack_t))->local_variables->data, ((mc_snapshot_stack_t)xbt_dynar_get_as(s2->stacks, cursor, mc_snapshot_stack_t))->local_variables->data, equals); if(diff_local > 0){ - if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){ + #ifdef MC_DEBUG if(is_diff == 0){ xbt_os_timer_stop(timer); - if(ct1 != NULL) - xbt_dynar_push_as(ct1->stacks_comparison_times, double, xbt_os_timer_elapsed(timer)); - if(ct2 != NULL) - xbt_dynar_push_as(ct2->stacks_comparison_times, double, xbt_os_timer_elapsed(timer)); + mc_comp_times->stacks_comparison_time = xbt_os_timer_elapsed(timer); } XBT_DEBUG("Different local variables between stacks %d", cursor + 1); errors++; is_diff = 1; - }else{ + #else xbt_dynar_free(&stacks1); xbt_dynar_free(&stacks2); xbt_dynar_free(&equals); - if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_verbose)) + #ifdef MC_VERBOSE XBT_VERB("Different local variables between stacks %d", cursor + 1); + #endif xbt_os_timer_free(timer); xbt_os_timer_stop(global_timer); - if(ct1 != NULL) - xbt_dynar_push_as(ct1->snapshot_comparison_times, double, xbt_os_timer_elapsed(global_timer)); - if(ct2 != NULL) - xbt_dynar_push_as(ct2->snapshot_comparison_times, double, xbt_os_timer_elapsed(global_timer)); + mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer); xbt_os_timer_free(global_timer); if(!raw_mem) MC_UNSET_RAW_MEM; return 1; - } + #endif } } cursor++; @@ -504,15 +462,17 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t c xbt_os_timer_free(timer); - if(!XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){ + #ifdef MC_VERBOSE xbt_os_timer_stop(global_timer); - if(ct1 != NULL) - xbt_dynar_push_as(ct1->snapshot_comparison_times, double, xbt_os_timer_elapsed(global_timer)); - if(ct2 != NULL) - xbt_dynar_push_as(ct2->snapshot_comparison_times, double, xbt_os_timer_elapsed(global_timer)); - } + mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer); + #endif + xbt_os_timer_free(global_timer); + #ifdef MC_DEBUG + print_comparison_times(); + #endif + if(!raw_mem) MC_UNSET_RAW_MEM; @@ -670,3 +630,14 @@ int MC_compare_snapshots(void *s1, void *s2){ return simcall_mc_compare_snapshots(s1, s2); } + +void print_comparison_times(){ + XBT_DEBUG("*** Comparison times ***"); + XBT_DEBUG("- Nb processes : %f", mc_comp_times->nb_processes_comparison_time); + XBT_DEBUG("- Nb chunks used : %f", mc_comp_times->chunks_used_comparison_time); + XBT_DEBUG("- Stacks sizes : %f", mc_comp_times->stacks_sizes_comparison_time); + XBT_DEBUG("- Binary global variables : %f", mc_comp_times->binary_global_variables_comparison_time); + XBT_DEBUG("- Libsimgrid global variables : %f", mc_comp_times->libsimgrid_global_variables_comparison_time); + XBT_DEBUG("- Heap : %f", mc_comp_times->heap_comparison_time); + XBT_DEBUG("- Stacks : %f", mc_comp_times->stacks_comparison_time); +} diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c index b7a356935e..6f1cc3a7da 100644 --- a/src/mc/mc_dpor.c +++ b/src/mc/mc_dpor.c @@ -77,7 +77,7 @@ static int is_visited_state(){ end = cursor - 1; if(chunks_used_test == current_chunks_used){ same_chunks_not_found = 0; - if(snapshot_compare(new_state->system_state, state_test->system_state, NULL, NULL) == 0){ + if(snapshot_compare(new_state->system_state, state_test->system_state) == 0){ xbt_dynar_remove_at(visited_states, cursor, NULL); xbt_dynar_insert_at(visited_states, cursor, &new_state); if(raw_mem_set) @@ -93,7 +93,7 @@ static int is_visited_state(){ chunks_used_test = state_test->system_state->heap_chunks_used; if(chunks_used_test != current_chunks_used) break; - if(snapshot_compare(new_state->system_state, state_test->system_state, NULL, NULL) == 0){ + if(snapshot_compare(new_state->system_state, state_test->system_state) == 0){ xbt_dynar_remove_at(visited_states, previous_cursor, NULL); xbt_dynar_insert_at(visited_states, previous_cursor, &new_state); if(raw_mem_set) @@ -110,7 +110,7 @@ static int is_visited_state(){ chunks_used_test = state_test->system_state->heap_chunks_used; if(chunks_used_test != current_chunks_used) break; - if(snapshot_compare(new_state->system_state, state_test->system_state, NULL, NULL) == 0){ + if(snapshot_compare(new_state->system_state, state_test->system_state) == 0){ xbt_dynar_remove_at(visited_states, next_cursor, NULL); xbt_dynar_insert_at(visited_states, next_cursor, &new_state); if(raw_mem_set) diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index 186335f8b5..244e01de20 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -86,6 +86,8 @@ void _mc_cfg_cb_visited(const char *name, int pos) { mc_state_t mc_current_state = NULL; char mc_replay_mode = FALSE; double *mc_time = NULL; +mc_comparison_times_t mc_comp_times = NULL; +double mc_snapshot_comparison_time; /* Safety */ @@ -122,6 +124,11 @@ static size_t data_bss_ignore_size(void *address); static void MC_get_global_variables(char *elf_file); void MC_do_the_modelcheck_for_real() { + + MC_SET_RAW_MEM; + mc_comp_times = xbt_new0(s_mc_comparison_times_t, 1); + MC_UNSET_RAW_MEM; + if (!_sg_mc_property_file || _sg_mc_property_file[0]=='\0') { if (mc_reduce_kind==e_mc_reduce_unset) mc_reduce_kind=e_mc_reduce_dpor; @@ -183,7 +190,9 @@ void MC_init(){ get_binary_plt_section(); MC_ignore_data_bss(&end_raw_heap, sizeof(end_raw_heap)); - + MC_ignore_data_bss(&mc_comp_times, sizeof(mc_comp_times)); + MC_ignore_data_bss(&mc_snapshot_comparison_time, sizeof(mc_snapshot_comparison_time)); + /* Get global variables */ MC_get_global_variables(xbt_binary_name); MC_get_global_variables(libsimgrid_path); diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c index 70560188b3..8067a737c0 100644 --- a/src/mc/mc_liveness.c +++ b/src/mc/mc_liveness.c @@ -51,141 +51,6 @@ int create_dump(int pair) return 0; } -void MC_print_comparison_times_statistics(mc_comparison_times_t ct){ - - XBT_DEBUG("Comparisons done : %d", ct->nb_comparisons); - - double total, min, max; - unsigned int cursor; - - if(xbt_dynar_length(ct->chunks_used_comparison_times) > 0){ - cursor = 0; - total = 0.0; - max = 0.0; - min = xbt_dynar_get_as(ct->chunks_used_comparison_times, cursor, double); - while(cursor < xbt_dynar_length(ct->chunks_used_comparison_times) - 1){ - total += xbt_dynar_get_as(ct->chunks_used_comparison_times, cursor, double); - if(xbt_dynar_get_as(ct->chunks_used_comparison_times, cursor, double) > max) - max = xbt_dynar_get_as(ct->chunks_used_comparison_times, cursor, double); - if(xbt_dynar_get_as(ct->chunks_used_comparison_times, cursor, double) < min) - min = xbt_dynar_get_as(ct->chunks_used_comparison_times, cursor, double); - cursor++; - } - XBT_DEBUG("Chunks used comparison -- Different states : %lu/%d, time (in seconds) : average = %lf, max = %lf, min = %lf", xbt_dynar_length(ct->chunks_used_comparison_times), ct->nb_comparisons, total/xbt_dynar_length(ct->chunks_used_comparison_times), max, min); - } - - if(xbt_dynar_length(ct->stacks_sizes_comparison_times) > 0){ - cursor = 0; - total = 0.0; - max = 0.0; - min = xbt_dynar_get_as(ct->stacks_sizes_comparison_times, cursor, double); - while(cursor < xbt_dynar_length(ct->stacks_sizes_comparison_times) - 1){ - total += xbt_dynar_get_as(ct->stacks_sizes_comparison_times, cursor, double); - if(xbt_dynar_get_as(ct->stacks_sizes_comparison_times, cursor, double) > max) - max = xbt_dynar_get_as(ct->stacks_sizes_comparison_times, cursor, double); - if(xbt_dynar_get_as(ct->stacks_sizes_comparison_times, cursor, double) < min) - min = xbt_dynar_get_as(ct->stacks_sizes_comparison_times, cursor, double); - cursor++; - } - XBT_DEBUG("Stacks sizes comparison -- Different states : %lu/%d, time (in seconds) : average = %lf, max = %lf, min = %lf", xbt_dynar_length(ct->stacks_sizes_comparison_times), ct->nb_comparisons, total/xbt_dynar_length(ct->stacks_sizes_comparison_times), max, min); - } - - if(xbt_dynar_length(ct->binary_global_variables_comparison_times) > 0){ - cursor = 0; - total = 0.0; - max = 0.0; - min = xbt_dynar_get_as(ct->binary_global_variables_comparison_times, cursor, double); - while(cursor < xbt_dynar_length(ct->binary_global_variables_comparison_times) - 1){ - total += xbt_dynar_get_as(ct->binary_global_variables_comparison_times, cursor, double); - if(xbt_dynar_get_as(ct->binary_global_variables_comparison_times, cursor, double) > max) - max = xbt_dynar_get_as(ct->binary_global_variables_comparison_times, cursor, double); - if(xbt_dynar_get_as(ct->binary_global_variables_comparison_times, cursor, double) < min) - min = xbt_dynar_get_as(ct->binary_global_variables_comparison_times, cursor, double); - cursor++; - } - XBT_DEBUG("Binary global variables comparison -- Different states : %lu/%d, time (in seconds) : average = %lf, max = %lf, min = %lf", xbt_dynar_length(ct->binary_global_variables_comparison_times), ct->nb_comparisons, total/xbt_dynar_length(ct->binary_global_variables_comparison_times), max, min); - } - - if(xbt_dynar_length(ct->libsimgrid_global_variables_comparison_times) > 0){ - cursor = 0; - total = 0.0; - max = 0.0; - min = xbt_dynar_get_as(ct->libsimgrid_global_variables_comparison_times, cursor, double); - while(cursor < xbt_dynar_length(ct->libsimgrid_global_variables_comparison_times) - 1){ - total += xbt_dynar_get_as(ct->libsimgrid_global_variables_comparison_times, cursor, double); - if(xbt_dynar_get_as(ct->libsimgrid_global_variables_comparison_times, cursor, double) > max) - max = xbt_dynar_get_as(ct->libsimgrid_global_variables_comparison_times, cursor, double); - if(xbt_dynar_get_as(ct->libsimgrid_global_variables_comparison_times, cursor, double) < min) - min = xbt_dynar_get_as(ct->libsimgrid_global_variables_comparison_times, cursor, double); - cursor++; - } - XBT_DEBUG("Libsimgrid global variables comparison -- Different states : %lu/%d, time (in seconds) : average = %lf, max = %lf, min = %lf", xbt_dynar_length(ct->libsimgrid_global_variables_comparison_times), ct->nb_comparisons, total/xbt_dynar_length(ct->libsimgrid_global_variables_comparison_times), max, min); - } - - if(xbt_dynar_length(ct->heap_comparison_times) > 0){ - cursor = 0; - total = 0.0; - max = 0.0; - min = xbt_dynar_get_as(ct->heap_comparison_times, cursor, double); - while(cursor < xbt_dynar_length(ct->heap_comparison_times) - 1){ - total += xbt_dynar_get_as(ct->heap_comparison_times, cursor, double); - if(xbt_dynar_get_as(ct->heap_comparison_times, cursor, double) > max) - max = xbt_dynar_get_as(ct->heap_comparison_times, cursor, double); - if(xbt_dynar_get_as(ct->heap_comparison_times, cursor, double) < min) - min = xbt_dynar_get_as(ct->heap_comparison_times, cursor, double); - cursor++; - } - XBT_DEBUG("Heap comparison -- Different states : %lu/%d, time (in seconds) : average = %lf, max = %lf, min = %lf", xbt_dynar_length(ct->heap_comparison_times), ct->nb_comparisons, total/xbt_dynar_length(ct->heap_comparison_times), max, min); - } - - if(xbt_dynar_length(ct->stacks_comparison_times) > 0){ - cursor = 0; - total = 0.0; - max = 0.0; - min = xbt_dynar_get_as(ct->stacks_comparison_times, cursor, double); - while(cursor < xbt_dynar_length(ct->stacks_comparison_times) - 1){ - total += xbt_dynar_get_as(ct->stacks_comparison_times, cursor, double); - if(xbt_dynar_get_as(ct->stacks_comparison_times, cursor, double) > max) - max = xbt_dynar_get_as(ct->stacks_comparison_times, cursor, double); - if(xbt_dynar_get_as(ct->stacks_comparison_times, cursor, double) < min) - min = xbt_dynar_get_as(ct->stacks_comparison_times, cursor, double); - cursor++; - } - XBT_DEBUG("Stacks comparison -- Different states : %lu/%d, time (in seconds) : average = %lf, max = %lf, min = %lf", xbt_dynar_length(ct->stacks_comparison_times), ct->nb_comparisons, total/xbt_dynar_length(ct->stacks_comparison_times), max, min); - } - - if(xbt_dynar_length(ct->snapshot_comparison_times) > 0){ - cursor = 0; - total = 0.0; - max = 0.0; - min = xbt_dynar_get_as(ct->snapshot_comparison_times, cursor, double); - while(cursor < xbt_dynar_length(ct->snapshot_comparison_times) - 1){ - total += xbt_dynar_get_as(ct->snapshot_comparison_times, cursor, double); - if(xbt_dynar_get_as(ct->snapshot_comparison_times, cursor, double) > max) - max = xbt_dynar_get_as(ct->snapshot_comparison_times, cursor, double); - if(xbt_dynar_get_as(ct->snapshot_comparison_times, cursor, double) < min) - min = xbt_dynar_get_as(ct->snapshot_comparison_times, cursor, double); - cursor++; - } - XBT_DEBUG("Snapshot comparison (Whole funnel) -- Different states : %lu/%d, time (in seconds) : average = %lf, max = %lf, min = %lf", xbt_dynar_length(ct->snapshot_comparison_times), ct->nb_comparisons, total/xbt_dynar_length(ct->snapshot_comparison_times), max, min); - } - -} - -mc_comparison_times_t new_comparison_times(){ - mc_comparison_times_t ct = NULL; - ct = xbt_new0(s_mc_comparison_times_t, 1); - ct->nb_comparisons = 0; - ct->snapshot_comparison_times = xbt_dynar_new(sizeof(double), NULL); - ct->chunks_used_comparison_times = xbt_dynar_new(sizeof(double), NULL); - ct->stacks_sizes_comparison_times = xbt_dynar_new(sizeof(double), NULL); - ct->binary_global_variables_comparison_times = xbt_dynar_new(sizeof(double), NULL); - ct->libsimgrid_global_variables_comparison_times = xbt_dynar_new(sizeof(double), NULL); - ct->heap_comparison_times = xbt_dynar_new(sizeof(double), NULL); - ct->stacks_comparison_times = xbt_dynar_new(sizeof(double), NULL); - return ct; -} - int reached(xbt_state_t st){ int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); @@ -197,7 +62,6 @@ int reached(xbt_state_t st){ new_pair->nb = xbt_dynar_length(reached_pairs) + 1; new_pair->automaton_state = st; new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL); - new_pair->comparison_times = new_comparison_times(); new_pair->system_state = MC_take_snapshot(); /* Get values of propositional symbols */ @@ -237,7 +101,7 @@ int reached(xbt_state_t st){ XBT_DEBUG("****** Pair reached #%d ******", pair_test->nb); if(automaton_state_compare(pair_test->automaton_state, st) == 0){ if(propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){ - if(snapshot_compare(new_pair->system_state, pair_test->system_state, new_pair->comparison_times, pair_test->comparison_times) == 0){ + if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){ if(raw_mem_set) MC_SET_RAW_MEM; @@ -245,17 +109,13 @@ int reached(xbt_state_t st){ MC_UNSET_RAW_MEM; return 1; - } + } }else{ XBT_DEBUG("Different values of propositional symbols"); } }else{ XBT_DEBUG("Different automaton state"); } - if(pair_test->comparison_times != NULL && XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){ - XBT_DEBUG("*** Comparison times statistics ***"); - MC_print_comparison_times_statistics(pair_test->comparison_times); - } } /* New pair reached */ @@ -285,7 +145,6 @@ void set_pair_reached(xbt_state_t st){ pair->nb = xbt_dynar_length(reached_pairs) + 1; pair->automaton_state = st; pair->prop_ato = xbt_dynar_new(sizeof(int), NULL); - pair->comparison_times = new_comparison_times(); pair->system_state = MC_take_snapshot(); /* Get values of propositional symbols */ @@ -361,7 +220,7 @@ int visited(xbt_state_t st){ XBT_DEBUG("****** Pair visited #%d ******", cursor + 1); if(automaton_state_compare(pair_test->automaton_state, st) == 0){ if(propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){ - if(snapshot_compare(new_pair->system_state, pair_test->system_state, NULL, NULL) == 0){ + if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){ if(raw_mem_set) MC_SET_RAW_MEM; else @@ -480,15 +339,6 @@ void pair_reached_free(mc_pair_reached_t pair){ if(pair){ pair->automaton_state = NULL; xbt_dynar_free(&(pair->prop_ato)); - if(pair->comparison_times != NULL){ - xbt_dynar_free(&(pair->comparison_times->snapshot_comparison_times)); - xbt_dynar_free(&(pair->comparison_times->chunks_used_comparison_times)); - xbt_dynar_free(&(pair->comparison_times->stacks_sizes_comparison_times)); - xbt_dynar_free(&(pair->comparison_times->binary_global_variables_comparison_times)); - xbt_dynar_free(&(pair->comparison_times->libsimgrid_global_variables_comparison_times)); - xbt_dynar_free(&(pair->comparison_times->heap_comparison_times)); - xbt_dynar_free(&(pair->comparison_times->stacks_comparison_times)); - } MC_free_snapshot(pair->system_state); xbt_free(pair); } diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index bddc9f7c0d..bf29aa9089 100644 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@ -24,6 +24,8 @@ /****************************** Snapshots ***********************************/ +#define nb_regions 3 /* binary data (data + BSS), libsimgrid data (data + BSS), std_heap */ + typedef struct s_mc_mem_region{ int type; void *start_addr; @@ -33,8 +35,10 @@ typedef struct s_mc_mem_region{ typedef struct s_mc_snapshot{ unsigned int num_reg; + int region_type[nb_regions]; size_t heap_chunks_used; mc_mem_region_t *regions; + size_t *stack_sizes; xbt_dynar_t stacks; int nb_processes; } s_mc_snapshot_t, *mc_snapshot_t; @@ -42,7 +46,6 @@ typedef struct s_mc_snapshot{ typedef struct s_mc_snapshot_stack{ xbt_strbuff_t local_variables; void *stack_pointer; - size_t size_used; }s_mc_snapshot_stack_t, *mc_snapshot_stack_t; typedef struct s_mc_global_t{ @@ -212,6 +215,27 @@ extern void *end_got_plt_libsimgrid; extern void *start_got_plt_binary; extern void *end_got_plt_binary; +/********************************** Snapshot comparison **********************************/ + +typedef struct s_mc_comparison_times{ + double nb_processes_comparison_time; + double chunks_used_comparison_time; + double stacks_sizes_comparison_time; + double binary_global_variables_comparison_time; + double libsimgrid_global_variables_comparison_time; + double heap_comparison_time; + double stacks_comparison_time; +}s_mc_comparison_times_t, *mc_comparison_times_t; + +extern mc_comparison_times_t mc_comp_times; +extern double mc_snapshot_comparison_time; + +int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2); +int SIMIX_pre_mc_compare_snapshots(smx_simcall_t simcall, mc_snapshot_t s1, mc_snapshot_t s2); +void print_comparison_times(void); + +//#define MC_DEBUG 1 +//#define MC_VERBOSE 1 /********************************** DPOR for safety **************************************/ typedef enum { @@ -250,23 +274,11 @@ typedef struct s_mc_pair{ xbt_state_t automaton_state; }s_mc_pair_t, *mc_pair_t; -typedef struct s_mc_comparison_times{ - int nb_comparisons; - xbt_dynar_t snapshot_comparison_times; - xbt_dynar_t chunks_used_comparison_times; - xbt_dynar_t stacks_sizes_comparison_times; - xbt_dynar_t binary_global_variables_comparison_times; - xbt_dynar_t libsimgrid_global_variables_comparison_times; - xbt_dynar_t heap_comparison_times; - xbt_dynar_t stacks_comparison_times; -}s_mc_comparison_times_t, *mc_comparison_times_t; - typedef struct s_mc_pair_reached{ int nb; xbt_state_t automaton_state; xbt_dynar_t prop_ato; mc_snapshot_t system_state; - mc_comparison_times_t comparison_times; }s_mc_pair_reached_t, *mc_pair_reached_t; typedef struct s_mc_pair_visited{ @@ -277,14 +289,11 @@ typedef struct s_mc_pair_visited{ int MC_automaton_evaluate_label(xbt_exp_label_t l); mc_pair_t new_pair(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st); -mc_comparison_times_t new_comparison_times(void); int reached(xbt_state_t st); void set_pair_reached(xbt_state_t st); int visited(xbt_state_t st); -int SIMIX_pre_mc_compare_snapshots(smx_simcall_t simcall, - mc_snapshot_t s1, mc_snapshot_t s2); -int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t ct1, mc_comparison_times_t ct2); + void MC_pair_delete(mc_pair_t pair); void MC_exit_liveness(void); mc_state_t MC_state_pair_new(void); @@ -294,7 +303,6 @@ void pair_visited_free(mc_pair_visited_t pair); void pair_visited_free_voidp(void *p); void MC_init_liveness(void); void MC_init_memory_map_info(void); -void MC_print_comparison_times_statistics(mc_comparison_times_t ct); int get_heap_region_index(mc_snapshot_t s);