model-checker : ignore stack areas in heap comparison algorithm for the comparison...

diff --git a/include/xbt/mmalloc.h b/include/xbt/mmalloc.h
index f7a279e..aa6eeaa 100644 (file)
--- a/include/xbt/mmalloc.h
+++ b/include/xbt/mmalloc.h
@@ -18,6 +18,8 @@
 #  include <stdio.h>            /* for NULL */
 #endif
 
+#include "xbt/dynar.h"
+
 /* Datatype representing a separate heap. The whole point of the mmalloc module
  * is to allow several such heaps in the process. It thus works by redefining
  * all the classical memory management functions (malloc and friends) with an
@@ -56,7 +58,7 @@ extern xbt_mheap_t mmalloc_get_default_md(void);
 void mmalloc_set_current_heap(xbt_mheap_t new_heap);
 xbt_mheap_t mmalloc_get_current_heap(void);
 
-int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2);
+int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2, xbt_dynar_t *stacks1, xbt_dynar_t *stacks2);
 int mmalloc_linear_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2);
 
 void mmalloc_backtrace_block_display(void* heapinfo, int block);

diff --git a/src/include/mc/datatypes.h b/src/include/mc/datatypes.h
index da5a3ca..dba1759 100644 (file)
--- a/src/include/mc/datatypes.h
+++ b/src/include/mc/datatypes.h
@@ -21,5 +21,10 @@ typedef struct s_mc_ignore_region{
   size_t size;
 }s_mc_ignore_region_t, *mc_ignore_region_t;
 
+typedef struct s_stack_region{
+  void *address;
+  char *process_name;
+}s_stack_region_t, *stack_region_t;
+
 SG_END_DECL()
 #endif                          /* _MC_MC_H */

diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h
index cbc7ce3..7a7956f 100644 (file)
--- a/src/include/mc/mc.h
+++ b/src/include/mc/mc.h
@@ -23,6 +23,7 @@ SG_BEGIN_DECL()
 extern char*_surf_mc_property_file; /* fixme: better location? */
 
 extern xbt_dynar_t mmalloc_ignore;
+extern xbt_dynar_t stacks_areas;
 
 /********************************* Global *************************************/
 void _mc_cfg_cb_reduce(const char *name, int pos);
@@ -42,6 +43,7 @@ void MC_automaton_load(const char *file);
 
 void MC_ignore_init(void);
 XBT_PUBLIC(void) MC_ignore(void *address, size_t size);
+void MC_new_stack_area(void *stack, char *name);
 
 /********************************* Memory *************************************/
 XBT_PUBLIC(void) MC_memory_init(void);  /* Initialize the memory subsystem */

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 9f46c20..ccc32ef 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -76,6 +76,7 @@ int compare;
 xbt_dynar_t mc_binary_local_variables = NULL;
 
 extern xbt_dynar_t mmalloc_ignore;
+extern xbt_dynar_t stacks_areas;
 
 xbt_automaton_t _mc_property_automaton = NULL;
 
