From: Marion Guthmuller Date: Fri, 11 Jan 2013 16:55:15 +0000 (+0100) Subject: model-checker : add chunks used into snapshot structure and size used into stack... X-Git-Tag: v3_9_rc1~86^2~18 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/c991ec54a886fe3f3e1460353790938e88a7af1f model-checker : add chunks used into snapshot structure and size used into stack snapshot structure --- diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c index 64d8c715a5..b3dd6ca964 100644 --- a/src/mc/mc_checkpoint.c +++ b/src/mc/mc_checkpoint.c @@ -161,6 +161,7 @@ mc_snapshot_t MC_take_snapshot() if (maps->regions[i].pathname == NULL){ if (reg.start_addr == std_heap){ // only save the std heap (and not the raw one) MC_snapshot_add_region(snapshot, 0, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr); + snapshot->heap_chunks_used = mmalloc_get_chunks_used(std_heap); heap = snapshot->regions[nb_reg]->data; nb_reg++; } @@ -386,6 +387,7 @@ static xbt_dynar_t take_snapshot_stacks(void *heap){ 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); } diff --git a/src/mc/mc_compare.c b/src/mc/mc_compare.c index 323c11f901..81e075e861 100644 --- a/src/mc/mc_compare.c +++ b/src/mc/mc_compare.c @@ -217,20 +217,20 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t c xbt_os_timer_start(timer); /* Compare number of blocks/fragments used in each heap */ - size_t chunks_used1 = mmalloc_get_chunks_used((xbt_mheap_t)s1->regions[heap_index]->data); - size_t chunks_used2 = mmalloc_get_chunks_used((xbt_mheap_t)s2->regions[heap_index]->data); - if(chunks_used1 != chunks_used2){ + + if(s1->heap_chunks_used != s2->heap_chunks_used){ + 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 chunks used in each heap : %zu - %zu", chunks_used1, chunks_used2); + 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)) - XBT_VERB("Different number of chunks used in each heap : %zu - %zu", chunks_used1, chunks_used2); + XBT_VERB("Different number of chunks used in each heap : %zu - %zu", s1->heap_chunks_used, s2->heap_chunks_used); xbt_os_timer_free(timer); xbt_os_timer_stop(global_timer); @@ -246,26 +246,22 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t c return 1; } }else{ + if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)) xbt_os_timer_stop(timer); } if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)) xbt_os_timer_start(timer); - + /* Compare size of stacks */ + unsigned int cursor = 0; - void *addr_stack1, *addr_stack2; - void *sp1, *sp2; size_t size_used1, size_used2; int is_diff = 0; while(cursor < xbt_dynar_length(stacks_areas)){ - addr_stack1 = (char *)s1->regions[heap_index]->data + ((char *)((stack_region_t)xbt_dynar_get_as(stacks_areas, cursor, stack_region_t))->address - (char *)std_heap); - addr_stack2 = (char *)s2->regions[heap_index]->data + ((char *)((stack_region_t)xbt_dynar_get_as(stacks_areas, cursor, stack_region_t))->address - (char *)std_heap); - sp1 = ((mc_snapshot_stack_t)xbt_dynar_get_as(s1->stacks, cursor, mc_snapshot_stack_t))->stack_pointer; - sp2 = ((mc_snapshot_stack_t)xbt_dynar_get_as(s2->stacks, cursor, mc_snapshot_stack_t))->stack_pointer; - size_used1 = ((stack_region_t)xbt_dynar_get_as(stacks_areas, cursor, stack_region_t))->size - ((char*)sp1 - (char*)addr_stack1); - size_used2 = ((stack_region_t)xbt_dynar_get_as(stacks_areas, cursor, stack_region_t))->size - ((char*)sp2 - (char*)addr_stack2); + 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; if(size_used1 != size_used2){ if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){ if(is_diff == 0){ @@ -306,6 +302,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t c } /* 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); if(is_diff != 0){ if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){ @@ -330,6 +327,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t c if(!raw_mem) MC_UNSET_RAW_MEM; + return 1; } } @@ -338,9 +336,10 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t c if(is_diff == 0) xbt_os_timer_stop(timer); xbt_os_timer_start(timer); - } + } /* 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); if(is_diff != 0){ if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){ @@ -365,6 +364,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t c if(!raw_mem) MC_UNSET_RAW_MEM; + return 1; } } @@ -376,6 +376,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t c } /* 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); @@ -411,6 +412,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t c if(!raw_mem) MC_UNSET_RAW_MEM; + return 1; } }else{ @@ -422,9 +424,11 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t c xbt_os_timer_start(timer); /* Stacks comparison */ + cursor = 0; stack_region_t stack_region1, stack_region2; int diff = 0, diff_local = 0; + void *sp1, *sp2; is_diff = 0; while(cursor < xbt_dynar_length(stacks1)){ @@ -474,8 +478,6 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t c cursor++; } - XBT_VERB("Chunks used after comparison of stacks : %zu", mmalloc_get_chunks_used(raw_heap)); - xbt_dynar_free(&stacks1); xbt_dynar_free(&stacks2); xbt_dynar_free(&equals); diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c index 017b0d0442..b7a356935e 100644 --- a/src/mc/mc_dpor.c +++ b/src/mc/mc_dpor.c @@ -56,7 +56,7 @@ static int is_visited_state(){ MC_SET_RAW_MEM; - size_t current_chunks_used = mmalloc_get_chunks_used((xbt_mheap_t)(new_state->system_state)->regions[get_heap_region_index(new_state->system_state)]->data); + size_t current_chunks_used = new_state->system_state->heap_chunks_used; unsigned int cursor = 0; int previous_cursor = 0, next_cursor = 0; @@ -70,7 +70,7 @@ static int is_visited_state(){ while(start <= end && same_chunks_not_found){ cursor = (start + end) / 2; state_test = (mc_safety_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_safety_visited_state_t); - chunks_used_test = mmalloc_get_chunks_used((xbt_mheap_t)(state_test->system_state)->regions[get_heap_region_index(state_test->system_state)]->data); + chunks_used_test = state_test->system_state->heap_chunks_used; if(chunks_used_test < current_chunks_used) start = cursor + 1; if(chunks_used_test > current_chunks_used) @@ -90,7 +90,7 @@ static int is_visited_state(){ previous_cursor = cursor - 1; while(previous_cursor >= 0){ state_test = (mc_safety_visited_state_t)xbt_dynar_get_as(visited_states, previous_cursor, mc_safety_visited_state_t); - chunks_used_test = mmalloc_get_chunks_used((xbt_mheap_t)(state_test->system_state)->regions[get_heap_region_index(state_test->system_state)]->data); + 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){ @@ -107,7 +107,7 @@ static int is_visited_state(){ next_cursor = cursor + 1; while(next_cursor < xbt_dynar_length(visited_states)){ state_test = (mc_safety_visited_state_t)xbt_dynar_get_as(visited_states, next_cursor, mc_safety_visited_state_t); - chunks_used_test = mmalloc_get_chunks_used((xbt_mheap_t)(state_test->system_state)->regions[get_heap_region_index(state_test->system_state)]->data); + 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){ @@ -126,7 +126,7 @@ static int is_visited_state(){ } state_test = (mc_safety_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_safety_visited_state_t); - chunks_used_test = mmalloc_get_chunks_used((xbt_mheap_t)(state_test->system_state)->regions[get_heap_region_index(state_test->system_state)]->data); + chunks_used_test = state_test->system_state->heap_chunks_used; if(chunks_used_test < current_chunks_used) xbt_dynar_insert_at(visited_states, cursor + 1, &new_state); diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index 84af06d9da..240839c791 100644 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@ -33,6 +33,7 @@ typedef struct s_mc_mem_region{ typedef struct s_mc_snapshot{ unsigned int num_reg; + size_t heap_chunks_used; mc_mem_region_t *regions; xbt_dynar_t stacks; } s_mc_snapshot_t, *mc_snapshot_t; @@ -40,6 +41,7 @@ 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{