X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/6c9922204dbafacbc6d1cc25d519f7c9a46c96e9..41626f8a47c96f54fa3b1ee61a90fb0af699dcbc:/src/mc/mc_ignore.c diff --git a/src/mc/mc_ignore.c b/src/mc/mc_ignore.c index 726cfefe46..f213822d98 100644 --- a/src/mc/mc_ignore.c +++ b/src/mc/mc_ignore.c @@ -9,13 +9,19 @@ #include "mc_private.h" #include "smpi/private.h" #include "mc/mc_snapshot.h" +#include "mc_ignore.h" +#include "mc_protocol.h" +#include "mc_client.h" XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_ignore, mc, "Logging specific to MC ignore mechanism"); /**************************** Global variables ******************************/ -xbt_dynar_t mc_checkpoint_ignore; +// Those structures live with the MCer and should be moved in the model_checker +// structure but they are currently used before the MC initialisation +// (in standalone mode). + extern xbt_dynar_t mc_heap_comparison_ignore; extern xbt_dynar_t stacks_areas; @@ -59,41 +65,22 @@ static void checkpoint_ignore_region_free_voidp(void *r) checkpoint_ignore_region_free((mc_checkpoint_ignore_region_t) * (void **) r); } -/***********************************************************************/ - -void MC_ignore_heap(void *address, size_t size) +xbt_dynar_t MC_checkpoint_ignore_new(void) { + return xbt_dynar_new(sizeof(mc_checkpoint_ignore_region_t), + checkpoint_ignore_region_free_voidp); +} - int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - - MC_SET_MC_HEAP; - - mc_heap_ignore_region_t region = NULL; - region = xbt_new0(s_mc_heap_ignore_region_t, 1); - region->address = address; - region->size = size; - - region->block = - ((char *) address - - (char *) std_heap->heapbase) / BLOCKSIZE + 1; - - if (std_heap->heapinfo[region->block].type == 0) { - region->fragment = -1; - std_heap->heapinfo[region->block].busy_block.ignore++; - } else { - region->fragment = - ((uintptr_t) (ADDR2UINT(address) % (BLOCKSIZE))) >> std_heap-> - heapinfo[region->block].type; - std_heap->heapinfo[region->block].busy_frag.ignore[region->fragment]++; - } +/***********************************************************************/ +// Mcer +void MC_heap_region_ignore_insert(mc_heap_ignore_region_t region) +{ if (mc_heap_comparison_ignore == NULL) { mc_heap_comparison_ignore = xbt_dynar_new(sizeof(mc_heap_ignore_region_t), heap_ignore_region_free_voidp); xbt_dynar_push(mc_heap_comparison_ignore, ®ion); - if (!raw_mem_set) - MC_SET_STD_HEAP; return; } @@ -102,39 +89,84 @@ void MC_ignore_heap(void *address, size_t size) int start = 0; int end = xbt_dynar_length(mc_heap_comparison_ignore) - 1; + // Find the position where we want to insert the mc_heap_ignore_region_t: while (start <= end) { cursor = (start + end) / 2; current_region = (mc_heap_ignore_region_t) xbt_dynar_get_as(mc_heap_comparison_ignore, cursor, mc_heap_ignore_region_t); - if (current_region->address == address) { + if (current_region->address == region->address) { heap_ignore_region_free(region); - if (!raw_mem_set) - MC_SET_STD_HEAP; return; - } else if (current_region->address < address) { + } else if (current_region->address < region->address) { start = cursor + 1; } else { end = cursor - 1; } } - if (current_region->address < address) + // Insert it mc_heap_ignore_region_t: + if (current_region->address < region->address) xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor + 1, ®ion); else xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor, ®ion); +} - if (!raw_mem_set) - MC_SET_STD_HEAP; +// MCed: +static void MC_heap_region_ignore_send(mc_heap_ignore_region_t region) +{ + s_mc_ignore_heap_message_t message; + message.type = MC_MESSAGE_IGNORE_HEAP; + message.region = *region; + if (MC_protocol_send(mc_client->fd, &message, sizeof(message))) + xbt_die("Could not send ignored region to MCer"); + XBT_DEBUG("Sent ignored region to the model-checker"); } -void MC_remove_ignore_heap(void *address, size_t size) +// MCed: +void MC_ignore_heap(void *address, size_t size) { + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); + + mc_heap_ignore_region_t region = xbt_new0(s_mc_heap_ignore_region_t, 1); + region->address = address; + region->size = size; + + region->block = + ((char *) address - + (char *) std_heap->heapbase) / BLOCKSIZE + 1; + + if (std_heap->heapinfo[region->block].type == 0) { + region->fragment = -1; + std_heap->heapinfo[region->block].busy_block.ignore++; + } else { + region->fragment = + ((uintptr_t) (ADDR2UINT(address) % (BLOCKSIZE))) >> std_heap-> + heapinfo[region->block].type; + std_heap->heapinfo[region->block].busy_frag.ignore[region->fragment]++; + } + + MC_heap_region_ignore_insert(region); + +#if 1 + if (mc_mode == MC_MODE_CLIENT) + MC_heap_region_ignore_send(region); +#endif + mmalloc_set_current_heap(heap); +} - int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); +void MC_remove_ignore_heap(void *address, size_t size) +{ + if (mc_mode == MC_MODE_CLIENT) { + s_mc_ignore_memory_message_t message; + message.type = MC_MESSAGE_UNIGNORE_HEAP; + message.addr = address; + message.size = size; + MC_client_send_message(&message, sizeof(message)); + } - MC_SET_MC_HEAP; + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); unsigned int cursor = 0; int start = 0; @@ -167,19 +199,14 @@ void MC_remove_ignore_heap(void *address, size_t size) xbt_dynar_remove_at(mc_heap_comparison_ignore, cursor, NULL); MC_remove_ignore_heap(address, size); } - - if (!raw_mem_set) - MC_SET_STD_HEAP; - + mmalloc_set_current_heap(heap); } +// MCer void MC_ignore_global_variable(const char *name) { mc_process_t process = &mc_model_checker->process; - int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - - MC_SET_MC_HEAP; - + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); xbt_assert(process->object_infos, "MC subsystem not initialized"); size_t n = process->object_infos_size; @@ -205,9 +232,7 @@ void MC_ignore_global_variable(const char *name) } } } - - if (!raw_mem_set) - MC_SET_STD_HEAP; + mmalloc_set_current_heap(heap); } /** \brief Ignore a local variable in a scope @@ -228,7 +253,7 @@ static void mc_ignore_local_variable_in_scope(const char *var_name, { // Processing of direct variables: - // If the current subprogram matche the given name: + // If the current subprogram matches the given name: if (!subprogram_name || (subprogram->name && strcmp(subprogram_name, subprogram->name) == 0)) { @@ -286,17 +311,13 @@ static void MC_ignore_local_variable_in_object(const char *var_name, } } +// MCer void MC_ignore_local_variable(const char *var_name, const char *frame_name) { mc_process_t process = &mc_model_checker->process; - - - int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - if (strcmp(frame_name, "*") == 0) frame_name = NULL; - - MC_SET_MC_HEAP; + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); size_t n = process->object_infos_size; size_t i; @@ -304,15 +325,20 @@ void MC_ignore_local_variable(const char *var_name, const char *frame_name) MC_ignore_local_variable_in_object(var_name, frame_name, process->object_infos[i]); } - if (!raw_mem_set) - MC_SET_STD_HEAP; + mmalloc_set_current_heap(heap); +} +void MC_stack_area_add(stack_region_t stack_area) +{ + if (stacks_areas == NULL) + stacks_areas = xbt_dynar_new(sizeof(stack_region_t), NULL); + xbt_dynar_push(stacks_areas, &stack_area); } /** @brief Register a stack in the model checker * * The stacks are allocated in the heap. The MC handle them especially - * when we analyse/compare the content of theap so it must be told where + * when we analyse/compare the content of the heap so it must be told where * they are with this function. * * @param stack @@ -322,18 +348,10 @@ void MC_ignore_local_variable(const char *var_name, const char *frame_name) */ void MC_new_stack_area(void *stack, smx_process_t process, void *context, size_t size) { + xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); - int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - - MC_SET_MC_HEAP; - - if (stacks_areas == NULL) - stacks_areas = xbt_dynar_new(sizeof(stack_region_t), NULL); - - stack_region_t region = NULL; - region = xbt_new0(s_stack_region_t, 1); + stack_region_t region = xbt_new0(s_stack_region_t, 1); region->address = stack; - region->process_name = process && process->name ? strdup(process->name) : NULL; region->context = context; region->size = size; region->block = @@ -346,49 +364,44 @@ void MC_new_stack_area(void *stack, smx_process_t process, void *context, size_t #endif region->process_index = -1; - xbt_dynar_push(stacks_areas, ®ion); + if (mc_mode == MC_MODE_CLIENT) { + s_mc_stack_region_message_t message; + message.type = MC_MESSAGE_STACK_REGION; + message.stack_region = *region; + MC_client_send_message(&message, sizeof(message)); + } - if (!raw_mem_set) - MC_SET_STD_HEAP; + MC_stack_area_add(region); + + mmalloc_set_current_heap(heap); } -void MC_ignore(void *addr, size_t size) +void MC_process_ignore_memory(mc_process_t process, void *addr, size_t size) { - - int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - - MC_SET_MC_HEAP; - - if (mc_checkpoint_ignore == NULL) - mc_checkpoint_ignore = - xbt_dynar_new(sizeof(mc_checkpoint_ignore_region_t), - checkpoint_ignore_region_free_voidp); - + xbt_dynar_t checkpoint_ignore = process->checkpoint_ignore; mc_checkpoint_ignore_region_t region = xbt_new0(s_mc_checkpoint_ignore_region_t, 1); region->addr = addr; region->size = size; - if (xbt_dynar_is_empty(mc_checkpoint_ignore)) { - xbt_dynar_push(mc_checkpoint_ignore, ®ion); + if (xbt_dynar_is_empty(checkpoint_ignore)) { + xbt_dynar_push(checkpoint_ignore, ®ion); } else { unsigned int cursor = 0; int start = 0; - int end = xbt_dynar_length(mc_checkpoint_ignore) - 1; + int end = xbt_dynar_length(checkpoint_ignore) - 1; mc_checkpoint_ignore_region_t current_region = NULL; while (start <= end) { cursor = (start + end) / 2; current_region = - (mc_checkpoint_ignore_region_t) xbt_dynar_get_as(mc_checkpoint_ignore, + (mc_checkpoint_ignore_region_t) xbt_dynar_get_as(checkpoint_ignore, cursor, mc_checkpoint_ignore_region_t); if (current_region->addr == addr) { if (current_region->size == size) { checkpoint_ignore_region_free(region); - if (!raw_mem_set) - MC_SET_STD_HEAP; return; } else if (current_region->size < size) { start = cursor + 1; @@ -404,17 +417,14 @@ void MC_ignore(void *addr, size_t size) if (current_region->addr == addr) { if (current_region->size < size) { - xbt_dynar_insert_at(mc_checkpoint_ignore, cursor + 1, ®ion); + xbt_dynar_insert_at(checkpoint_ignore, cursor + 1, ®ion); } else { - xbt_dynar_insert_at(mc_checkpoint_ignore, cursor, ®ion); + xbt_dynar_insert_at(checkpoint_ignore, cursor, ®ion); } } else if (current_region->addr < addr) { - xbt_dynar_insert_at(mc_checkpoint_ignore, cursor + 1, ®ion); + xbt_dynar_insert_at(checkpoint_ignore, cursor + 1, ®ion); } else { - xbt_dynar_insert_at(mc_checkpoint_ignore, cursor, ®ion); + xbt_dynar_insert_at(checkpoint_ignore, cursor, ®ion); } } - - if (!raw_mem_set) - MC_SET_STD_HEAP; }