[mc] Support for reading heap state from another process

diff --git a/src/mc/mc_base.c b/src/mc/mc_base.c
index 82ca8c6..34a5bad 100644 (file)
--- 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"
 
 #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");
 
 /**
 XBT_LOG_NEW_CATEGORY(mc, "All MC categories");
 
 /**

diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c
index 45201cf..ccfb513 100644 (file)
--- 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;
 }
 
   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) {
   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);
   }
 
     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);
   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()) {
 
 #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_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);
   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
 
   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 */
 
   /* 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_softdirty_reset();
 


@@ -782,6 +786,8 @@ void MC_restore_snapshot(mc_snapshot_t snapshot)
   if (use_soft_dirty) {
     mc_model_checker->parent_snapshot = 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)
 }
 
 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 9c01b85..c96db70 100644 (file)
--- 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)
 {
 
 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;
   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;
     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);
       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)
 {
 
 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;
   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;
     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);
       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 ca13c3e..2f7ce7e 100644 (file)
--- 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)
 {
                                    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;
   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.
 
       // * 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_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:
              && 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)
 {
 
 int snapshot_compare(void *state1, void *state2)
 {

+  mc_process_t process = &mc_model_checker->process;
+

   mc_snapshot_t s1, s2;
   int num1, num2;
 
   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 */
 #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));
     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) {
     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 089a9b2..4adf44b 100644 (file)
--- 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)
 {
 
 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 */
   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);
 
   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:
   // 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) {
 
 
   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_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;
 
 
   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;
 
 
   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;
 
 
   malloc_info heapinfo_temp1, heapinfo_temp2;
 

diff --git a/src/mc/mc_hash.c b/src/mc/mc_hash.c
index 0a194da..b83bc83 100644 (file)
--- 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_object_info_t info, const void *address,
                           dw_type_t type)
 {

+  mc_process_t process = &mc_model_checker->process;

 top:
 
   switch (type->type) {
 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 <= (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;
       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 <= 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;
 
     if (!valid_pointer)
       continue;
 

diff --git a/src/mc/mc_object_info.c b/src/mc/mc_object_info.c
index 35789e5..d89471b 100644 (file)
--- 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;
 }
   }
   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 ea77753..cd46859 100644 (file)
--- 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);
 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 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 79caa3a..aec83aa 100644 (file)
--- 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)
 
   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);
 
   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 d771039..ada6195 100644 (file)
--- a/src/mc/mc_process.c
+++ b/src/mc/mc_process.c
@@ -1,3 +1,4 @@
+#include <assert.h>

 #include <stddef.h>
 #include <stdbool.h>
 #include <stdint.h>
 #include <stddef.h>
 #include <stdbool.h>
 #include <stdint.h>


@@ -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->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);
   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)
 }
 
 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);
   }
   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]*$"
 }
 
 #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;
 }
 
   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);
 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);
 }
 
     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)
 // ***** 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 c8cd39e..4513fe2 100644 (file)
--- a/src/mc/mc_process.h
+++ b/src/mc/mc_process.h
@@ -13,7 +13,13 @@
 
 #include <sys/types.h>
 
 
 #include <sys/types.h>
 

+#include <xbt/mmalloc.h>
+#include "xbt/mmalloc/mmprivate.h"
+
+#include "simix/popping_private.h"
+

 #include "mc_forward.h"
 #include "mc_forward.h"

+#include "mc_mmalloc.h" // std_heap

 #include "mc_memory_map.h"
 
 SG_BEGIN_DECL()
 #include "mc_memory_map.h"
 
 SG_BEGIN_DECL()


@@ -23,6 +29,13 @@ typedef enum {
   MC_PROCESS_SELF_FLAG = 1,
 } e_mc_process_flags_t;
 
   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 {
 /** 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;
   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);
 
 };
 
 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)
 {
 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);
 
 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
 SG_END_DECL()
 
 #endif

diff --git a/src/mc/mc_snapshot.h b/src/mc/mc_snapshot.h
index ca27497..e6e0255 100644 (file)
--- 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))
 }
 
 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");
   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);
 }
 
   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 8ac5d0f..95fcc37 100644 (file)
--- 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()
 {
  */
 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);
   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;
   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)
 {
                                       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);
   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;
   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 b339a4a..69806ac 100644 (file)
--- a/src/simix/popping_generated.c
+++ b/src/simix/popping_generated.c
@@ -15,6 +15,8 @@
 
 #include "smx_private.h"
 #ifdef HAVE_MC
 
 #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);
 #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));
  */
 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;
   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 41bd69d..321a63b 100755 (executable)
--- 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 "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('#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(' */\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');
   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 d553f4a..8490906 100644 (file)
--- 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);
 }
 
   // 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;
   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;
 }
 
   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;
 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 0ed914a..67c5bba 100644 (file)
--- 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);
 
 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 */
 #endif                          /* __MMPRIVATE_H */

diff --git a/teshsuite/mc/dwarf/dwarf.c b/teshsuite/mc/dwarf/dwarf.c
index 5c84dfe..e6a5dd6 100644 (file)
--- 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;
 }
 
   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_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;
   
 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);
   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);