model-checker : ignore irrelevant differences for heap comparison algorithm

diff --git a/src/include/mc/datatypes.h b/src/include/mc/datatypes.h
index 0b64046..4c6cda3 100644 (file)
--- a/src/include/mc/datatypes.h
+++ b/src/include/mc/datatypes.h
@@ -14,5 +14,10 @@ SG_BEGIN_DECL()
 /******************************* Transitions **********************************/
 typedef struct s_mc_transition *mc_transition_t;
 
+typedef struct s_mc_ignore_region{
+  void *address;
+  size_t size;
+}s_mc_ignore_region_t, *mc_ignore_region_t;
+
 SG_END_DECL()
 #endif                          /* _MC_MC_H */

diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h
index 1febbe0..9892190 100644 (file)
--- a/src/include/mc/mc.h
+++ b/src/include/mc/mc.h
@@ -37,6 +37,9 @@ XBT_PUBLIC(void) MC_process_clock_add(smx_process_t, double);
 XBT_PUBLIC(double) MC_process_clock_get(smx_process_t);
 void MC_automaton_load(const char *file);
 
+void MC_ignore_init(void);
+XBT_PUBLIC(void) MC_ignore(void *address, size_t size);
+
 /********************************* Memory *************************************/
 XBT_PUBLIC(void) MC_memory_init(void);  /* Initialize the memory subsystem */
 XBT_PUBLIC(void) MC_memory_exit(void);

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index bee23e1..0d58509 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -72,6 +72,7 @@ mc_stats_pair_t mc_stats_pair = NULL;
 xbt_fifo_t mc_stack_liveness = NULL;
 mc_snapshot_t initial_snapshot_liveness = NULL;
 int compare;
+extern xbt_dynar_t mmalloc_ignore;
 
 xbt_automaton_t _mc_property_automaton = NULL;
 
@@ -161,6 +162,11 @@ void MC_modelcheck_liveness(){
   
   mc_time = xbt_new0(double, simix_process_maxpid);
 
+  /* mc_time refers to clock for each process -> ignore it for heap comparison */
+  int i;
+  for(i = 0; i<simix_process_maxpid; i++)
+    MC_ignore(&(mc_time[i]), sizeof(double));
+  
   compare = 0;
 
   /* Initialize the data structures that must be persistent across every
@@ -632,3 +638,19 @@ void MC_automaton_new_propositional_symbol(const char* id, void* fct) {
     MC_UNSET_RAW_MEM;
   
 }
+
+void MC_ignore_init(){
+  MC_SET_RAW_MEM;
+  mmalloc_ignore = xbt_dynar_new(sizeof(mc_ignore_region_t), NULL);
+  MC_UNSET_RAW_MEM;
+}
+
+void MC_ignore(void *address, size_t size){
+  MC_SET_RAW_MEM;
+  mc_ignore_region_t region = NULL;
+  region = xbt_new0(s_mc_ignore_region_t, 1);
+  region->address = address;
+  region->size = size;
+  xbt_dynar_push(mmalloc_ignore, &region);
+  MC_UNSET_RAW_MEM;
+}

diff --git a/src/msg/msg_global.c b/src/msg/msg_global.c
index 5383a20..ca077e1 100644 (file)
--- a/src/msg/msg_global.c
+++ b/src/msg/msg_global.c
@@ -49,6 +49,14 @@ void MSG_init_nocheck(int *argc, char **argv) {
     msg_global->process_data_cleanup = NULL;
     msg_global->vms = xbt_swag_new(xbt_swag_offset(vm,all_vms_hookup));
 
+    if(MC_IS_ENABLED){
+      /* Create list of elements to ignore for heap comparison algorithm */
+      MC_ignore_init();
+      /* Ignore total amount of messages sent during the simulation for heap comparison */
+      MC_ignore(&(msg_global->sent_msg), sizeof(msg_global->sent_msg));
+   
+    }
+
     /* initialization of the action module */
     _MSG_action_init();
 
@@ -108,7 +116,7 @@ msg_error_t MSG_main(void)
   fflush(stdout);
   fflush(stderr);
 
-  if (MC_IS_ENABLED) {
+  if (MC_IS_ENABLED) { 
     MC_do_the_modelcheck_for_real();
   } else {
     SIMIX_run();

diff --git a/src/xbt/mmalloc/mm_diff.c b/src/xbt/mmalloc/mm_diff.c
index cd446af..8e209cf 100644 (file)
--- a/src/xbt/mmalloc/mm_diff.c
+++ b/src/xbt/mmalloc/mm_diff.c
@@ -14,6 +14,8 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mm_diff, xbt,
 
 extern char *xbt_binary_name;
 
+xbt_dynar_t mmalloc_ignore;
+
 typedef struct s_heap_area_pair{
   int block1;
   int fragment1;
@@ -29,6 +31,8 @@ static int is_new_heap_area_pair(xbt_dynar_t list, int block1, int fragment1, in
 static int compare_area(void *area1, void* area2, size_t size, xbt_dynar_t previous);
 static void match_equals(xbt_dynar_t list);
 
+static size_t heap_comparison_ignore(void *address);
+
 void mmalloc_backtrace_block_display(void* heapinfo, int block){
 
   xbt_ex_t e;
@@ -350,17 +354,37 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){
 
 }
 
+static size_t heap_comparison_ignore(void *address){
+  unsigned int cursor = 0;
+  mc_ignore_region_t region;
+  xbt_dynar_foreach(mmalloc_ignore, cursor, region){
+    if(region->address == address)
+      return region->size;
+  }
+  return 0;
+}
+
 
 static int compare_area(void *area1, void* area2, size_t size, xbt_dynar_t previous){
 
-  size_t i = 0, pointer_align = 0;
+  size_t i = 0, pointer_align = 0, ignore1 = 0, ignore2 = 0;
   void *address_pointed1, *address_pointed2, *addr_block_pointed1, *addr_block_pointed2, *addr_frag_pointed1, *addr_frag_pointed2;
   size_t block_pointed1, block_pointed2, frag_pointed1, frag_pointed2;
   size_t frag_size;
   int res_compare;
-  
+  void *current_area1, *current_area2;
+ 
   while(i<size){
 
+    current_area1 = (char*)((xbt_mheap_t)s_heap)->heapbase + ((((char *)area1) + i) - (char *)heapbase1);
+    if((ignore1 = heap_comparison_ignore(current_area1)) > 0){
+      current_area2 = (char*)((xbt_mheap_t)s_heap)->heapbase + ((((char *)area2) + i) - (char *)heapbase2);
+      if((ignore2 = heap_comparison_ignore(current_area2))  == ignore1){
+        i = i + ignore2;
+        continue;
+      }
+    }
+   
     if(memcmp(((char *)area1) + i, ((char *)area2) + i, 1) != 0){
 
       /* Check pointer difference */