From: Gabriel Corona Date: Tue, 14 Apr 2015 12:02:51 +0000 (+0200) Subject: Merge branch 'master' into mc-process X-Git-Tag: v3_12~732^2~61 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/9932a0c0d2c44e34633c97a827b2b04d615cb4e9 Merge branch 'master' into mc-process Conflicts: teshsuite/mc/replay/random_bug.c --- 9932a0c0d2c44e34633c97a827b2b04d615cb4e9 diff --cc buildtools/Cmake/DefinePackages.cmake index ff3495096c,75b1d8aaad..15a6ec5c8f --- a/buildtools/Cmake/DefinePackages.cmake +++ b/buildtools/Cmake/DefinePackages.cmake @@@ -642,26 -627,17 +637,29 @@@ set(MC_SR src/mc/mc_visited.c src/mc/mc_memory_map.h src/mc/memory_map.c + src/mc/mc_client.c + src/mc/mc_client_api.c + src/mc/mc_client.h + src/mc/mc_protocol.h + src/mc/mc_protocol.c + src/mc/mc_server.cpp + src/mc/mc_server.h + src/mc/mc_smx.h + src/mc/mc_smx.c ) +set(MC_SIMGRID_MC_SRC + src/mc/simgrid_mc.cpp) + set(headers_to_install - include/instr/instr.h - include/msg/datatypes.h include/msg/msg.h - include/simdag/datatypes.h + include/msg/datatypes.h include/simdag/simdag.h + include/simdag/datatypes.h + + include/simgrid/instr.h + include/simgrid/msg.h + include/simgrid/simdag.h include/simgrid.h include/simgrid/datatypes.h include/simgrid/modelchecker.h diff --cc examples/msg/mc/bugged1.c index 62539cd4c1,62539cd4c1..4a7aa9eb95 --- a/examples/msg/mc/bugged1.c +++ b/examples/msg/mc/bugged1.c @@@ -9,7 -9,7 +9,7 @@@ /* which is incorrect because the message ordering is non-deterministic */ /******************************************************************************/ --#include ++#include #include #define N 3 diff --cc examples/msg/mc/bugged2.c index 5d0e375af3,5d0e375af3..93bf21d89f --- a/examples/msg/mc/bugged2.c +++ b/examples/msg/mc/bugged2.c @@@ -9,7 -9,7 +9,7 @@@ /* which is incorrect because the message ordering is non-deterministic */ /******************************************************************************/ --#include ++#include #include #define N 3 diff --cc examples/msg/mc/bugged3.c index 5f949c0d45,5f949c0d45..f7c1d26f98 --- a/examples/msg/mc/bugged3.c +++ b/examples/msg/mc/bugged3.c @@@ -13,7 -13,7 +13,7 @@@ /* same buffer for reception (task1). */ /******************************************************************************/ --#include ++#include #include XBT_LOG_NEW_DEFAULT_CATEGORY(bugged3, "this example"); diff --cc examples/msg/mc/electric_fence.c index 0e031419ca,0e031419ca..a067724807 --- a/examples/msg/mc/electric_fence.c +++ b/examples/msg/mc/electric_fence.c @@@ -11,7 -11,7 +11,7 @@@ /* --cfg=model-check/max_depth:) is reached. */ /******************************************************************************/ --#include ++#include #include #define N 2 diff --cc src/mc/mc_base.c index b380bb3b16,2a587228ab..65052ef791 --- a/src/mc/mc_base.c +++ b/src/mc/mc_base.c @@@ -12,23 -10,13 +12,25 @@@ #include "../simix/smx_private.h" #include "mc_record.h" +#ifdef HAVE_MC +#include "mc_process.h" +#include "mc_model_checker.h" +#include "mc_protocol.h" +#include "mc_smx.h" +#include "mc_server.h" +#endif + XBT_LOG_NEW_CATEGORY(mc, "All MC categories"); -/** - * \brief Schedules all the process that are ready to run - */ void MC_wait_for_requests(void) { ++#ifdef HAVE_MC + if (mc_mode == MC_MODE_SERVER) { + MC_server_wait_client(&mc_model_checker->process); + return; + } ++#endif + smx_process_t process; smx_simcall_t req; unsigned int iter; diff --cc src/mc/mc_global.c index 8d498deacb,790d1e9b22..faf1eaf685 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@@ -22,12 -21,11 +22,12 @@@ #include "xbt/fifo.h" #include "xbt/automaton.h" #include "xbt/dict.h" - #include "mc_server.h" ++#include "mc_record.h" #ifdef HAVE_MC -#define UNW_LOCAL_ONLY ++#include "mc_server.h" #include - +#include - #include "../xbt/mmalloc/mmprivate.h" #include "mc_object_info.h" #include "mc_comm_pattern.h" @@@ -747,14 -885,3 +747,16 @@@ void MC_process_clock_add(smx_process_ { mc_time[process->pid] += amount; } + ++#ifdef HAVE_MC +void MC_report_assertion_error(void) +{ + XBT_INFO("**************************"); + XBT_INFO("*** PROPERTY NOT VALID ***"); + XBT_INFO("**************************"); + XBT_INFO("Counter-example execution trace:"); + MC_record_dump_path(mc_stack); + MC_dump_stack_safety(mc_stack); + MC_print_statistics(mc_stats); +} ++#endif diff --cc src/mc/mc_private.h index fed2f4d562,997aca035a..c19aa1fac7 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@@ -30,8 -27,8 +30,7 @@@ #include "../xbt/mmalloc/mmprivate.h" #include "xbt/automaton.h" #include "xbt/hash.h" - #include "msg/msg.h" -#include "simgrid/msg.h" --#include "msg/datatypes.h" ++#include #include "xbt/strbuff.h" #include "xbt/parmap.h" diff --cc src/mc/mc_process.h index 8159b3e700,0000000000..5e2175c716 mode 100644,000000..100644 --- a/src/mc/mc_process.h +++ b/src/mc/mc_process.h @@@ -1,215 -1,0 +1,218 @@@ +/* Copyright (c) 2008-2014. 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. */ + +#ifndef MC_PROCESS_H +#define MC_PROCESS_H + +#include +#include + +#include "simgrid_config.h" + +#include + +#include ++ ++#ifdef HAVE_MC +#include "xbt/mmalloc/mmprivate.h" ++#endif + +#include "simix/popping_private.h" +#include "simix/smx_private.h" + +#include "mc_forward.h" +#include "mc_mmalloc.h" // std_heap +#include "mc_memory_map.h" +#include "mc_address_space.h" +#include "mc_protocol.h" + +SG_BEGIN_DECL() + +int MC_process_vm_open(pid_t pid, int flags); + +typedef enum { + MC_PROCESS_NO_FLAG = 0, + MC_PROCESS_SELF_FLAG = 1, +} e_mc_process_flags_t; + +// Those flags are used to track down which cached information +// is still up to date and which information needs to be updated. +typedef enum { + MC_PROCESS_CACHE_FLAG_HEAP = 1, + MC_PROCESS_CACHE_FLAG_MALLOC_INFO = 2, + MC_PROCESS_CACHE_FLAG_SIMIX_PROCESSES = 4, +} e_mc_process_cache_flags_t ; + +typedef struct s_mc_smx_process_info s_mc_smx_process_info_t, *mc_smx_process_info_t; + +/** Representation of a process + */ +struct s_mc_process { + s_mc_address_space_t address_space; + e_mc_process_flags_t process_flags; + pid_t pid; + int socket; + int status; + bool running; + memory_map_t memory_map; + void *maestro_stack_start, *maestro_stack_end; + mc_object_info_t libsimgrid_info; + mc_object_info_t binary_info; + mc_object_info_t* object_infos; + size_t object_infos_size; + int memory_file; + + /** Copy of `simix_global->process_list` + * + * See mc_smx.c. + */ + xbt_dynar_t smx_process_infos; + + /** Copy of `simix_global->process_to_destroy` + * + * See mc_smx.c. + */ + xbt_dynar_t smx_old_process_infos; + + /** State of the cache (which variables are up to date) */ + e_mc_process_cache_flags_t cache_flags; + + /** Address of the heap structure in the MCed process. */ + void* heap_address; + + /** Copy of the heap structure of the process + * + * This is refreshed with the `MC_process_refresh` call. + * This is not used if the process is the current one: + * use `MC_process_get_heap_info` in order to use it. + */ + xbt_mheap_t heap; + + /** Copy of the allocation info structure + * + * This is refreshed with the `MC_process_refresh` call. + * This is not used if the process is the current one: + * use `MC_process_get_malloc_info` in order to use it. + */ + malloc_info* heap_info; + + // ***** Libunwind-data + + /** Full-featured MC-aware libunwind address space for the process + * + * This address space is using a mc_unw_context_t + * (with mc_process_t/mc_address_space_t and unw_context_t). + */ + unw_addr_space_t unw_addr_space; + + /** Underlying libunwind addres-space + * + * The `find_proc_info`, `put_unwind_info`, `get_dyn_info_list_addr` + * operations of the native MC address space is currently delegated + * to this address space (either the local or a ptrace unwinder). + */ + unw_addr_space_t unw_underlying_addr_space; + + /** The corresponding context + */ + void* unw_underlying_context; + + xbt_dynar_t checkpoint_ignore; +}; + +bool MC_is_process(mc_address_space_t p); + +void MC_process_init(mc_process_t process, pid_t pid, int sockfd); +void MC_process_clear(mc_process_t process); + +/** Refresh the information about the process + * + * Do not use direclty, this is used by the getters when appropriate + * in order to have fresh data. + */ +void MC_process_refresh_heap(mc_process_t process); + +/** Refresh the information about the process + * + * Do not use direclty, this is used by the getters when appropriate + * in order to have fresh data. + * */ +void MC_process_refresh_malloc_info(mc_process_t process); + +static inline +bool MC_process_is_self(mc_process_t process) +{ + return process->process_flags & MC_PROCESS_SELF_FLAG; +} + +/* Process memory access: */ + +/** Read data from a process memory + * + * @param process the process + * @param local local memory address (destination) + * @param remote target process memory address (source) + * @param len data size + */ +const void* MC_process_read(mc_process_t process, + e_adress_space_read_flags_t flags, + void* local, const void* remote, size_t len, + int process_index); + +// Simplified versions/wrappers (whould be moved in mc_address_space): +const void* MC_process_read_simple(mc_process_t process, + void* local, const void* remote, size_t len); +const void* MC_process_read_dynar_element(mc_process_t process, + void* local, const void* remote_dynar, size_t i, size_t len); +unsigned long MC_process_read_dynar_length(mc_process_t process, const void* remote_dynar); + +/** Write data to a process memory + * + * @param process the process + * @param local local memory address (source) + * @param remote target process memory address (target) + * @param len data size + */ +void MC_process_write(mc_process_t process, const void* local, void* remote, size_t len); + +void MC_process_clear_memory(mc_process_t process, void* remote, size_t len); + +/* Functions, variables of the process: */ + +mc_object_info_t MC_process_find_object_info(mc_process_t process, const void* addr); +mc_object_info_t MC_process_find_object_info_exec(mc_process_t process, const void* addr); +mc_object_info_t MC_process_find_object_info_rw(mc_process_t process, const void* addr); + +dw_frame_t MC_process_find_function(mc_process_t process, const void* ip); + +void MC_process_read_variable(mc_process_t process, const char* name, void* target, size_t size); +char* MC_process_read_string(mc_process_t, void* address); + +static inline xbt_mheap_t MC_process_get_heap(mc_process_t process) +{ + if (MC_process_is_self(process)) + return std_heap; + if (!(process->cache_flags & MC_PROCESS_CACHE_FLAG_HEAP)) + MC_process_refresh_heap(process); + return process->heap; +} + +static inline malloc_info* MC_process_get_malloc_info(mc_process_t process) +{ + if (MC_process_is_self(process)) + return std_heap->heapinfo; + if (!(process->cache_flags & MC_PROCESS_CACHE_FLAG_MALLOC_INFO)) + MC_process_refresh_malloc_info(process); + return process->heap_info; +} + +/** Find (one occurence of) the named variable definition + */ +dw_variable_t MC_process_find_variable_by_name(mc_process_t process, const char* name); + +SG_END_DECL() + +#endif diff --cc teshsuite/mc/replay/random_bug.c index 4b8613c747,fea8c27ac3..fba41c7ef2 --- a/teshsuite/mc/replay/random_bug.c +++ b/teshsuite/mc/replay/random_bug.c @@@ -6,13 -6,9 +6,12 @@@ #include +#include - - #include + #include #include +XBT_LOG_NEW_DEFAULT_CATEGORY(random_bug, "Application"); + /** An (fake) application with a bug occuring for some random values */ static int app(int argc, char *argv[])