X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/cf9a823f1cfd8b0098a039bff8ff6567e9beac91..9c40447cb76e20937a7c2a5acedcd84a22990514:/src/mc/mc_ignore.c?ds=sidebyside diff --git a/src/mc/mc_ignore.c b/src/mc/mc_ignore.c index 5f8ea90b6f..d0c2c37bbf 100644 --- a/src/mc/mc_ignore.c +++ b/src/mc/mc_ignore.c @@ -18,7 +18,10 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_ignore, mc, /**************************** 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; @@ -62,19 +65,21 @@ static void checkpoint_ignore_region_free_voidp(void *r) checkpoint_ignore_region_free((mc_checkpoint_ignore_region_t) * (void **) r); } +xbt_dynar_t MC_checkpoint_ignore_new(void) +{ + return xbt_dynar_new(sizeof(mc_checkpoint_ignore_region_t), + checkpoint_ignore_region_free_voidp); +} + /***********************************************************************/ void MC_heap_region_ignore_insert(mc_heap_ignore_region_t region) { - int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - 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; } @@ -92,8 +97,6 @@ void MC_heap_region_ignore_insert(mc_heap_ignore_region_t region) mc_heap_ignore_region_t); 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 < region->address) { start = cursor + 1; @@ -107,15 +110,12 @@ void MC_heap_region_ignore_insert(mc_heap_ignore_region_t region) 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; } void MC_heap_region_ignore_send(mc_heap_ignore_region_t region) { - s_mc_ignore_region_message_t message; - message.type = MC_MESSAGE_IGNORE_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"); @@ -125,15 +125,10 @@ void MC_heap_region_ignore_send(mc_heap_ignore_region_t region) // FIXME, cross-process support? (or make this it is used on the app-side) void MC_ignore_heap(void *address, size_t size) { - if(!std_heap) - return; - 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); + mc_heap_ignore_region_t region = xbt_new0(s_mc_heap_ignore_region_t, 1); region->address = address; region->size = size; @@ -164,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); @@ -344,6 +346,13 @@ void MC_ignore_local_variable(const char *var_name, const char *frame_name) } +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 @@ -359,16 +368,10 @@ void MC_new_stack_area(void *stack, smx_process_t process, void *context, size_t { 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 = @@ -381,50 +384,45 @@ 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)); + } + + MC_stack_area_add(region); if (!raw_mem_set) 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; - - // FIXME, cross-process support - 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; @@ -440,17 +438,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; }