#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");
/**
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()) {
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);
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();
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)
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;
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);
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;
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);
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;
// * 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:
int snapshot_compare(void *state1, void *state2)
{
+ mc_process_t process = &mc_model_checker->process;
+
mc_snapshot_t s1, s2;
int num1, num2;
#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) {
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 */
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) {
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;
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;
mc_object_info_t info, const void *address,
dw_type_t type)
{
+ mc_process_t process = &mc_model_checker->process;
top:
switch (type->type) {
&& 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;
&& 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;
}
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;
+}
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);
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);
+#include <assert.h>
#include <stddef.h>
#include <stdbool.h>
#include <stdint.h>
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)
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]*$"
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);
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)
#include <sys/types.h>
+#include <xbt/mmalloc.h>
+#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()
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 {
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)
{
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
}
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);
}
*/
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;
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;
#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);
*/
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;
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');
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');
// 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;
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 */
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;
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);