From d929149dc5f210fc2599db0407351ba27ad3a2ec Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Thu, 11 Dec 2014 13:14:32 +0100 Subject: [PATCH] [mc] Support for reading heap state from another process --- src/mc/mc_base.c | 5 +++ src/mc/mc_checkpoint.c | 22 +++++++---- src/mc/mc_comm_determinism.c | 8 +++- src/mc/mc_compare.cpp | 12 ++++-- src/mc/mc_diff.c | 16 ++++++-- src/mc/mc_hash.c | 9 +++-- src/mc/mc_object_info.c | 12 ++++++ src/mc/mc_object_info.h | 1 + src/mc/mc_page_snapshot.cpp | 2 +- src/mc/mc_process.c | 68 ++++++++++++++++++++++++++++++++ src/mc/mc_process.h | 74 +++++++++++++++++++++++++++++++++++ src/mc/mc_snapshot.h | 6 ++- src/mc/mc_visited.c | 10 ++++- src/simix/popping_generated.c | 7 ++++ src/simix/simcalls.py | 8 +++- src/xbt/mmalloc/mm_module.c | 32 ++++++++------- src/xbt/mmalloc/mmprivate.h | 2 + teshsuite/mc/dwarf/dwarf.c | 13 +----- 18 files changed, 253 insertions(+), 54 deletions(-) diff --git a/src/mc/mc_base.c b/src/mc/mc_base.c index 82ca8c6a4f..34a5bad3c7 100644 --- a/src/mc/mc_base.c +++ b/src/mc/mc_base.c @@ -10,6 +10,11 @@ #include "../simix/smx_private.h" #include "mc_record.h" +#ifdef HAVE_MC +#include "mc_process.h" +#include "mc_model_checker.h" +#endif + XBT_LOG_NEW_CATEGORY(mc, "All MC categories"); /** diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c index 45201cf7af..ccfb513939 100644 --- a/src/mc/mc_checkpoint.c +++ b/src/mc/mc_checkpoint.c @@ -244,26 +244,29 @@ static void MC_snapshot_add_region(int index, mc_snapshot_t snapshot, mc_region_ return; } -static void MC_get_memory_regions(mc_snapshot_t snapshot) +static void MC_get_memory_regions(mc_process_t process, mc_snapshot_t snapshot) { - const mc_process_t process = &mc_model_checker->process; const size_t n = process->object_infos_size; snapshot->snapshot_regions_count = n + 1; snapshot->snapshot_regions = xbt_new0(mc_mem_region_t, n + 1); for (size_t i = 0; i!=n; ++i) { - mc_object_info_t object_info = mc_model_checker->process.object_infos[i]; + mc_object_info_t object_info = process->object_infos[i]; MC_snapshot_add_region(i, snapshot, MC_REGION_TYPE_DATA, object_info, object_info->start_rw, object_info->start_rw, object_info->end_rw - object_info->start_rw); } - void *start_heap = std_heap->base; - void *end_heap = std_heap->breakval; + xbt_mheap_t heap = MC_process_get_heap(process); + void *start_heap = heap->base; + void *end_heap = heap->breakval; + MC_snapshot_add_region(n, snapshot, MC_REGION_TYPE_HEAP, NULL, start_heap, start_heap, (char *) end_heap - (char *) start_heap); - snapshot->heap_bytes_used = mmalloc_get_bytes_used(std_heap); + snapshot->heap_bytes_used = mmalloc_get_bytes_used_remote( + heap->heaplimit, + MC_process_get_malloc_info(process)); #ifdef HAVE_SMPI if (smpi_privatize_global_variables && smpi_process_count()) { @@ -679,6 +682,7 @@ static void MC_get_current_fd(mc_snapshot_t snapshot){ mc_snapshot_t MC_take_snapshot(int num_state) { + mc_process_t mc_process = &mc_model_checker->process; mc_snapshot_t snapshot = xbt_new0(s_mc_snapshot_t, 1); snapshot->enabled_processes = xbt_dynar_new(sizeof(int), NULL); @@ -693,10 +697,10 @@ mc_snapshot_t MC_take_snapshot(int num_state) const bool use_soft_dirty = _sg_mc_sparse_checkpoint && _sg_mc_soft_dirty - && MC_process_is_self(&mc_model_checker->process); + && MC_process_is_self(mc_process); /* Save the std heap and the writable mapped pages of libsimgrid and binary */ - MC_get_memory_regions(snapshot); + MC_get_memory_regions(mc_process, snapshot); if (use_soft_dirty) mc_softdirty_reset(); @@ -782,6 +786,8 @@ void MC_restore_snapshot(mc_snapshot_t snapshot) if (use_soft_dirty) { mc_model_checker->parent_snapshot = snapshot; } + + mc_model_checker->process.cache_flags = 0; } mc_snapshot_t simcall_HANDLER_mc_snapshot(smx_simcall_t simcall) diff --git a/src/mc/mc_comm_determinism.c b/src/mc/mc_comm_determinism.c index 9c01b85e0e..c96db7068b 100644 --- a/src/mc/mc_comm_determinism.c +++ b/src/mc/mc_comm_determinism.c @@ -153,6 +153,7 @@ static void print_communications_pattern(xbt_dynar_t comms_pattern) static void update_comm_pattern(mc_comm_pattern_t comm_pattern, smx_synchro_t comm) { + mc_process_t process = &mc_model_checker->process; void *addr_pointed; comm_pattern->src_proc = comm->comm.src_proc->pid; comm_pattern->dst_proc = comm->comm.dst_proc->pid; @@ -164,7 +165,8 @@ static void update_comm_pattern(mc_comm_pattern_t comm_pattern, smx_synchro_t co comm_pattern->data_size = *(comm->comm.dst_buff_size); comm_pattern->data = xbt_malloc0(comm_pattern->data_size); addr_pointed = *(void **) comm->comm.src_buff; - if (addr_pointed > (void*) std_heap && addr_pointed < std_heap->breakval) + if (addr_pointed > (void*) process->heap_address + && addr_pointed < MC_process_get_heap(process)->breakval) memcpy(comm_pattern->data, addr_pointed, comm_pattern->data_size); else memcpy(comm_pattern->data, comm->comm.src_buff, comm_pattern->data_size); @@ -175,6 +177,7 @@ static void update_comm_pattern(mc_comm_pattern_t comm_pattern, smx_synchro_t co void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, mc_call_type call_type) { + mc_process_t process = &mc_model_checker->process; mc_comm_pattern_t pattern = NULL; pattern = xbt_new0(s_mc_comm_pattern_t, 1); pattern->num = ++nb_comm_pattern; @@ -188,7 +191,8 @@ void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, mc_call_type call pattern->data_size = pattern->comm->comm.src_buff_size; pattern->data = xbt_malloc0(pattern->data_size); addr_pointed = *(void **) pattern->comm->comm.src_buff; - if (addr_pointed > (void*) std_heap && addr_pointed < std_heap->breakval) + if (addr_pointed > (void*) process->heap_address + && addr_pointed < MC_process_get_heap(process)->breakval) memcpy(pattern->data, addr_pointed, pattern->data_size); else memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size); diff --git a/src/mc/mc_compare.cpp b/src/mc/mc_compare.cpp index ca13c3e002..2f7ce7ead0 100644 --- a/src/mc/mc_compare.cpp +++ b/src/mc/mc_compare.cpp @@ -102,6 +102,8 @@ static int compare_areas_with_type(struct mc_compare_state& state, void* real_area2, mc_snapshot_t snapshot2, mc_mem_region_t region2, dw_type_t type, int pointer_level) { + mc_process_t process = &mc_model_checker->process; + unsigned int cursor = 0; dw_type_t member, subtype, subsubtype; int elm_size, i, res; @@ -190,10 +192,10 @@ static int compare_areas_with_type(struct mc_compare_state& state, // * a pointer leads to the read-only segment of the current object; // * a pointer lead to a different ELF object. - if (addr_pointed1 > std_heap + if (addr_pointed1 > process->heap_address && addr_pointed1 < mc_snapshot_get_heap_end(snapshot1)) { if (! - (addr_pointed2 > std_heap + (addr_pointed2 > process->heap_address && addr_pointed2 < mc_snapshot_get_heap_end(snapshot2))) return 1; // The pointers are both in the heap: @@ -383,6 +385,8 @@ static int compare_local_variables(int process_index, int snapshot_compare(void *state1, void *state2) { + mc_process_t process = &mc_model_checker->process; + mc_snapshot_t s1, s2; int num1, num2; @@ -481,9 +485,9 @@ int snapshot_compare(void *state1, void *state2) #endif /* Init heap information used in heap comparison algorithm */ - xbt_mheap_t heap1 = (xbt_mheap_t) mc_snapshot_read(std_heap, s1, MC_NO_PROCESS_INDEX, + xbt_mheap_t heap1 = (xbt_mheap_t) mc_snapshot_read(process->heap_address, s1, MC_NO_PROCESS_INDEX, alloca(sizeof(struct mdesc)), sizeof(struct mdesc)); - xbt_mheap_t heap2 = (xbt_mheap_t) mc_snapshot_read(std_heap, s2, MC_NO_PROCESS_INDEX, + xbt_mheap_t heap2 = (xbt_mheap_t) mc_snapshot_read(process->heap_address, s2, MC_NO_PROCESS_INDEX, alloca(sizeof(struct mdesc)), sizeof(struct mdesc)); res_init = init_heap_information(heap1, heap2, s1->to_ignore, s2->to_ignore); if (res_init == -1) { diff --git a/src/mc/mc_diff.c b/src/mc/mc_diff.c index 089a9b2cd0..4adf44bb1d 100644 --- a/src/mc/mc_diff.c +++ b/src/mc/mc_diff.c @@ -430,6 +430,7 @@ mc_mem_region_t MC_get_heap_region(mc_snapshot_t snapshot) int mmalloc_compare_heap(mc_snapshot_t snapshot1, mc_snapshot_t snapshot2) { + mc_process_t process = &mc_model_checker->process; struct s_mc_diff *state = mc_diff_info; /* Start comparison */ @@ -449,9 +450,12 @@ int mmalloc_compare_heap(mc_snapshot_t snapshot1, mc_snapshot_t snapshot2) mc_mem_region_t heap_region1 = MC_get_heap_region(snapshot1); mc_mem_region_t heap_region2 = MC_get_heap_region(snapshot2); + // This is the address of std_heap->heapinfo in the application process: + void* heapinfo_address = &((xbt_mheap_t) process->heap_address)->heapinfo; + // This is in snapshot do not use them directly: - malloc_info* heapinfos1 = mc_snapshot_read_pointer(&std_heap->heapinfo, snapshot1, MC_NO_PROCESS_INDEX); - malloc_info* heapinfos2 = mc_snapshot_read_pointer(&std_heap->heapinfo, snapshot2, MC_NO_PROCESS_INDEX); + malloc_info* heapinfos1 = mc_snapshot_read_pointer(heapinfo_address, snapshot1, MC_NO_PROCESS_INDEX); + malloc_info* heapinfos2 = mc_snapshot_read_pointer(heapinfo_address, snapshot2, MC_NO_PROCESS_INDEX); while (i1 <= state->heaplimit) { @@ -1135,6 +1139,7 @@ int compare_heap_area(int process_index, void *area1, void *area2, mc_snapshot_t mc_snapshot_t snapshot2, xbt_dynar_t previous, dw_type_t type, int pointer_level) { + mc_process_t process = &mc_model_checker->process; struct s_mc_diff *state = mc_diff_info; @@ -1151,8 +1156,11 @@ int compare_heap_area(int process_index, void *area1, void *area2, mc_snapshot_t int match_pairs = 0; - malloc_info* heapinfos1 = mc_snapshot_read_pointer(&std_heap->heapinfo, snapshot1, process_index); - malloc_info* heapinfos2 = mc_snapshot_read_pointer(&std_heap->heapinfo, snapshot2, process_index); + // This is the address of std_heap->heapinfo in the application process: + void* heapinfo_address = &((xbt_mheap_t) process->heap_address)->heapinfo; + + malloc_info* heapinfos1 = mc_snapshot_read_pointer(heapinfo_address, snapshot1, process_index); + malloc_info* heapinfos2 = mc_snapshot_read_pointer(heapinfo_address, snapshot2, process_index); malloc_info heapinfo_temp1, heapinfo_temp2; diff --git a/src/mc/mc_hash.c b/src/mc/mc_hash.c index 0a194dadc2..b83bc83be8 100644 --- a/src/mc/mc_hash.c +++ b/src/mc/mc_hash.c @@ -81,6 +81,7 @@ static void mc_hash_value(mc_hash_t * hash, mc_hashing_state * state, mc_object_info_t info, const void *address, dw_type_t type) { + mc_process_t process = &mc_model_checker->process; top: switch (type->type) { @@ -175,8 +176,8 @@ top: && pointed <= (void *) binary_info->end_rw) || (pointed >= (void *) libsimgrid_info->start_rw && pointed <= (void *) libsimgrid_info->end_rw) - || (pointed >= std_heap - && pointed < (void *) ((const char *) std_heap + STD_HEAP_SIZE)); + || (pointed >= process->heap_address + && pointed < (void *) ((const char *) process->heap_address + STD_HEAP_SIZE)); if (!valid_pointer) { XBT_DEBUG("Hashed pointed data %p is in an ignored range", pointed); return; @@ -224,8 +225,8 @@ static void mc_hash_object_globals(mc_hash_t * hash, mc_hashing_state * state, && address <= binary_info->end_rw) || (address >= libsimgrid_info->start_rw && address <= libsimgrid_info->end_rw) - || (address >= (const char *) std_heap - && address < (const char *) std_heap + STD_HEAP_SIZE); + || (address >= (const char *) process->heap_address + && address < (const char *) process->heap_address + STD_HEAP_SIZE); if (!valid_pointer) continue; diff --git a/src/mc/mc_object_info.c b/src/mc/mc_object_info.c index 35789e5ff7..d89471bf2d 100644 --- a/src/mc/mc_object_info.c +++ b/src/mc/mc_object_info.c @@ -24,3 +24,15 @@ dw_frame_t MC_file_object_info_find_function(mc_object_info_t info, void *ip) } return NULL; } + +dw_variable_t MC_file_object_info_find_variable_by_name(mc_object_info_t info, const char* name) +{ + unsigned int cursor = 0; + dw_variable_t variable; + xbt_dynar_foreach(info->global_variables, cursor, variable){ + if(!strcmp(name, variable->name)) + return variable; + } + + return NULL; +} diff --git a/src/mc/mc_object_info.h b/src/mc/mc_object_info.h index ea7775336a..cd46859375 100644 --- a/src/mc/mc_object_info.h +++ b/src/mc/mc_object_info.h @@ -100,6 +100,7 @@ mc_object_info_t MC_find_object_info(memory_map_t maps, const char* name, int ex void MC_free_object_info(mc_object_info_t* p); dw_frame_t MC_file_object_info_find_function(mc_object_info_t info, void *ip); +dw_variable_t MC_file_object_info_find_variable_by_name(mc_object_info_t info, const char* name); void MC_post_process_object_info(mc_process_t process, mc_object_info_t info); diff --git a/src/mc/mc_page_snapshot.cpp b/src/mc/mc_page_snapshot.cpp index 79caa3af30..aec83aa0f2 100644 --- a/src/mc/mc_page_snapshot.cpp +++ b/src/mc/mc_page_snapshot.cpp @@ -31,7 +31,7 @@ size_t* mc_take_page_snapshot_region(mc_process_t process, void* temp = NULL; if (!is_self) - temp = malloc(xbt_pagebits); + temp = malloc(xbt_pagesize); for (size_t i=0; i!=page_count; ++i) { bool softclean = pagemap && !(pagemap[i] & SOFT_DIRTY); diff --git a/src/mc/mc_process.c b/src/mc/mc_process.c index d7710399e0..ada619562e 100644 --- a/src/mc/mc_process.c +++ b/src/mc/mc_process.c @@ -1,3 +1,4 @@ +#include #include #include #include @@ -29,8 +30,20 @@ void MC_process_init(mc_process_t process, pid_t pid) process->process_flags |= MC_PROCESS_SELF_FLAG; process->memory_map = MC_get_memory_map(pid); process->memory_file = -1; + process->cache_flags = 0; + process->heap = NULL; + process->heap_info = NULL; MC_process_init_memory_map_info(process); MC_process_open_memory_file(process); + + // Read std_heap (is a struct mdesc*): + dw_variable_t std_heap_var = MC_process_find_variable_by_name(process, "std_heap"); + if (!std_heap_var) + xbt_die("No heap information in the target process"); + if(!std_heap_var->address) + xbt_die("No constant address for this variable"); + MC_process_read(process, &process->heap_address, + std_heap_var->address, sizeof(struct mdesc*)); } void MC_process_clear(mc_process_t process) @@ -54,6 +67,46 @@ void MC_process_clear(mc_process_t process) if (process->memory_file >= 0) { close(process->memory_file); } + + process->cache_flags = 0; + + free(process->heap); + process->heap = NULL; + + free(process->heap_info); + process->heap_info = NULL; +} + +void MC_process_refresh_heap(mc_process_t process) +{ + assert(!MC_process_is_self(process)); + // Read/dereference/refresh the std_heap pointer: + if (!process->heap) { + xbt_mheap_t oldheap = mmalloc_get_current_heap(); + MC_SET_MC_HEAP; + process->heap = malloc(sizeof(struct mdesc)); + mmalloc_set_current_heap(oldheap); + } + MC_process_read(process, process->heap, + process->heap_address, sizeof(struct mdesc)); +} + +void MC_process_refresh_malloc_info(mc_process_t process) +{ + assert(!MC_process_is_self(process)); + if (!process->cache_flags & MC_PROCESS_CACHE_FLAG_HEAP) + MC_process_refresh_heap(process); + // Refresh process->heapinfo: + size_t malloc_info_bytesize = process->heap->heaplimit * sizeof(malloc_info); + + xbt_mheap_t oldheap = mmalloc_get_current_heap(); + MC_SET_MC_HEAP; + process->heap_info = (malloc_info*) realloc(process->heap_info, + malloc_info_bytesize); + mmalloc_set_current_heap(oldheap); + + MC_process_read(process, process->heap_info, + process->heap->heapinfo, malloc_info_bytesize); } #define SO_RE "\\.so[\\.0-9]*$" @@ -217,6 +270,8 @@ mc_object_info_t MC_process_find_object_info(mc_process_t process, void *ip) return NULL; } +// Functions, variables… + dw_frame_t MC_process_find_function(mc_process_t process, void *ip) { mc_object_info_t info = MC_process_find_object_info(process, ip); @@ -226,6 +281,19 @@ dw_frame_t MC_process_find_function(mc_process_t process, void *ip) return MC_file_object_info_find_function(info, ip); } +dw_variable_t MC_process_find_variable_by_name(mc_process_t process, const char* name) +{ + const size_t n = process->object_infos_size; + size_t i; + for (i=0; i!=n; ++i) { + mc_object_info_t info =process->object_infos[i]; + dw_variable_t var = MC_file_object_info_find_variable_by_name(info, name); + if (var) + return var; + } + return NULL; +} + // ***** Memory access static void MC_process_open_memory_file(mc_process_t process) diff --git a/src/mc/mc_process.h b/src/mc/mc_process.h index c8cd39e404..4513fe280d 100644 --- a/src/mc/mc_process.h +++ b/src/mc/mc_process.h @@ -13,7 +13,13 @@ #include +#include +#include "xbt/mmalloc/mmprivate.h" + +#include "simix/popping_private.h" + #include "mc_forward.h" +#include "mc_mmalloc.h" // std_heap #include "mc_memory_map.h" SG_BEGIN_DECL() @@ -23,6 +29,13 @@ typedef enum { 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, +} e_mc_process_cache_flags_t ; + /** Representation of a process */ struct s_mc_process { @@ -35,11 +48,50 @@ struct s_mc_process { mc_object_info_t* object_infos; size_t object_infos_size; int memory_file; + + // Cache: don't use those fields directly but with the getters + // which ensure that proper synchronisation has been done. + + e_mc_process_cache_flags_t cache_flags; + + /** Address of the heap structure in the target 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; }; void MC_process_init(mc_process_t process, pid_t pid); 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) { @@ -71,6 +123,28 @@ void MC_process_write(mc_process_t process, const void* local, void* remote, siz mc_object_info_t MC_process_find_object_info(mc_process_t process, void* ip); dw_frame_t MC_process_find_function(mc_process_t process, void* ip); +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 --git a/src/mc/mc_snapshot.h b/src/mc/mc_snapshot.h index ca274972a1..e6e0255b4b 100644 --- a/src/mc/mc_snapshot.h +++ b/src/mc/mc_snapshot.h @@ -303,10 +303,12 @@ void* mc_snapshot_read_pointer(void* addr, mc_snapshot_t snapshot, int process_i } static inline __attribute__ ((always_inline)) - void* mc_snapshot_get_heap_end(mc_snapshot_t snapshot) { +void* mc_snapshot_get_heap_end(mc_snapshot_t snapshot) { if(snapshot==NULL) xbt_die("snapshot is NULL"); - void** addr = &(std_heap->breakval); + // This is &std_heap->breakval in the target process: + void** addr = &MC_process_get_heap(&mc_model_checker->process)->breakval; + // Read (std_heap->breakval) in the target process (*addr i.e. std_heap->breakval): return mc_snapshot_read_pointer(addr, snapshot, MC_ANY_PROCESS_INDEX); } diff --git a/src/mc/mc_visited.c b/src/mc/mc_visited.c index 8ac5d0fa73..95fcc37052 100644 --- a/src/mc/mc_visited.c +++ b/src/mc/mc_visited.c @@ -37,9 +37,12 @@ void visited_state_free_voidp(void *s) */ static mc_visited_state_t visited_state_new() { + mc_process_t process = &(mc_model_checker->process); mc_visited_state_t new_state = NULL; new_state = xbt_new0(s_mc_visited_state_t, 1); - new_state->heap_bytes_used = mmalloc_get_bytes_used(std_heap); + new_state->heap_bytes_used = mmalloc_get_bytes_used_remote( + MC_process_get_heap(process)->heaplimit, + MC_process_get_malloc_info(process)); new_state->nb_processes = xbt_swag_size(simix_global->process_list); new_state->system_state = MC_take_snapshot(mc_stats->expanded_states); new_state->num = mc_stats->expanded_states; @@ -52,11 +55,14 @@ mc_visited_pair_t MC_visited_pair_new(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions) { + mc_process_t process = &(mc_model_checker->process); mc_visited_pair_t pair = NULL; pair = xbt_new0(s_mc_visited_pair_t, 1); pair->graph_state = MC_state_new(); pair->graph_state->system_state = MC_take_snapshot(pair_num); - pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap); + pair->heap_bytes_used = mmalloc_get_bytes_used_remote( + MC_process_get_heap(process)->heaplimit, + MC_process_get_malloc_info(process)); pair->nb_processes = xbt_swag_size(simix_global->process_list); pair->automaton_state = automaton_state; pair->num = pair_num; diff --git a/src/simix/popping_generated.c b/src/simix/popping_generated.c index b339a4a1a0..69806ac5df 100644 --- a/src/simix/popping_generated.c +++ b/src/simix/popping_generated.c @@ -15,6 +15,8 @@ #include "smx_private.h" #ifdef HAVE_MC +#include "mc/mc_process.h" +#include "mc/mc_model_checker.h" #endif XBT_LOG_EXTERNAL_DEFAULT_CATEGORY(simix_popping); @@ -162,6 +164,11 @@ const char* simcall_names[] = { */ void SIMIX_simcall_handle(smx_simcall_t simcall, int value) { XBT_DEBUG("Handling simcall %p: %s", simcall, SIMIX_simcall_name(simcall->call)); + #ifdef HAVE_MC + if (mc_model_checker) { + mc_model_checker->process.cache_flags = 0; + } + #endif SIMCALL_SET_MC_VALUE(simcall, value); if (simcall->issuer->context->iwannadie && simcall->call != SIMCALL_PROCESS_CLEANUP) return; diff --git a/src/simix/simcalls.py b/src/simix/simcalls.py index 41bd69d13a..321a63bf9d 100755 --- a/src/simix/simcalls.py +++ b/src/simix/simcalls.py @@ -281,7 +281,8 @@ if __name__=='__main__': fd.write('#include "smx_private.h"\n'); fd.write('#ifdef HAVE_MC\n'); - # fd.write('#include "mc/mc_private.h"\n'); + fd.write('#include "mc/mc_process.h"\n'); + fd.write('#include "mc/mc_model_checker.h"\n'); fd.write('#endif\n'); fd.write('\n'); fd.write('XBT_LOG_EXTERNAL_DEFAULT_CATEGORY(simix_popping);\n\n'); @@ -302,6 +303,11 @@ if __name__=='__main__': fd.write(' */\n'); fd.write('void SIMIX_simcall_handle(smx_simcall_t simcall, int value) {\n'); fd.write(' XBT_DEBUG("Handling simcall %p: %s", simcall, SIMIX_simcall_name(simcall->call));\n'); + fd.write(' #ifdef HAVE_MC\n'); + fd.write(' if (mc_model_checker) {\n'); + fd.write(' mc_model_checker->process.cache_flags = 0;\n'); + fd.write(' }\n'); + fd.write(' #endif\n'); fd.write(' SIMCALL_SET_MC_VALUE(simcall, value);\n'); fd.write(' if (simcall->issuer->context->iwannadie && simcall->call != SIMCALL_PROCESS_CLEANUP)\n'); fd.write(' return;\n'); diff --git a/src/xbt/mmalloc/mm_module.c b/src/xbt/mmalloc/mm_module.c index d553f4af67..8490906407 100644 --- a/src/xbt/mmalloc/mm_module.c +++ b/src/xbt/mmalloc/mm_module.c @@ -353,27 +353,31 @@ void mmalloc_postexit(void) // xbt_mheap_destroy_no_free(__mmalloc_default_mdp); } -size_t mmalloc_get_bytes_used(xbt_mheap_t heap){ - int i = 0, j = 0; +// This is the underlying implementation of mmalloc_get_bytes_used_remote. +// Is it used directly in order to evaluate the bytes used from a different +// process. +size_t mmalloc_get_bytes_used_remote(size_t heaplimit, const malloc_info* heapinfo) +{ int bytes = 0; - - while(i<=((struct mdesc *)heap)->heaplimit){ - if(((struct mdesc *)heap)->heapinfo[i].type == MMALLOC_TYPE_UNFRAGMENTED){ - if(((struct mdesc *)heap)->heapinfo[i].busy_block.busy_size > 0) - bytes += ((struct mdesc *)heap)->heapinfo[i].busy_block.busy_size; - - } else if(((struct mdesc *)heap)->heapinfo[i].type > 0){ - for(j=0; j < (size_t) (BLOCKSIZE >> ((struct mdesc *)heap)->heapinfo[i].type); j++){ - if(((struct mdesc *)heap)->heapinfo[i].busy_frag.frag_size[j] > 0) - bytes += ((struct mdesc *)heap)->heapinfo[i].busy_frag.frag_size[j]; + for (size_t i=0; i<=heaplimit; ++i){ + if (heapinfo[i].type == MMALLOC_TYPE_UNFRAGMENTED){ + if (heapinfo[i].busy_block.busy_size > 0) + bytes += heapinfo[i].busy_block.busy_size; + } else if (heapinfo[i].type > 0) { + for (size_t j=0; j < (size_t) (BLOCKSIZE >> heapinfo[i].type); j++){ + if(heapinfo[i].busy_frag.frag_size[j] > 0) + bytes += heapinfo[i].busy_frag.frag_size[j]; } } - i++; } - return bytes; } +size_t mmalloc_get_bytes_used(const xbt_mheap_t heap){ + const struct mdesc* heap_data = (const struct mdesc *) heap; + return mmalloc_get_bytes_used_remote(heap_data->heaplimit, heap_data->heapinfo); +} + ssize_t mmalloc_get_busy_size(xbt_mheap_t heap, void *ptr){ ssize_t block = ((char*)ptr - (char*)(heap->heapbase)) / BLOCKSIZE + 1; diff --git a/src/xbt/mmalloc/mmprivate.h b/src/xbt/mmalloc/mmprivate.h index 0ed914ad3e..67c5bba166 100644 --- a/src/xbt/mmalloc/mmprivate.h +++ b/src/xbt/mmalloc/mmprivate.h @@ -324,4 +324,6 @@ void mmcheck(xbt_mheap_t heap); int mmalloc_exec_using_mm(int argc, const char** argv); void mmalloc_ensure_using_mm(int argc, const char** argv); +size_t mmalloc_get_bytes_used_remote(size_t heaplimit, const malloc_info* heapinfo); + #endif /* __MMPRIVATE_H */ diff --git a/teshsuite/mc/dwarf/dwarf.c b/teshsuite/mc/dwarf/dwarf.c index 5c84dfe524..e6a5dd684f 100644 --- a/teshsuite/mc/dwarf/dwarf.c +++ b/teshsuite/mc/dwarf/dwarf.c @@ -34,17 +34,6 @@ static dw_type_t find_type_by_name(mc_object_info_t info, const char* name) { return NULL; } -static dw_variable_t find_global_variable_by_name(mc_object_info_t info, const char* name) { - unsigned int cursor = 0; - dw_variable_t variable; - xbt_dynar_foreach(info->global_variables, cursor, variable){ - if(!strcmp(name, variable->name)) - return variable; - } - - return NULL; -} - static dw_frame_t find_function_by_name(mc_object_info_t info, const char* name) { xbt_dict_cursor_t cursor = 0; dw_frame_t subprogram; @@ -100,7 +89,7 @@ static void test_local_variable(mc_object_info_t info, const char* function, con static dw_variable_t test_global_variable(mc_object_info_t info, const char* name, void* address, long byte_size) { mc_process_t process = &mc_model_checker->process; - dw_variable_t variable = find_global_variable_by_name(info, name); + dw_variable_t variable = MC_file_object_info_find_variable_by_name(info, name); xbt_assert(variable, "Global variable %s was not found", name); xbt_assert(!strcmp(variable->name, name), "Name mismatch for %s", name); xbt_assert(variable->global, "Variable %s is not global", name); -- 2.20.1