@@ -651,6 +652,7 @@ void MC_automaton_new_propositional_symbol(const char* id, void* fct) {
 void MC_ignore_init(){
   MC_SET_RAW_MEM;
   mmalloc_ignore = xbt_dynar_new(sizeof(mc_ignore_region_t), NULL);
+  stacks_areas = xbt_dynar_new(sizeof(stack_region_t), NULL);
   MC_UNSET_RAW_MEM;
 }
 
@@ -682,6 +684,16 @@ void MC_ignore(void *address, size_t size){
   MC_UNSET_RAW_MEM;
 }
 
+void MC_new_stack_area(void *stack, char *name){
+  MC_SET_RAW_MEM;
+  stack_region_t region = NULL;
+  region = xbt_new0(s_stack_region_t, 1);
+  region->address = stack;
+  region->process_name = strdup(name);
+  xbt_dynar_push(stacks_areas, &region);
+  MC_UNSET_RAW_MEM;
+}
+
 /************ DWARF ***********/
 
 static e_dw_location_type get_location(char *expr, dw_location_t entry);

diff --git a/src/simix/smx_context_base.c b/src/simix/smx_context_base.c
index 8fd10e4..c934a08 100644 (file)
--- a/src/simix/smx_context_base.c
+++ b/src/simix/smx_context_base.c
@@ -10,6 +10,7 @@
 #include "xbt/function_types.h"
 #include "simgrid/simix.h"
 #include "smx_private.h"
+#include "mc/mc.h"
 
 XBT_LOG_EXTERNAL_DEFAULT_CATEGORY(bindings);
 
@@ -46,6 +47,16 @@ smx_ctx_base_factory_create_context_sized(size_t size,
 {
   smx_context_t context = xbt_malloc0(size);
 
+  /* Store the address of the stack in heap to compare it apart of heap comparison */
+  if(MC_IS_ENABLED){
+
+    if(mmalloc_ignore == NULL)
+      MC_ignore_init(); 
+    
+    MC_ignore(context, size);
+
+  }
+
   /* If the user provided a function for the process then use it.
      Otherwise, it is the context for maestro and we should set it as the
      current context */
@@ -59,6 +70,9 @@ smx_ctx_base_factory_create_context_sized(size_t size,
   }
   context->data = data;
 
+  if(MC_IS_ENABLED)
+    MC_new_stack_area(context, ((smx_process_t)context->data)->name);
+
   return context;
 }
 

diff --git a/src/xbt/mmalloc/mm_diff.c b/src/xbt/mmalloc/mm_diff.c
index 7b1d983..8bc6173 100644 (file)
--- a/src/xbt/mmalloc/mm_diff.c
+++ b/src/xbt/mmalloc/mm_diff.c
@@ -8,6 +8,7 @@
 #include "xbt/ex_interface.h" /* internals of backtrace setup */
 #include "xbt/str.h"
 #include "mc/mc.h"
+#include "xbt/mmalloc.h"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mm_diff, xbt,
                                 "Logging specific to mm_diff in mmalloc");
@@ -15,6 +16,7 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mm_diff, xbt,
 extern char *xbt_binary_name;
 
 xbt_dynar_t mmalloc_ignore;
+xbt_dynar_t stacks_areas;
 
 typedef struct s_heap_area_pair{
   int block1;
@@ -34,6 +36,8 @@ static void match_equals(xbt_dynar_t list);
 static int in_mmalloc_ignore(int block, int fragment);
 static size_t heap_comparison_ignore(void *address);
 
+static char* is_stack(void *address);
+
 void mmalloc_backtrace_block_display(void* heapinfo, int block){
 
   xbt_ex_t e;
@@ -91,7 +95,7 @@ size_t heaplimit, heapsize1, heapsize2;
 
 int ignore_done;
 
-int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){
+int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2, xbt_dynar_t *stack1, xbt_dynar_t *stack2){
 
   if(heap1 == NULL && heap1 == NULL){
     XBT_DEBUG("Malloc descriptors null");
@@ -120,6 +124,8 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){
   /* Start comparison */
   size_t i1, i2, j1, j2, k, current_block, current_fragment;
   void *addr_block1, *addr_block2, *addr_frag1, *addr_frag2;
+  void *real_addr_block1, *real_addr_block2;
+  char *stack_name;
 
   xbt_dynar_t previous = xbt_dynar_new(sizeof(heap_area_pair_t), heap_area_pair_free_voidp);
 
@@ -172,6 +178,15 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){
     addr_block1 = ((void*) (((ADDR2UINT(i1)) - 1) * BLOCKSIZE + (char*)heapbase1));
 
     if(heapinfo1[i1].type == 0){  /* Large block */
+      
+      real_addr_block1 = (char*)((xbt_mheap_t)s_heap)->heapbase + (((char *)addr_block1) - (char *)heapbase1);
+
+      if((stack_name = is_stack(real_addr_block1)) != NULL){
+        stack_region_t stack = xbt_new0(s_stack_region_t, 1);
+        stack->address = addr_block1;
+        stack->process_name = strdup(stack_name);
+        xbt_dynar_push(*stack1, &stack);
+      }
 
       if(heapinfo1[i1].busy_block.busy_size == 0){
         i1++;
@@ -187,7 +202,17 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){
         if(heapinfo1[current_block].busy_block.busy_size == heapinfo2[current_block].busy_block.busy_size){
 
           addr_block2 = ((void*) (((ADDR2UINT(current_block)) - 1) * BLOCKSIZE + (char*)heapbase2));
+
+          real_addr_block2 = (char*)((xbt_mheap_t)s_heap)->heapbase + (((char *)addr_block2) - (char *)heapbase2);
           
+          if((stack_name = is_stack(real_addr_block2)) != NULL){
+            stack_region_t stack = xbt_new0(s_stack_region_t, 1);
+            stack->address = addr_block2;
+            stack->process_name = strdup(stack_name);
+            xbt_dynar_push(*stack2, &stack);
+          }
+
+        
           add_heap_area_pair(previous, current_block, -1, current_block, -1);
           
           if(ignore_done < xbt_dynar_length(mmalloc_ignore)){
@@ -217,6 +242,17 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){
 
       while(i2 <= heaplimit && !equal){
 
+        addr_block2 = ((void*) (((ADDR2UINT(i2)) - 1) * BLOCKSIZE + (char*)heapbase2));
+        
+        real_addr_block2 = (char*)((xbt_mheap_t)s_heap)->heapbase + (((char *)addr_block2) - (char *)heapbase2);
+        
+        if((stack_name = is_stack(real_addr_block2)) != NULL){
+          stack_region_t stack = xbt_new0(s_stack_region_t, 1);
+          stack->address = addr_block2;
+          stack->process_name = strdup(stack_name);
+          xbt_dynar_push(*stack2, &stack);
+        }
+           
         if(i2 == current_block){
           i2++;
           continue;
@@ -242,8 +278,6 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){
           continue;
         }
 
-        addr_block2 = ((void*) (((ADDR2UINT(i2)) - 1) * BLOCKSIZE + (char*)heapbase2));
-
         /* Comparison */
         add_heap_area_pair(previous, i1, -1, i2, -1);
         
@@ -842,3 +876,14 @@ int mmalloc_linear_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){
   
 }
 
+static char * is_stack(void *address){
+  unsigned int cursor = 0;
+  stack_region_t stack;
+
+  xbt_dynar_foreach(stacks_areas, cursor, stack){
+    if(address == stack->address)
+      return stack->process_name;
+  }
+
+  return NULL;
+}