From: Marion Guthmuller Date: Mon, 11 Feb 2013 08:06:06 +0000 (+0100) Subject: model-checker : cleanups in mc_snapshot structure X-Git-Tag: v3_9_90~462 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/3a9ba94edbd1ef8375ba5e7bca9b02f45d4d8b89?ds=sidebyside model-checker : cleanups in mc_snapshot structure --- diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c index f4ec6ef414..46b70965a3 100644 --- a/src/mc/mc_checkpoint.c +++ b/src/mc/mc_checkpoint.c @@ -42,7 +42,6 @@ static xbt_dynar_t take_snapshot_ignore(void); static mc_mem_region_t MC_region_new(int type, void *start_addr, size_t size) { mc_mem_region_t new_reg = xbt_new0(s_mc_mem_region_t, 1); - new_reg->type = type; new_reg->start_addr = start_addr; new_reg->size = size; new_reg->data = xbt_malloc0(size); @@ -72,10 +71,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) { 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++; + snapshot->regions[type] = new_reg; return; } @@ -163,7 +159,7 @@ mc_snapshot_t MC_take_snapshot() 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_bytes_used = mmalloc_get_bytes_used(std_heap); - heap = snapshot->regions[snapshot->num_reg - 1]->data; + heap = snapshot->regions[0]->data; } i++; } else{ @@ -221,7 +217,7 @@ mc_snapshot_t MC_take_snapshot() void MC_restore_snapshot(mc_snapshot_t snapshot) { unsigned int i; - for(i=0; i < snapshot->num_reg; i++){ + for(i=0; i < NB_REGIONS; i++){ MC_region_restore(snapshot->regions[i]); } @@ -230,10 +226,9 @@ void MC_restore_snapshot(mc_snapshot_t snapshot) void MC_free_snapshot(mc_snapshot_t snapshot) { unsigned int i; - for(i=0; i < snapshot->num_reg; i++) + for(i=0; i < NB_REGIONS; i++) MC_region_destroy(snapshot->regions[i]); - xbt_free(snapshot->regions); xbt_dynar_free(&(snapshot->stacks)); xbt_dynar_free(&(snapshot->to_ignore)); xbt_free(snapshot); diff --git a/src/mc/mc_compare.c b/src/mc/mc_compare.c index 6aa077780c..005381c396 100644 --- a/src/mc/mc_compare.c +++ b/src/mc/mc_compare.c @@ -167,21 +167,6 @@ int SIMIX_pre_mc_compare_snapshots(smx_simcall_t simcall, return snapshot_compare(s1, s2); } -int get_heap_region_index(mc_snapshot_t s){ - int i = 0; - while(i < s->num_reg){ - switch(s->regions[i]->type){ - case 0: - return i; - break; - default: - i++; - break; - } - } - return -1; -} - int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){ int raw_mem = (mmalloc_get_current_heap() == raw_heap); @@ -300,36 +285,11 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){ 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->region_type[i]){ - case 0: - heap_index = i; - i++; - break; - case 1: - data_libsimgrid_index = i; - i++; - 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->region_type[i] == 2) - i++; - break; - } - } - /* Init heap information used in heap comparison algorithm */ - init_heap_information((xbt_mheap_t)s1->regions[heap_index]->data, (xbt_mheap_t)s2->regions[heap_index]->data, s1->to_ignore, s2->to_ignore); + init_heap_information((xbt_mheap_t)s1->regions[0]->data, (xbt_mheap_t)s2->regions[0]->data, s1->to_ignore, s2->to_ignore); /* Compare binary global variables */ - is_diff = compare_global_variables(s1->region_type[data_program_index], s1->regions[data_program_index]->data, s2->regions[data_program_index]->data); + is_diff = compare_global_variables(2, s1->regions[2]->data, s2->regions[2]->data); if(is_diff != 0){ #ifdef MC_DEBUG xbt_os_timer_stop(timer); @@ -360,7 +320,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){ #endif /* Compare libsimgrid global variables */ - is_diff = compare_global_variables(s1->region_type[data_libsimgrid_index], s1->regions[data_libsimgrid_index]->data, s2->regions[data_libsimgrid_index]->data); + is_diff = compare_global_variables(1, s1->regions[1]->data, s2->regions[1]->data); if(is_diff != 0){ #ifdef MC_DEBUG xbt_os_timer_stop(timer); @@ -433,7 +393,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){ /* Compare heap */ - if(mmalloc_compare_heap((xbt_mheap_t)s1->regions[heap_index]->data, (xbt_mheap_t)s2->regions[heap_index]->data)){ + if(mmalloc_compare_heap((xbt_mheap_t)s1->regions[0]->data, (xbt_mheap_t)s2->regions[0]->data)){ #ifdef MC_DEBUG xbt_os_timer_stop(timer); diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index 699a467a12..c0b6287683 100644 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@ -26,23 +26,20 @@ /****************************** Snapshots ***********************************/ -#define nb_regions 3 /* binary data (data + BSS), libsimgrid data (data + BSS), std_heap */ +#define NB_REGIONS 3 /* binary data (data + BSS) (type = 2), libsimgrid data (data + BSS) (type = 1), std_heap (type = 0)*/ typedef struct s_mc_mem_region{ - int type; void *start_addr; void *data; size_t size; } s_mc_mem_region_t, *mc_mem_region_t; typedef struct s_mc_snapshot{ - unsigned int num_reg; - int region_type[nb_regions]; size_t heap_bytes_used; - mc_mem_region_t *regions; + mc_mem_region_t regions[NB_REGIONS]; + int nb_processes; size_t *stack_sizes; xbt_dynar_t stacks; - int nb_processes; xbt_dynar_t to_ignore; } s_mc_snapshot_t, *mc_snapshot_t;