From: Gabriel Corona Date: Fri, 21 Mar 2014 11:45:05 +0000 (+0100) Subject: Merge branch 'mc++' X-Git-Tag: v3_11~199^2~2 X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/f2df13795e01302813a6aef10825ec7e922ce530 Merge branch 'mc++' Conflicts: src/simgrid/sg_config.c src/xbt/mmalloc/mm_diff.c --- f2df13795e01302813a6aef10825ec7e922ce530 diff --cc src/simgrid/sg_config.c index fd2dfd2aa8,4ebfb8ee45..9a97006461 --- a/src/simgrid/sg_config.c +++ b/src/simgrid/sg_config.c @@@ -595,9 -587,21 +595,21 @@@ void sg_config_init(int *argc, char **a /* do liveness model-checking */ xbt_cfg_register(&_sg_cfg_set, "model-check/property", "Specify the name of the file containing the property. It must be the result of the ltl2ba program.", - xbt_cfgelm_string, 0, 1, _mc_cfg_cb_property, NULL); + xbt_cfgelm_string, 1, 1, _mc_cfg_cb_property, NULL); xbt_cfg_setdefault_string(_sg_cfg_set, "model-check/property", ""); + /* do communications determinism model-checking */ + xbt_cfg_register(&_sg_cfg_set, "model-check/communications_determinism", + "Enable/disable the detection of determinism in the communications schemes", - xbt_cfgelm_boolean, 0, 1, _mc_cfg_cb_comms_determinism, NULL); ++ xbt_cfgelm_boolean, 1, 1, _mc_cfg_cb_comms_determinism, NULL); + xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/communications_determinism", "no"); + + /* do send determinism model-checking */ + xbt_cfg_register(&_sg_cfg_set, "model-check/send_determinism", + "Enable/disable the detection of send-determinism in the communications schemes", - xbt_cfgelm_boolean, 0, 1, _mc_cfg_cb_send_determinism, NULL); ++ xbt_cfgelm_boolean, 1, 1, _mc_cfg_cb_send_determinism, NULL); + xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/send_determinism", "no"); + /* Specify the kind of model-checking reduction */ xbt_cfg_register(&_sg_cfg_set, "model-check/reduction", "Specify the kind of exploration reduction (either none or DPOR)", @@@ -607,9 -611,15 +619,15 @@@ /* Enable/disable timeout for wait requests with model-checking */ xbt_cfg_register(&_sg_cfg_set, "model-check/timeout", "Enable/Disable timeout for wait requests", - xbt_cfgelm_boolean, 0, 1, _mc_cfg_cb_timeout, NULL); + xbt_cfgelm_boolean, 1, 1, _mc_cfg_cb_timeout, NULL); xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/timeout", "no"); + /* Enable/disable global hash computation with model-checking */ + xbt_cfg_register(&_sg_cfg_set, "model-check/hash", + "Enable/Disable state hash for state comparison", - xbt_cfgelm_boolean, 0, 1, _mc_cfg_cb_hash, NULL); ++ xbt_cfgelm_boolean, 1, 1, _mc_cfg_cb_hash, NULL); + xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/hash", "no"); + /* Set max depth exploration */ xbt_cfg_register(&_sg_cfg_set, "model-check/max_depth", "Specify the max depth of exploration (default : 1000)", diff --cc src/xbt/mmalloc/mm_diff.c index 39cd21cb80,a17a4a311b..7258e6f1b3 --- a/src/xbt/mmalloc/mm_diff.c +++ b/src/xbt/mmalloc/mm_diff.c @@@ -314,30 -345,30 +345,30 @@@ int init_heap_information(xbt_mheap_t h int i, j; - heaplimit = ((struct mdesc *)heap1)->heaplimit; + state->heaplimit = ((struct mdesc *)heap1)->heaplimit; - s_heap = (char *)mmalloc_get_current_heap() - STD_HEAP_SIZE - xbt_pagesize; - state->s_heap = (char *)mmalloc_get_current_heap() - STD_HEAP_SIZE - getpagesize(); ++ state->s_heap = (char *)mmalloc_get_current_heap() - STD_HEAP_SIZE - xbt_pagesize; - heapbase1 = (char *)heap1 + BLOCKSIZE; - heapbase2 = (char *)heap2 + BLOCKSIZE; + state->heapbase1 = (char *)heap1 + BLOCKSIZE; + state->heapbase2 = (char *)heap2 + BLOCKSIZE; - heapinfo1 = (malloc_info *)((char *)heap1 + ((uintptr_t)((char *)((struct mdesc *)heap1)->heapinfo - (char *)s_heap))); - heapinfo2 = (malloc_info *)((char *)heap2 + ((uintptr_t)((char *)((struct mdesc *)heap2)->heapinfo - (char *)s_heap))); + state->heapinfo1 = (malloc_info *)((char *)heap1 + ((uintptr_t)((char *)((struct mdesc *)heap1)->heapinfo - (char *)state->s_heap))); + state->heapinfo2 = (malloc_info *)((char *)heap2 + ((uintptr_t)((char *)((struct mdesc *)heap2)->heapinfo - (char *)state->s_heap))); - heapsize1 = heap1->heapsize; - heapsize2 = heap2->heapsize; + state->heapsize1 = heap1->heapsize; + state->heapsize2 = heap2->heapsize; - to_ignore1 = i1; - to_ignore2 = i2; + state->to_ignore1 = i1; + state-> to_ignore2 = i2; - equals_to1 = malloc(heaplimit * sizeof(heap_area_t *)); - types1 = malloc(heaplimit * sizeof(type_name *)); - for(i=0; i<=heaplimit; i++){ - equals_to1[i] = malloc(MAX_FRAGMENT_PER_BLOCK * sizeof(heap_area_t)); - types1[i] = malloc(MAX_FRAGMENT_PER_BLOCK * sizeof(type_name)); + state->equals_to1 = malloc(state->heaplimit * sizeof(heap_area_t *)); + state->types1 = malloc(state->heaplimit * sizeof(type_name *)); + for(i=0; i<=state->heaplimit; i++){ + state->equals_to1[i] = malloc(MAX_FRAGMENT_PER_BLOCK * sizeof(heap_area_t)); + state->types1[i] = malloc(MAX_FRAGMENT_PER_BLOCK * sizeof(type_name)); for(j=0; jequals_to1[i][j] = NULL; + state->types1[i][j] = NULL; } } @@@ -1370,18 -1433,18 +1433,18 @@@ int mmalloc_linear_compare_heap(xbt_mhe } /* Heap information */ - heaplimit = ((struct mdesc *)heap1)->heaplimit; + state->heaplimit = ((struct mdesc *)heap1)->heaplimit; - s_heap = (char *)mmalloc_get_current_heap() - STD_HEAP_SIZE - xbt_pagesize; - state->s_heap = (char *)mmalloc_get_current_heap() - STD_HEAP_SIZE - getpagesize(); ++ state->s_heap = (char *)mmalloc_get_current_heap() - STD_HEAP_SIZE - xbt_pagesize; - heapbase1 = (char *)heap1 + BLOCKSIZE; - heapbase2 = (char *)heap2 + BLOCKSIZE; + state->heapbase1 = (char *)heap1 + BLOCKSIZE; + state->heapbase2 = (char *)heap2 + BLOCKSIZE; - heapinfo1 = (malloc_info *)((char *)heap1 + ((uintptr_t)((char *)heap1->heapinfo - (char *)s_heap))); - heapinfo2 = (malloc_info *)((char *)heap2 + ((uintptr_t)((char *)heap2->heapinfo - (char *)s_heap))); + state->heapinfo1 = (malloc_info *)((char *)heap1 + ((uintptr_t)((char *)heap1->heapinfo - (char *)state->s_heap))); + state->heapinfo2 = (malloc_info *)((char *)heap2 + ((uintptr_t)((char *)heap2->heapinfo - (char *)state->s_heap))); - heapsize1 = heap1->heapsize; - heapsize2 = heap2->heapsize; + state->heapsize1 = heap1->heapsize; + state->heapsize2 = heap2->heapsize; /* Start comparison */ size_t i, j, k;