From 4980d4cb7fd8b75fbb6ab9619b73b536da24ca93 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Thu, 2 Aug 2012 11:29:55 +0200 Subject: [PATCH] model-checker : add block and fragment number in mc_ignore_region --- src/include/mc/datatypes.h | 2 + src/mc/mc_global.c | 8 ++++ src/mc/mc_private.h | 14 +++--- src/xbt/mmalloc/mm_diff.c | 93 +++++++++++++++++++++++++++++++++----- 4 files changed, 98 insertions(+), 19 deletions(-) diff --git a/src/include/mc/datatypes.h b/src/include/mc/datatypes.h index 4c6cda3036..da5a3ca852 100644 --- a/src/include/mc/datatypes.h +++ b/src/include/mc/datatypes.h @@ -15,6 +15,8 @@ SG_BEGIN_DECL() typedef struct s_mc_transition *mc_transition_t; typedef struct s_mc_ignore_region{ + int block; + int fragment; void *address; size_t size; }s_mc_ignore_region_t, *mc_ignore_region_t; diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index d91af1451a..fa4725353d 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -10,6 +10,7 @@ #include "../surf/surf_private.h" #include "../simix/smx_private.h" +#include "../xbt/mmalloc/mmprivate.h" #include "xbt/fifo.h" #include "mc_private.h" #include "xbt/automaton.h" @@ -653,6 +654,13 @@ void MC_ignore(void *address, size_t size){ region = xbt_new0(s_mc_ignore_region_t, 1); region->address = address; region->size = size; + region->block = ((char*)address - (char*)((xbt_mheap_t)std_heap)->heapbase) / BLOCKSIZE + 1; + + if(((xbt_mheap_t)std_heap)->heapinfo[region->block].type == 0){ + region->fragment = -1; + }else{ + region->fragment = ((uintptr_t) (ADDR2UINT (address) % (BLOCKSIZE))) >> ((xbt_mheap_t)std_heap)->heapinfo[region->block].type; + } unsigned int cursor = 0; mc_ignore_region_t current_region; diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index 86431c79a4..6e36d0a699 100644 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@ -143,13 +143,13 @@ extern void *raw_heap; /* an API to query about the status of a heap, we simply call mmstats and */ /* because I now how does structure looks like, then I redefine it here */ -struct mstats { - size_t bytes_total; /* Total size of the heap. */ - size_t chunks_used; /* Chunks allocated by the user. */ - size_t bytes_used; /* Byte total of user-allocated chunks. */ - size_t chunks_free; /* Chunks in the free list. */ - size_t bytes_free; /* Byte total of chunks in the free list. */ -}; +/* struct mstats { */ +/* size_t bytes_total; /\* Total size of the heap. *\/ */ +/* size_t chunks_used; /\* Chunks allocated by the user. *\/ */ +/* size_t bytes_used; /\* Byte total of user-allocated chunks. *\/ */ +/* size_t chunks_free; /\* Chunks in the free list. *\/ */ +/* size_t bytes_free; /\* Byte total of chunks in the free list. *\/ */ +/* }; */ #define MC_SET_RAW_MEM mmalloc_set_current_heap(raw_heap) #define MC_UNSET_RAW_MEM mmalloc_set_current_heap(std_heap) diff --git a/src/xbt/mmalloc/mm_diff.c b/src/xbt/mmalloc/mm_diff.c index 395ec57975..a33b54a872 100644 --- a/src/xbt/mmalloc/mm_diff.c +++ b/src/xbt/mmalloc/mm_diff.c @@ -28,9 +28,10 @@ static void heap_area_pair_free_voidp(void *d); static int add_heap_area_pair(xbt_dynar_t list, int block1, int fragment1, int block2, int fragment2); static int is_new_heap_area_pair(xbt_dynar_t list, int block1, int fragment1, int block2, int fragment2); -static int compare_area(void *area1, void* area2, size_t size, xbt_dynar_t previous); +static int compare_area(void *area1, void* area2, size_t size, xbt_dynar_t previous, int check_ignore); static void match_equals(xbt_dynar_t list); +static int in_mmalloc_ignore(int block, int fragment); static size_t heap_comparison_ignore(void *address); void mmalloc_backtrace_block_display(void* heapinfo, int block){ @@ -123,7 +124,7 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){ xbt_dynar_t previous = xbt_dynar_new(sizeof(heap_area_pair_t), heap_area_pair_free_voidp); - int equal; + int equal, res_compare; ignore_done = 0; @@ -168,10 +169,20 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){ } addr_block2 = ((void*) (((ADDR2UINT(i2)) - 1) * BLOCKSIZE + (char*)heapbase2)); - + /* Comparison */ add_heap_area_pair(previous, i1, -1, i2, -1); - if(!compare_area(addr_block1, addr_block2, heapinfo1[i1].busy_block.busy_size, previous)){ + + if(ignore_done < xbt_dynar_length(mmalloc_ignore)){ + if(in_mmalloc_ignore((int)i1, -1)) + res_compare = compare_area(addr_block1, addr_block2, heapinfo1[i1].busy_block.busy_size, previous, 1); + else + res_compare = compare_area(addr_block1, addr_block2, heapinfo1[i1].busy_block.busy_size, previous, 0); + }else{ + res_compare = compare_area(addr_block1, addr_block2, heapinfo1[i1].busy_block.busy_size, previous, 0); + } + + if(!res_compare){ for(k=0; k < heapinfo2[i2].busy_block.size; k++) heapinfo2[i2+k].busy_block.equal_to = 1; for(k=0; k < heapinfo1[i1].busy_block.size; k++) @@ -223,7 +234,17 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){ /* Comparison */ add_heap_area_pair(previous, i1, j1, i2, j2); - if(!compare_area(addr_frag1, addr_frag2, heapinfo1[i1].busy_frag.frag_size[j1], previous)){ + + if(ignore_done < xbt_dynar_length(mmalloc_ignore)){ + if(in_mmalloc_ignore((int)i1, (int)j1)) + res_compare = compare_area(addr_frag1, addr_frag2, heapinfo1[i1].busy_frag.frag_size[j1], previous, 1); + else + res_compare = compare_area(addr_frag1, addr_frag2, heapinfo1[i1].busy_frag.frag_size[j1], previous, 0); + }else{ + res_compare = compare_area(addr_frag1, addr_frag2, heapinfo1[i1].busy_frag.frag_size[j1], previous, 0); + } + + if(!res_compare){ heapinfo2[i2].busy_frag.equal_to[j2] = 1; heapinfo1[i1].busy_frag.equal_to[j1] = 1; equal = 1; @@ -358,6 +379,33 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){ } +static int in_mmalloc_ignore(int block, int fragment){ + + unsigned int cursor = 0; + int start = 0; + int end = xbt_dynar_length(mmalloc_ignore) - 1; + mc_ignore_region_t region; + + while(start <= end){ + cursor = (start + end) / 2; + region = (mc_ignore_region_t)xbt_dynar_get_as(mmalloc_ignore, cursor, mc_ignore_region_t); + if(region->block == block){ + if(region->fragment == fragment) + return 1; + if(region->fragment < fragment) + start = cursor + 1; + if(region->fragment > fragment) + end = cursor - 1; + } + if(region->block < block) + start = cursor + 1; + if(region->block > block) + end = cursor - 1; + } + + return 0; +} + static size_t heap_comparison_ignore(void *address){ unsigned int cursor = 0; int start = 0; @@ -379,7 +427,7 @@ static size_t heap_comparison_ignore(void *address){ } -static int compare_area(void *area1, void* area2, size_t size, xbt_dynar_t previous){ +static int compare_area(void *area1, void* area2, size_t size, xbt_dynar_t previous, int check_ignore){ size_t i = 0, pointer_align = 0, ignore1 = 0, ignore2 = 0; void *address_pointed1, *address_pointed2, *addr_block_pointed1, *addr_block_pointed2, *addr_frag_pointed1, *addr_frag_pointed2; @@ -390,7 +438,7 @@ static int compare_area(void *area1, void* area2, size_t size, xbt_dynar_t previ while(iheapbase + ((((char *)area1) + i) - (char *)heapbase1); if((ignore1 = heap_comparison_ignore(current_area1)) > 0){ @@ -435,8 +483,15 @@ static int compare_area(void *area1, void* area2, size_t size, xbt_dynar_t previ } if(add_heap_area_pair(previous, block_pointed1, -1, block_pointed2, -1)){ - - res_compare = compare_area(addr_block_pointed1, addr_block_pointed2, heapinfo1[block_pointed1].busy_block.busy_size, previous); + + if(ignore_done < xbt_dynar_length(mmalloc_ignore)){ + if(in_mmalloc_ignore(block_pointed1, -1)) + res_compare = compare_area(addr_block_pointed1, addr_block_pointed2, heapinfo1[block_pointed1].busy_block.busy_size, previous, 1); + else + res_compare = compare_area(addr_block_pointed1, addr_block_pointed2, heapinfo1[block_pointed1].busy_block.busy_size, previous, 0); + }else{ + res_compare = compare_area(addr_block_pointed1, addr_block_pointed2, heapinfo1[block_pointed1].busy_block.busy_size, previous, 0); + } if(res_compare) return 1; @@ -459,8 +514,15 @@ static int compare_area(void *area1, void* area2, size_t size, xbt_dynar_t previ if(add_heap_area_pair(previous, block_pointed1, frag_pointed1, block_pointed2, frag_pointed2)){ - res_compare = compare_area(addr_frag_pointed1, addr_frag_pointed2, heapinfo1[block_pointed1].busy_frag.frag_size[frag_pointed1], previous); - + if(ignore_done < xbt_dynar_length(mmalloc_ignore)){ + if(in_mmalloc_ignore(block_pointed1, frag_pointed1)) + res_compare = compare_area(addr_frag_pointed1, addr_frag_pointed2, heapinfo1[block_pointed1].busy_frag.frag_size[frag_pointed1], previous, 1); + else + res_compare = compare_area(addr_frag_pointed1, addr_frag_pointed2, heapinfo1[block_pointed1].busy_frag.frag_size[frag_pointed1], previous, 0); + }else{ + res_compare = compare_area(addr_frag_pointed1, addr_frag_pointed2, heapinfo1[block_pointed1].busy_frag.frag_size[frag_pointed1], previous, 0); + } + if(res_compare) return 1; @@ -489,7 +551,14 @@ static int compare_area(void *area1, void* area2, size_t size, xbt_dynar_t previ if(add_heap_area_pair(previous, block_pointed1, frag_pointed1, block_pointed2, frag_pointed2)){ - res_compare = compare_area(addr_frag_pointed1, addr_frag_pointed2, heapinfo1[block_pointed1].busy_frag.frag_size[frag_pointed1], previous); + if(ignore_done < xbt_dynar_length(mmalloc_ignore)){ + if(in_mmalloc_ignore(block_pointed1, frag_pointed1)) + res_compare = compare_area(addr_frag_pointed1, addr_frag_pointed2, heapinfo1[block_pointed1].busy_frag.frag_size[frag_pointed1], previous, 1); + else + res_compare = compare_area(addr_frag_pointed1, addr_frag_pointed2, heapinfo1[block_pointed1].busy_frag.frag_size[frag_pointed1], previous, 0); + }else{ + res_compare = compare_area(addr_frag_pointed1, addr_frag_pointed2, heapinfo1[block_pointed1].busy_frag.frag_size[frag_pointed1], previous, 0); + } if(res_compare) return 1; -- 2.20.1