From: Gabriel Corona Date: Fri, 11 Mar 2016 16:02:43 +0000 (+0100) Subject: [mc] Move client-side message processing in the Client class X-Git-Tag: v3_13~451^2 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/d0db566319780080d97b6b0e66717959b42ff228 [mc] Move client-side message processing in the Client class --- diff --git a/src/mc/Client.cpp b/src/mc/Client.cpp index a36075f6b6..38ebb687ab 100644 --- a/src/mc/Client.cpp +++ b/src/mc/Client.cpp @@ -15,6 +15,8 @@ #include #include +#include "src/internal_config.h" + #include "src/mc/mc_protocol.h" #include "src/mc/Client.hpp" @@ -148,5 +150,96 @@ void Client::mainLoop(void) } } +void Client::reportAssertionFailure(const char* description) +{ + if (channel_.send(MC_MESSAGE_ASSERTION_FAILED)) + xbt_die("Could not send assertion to model-checker"); + this->handleMessages(); +} + +void Client::ignoreMemory(void* addr, std::size_t size) +{ + s_mc_ignore_memory_message_t message; + message.type = MC_MESSAGE_IGNORE_MEMORY; + message.addr = (std::uintptr_t) addr; + message.size = size; + if (channel_.send(message)) + xbt_die("Could not send IGNORE_MEMORY mesage to model-checker"); +} + +void Client::ignoreHeap(void* address, std::size_t size) +{ + xbt_mheap_t heap = mmalloc_get_current_heap(); + + s_mc_ignore_heap_message_t message; + message.type = MC_MESSAGE_IGNORE_HEAP; + message.address = address; + message.size = size; + message.block = + ((char *) address - + (char *) heap->heapbase) / BLOCKSIZE + 1; + if (heap->heapinfo[message.block].type == 0) { + message.fragment = -1; + heap->heapinfo[message.block].busy_block.ignore++; + } else { + message.fragment = + ((uintptr_t) (ADDR2UINT(address) % (BLOCKSIZE))) >> + heap->heapinfo[message.block].type; + heap->heapinfo[message.block].busy_frag.ignore[message.fragment]++; + } + + if (channel_.send(message)) + xbt_die("Could not send ignored region to MCer"); +} + +void Client::unignoreHeap(void* address, std::size_t size) +{ + s_mc_ignore_memory_message_t message; + message.type = MC_MESSAGE_UNIGNORE_HEAP; + message.addr = (std::uintptr_t) address; + message.size = size; + if (channel_.send(message)) + xbt_die("Could not send IGNORE_HEAP mesasge to model-checker"); +} + +void Client::declareSymbol(const char *name, int* value) +{ + s_mc_register_symbol_message_t message; + message.type = MC_MESSAGE_REGISTER_SYMBOL; + if (strlen(name) + 1 > sizeof(message.name)) + xbt_die("Symbol is too long"); + strncpy(message.name, name, sizeof(message.name)); + message.callback = nullptr; + message.data = value; + if (channel_.send(message)) + xbt_die("Could send REGISTER_SYMBOL message to model-checker"); +} + +void Client::declareStack(void *stack, size_t size, smx_process_t process, ucontext_t* context) +{ + xbt_mheap_t heap = mmalloc_get_current_heap(); + + s_stack_region_t region; + memset(®ion, 0, sizeof(region)); + region.address = stack; + region.context = context; + region.size = size; + region.block = + ((char *) stack - + (char *) heap->heapbase) / BLOCKSIZE + 1; +#if HAVE_SMPI + if (smpi_privatize_global_variables && process) + region.process_index = smpi_process_index_of_smx_process(process); + else +#endif + region.process_index = -1; + + s_mc_stack_region_message_t message; + message.type = MC_MESSAGE_STACK_REGION; + message.stack_region = region; + if (channel_.send(message)) + xbt_die("Coule not send STACK_REGION to model-checker"); +} + } } diff --git a/src/mc/Client.hpp b/src/mc/Client.hpp index 8ed4907dfe..69248bcfc7 100644 --- a/src/mc/Client.hpp +++ b/src/mc/Client.hpp @@ -13,6 +13,8 @@ #include +#include + #include "src/mc/mc_protocol.h" #include "src/mc/Channel.hpp" @@ -31,6 +33,12 @@ public: Channel const& getChannel() const { return channel_; } Channel& getChannel() { return channel_; } void mainLoop(void); + void reportAssertionFailure(const char* description = nullptr); + void ignoreMemory(void* addr, std::size_t size); + void ignoreHeap(void* addr, std::size_t size); + void unignoreHeap(void* addr, std::size_t size); + void declareSymbol(const char *name, int* value); + void declareStack(void *stack, size_t size, smx_process_t process, ucontext_t* context); // Singleton :/ // TODO, remove the singleton antipattern. diff --git a/src/mc/mc_client_api.cpp b/src/mc/mc_client_api.cpp index d362072369..9f6c5751cb 100644 --- a/src/mc/mc_client_api.cpp +++ b/src/mc/mc_client_api.cpp @@ -29,19 +29,15 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_client_api, mc, void MC_assert(int prop) { - if (MC_is_active() && !prop) { - if (simgrid::mc::Client::get()->getChannel().send(MC_MESSAGE_ASSERTION_FAILED)) - xbt_die("Could not send assertion to model-checker"); - simgrid::mc::Client::get()->handleMessages(); - } + if (MC_is_active() && !prop) + simgrid::mc::Client::get()->reportAssertionFailure(); } void MC_cut(void) { - // FIXME, this is a function called in the model-checked - // but the variable must be set in the model-checker. - // We should send a message here instead. - user_max_depth_reached = 1; + // FIXME, We want to do this in the model-checker: + // user_max_depth_reached = 1; + xbt_die("MC_cut() not implemented"); } void MC_ignore(void* addr, size_t size) @@ -49,13 +45,7 @@ void MC_ignore(void* addr, size_t size) xbt_assert(mc_mode != MC_MODE_SERVER); if (mc_mode != MC_MODE_CLIENT) return; - - s_mc_ignore_memory_message_t message; - message.type = MC_MESSAGE_IGNORE_MEMORY; - message.addr = (std::uintptr_t) addr; - message.size = size; - if (simgrid::mc::Client::get()->getChannel().send(message)) - xbt_die("Could not send IGNORE_MEMORY mesage to model-checker"); + simgrid::mc::Client::get()->ignoreMemory(addr, size); } void MC_automaton_new_propositional_symbol(const char *id, int(*fct)(void)) @@ -74,14 +64,43 @@ void MC_automaton_new_propositional_symbol_pointer(const char *name, int* value) xbt_assert(mc_mode != MC_MODE_SERVER); if (mc_mode != MC_MODE_CLIENT) return; + simgrid::mc::Client::get()->declareSymbol(name, value); +} - s_mc_register_symbol_message_t message; - message.type = MC_MESSAGE_REGISTER_SYMBOL; - if (strlen(name) + 1 > sizeof(message.name)) - xbt_die("Symbol is too long"); - strncpy(message.name, name, sizeof(message.name)); - message.callback = nullptr; - message.data = value; - if (simgrid::mc::Client::get()->getChannel().send(message)) - xbt_die("Could send REGISTER_SYMBOL message to model-checker"); +/** @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 the heap so it must be told where + * they are with this function. + * + * @param stack + * @param process Process owning the stack + * @param context + * @param size Size of the stack + */ +void MC_register_stack_area(void *stack, smx_process_t process, ucontext_t* context, size_t size) +{ + if (mc_mode != MC_MODE_CLIENT) + return; + simgrid::mc::Client::get()->declareStack(stack, size, process, context); +} + +void MC_ignore_global_variable(const char *name) +{ + // TODO, send a message to the model_checker + xbt_die("Unimplemented"); +} + +void MC_ignore_heap(void *address, size_t size) +{ + if (mc_mode != MC_MODE_CLIENT) + return; + simgrid::mc::Client::get()->ignoreHeap(address, size); +} + +void MC_remove_ignore_heap(void *address, size_t size) +{ + if (mc_mode != MC_MODE_CLIENT) + return; + simgrid::mc::Client::get()->unignoreHeap(address, size); } diff --git a/src/mc/mc_ignore.cpp b/src/mc/mc_ignore.cpp deleted file mode 100644 index 16548a6f02..0000000000 --- a/src/mc/mc_ignore.cpp +++ /dev/null @@ -1,109 +0,0 @@ -/* Copyright (c) 2008-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 "src/internal_config.h" -#include "src/mc/mc_private.h" -#include "src/smpi/private.h" -#include "src/mc/mc_snapshot.h" -#include "src/mc/mc_ignore.h" -#include "src/mc/mc_protocol.h" -#include "src/mc/Client.hpp" - -XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_ignore, mc, - "Logging specific to MC ignore mechanism"); - -extern "C" { - -// ***** Model-checked - -void MC_ignore_heap(void *address, size_t size) -{ - if (mc_mode != MC_MODE_CLIENT) - return; - - xbt_mheap_t heap = mmalloc_get_current_heap(); - - s_mc_ignore_heap_message_t message; - message.type = MC_MESSAGE_IGNORE_HEAP; - message.address = address; - message.size = size; - message.block = - ((char *) address - - (char *) heap->heapbase) / BLOCKSIZE + 1; - if (heap->heapinfo[message.block].type == 0) { - message.fragment = -1; - heap->heapinfo[message.block].busy_block.ignore++; - } else { - message.fragment = - ((uintptr_t) (ADDR2UINT(address) % (BLOCKSIZE))) >> - heap->heapinfo[message.block].type; - heap->heapinfo[message.block].busy_frag.ignore[message.fragment]++; - } - - if (simgrid::mc::Client::get()->getChannel().send(message)) - xbt_die("Could not send ignored region to MCer"); -} - -void MC_remove_ignore_heap(void *address, size_t size) -{ - if (mc_mode != MC_MODE_CLIENT) - return; - - s_mc_ignore_memory_message_t message; - message.type = MC_MESSAGE_UNIGNORE_HEAP; - message.addr = (std::uintptr_t) address; - message.size = size; - if (simgrid::mc::Client::get()->getChannel().send(message)) - xbt_die("Could not send UNIGNORE_HEAP mesasge to model-checker"); -} - -void MC_ignore_global_variable(const char *name) -{ - // TODO, send a message to the model_checker - xbt_die("Unimplemented"); -} - -/** @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 the heap so it must be told where - * they are with this function. - * - * @param stack - * @param process Process owning the stack - * @param context - * @param size Size of the stack - */ -void MC_register_stack_area(void *stack, smx_process_t process, ucontext_t* context, size_t size) -{ - if (mc_mode != MC_MODE_CLIENT) - return; - - xbt_mheap_t heap = mmalloc_get_current_heap(); - - s_stack_region_t region; - memset(®ion, 0, sizeof(region)); - region.address = stack; - region.context = context; - region.size = size; - region.block = - ((char *) stack - - (char *) heap->heapbase) / BLOCKSIZE + 1; -#if HAVE_SMPI - if (smpi_privatize_global_variables && process) - region.process_index = smpi_process_index_of_smx_process(process); - else -#endif - region.process_index = -1; - - s_mc_stack_region_message_t message; - message.type = MC_MESSAGE_STACK_REGION; - message.stack_region = region; - if (simgrid::mc::Client::get()->getChannel().send(message)) - xbt_die("Coule not send STACK_REGION to model-checker"); -} - -} diff --git a/src/xbt/log.c b/src/xbt/log.c index 8701f99a6e..1428f70217 100644 --- a/src/xbt/log.c +++ b/src/xbt/log.c @@ -627,7 +627,6 @@ static void xbt_log_connect_categories(void) XBT_LOG_CONNECT(mc_diff); XBT_LOG_CONNECT(mc_dwarf); XBT_LOG_CONNECT(mc_hash); - XBT_LOG_CONNECT(mc_ignore); XBT_LOG_CONNECT(mc_liveness); XBT_LOG_CONNECT(mc_memory); XBT_LOG_CONNECT(mc_page_snapshot); diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake index ed8fb64f07..0979e0cfc1 100644 --- a/tools/cmake/DefinePackages.cmake +++ b/tools/cmake/DefinePackages.cmake @@ -593,7 +593,6 @@ set(MC_SRC src/mc/mc_dwarf_tagnames.cpp src/mc/mc_hash.hpp src/mc/mc_hash.cpp - src/mc/mc_ignore.cpp src/mc/mc_ignore.h src/mc/mc_mmalloc.h src/mc/mc_liveness.h