X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/910500315ef51a0f48ca6f6b70b335b986d4e17b..a5ca7957443f89e7fef7929dcd70ba4fd2695e67:/src/mc/mc_ignore.c diff --git a/src/mc/mc_ignore.c b/src/mc/mc_ignore.c index 0675eb9dd2..bde464c8cf 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,21 @@ 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]++; - } +/***********************************************************************/ +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,28 +88,70 @@ 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); +} + +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"); +} + +// FIXME, cross-process support? (or make this it is used on the app-side) +void MC_ignore_heap(void *address, size_t size) +{ + int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); + MC_SET_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 if (!raw_mem_set) MC_SET_STD_HEAP; @@ -131,6 +159,13 @@ void MC_ignore_heap(void *address, size_t size) 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)); + } int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); @@ -173,6 +208,7 @@ void MC_remove_ignore_heap(void *address, size_t size) } +// FIXME, cross-process support? void MC_ignore_global_variable(const char *name) { mc_process_t process = &mc_model_checker->process; @@ -221,6 +257,7 @@ void MC_ignore_global_variable(const char *name) * \param subprogram (possibly inlined) Subprogram of the scope * \param scope Current scope */ + // FIXME, cross-process support (messaging?) static void mc_ignore_local_variable_in_scope(const char *var_name, const char *subprogram_name, dw_frame_t subprogram, @@ -228,7 +265,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)) { @@ -298,9 +335,11 @@ void MC_ignore_local_variable(const char *var_name, const char *frame_name) MC_SET_MC_HEAP; - MC_ignore_local_variable_in_object(var_name, frame_name, process->libsimgrid_info); - if (frame_name != NULL) - MC_ignore_local_variable_in_object(var_name, frame_name, process->binary_info); + size_t n = process->object_infos_size; + size_t i; + for (i=0; i!=n; ++i) { + MC_ignore_local_variable_in_object(var_name, frame_name, process->object_infos[i]); + } if (!raw_mem_set) MC_SET_STD_HEAP; @@ -310,7 +349,7 @@ void MC_ignore_local_variable(const char *var_name, const char *frame_name) /** @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 @@ -350,43 +389,32 @@ void MC_new_stack_area(void *stack, smx_process_t process, void *context, size_t MC_SET_STD_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; @@ -402,17 +430,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; }