From: Gabriel Corona Date: Fri, 6 Feb 2015 10:29:56 +0000 (+0100) Subject: [mc] Implement remote support for MC_ignore X-Git-Tag: v3_12~732^2~132 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/02f267e2895f3985fe73344a8b96ac05363b8b62 [mc] Implement remote support for MC_ignore --- diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c index bce4bbd5c6..fe602a4a00 100644 --- a/src/mc/mc_checkpoint.c +++ b/src/mc/mc_checkpoint.c @@ -599,7 +599,7 @@ static void MC_snapshot_handle_ignore(mc_snapshot_t snapshot) unsigned int cursor = 0; mc_checkpoint_ignore_region_t region; // FIXME, cross-process support (mc_checkpoint_ignore) - xbt_dynar_foreach (mc_checkpoint_ignore, cursor, region) { + xbt_dynar_foreach (mc_model_checker->process.checkpoint_ignore, cursor, region) { s_mc_snapshot_ignored_data_t ignored_data; ignored_data.start = region->addr; ignored_data.size = region->size; @@ -612,7 +612,7 @@ static void MC_snapshot_handle_ignore(mc_snapshot_t snapshot) } // Zero the memory: - xbt_dynar_foreach (mc_checkpoint_ignore, cursor, region) { + xbt_dynar_foreach (mc_model_checker->process.checkpoint_ignore, cursor, region) { MC_process_clear_memory(snapshot->process, region->addr, region->size); } diff --git a/src/mc/mc_client.c b/src/mc/mc_client.c index 55cc2ca388..c903246cce 100644 --- a/src/mc/mc_client.c +++ b/src/mc/mc_client.c @@ -13,10 +13,16 @@ #include #include +#include #include "mc_protocol.h" #include "mc_client.h" +// We won't need those once the separation MCer/MCed is complete: +#include "mc_mmalloc.h" +#include "mc_ignore.h" +#include "mc_model_checker.h" + XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_client, mc, "MC client logic"); mc_client_t mc_client; @@ -56,6 +62,12 @@ void MC_client_hello(void) XBT_DEBUG("Greeted the MC server"); } +void MC_client_send_message(void* message, size_t size) +{ + if (MC_protocol_send(mc_client->fd, message, size)) + xbt_die("Could not send message %i", (int) ((mc_message_t)message)->type); +} + void MC_client_handle_messages(void) { while (1) { @@ -80,3 +92,21 @@ void MC_client_handle_messages(void) } } } + +void MC_ignore(void* addr, size_t size) +{ + if (mc_mode == MC_MODE_CLIENT) { + s_mc_ignore_memory_message_t message; + message.type = MC_MESSAGE_IGNORE_MEMORY; + message.addr = addr; + message.size = size; + MC_client_send_message(&message, sizeof(message)); + } + + // TODO, remove this once the migration has been completed + int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); + MC_SET_MC_HEAP; + MC_process_ignore_memory(&mc_model_checker->process, addr, size); + if (!raw_mem_set) + MC_SET_STD_HEAP; +} diff --git a/src/mc/mc_client.h b/src/mc/mc_client.h index 12234edeac..638a8eafda 100644 --- a/src/mc/mc_client.h +++ b/src/mc/mc_client.h @@ -21,6 +21,10 @@ extern mc_client_t mc_client; void MC_client_init(void); void MC_client_hello(void); void MC_client_handle_messages(void); +void MC_client_send_message(void* message, size_t size); + +void MC_ignore(void* addr, size_t size); + SG_END_DECL() diff --git a/src/mc/mc_ignore.c b/src/mc/mc_ignore.c index 5f8ea90b6f..d80a13014e 100644 --- a/src/mc/mc_ignore.c +++ b/src/mc/mc_ignore.c @@ -18,7 +18,7 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_ignore, mc, /**************************** Global variables ******************************/ -xbt_dynar_t mc_checkpoint_ignore; + extern xbt_dynar_t mc_heap_comparison_ignore; extern xbt_dynar_t stacks_areas; @@ -62,19 +62,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 +94,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,9 +107,6 @@ 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) @@ -129,7 +126,6 @@ void MC_ignore_heap(void *address, size_t size) return; int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - MC_SET_MC_HEAP; mc_heap_ignore_region_t region = NULL; @@ -387,44 +383,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; - - // 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 +424,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; } diff --git a/src/mc/mc_ignore.h b/src/mc/mc_ignore.h new file mode 100644 index 0000000000..35572d4825 --- /dev/null +++ b/src/mc/mc_ignore.h @@ -0,0 +1,21 @@ +/* Copyright (c) 2015. The SimGrid Team. All rights reserved. */ + +/* This program is free software; you can redistribute it and/or modify it + * under the terms of the license (GNU LGPL) which comes with this package. */ + +#include + +#include "mc/datatypes.h" +#include "mc_process.h" + +#include "xbt/misc.h" /* SG_BEGIN_DECL */ + +SG_BEGIN_DECL(); + +void MC_heap_region_ignore_insert(mc_heap_ignore_region_t region); +void MC_heap_region_ignore_send(mc_heap_ignore_region_t region); +void MC_process_ignore_memory(mc_process_t process, void *addr, size_t size); + +xbt_dynar_t MC_checkpoint_ignore_new(void); + +SG_END_DECL(); diff --git a/src/mc/mc_model_checker.h b/src/mc/mc_model_checker.h index e8e7c8274e..308cf127ff 100644 --- a/src/mc/mc_model_checker.h +++ b/src/mc/mc_model_checker.h @@ -17,15 +17,6 @@ SG_BEGIN_DECL() -typedef enum { - MC_MODE_NONE = 0, - MC_MODE_STANDALONE, - MC_MODE_CLIENT, - MC_MODE_SERVER -} e_mc_mode_t; - -extern e_mc_mode_t mc_mode; - /** @brief State of the model-checker (global variables for the model checker) * * Each part of the state of the model chercker represented as a global diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index 7f092a5489..f6087c6678 100644 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@ -41,10 +41,6 @@ SG_BEGIN_DECL() typedef struct s_mc_function_index_item s_mc_function_index_item_t, *mc_function_index_item_t; -/****************************** Snapshots ***********************************/ - -extern xbt_dynar_t mc_checkpoint_ignore; - /********************************* MC Global **********************************/ /** Initialisation of the model-checker diff --git a/src/mc/mc_process.c b/src/mc/mc_process.c index fd3942043b..10d0a45d6e 100644 --- a/src/mc/mc_process.c +++ b/src/mc/mc_process.c @@ -21,6 +21,8 @@ #include "mc_object_info.h" #include "mc_address_space.h" #include "mc_unw.h" +#include "mc_snapshot.h" +#include "mc_ignore.h" XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_process, mc, "MC process information"); @@ -28,6 +30,10 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_process, mc, static void MC_process_init_memory_map_info(mc_process_t process); static void MC_process_open_memory_file(mc_process_t process); +// ***** Destructor callbacks + +// ***** mc_address_space methods for mc_process + static mc_process_t MC_process_get_process(mc_process_t p) { return p; } @@ -42,6 +48,8 @@ bool MC_is_process(mc_address_space_t p) return p->address_space_class == &mc_process_class; } +// ***** mc_process + void MC_process_init(mc_process_t process, pid_t pid, int sockfd) { process->address_space.address_space_class = &mc_process_class; @@ -70,6 +78,8 @@ void MC_process_init(mc_process_t process, pid_t pid, int sockfd) &process->heap_address, std_heap_var->address, sizeof(struct mdesc*), MC_PROCESS_INDEX_DISABLED); + process->checkpoint_ignore = MC_checkpoint_ignore_new(); + process->unw_addr_space = unw_create_addr_space(&mc_unw_accessors , __BYTE_ORDER); if (process->process_flags & MC_PROCESS_SELF_FLAG) { process->unw_underlying_addr_space = unw_local_addr_space; @@ -92,6 +102,8 @@ void MC_process_clear(mc_process_t process) process->maestro_stack_start = NULL; process->maestro_stack_end = NULL; + xbt_dynar_free(&process->checkpoint_ignore); + size_t i; for (i=0; i!=process->object_infos_size; ++i) { MC_free_object_info(&process->object_infos[i]); diff --git a/src/mc/mc_process.h b/src/mc/mc_process.h index b8c551436d..1e4384d153 100644 --- a/src/mc/mc_process.h +++ b/src/mc/mc_process.h @@ -102,6 +102,8 @@ struct s_mc_process { /** The corresponding context */ void* unw_underlying_context; + + xbt_dynar_t checkpoint_ignore; }; bool MC_is_process(mc_address_space_t p); diff --git a/src/mc/mc_protocol.h b/src/mc/mc_protocol.h index be17129e95..70fcbbf3ae 100644 --- a/src/mc/mc_protocol.h +++ b/src/mc/mc_protocol.h @@ -23,6 +23,17 @@ SG_BEGIN_DECL() /** Environment variable name used to pass the communication socket */ #define MC_ENV_SOCKET_FD "SIMGRID_MC_SOCKET_FD" +// ***** MC mode + +typedef enum { + MC_MODE_NONE = 0, + MC_MODE_STANDALONE, + MC_MODE_CLIENT, + MC_MODE_SERVER +} e_mc_mode_t; + +extern e_mc_mode_t mc_mode; + // ***** Messages typedef enum { @@ -30,6 +41,7 @@ typedef enum { MC_MESSAGE_HELLO = 1, MC_MESSAGE_CONTINUE = 2, MC_MESSAGE_IGNORE_REGION = 3, + MC_MESSAGE_IGNORE_MEMORY = 4, } e_mc_message_type; #define MC_MESSAGE_LENGTH 512 @@ -55,6 +67,12 @@ typedef struct s_mc_ignore_region_message { s_mc_heap_ignore_region_t region; } s_mc_ignore_region_message_t, *mc_ignore_region_message_t; +typedef struct s_mc_ignore_memory_message { + e_mc_message_type type; + void *addr; + size_t size; +} s_mc_ignore_memory_message_t, *mc_ignore_memory_message_t; + int MC_protocol_send(int socket, void* message, size_t size); int MC_protocol_send_simple_message(int socket, int type); int MC_protocol_hello(int socket); diff --git a/src/mc/mc_server.cpp b/src/mc/mc_server.cpp index 88f2bb0749..2308a8532c 100644 --- a/src/mc/mc_server.cpp +++ b/src/mc/mc_server.cpp @@ -19,6 +19,7 @@ #include "mc_protocol.h" #include "mc_server.h" #include "mc_private.h" +#include "mc_ignore.h" XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_server, mc, "MC server logic"); @@ -124,7 +125,7 @@ void throw_socket_error(int fd) void s_mc_server::handle_events() { - s_mc_message_t message; + char buffer[MC_MESSAGE_LENGTH]; struct pollfd* socket_pollfd = &fds[SOCKET_FD_INDEX]; struct pollfd* signalfd_pollfd = &fds[SIGNAL_FD_INDEX]; @@ -139,16 +140,40 @@ void s_mc_server::handle_events() if (socket_pollfd->revents) { if (socket_pollfd->revents & POLLIN) { - ssize_t size = recv(socket_pollfd->fd, &message, sizeof(message), MSG_DONTWAIT); + + ssize_t size = recv(socket_pollfd->fd, buffer, sizeof(buffer), MSG_DONTWAIT); if (size == -1 && errno != EAGAIN) throw std::system_error(errno, std::system_category()); - else switch(message.type) { + + s_mc_message_t base_message; + if (size < (ssize_t) sizeof(base_message)) + xbt_die("Broken message"); + memcpy(&base_message, buffer, sizeof(base_message)); + + switch(base_message.type) { + case MC_MESSAGE_IGNORE_REGION: XBT_DEBUG("Received ignored region"); - // Ignored for now + if (size != sizeof(s_mc_ignore_region_message_t)) + xbt_die("Broken messsage"); + // TODO, handle the message break; + + case MC_MESSAGE_IGNORE_MEMORY: + { + XBT_DEBUG("Received ignored memory"); + if (size != sizeof(s_mc_ignore_memory_message_t)) + xbt_die("Broken messsage"); + s_mc_ignore_memory_message_t message; + memcpy(&message, buffer, sizeof(message)); + MC_process_ignore_memory(&mc_model_checker->process, + message.addr, message.size); + } + break; + default: xbt_die("Unexpected message from model-checked application"); + } return; }