model-checker : add ignore mechanism for global variables (data + bss segments) in...

diff --git a/src/include/mc/datatypes.h b/src/include/mc/datatypes.h
index 06a4cbf..d21613c 100644 (file)
--- a/src/include/mc/datatypes.h
+++ b/src/include/mc/datatypes.h
@@ -30,6 +30,11 @@ typedef struct s_mc_stack_ignore_variable{
   char *frame;
 }s_mc_stack_ignore_variable_t, *mc_stack_ignore_variable_t;
 
+typedef struct s_mc_data_bss_ignore_variable{
+  void *address;
+  size_t size;
+}s_mc_data_bss_ignore_variable_t, *mc_data_bss_ignore_variable_t;
+
 typedef struct s_stack_region{
   void *address;
   char *process_name;

diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h
index 0eb4b69..ec2c548 100644 (file)
--- a/src/include/mc/mc.h
+++ b/src/include/mc/mc.h
@@ -45,6 +45,7 @@ void MC_automaton_load(const char *file);
 /****************************** MC ignore **********************************/
 XBT_PUBLIC(void) MC_ignore_heap(void *address, size_t size);
 XBT_PUBLIC(void) MC_ignore_stack(const char *var_name, const char *frame);
+XBT_PUBLIC(void) MC_ignore_data_bss(void *address, size_t size);
 void MC_new_stack_area(void *stack, char *name, void *context, size_t size);
 
 /********************************* Memory *************************************/

diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c
index bbe8fd6..6ccdb78 100644 (file)
--- a/src/mc/mc_checkpoint.c
+++ b/src/mc/mc_checkpoint.c
@@ -19,6 +19,7 @@ void *start_plt_libsimgrid, *end_plt_libsimgrid;
 void *start_plt_binary, *end_plt_binary;
 char *libsimgrid_path;
 void *start_data_libsimgrid, *start_bss_libsimgrid;
+void *start_data_binary, *start_bss_binary;
 void *start_text_binary;
 void *end_raw_heap;
 
@@ -136,6 +137,14 @@ void MC_init_memory_map_info(){
           reg = maps->regions[i];
           if(reg.pathname == NULL && (reg.prot & PROT_WRITE) && i < maps->mapsize)
             start_bss_libsimgrid = reg.start_addr;
+        }else if (!memcmp(basename(maps->regions[i].pathname), basename(xbt_binary_name), strlen(basename(xbt_binary_name)))){
+          start_data_binary = reg.start_addr;
+          i++;
+          reg = maps->regions[i];
+          if(reg.pathname == NULL && (reg.prot & PROT_WRITE) && reg.start_addr != std_heap && reg.start_addr != raw_heap && i < maps->mapsize){
+            start_bss_binary = reg.start_addr;
+            i++;
+          }
         }
       }
     }else if ((reg.prot & PROT_READ)){
@@ -197,18 +206,26 @@ mc_snapshot_t MC_take_snapshot_liveness()
           nb_reg++;
           i++;
           reg = maps->regions[i];
-          while(reg.pathname == NULL && (reg.prot & PROT_WRITE) && i < maps->mapsize){
+          if(reg.pathname == NULL && (reg.prot & PROT_WRITE) && i < maps->mapsize){
             MC_snapshot_add_region(snapshot, 1, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr);
-            i++;
             reg = maps->regions[i];
+            i++;
             nb_reg++;
           }
         } else {
           if (!memcmp(basename(maps->regions[i].pathname), basename(xbt_binary_name), strlen(basename(xbt_binary_name)))){
             MC_snapshot_add_region(snapshot, 2, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr);
             nb_reg++;
+            i++;
+            reg = maps->regions[i];
+            if(reg.pathname == NULL && (reg.prot & PROT_WRITE) && reg.start_addr != std_heap && reg.start_addr != raw_heap && i < maps->mapsize){
+              MC_snapshot_add_region(snapshot, 2, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr);
+              reg = maps->regions[i];
+              nb_reg++;
+            }
+          }else{
+            i++;
           }
-          i++;
         }
       }
     }else if ((reg.prot & PROT_READ)){

diff --git a/src/mc/mc_compare.c b/src/mc/mc_compare.c
index c80f046..0333aff 100644 (file)
--- a/src/mc/mc_compare.c
+++ b/src/mc/mc_compare.c
@@ -10,13 +10,14 @@
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_compare, mc,
                                 "Logging specific to mc_compare");
 
-static int data_program_region_compare(void *d1, void *d2, size_t size);
-static int data_libsimgrid_region_compare(void *d1, void *d2, size_t size);
+static int data_bss_program_region_compare(void *d1, void *d2, size_t size);
+static int data_bss_libsimgrid_region_compare(void *d1, void *d2, size_t size);
 static int heap_region_compare(void *d1, void *d2, size_t size);
 
 static int compare_stack(stack_region_t s1, stack_region_t s2, void *sp1, void *sp2, void *heap1, void *heap2, xbt_dynar_t equals);
 static int is_heap_equality(xbt_dynar_t equals, void *a1, void *a2);
 static size_t heap_ignore_size(void *address);
+static size_t data_bss_ignore_size(void *address);
 
 static void stack_region_free(stack_region_t s);
 static void heap_equality_free(heap_equality_t e);
@@ -44,7 +45,27 @@ static size_t heap_ignore_size(void *address){
   return 0;
 }
 
-static int data_program_region_compare(void *d1, void *d2, size_t size){
+static size_t data_bss_ignore_size(void *address){
+  unsigned int cursor = 0;
+  int start = 0;
+  int end = xbt_dynar_length(mc_data_bss_comparison_ignore) - 1;
+  mc_data_bss_ignore_variable_t var;
+
+  while(start <= end){
+    cursor = (start + end) / 2;
+    var = (mc_data_bss_ignore_variable_t)xbt_dynar_get_as(mc_data_bss_comparison_ignore, cursor, mc_data_bss_ignore_variable_t);
+    if(var->address == address)
+      return var->size;
+    if(var->address < address)
+      start = cursor + 1;
+    if(var->address > address)
+      end = cursor - 1;   
+  }
+
+  return 0;
+}
+
+static int data_bss_program_region_compare(void *d1, void *d2, size_t size){
 
   size_t i = 0;
   int pointer_align;
@@ -70,7 +91,7 @@ static int data_program_region_compare(void *d1, void *d2, size_t size){
   return 0;
 }
 
-static int data_libsimgrid_region_compare(void *d1, void *d2, size_t size){
+static int data_bss_libsimgrid_region_compare(void *d1, void *d2, size_t size){
 
   size_t i = 0, ignore_size = 0;
   int pointer_align;
@@ -78,10 +99,10 @@ static int data_libsimgrid_region_compare(void *d1, void *d2, size_t size){
 
   for(i=0; i<size; i++){
     if(memcmp(((char *)d1) + i, ((char *)d2) + i, 1) != 0){
-      if((ignore_size = heap_ignore_size((char *)start_data_libsimgrid+i)) > 0){
+      if((ignore_size = data_bss_ignore_size((char *)start_data_libsimgrid+i)) > 0){
         i = i + ignore_size;
         continue;
-      }else if((ignore_size = heap_ignore_size((char *)start_bss_libsimgrid+i)) > 0){
+      }else if((ignore_size = data_bss_ignore_size((char *)start_bss_libsimgrid+i)) > 0){
         i = i + ignore_size;
         continue;
       }
@@ -94,7 +115,7 @@ static int data_libsimgrid_region_compare(void *d1, void *d2, size_t size){
         continue;
       }else{
         if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_verbose)){
-          XBT_VERB("Different byte (offset=%zu) (%p - %p) in data libsimgrid region", i, (char *)d1 + i, (char *)d2 + i);
+          XBT_VERB("Different byte (offset=%zu) (%p - %p) in libsimgrid region", i, (char *)d1 + i, (char *)d2 + i);
           XBT_VERB("Addresses pointed : %p - %p\n", addr_pointed1, addr_pointed2);
         }
         return 1;
@@ -175,6 +196,8 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
     case 2:
       data_program_index = i;
       i++;
+      while( i < s1->num_reg && s1->regions[i]->type == 2)
+        i++;
       break;
     }
   }
@@ -222,16 +245,17 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
     cursor++;
   }
 
+
   /* Compare program data segment(s) */
   i = data_program_index;
   while(i < s1->num_reg && s1->regions[i]->type == 2){
-    if(data_program_region_compare(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
+    if(data_bss_program_region_compare(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
       if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){
         XBT_DEBUG("Different memcmp for data in program");
         errors++;
       }else{
         if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_verbose))
-          XBT_VERB("Different memcmp for data in program");
+          XBT_VERB("Different memcmp for data in program"); 
         if(!raw_mem_set)
           MC_UNSET_RAW_MEM;
         return 1;
@@ -243,7 +267,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
   /* Compare libsimgrid data segment(s) */
   i = data_libsimgrid_index;
   while(i < s1->num_reg && s1->regions[i]->type == 1){
-    if(data_libsimgrid_region_compare(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
+    if(data_bss_libsimgrid_region_compare(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
       if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){
         XBT_DEBUG("Different memcmp for data in libsimgrid");
         errors++;

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 7457fc5..8108d3d 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -89,6 +89,7 @@ xbt_dict_t mc_local_variables = NULL;
 
 /* Ignore mechanism */
 xbt_dynar_t mc_stack_comparison_ignore;
+xbt_dynar_t mc_data_bss_comparison_ignore;
 extern xbt_dynar_t mc_heap_comparison_ignore;
 extern xbt_dynar_t stacks_areas;
 
@@ -728,6 +729,64 @@ void MC_ignore_heap(void *address, size_t size){
     MC_SET_RAW_MEM;
 }
 
+void MC_ignore_data_bss(void *address, size_t size){
+
+  raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+
+  MC_SET_RAW_MEM;
+  
+  if(mc_data_bss_comparison_ignore == NULL)
+    mc_data_bss_comparison_ignore = xbt_dynar_new(sizeof(mc_data_bss_ignore_variable_t), NULL);
+
+  if(xbt_dynar_is_empty(mc_data_bss_comparison_ignore)){
+
+    mc_data_bss_ignore_variable_t var = NULL;
+    var = xbt_new0(s_mc_data_bss_ignore_variable_t, 1);
+    var->address = address;
+    var->size = size;
+
+    xbt_dynar_insert_at(mc_data_bss_comparison_ignore, 0, &var);
+
+  }else{
+    
+    unsigned int cursor = 0;
+    int start = 0;
+    int end = xbt_dynar_length(mc_data_bss_comparison_ignore) - 1;
+    mc_data_bss_ignore_variable_t current_var = NULL;
+
+    while(start <= end){
+      cursor = (start + end) / 2;
+      current_var = (mc_data_bss_ignore_variable_t)xbt_dynar_get_as(mc_data_bss_comparison_ignore, cursor, mc_data_bss_ignore_variable_t);
+      if(current_var->address == address){
+        MC_UNSET_RAW_MEM;
+        if(raw_mem_set)
+          MC_SET_RAW_MEM;
+        return;
+      }
+      if(current_var->address < address)
+        start = cursor + 1;
+      if(current_var->address > address)
+        end = cursor - 1;
+    }
+ 
+    mc_data_bss_ignore_variable_t var = NULL;
+    var = xbt_new0(s_mc_data_bss_ignore_variable_t, 1);
+    var->address = address;
+    var->size = size;
+
+    if(current_var->address > address)
+      xbt_dynar_insert_at(mc_data_bss_comparison_ignore, cursor + 1, &var);
+    else
+      xbt_dynar_insert_at(mc_data_bss_comparison_ignore, cursor, &var);
+
+  }
+
+  MC_UNSET_RAW_MEM;
+
+  if(raw_mem_set)
+    MC_SET_RAW_MEM;
+}
+
 void MC_ignore_stack(const char *var_name, const char *frame){
   
   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index 05d2a74..61dc577 100644 (file)
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -225,6 +225,7 @@ extern void *end_plt_libsimgrid;
 extern void *start_plt_binary;
 extern void *end_plt_binary;
 extern xbt_dynar_t mc_stack_comparison_ignore;
+extern xbt_dynar_t mc_data_bss_comparison_ignore;
 extern void *start_bss_libsimgrid;
 
 typedef struct s_mc_pair{

diff --git a/src/simix/smx_network.c b/src/simix/smx_network.c
index c22ed83..82313fb 100644 (file)
--- a/src/simix/smx_network.c
+++ b/src/simix/smx_network.c
@@ -31,7 +31,7 @@ void SIMIX_network_init(void)
 {
   rdv_points = xbt_dict_new_homogeneous(SIMIX_rdv_free);
   if(MC_is_active())
-    MC_ignore_heap(&smx_total_comms, sizeof(smx_total_comms));
+    MC_ignore_data_bss(&smx_total_comms, sizeof(smx_total_comms));
 }
 
 void SIMIX_network_exit(void)