Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : parallel comparison of system states for liveness model-checking
authorMarion Guthmuller <marion.guthmuller@loria.fr>
Sat, 21 Sep 2013 20:47:01 +0000 (22:47 +0200)
committerMarion Guthmuller <marion.guthmuller@loria.fr>
Sat, 21 Sep 2013 20:50:29 +0000 (22:50 +0200)
13 files changed:
include/xbt/mmalloc.h
include/xbt/parmap.h
src/mc/mc_checkpoint.c
src/mc/mc_compare.c
src/mc/mc_global.c
src/mc/mc_liveness.c
src/mc/mc_private.h
src/xbt/mmalloc/mfree.c
src/xbt/mmalloc/mm_diff.c
src/xbt/mmalloc/mmalloc.c
src/xbt/mmalloc/mmprivate.h
src/xbt/mmalloc/mrealloc.c
src/xbt/parmap.c

index edc4efb..32fa620 100644 (file)
@@ -58,7 +58,7 @@ xbt_mheap_t mmalloc_get_current_heap(void);
 
 int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2);
 int mmalloc_linear_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2);
 
 int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2);
 int mmalloc_linear_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2);
-void init_heap_information(xbt_mheap_t heap1, xbt_mheap_t heap2, xbt_dynar_t to_ignore1, xbt_dynar_t to_ignore2);
+int init_heap_information(xbt_mheap_t heap1, xbt_mheap_t heap2, xbt_dynar_t to_ignore1, xbt_dynar_t to_ignore2);
 int compare_heap_area(void *area1, void* area2, xbt_dynar_t previous, xbt_dict_t all_types, xbt_dict_t other_types, char *type, int pointer_level);
 void reset_heap_information(void);
 int get_pointed_area_size(void *area, int heap);
 int compare_heap_area(void *area1, void* area2, xbt_dynar_t previous, xbt_dict_t all_types, xbt_dict_t other_types, char *type, int pointer_level);
 void reset_heap_information(void);
 int get_pointed_area_size(void *area, int heap);
index 3b9f9ed..d26d914 100644 (file)
@@ -52,6 +52,16 @@ XBT_PUBLIC(void) xbt_parmap_apply(xbt_parmap_t parmap,
                                   xbt_dynar_t data);
 XBT_PUBLIC(void*) xbt_parmap_next(xbt_parmap_t parmap);
 
                                   xbt_dynar_t data);
 XBT_PUBLIC(void*) xbt_parmap_next(xbt_parmap_t parmap);
 
+#ifdef HAVE_MC
+XBT_PUBLIC(xbt_parmap_t) xbt_parmap_mc_new(unsigned int num_workers,
+    e_xbt_parmap_mode_t mode);
+
+XBT_PUBLIC(int) xbt_parmap_mc_apply(xbt_parmap_t parmap, 
+                         int_f_pvoid_pvoid_t fun, 
+                         void *data,
+                         unsigned int length,
+                         void* ref_snapshot);
+#endif
 /** \} */
 
 SG_END_DECL()
 /** \} */
 
 SG_END_DECL()
index 7b36469..f6612b7 100644 (file)
@@ -726,10 +726,6 @@ static void MC_dump_checkpoint_ignore(mc_snapshot_t snapshot){
 
 mc_snapshot_t MC_take_snapshot(){
 
 
 mc_snapshot_t MC_take_snapshot(){
 
-  int raw_mem = (mmalloc_get_current_heap() == raw_heap);
-  
-  MC_SET_RAW_MEM;
-
   mc_snapshot_t snapshot = xbt_new0(s_mc_snapshot_t, 1);
   snapshot->nb_processes = xbt_swag_size(simix_global->process_list);
 
   mc_snapshot_t snapshot = xbt_new0(s_mc_snapshot_t, 1);
   snapshot->nb_processes = xbt_swag_size(simix_global->process_list);
 
@@ -746,11 +742,6 @@ mc_snapshot_t MC_take_snapshot(){
 
   MC_dump_checkpoint_ignore(snapshot);
 
 
   MC_dump_checkpoint_ignore(snapshot);
 
-  MC_UNSET_RAW_MEM;
-
-  if(raw_mem)
-    MC_SET_RAW_MEM;
-
   return snapshot;
 
 }
   return snapshot;
 
 }
index 2422ad6..85c2901 100644 (file)
@@ -15,7 +15,7 @@ typedef struct s_pointers_pair{
   void *p2;
 }s_pointers_pair_t, *pointers_pair_t;
 
   void *p2;
 }s_pointers_pair_t, *pointers_pair_t;
 
-xbt_dynar_t compared_pointers;
+__thread xbt_dynar_t compared_pointers;
 
 /************************** Free functions ****************************/
 /********************************************************************/
 
 /************************** Free functions ****************************/
 /********************************************************************/
@@ -271,17 +271,17 @@ static int compare_global_variables(int region_type, mc_mem_region_t r1, mc_mem_
       offset = (char *)current_var->address.address - (char *)start_data_libsimgrid;
 
     res = compare_areas_with_type((char *)r1->data + offset, (char *)r2->data + offset, types, other_types, current_var->type_origin, r1->size, region_type, start_data, 0);
       offset = (char *)current_var->address.address - (char *)start_data_libsimgrid;
 
     res = compare_areas_with_type((char *)r1->data + offset, (char *)r2->data + offset, types, other_types, current_var->type_origin, r1->size, region_type, start_data, 0);
-    if(res == -1){
-      xbt_dynar_cursor_rm(variables, &cursor);
-    }else if(res == 1){
-      XBT_VERB("Global variable %s (%p - %p) is different between snapshots", current_var->name, (char *)r1->data + offset, (char *)r2->data + offset);
+    if(res == 1){
+      XBT_VERB("Global variable %s is different between snapshots", current_var->name);
       xbt_dynar_free(&compared_pointers);
       xbt_dynar_free(&compared_pointers);
+      compared_pointers = NULL;
       return 1;
     }
 
   }
 
   xbt_dynar_free(&compared_pointers);
       return 1;
     }
 
   }
 
   xbt_dynar_free(&compared_pointers);
+  compared_pointers = NULL;
 
   return 0;
 
 
   return 0;
 
@@ -299,6 +299,7 @@ static int compare_local_variables(mc_snapshot_stack_t stack1, mc_snapshot_stack
   if(xbt_dynar_length(stack1->local_variables) != xbt_dynar_length(stack2->local_variables)){
     XBT_VERB("Different number of local variables");
     xbt_dynar_free(&compared_pointers);
   if(xbt_dynar_length(stack1->local_variables) != xbt_dynar_length(stack2->local_variables)){
     XBT_VERB("Different number of local variables");
     xbt_dynar_free(&compared_pointers);
+    compared_pointers = NULL;
     return 1;
   }else{
     unsigned int cursor = 0;
     return 1;
   }else{
     unsigned int cursor = 0;
@@ -318,24 +319,26 @@ static int compare_local_variables(mc_snapshot_stack_t stack1, mc_snapshot_stack
       else
         res = compare_areas_with_type( (char *)heap1 + offset1, (char *)heap2 + offset2, mc_variables_type_binary, mc_variables_type_libsimgrid, current_var1->type, 0, 2, start_data_binary, 0l);
       if(res == 1){
       else
         res = compare_areas_with_type( (char *)heap1 + offset1, (char *)heap2 + offset2, mc_variables_type_binary, mc_variables_type_libsimgrid, current_var1->type, 0, 2, start_data_binary, 0l);
       if(res == 1){
-        XBT_VERB("Local variable %s (%p - %p)  in frame %s  is different between snapshots", current_var1->name, (char *)heap1 + offset1, (char *)heap2 + offset2, current_var1->frame);
+        XBT_VERB("Local variable %s in frame %s  is different between snapshots", current_var1->name, current_var1->frame);
         xbt_dynar_free(&compared_pointers);
         xbt_dynar_free(&compared_pointers);
+        compared_pointers = NULL;
         return res;
       }
       cursor++;
     }
     xbt_dynar_free(&compared_pointers);
         return res;
       }
       cursor++;
     }
     xbt_dynar_free(&compared_pointers);
+    compared_pointers = NULL;
     return 0;
   }
 }
 
     return 0;
   }
 }
 
-int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
+int snapshot_compare(void *p1, void *p2){
+
+  mc_snapshot_t s1 = ((mc_pair_t)p1)->graph_state->system_state;
+  mc_snapshot_t s2 = ((mc_pair_t)p2)->graph_state->system_state;
 
 
-  int raw_mem = (mmalloc_get_current_heap() == raw_heap);
-  
-  MC_SET_RAW_MEM;
-     
   int errors = 0;
   int errors = 0;
+  int res_init;
 
   xbt_os_timer_t global_timer = xbt_os_timer_new();
   xbt_os_timer_t timer = xbt_os_timer_new();
 
   xbt_os_timer_t global_timer = xbt_os_timer_new();
   xbt_os_timer_t timer = xbt_os_timer_new();
@@ -359,12 +362,12 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
         xbt_os_walltimer_stop(timer);
         mc_comp_times->stacks_sizes_comparison_time = xbt_os_timer_elapsed(timer);
       }
         xbt_os_walltimer_stop(timer);
         mc_comp_times->stacks_sizes_comparison_time = xbt_os_timer_elapsed(timer);
       }
-      XBT_DEBUG("Different size used in stacks : %zu - %zu", size_used1, size_used2);
+      XBT_DEBUG("(%d - %d) Different size used in stacks : %zu - %zu", ((mc_pair_t)p1)->num, ((mc_pair_t)p2)->num, size_used1, size_used2);
       errors++;
       is_diff = 1;
     #else
       #ifdef MC_VERBOSE
       errors++;
       is_diff = 1;
     #else
       #ifdef MC_VERBOSE
-        XBT_VERB("Different size used in stacks : %zu - %zu", size_used1, size_used2);
+      XBT_VERB("(%d - %d) Different size used in stacks : %zu - %zu", ((mc_pair_t)p1)->num, ((mc_pair_t)p2)->num, size_used1, size_used2);
       #endif
 
       xbt_os_walltimer_stop(timer);
       #endif
 
       xbt_os_walltimer_stop(timer);
@@ -373,9 +376,6 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
       mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
       xbt_os_timer_free(global_timer);
 
       mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
       xbt_os_timer_free(global_timer);
 
-      if(!raw_mem)
-        MC_UNSET_RAW_MEM;
-
       return 1;
     #endif  
     }
       return 1;
     #endif  
     }
@@ -407,9 +407,6 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
         mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
         xbt_os_timer_free(global_timer);
 
         mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
         xbt_os_timer_free(global_timer);
 
-        if(!raw_mem)
-          MC_UNSET_RAW_MEM;
-
         return 1;
       #endif
     }
         return 1;
       #endif
     }
@@ -438,9 +435,6 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
         mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
         xbt_os_timer_free(global_timer);
 
         mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
         xbt_os_timer_free(global_timer);
 
-        if(!raw_mem)
-          MC_UNSET_RAW_MEM;
-        
         return 1;
       #endif
     }
         return 1;
       #endif
     }
@@ -451,7 +445,27 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
   #endif
 
   /* Init heap information used in heap comparison algorithm */
   #endif
 
   /* Init heap information used in heap comparison algorithm */
-  init_heap_information((xbt_mheap_t)s1->regions[0]->data, (xbt_mheap_t)s2->regions[0]->data, s1->to_ignore, s2->to_ignore);
+  res_init = init_heap_information((xbt_mheap_t)s1->regions[0]->data, (xbt_mheap_t)s2->regions[0]->data, s1->to_ignore, s2->to_ignore);
+  if(res_init == -1){
+     #ifdef MC_DEBUG
+    XBT_DEBUG("(%d - %d) Different heap information", ((mc_pair_t)p1)->num, ((mc_pair_t)p2)->num); 
+        errors++; 
+      #else
+        #ifdef MC_VERBOSE
+        XBT_VERB("(%d - %d) Different heap information", ((mc_pair_t)p1)->num, ((mc_pair_t)p2)->num); 
+        #endif
+
+        xbt_os_walltimer_stop(global_timer);
+        mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
+        xbt_os_timer_free(global_timer);
+
+        return 1;
+      #endif
+  }
+
+  #ifdef MC_DEBUG
+    xbt_os_walltimer_start(timer);
+  #endif
 
   /* Stacks comparison */
   unsigned int  cursor = 0;
 
   /* Stacks comparison */
   unsigned int  cursor = 0;
@@ -469,13 +483,13 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
           xbt_os_walltimer_stop(timer);
           mc_comp_times->stacks_comparison_time = xbt_os_timer_elapsed(timer);
         }
           xbt_os_walltimer_stop(timer);
           mc_comp_times->stacks_comparison_time = xbt_os_timer_elapsed(timer);
         }
-        XBT_DEBUG("Different local variables between stacks %d", cursor + 1);
+        XBT_DEBUG("(%d - %d) Different local variables between stacks %d", ((mc_pair_t)p1)->num, ((mc_pair_t)p2)->num, cursor + 1);
         errors++;
         is_diff = 1;
       #else
         
         #ifdef MC_VERBOSE
         errors++;
         is_diff = 1;
       #else
         
         #ifdef MC_VERBOSE
-          XBT_VERB("Different local variables between stacks %d", cursor + 1);
+        XBT_VERB("(%d - %d) Different local variables between stacks %d", ((mc_pair_t)p1)->num, ((mc_pair_t)p2)->num, cursor + 1);
         #endif
           
         reset_heap_information();
         #endif
           
         reset_heap_information();
@@ -484,10 +498,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
         xbt_os_walltimer_stop(global_timer);
         mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
         xbt_os_timer_free(global_timer);
         xbt_os_walltimer_stop(global_timer);
         mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
         xbt_os_timer_free(global_timer);
-        
-        if(!raw_mem)
-          MC_UNSET_RAW_MEM;
-        
         return 1;
       #endif
     }
         return 1;
       #endif
     }
@@ -506,11 +517,11 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
     #ifdef MC_DEBUG
       xbt_os_walltimer_stop(timer);
       mc_comp_times->binary_global_variables_comparison_time = xbt_os_timer_elapsed(timer);
     #ifdef MC_DEBUG
       xbt_os_walltimer_stop(timer);
       mc_comp_times->binary_global_variables_comparison_time = xbt_os_timer_elapsed(timer);
-      XBT_DEBUG("Different global variables in binary");
+      XBT_DEBUG("(%d - %d) Different global variables in binary", ((mc_pair_t)p1)->num, ((mc_pair_t)p2)->num);
       errors++;
     #else
       #ifdef MC_VERBOSE
       errors++;
     #else
       #ifdef MC_VERBOSE
-        XBT_VERB("Different global variables in binary");
+      XBT_VERB("(%d - %d) Different global variables in binary", ((mc_pair_t)p1)->num, ((mc_pair_t)p2)->num);
       #endif
 
       reset_heap_information();
       #endif
 
       reset_heap_information();
@@ -519,9 +530,6 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
       xbt_os_walltimer_stop(global_timer);
       mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
       xbt_os_timer_free(global_timer);
       xbt_os_walltimer_stop(global_timer);
       mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
       xbt_os_timer_free(global_timer);
-    
-      if(!raw_mem)
-        MC_UNSET_RAW_MEM;
 
       return 1;
     #endif
 
       return 1;
     #endif
@@ -539,11 +547,11 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
     #ifdef MC_DEBUG
       xbt_os_walltimer_stop(timer);
       mc_comp_times->libsimgrid_global_variables_comparison_time = xbt_os_timer_elapsed(timer);
     #ifdef MC_DEBUG
       xbt_os_walltimer_stop(timer);
       mc_comp_times->libsimgrid_global_variables_comparison_time = xbt_os_timer_elapsed(timer);
-      XBT_DEBUG("Different global variables in libsimgrid");
+      XBT_DEBUG("(%d - %d) Different global variables in libsimgrid", ((mc_pair_t)p1)->num, ((mc_pair_t)p2)->num);
       errors++;
     #else
       #ifdef MC_VERBOSE
       errors++;
     #else
       #ifdef MC_VERBOSE
-        XBT_VERB("Different global variables in libsimgrid");
+      XBT_VERB("(%d - %d) Different global variables in libsimgrid", ((mc_pair_t)p1)->num, ((mc_pair_t)p2)->num);
       #endif
         
       reset_heap_information();
       #endif
         
       reset_heap_information();
@@ -552,14 +560,11 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
       xbt_os_walltimer_stop(global_timer);
       mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
       xbt_os_timer_free(global_timer);
       xbt_os_walltimer_stop(global_timer);
       mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
       xbt_os_timer_free(global_timer);
-    
-      if(!raw_mem)
-        MC_UNSET_RAW_MEM;
 
       return 1;
     #endif
   }
 
       return 1;
     #endif
   }
-    
+
   #ifdef MC_DEBUG
     xbt_os_walltimer_start(timer);
   #endif
   #ifdef MC_DEBUG
     xbt_os_walltimer_start(timer);
   #endif
@@ -570,12 +575,12 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
     #ifdef MC_DEBUG
       xbt_os_walltimer_stop(timer);
       mc_comp_times->heap_comparison_time = xbt_os_timer_elapsed(timer); 
     #ifdef MC_DEBUG
       xbt_os_walltimer_stop(timer);
       mc_comp_times->heap_comparison_time = xbt_os_timer_elapsed(timer); 
-      XBT_DEBUG("Different heap (mmalloc_compare)");
+      XBT_DEBUG("(%d - %d) Different heap (mmalloc_compare)", ((mc_pair_t)p1)->num, ((mc_pair_t)p2)->num);
       errors++;
     #else
  
       #ifdef MC_VERBOSE
       errors++;
     #else
  
       #ifdef MC_VERBOSE
-        XBT_VERB("Different heap (mmalloc_compare)");
+      XBT_VERB("(%d - %d) Different heap (mmalloc_compare)", ((mc_pair_t)p1)->num, ((mc_pair_t)p2)->num);
       #endif
        
       reset_heap_information();
       #endif
        
       reset_heap_information();
@@ -585,9 +590,6 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
       mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
       xbt_os_timer_free(global_timer);
 
       mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
       xbt_os_timer_free(global_timer);
 
-      if(!raw_mem)
-        MC_UNSET_RAW_MEM;
-
       return 1;
     #endif
   }else{
       return 1;
     #endif
   }else{
@@ -612,9 +614,6 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
     print_comparison_times();
   #endif
 
     print_comparison_times();
   #endif
 
-  if(!raw_mem)
-    MC_UNSET_RAW_MEM;
-
   return errors > 0;
   
 }
   return errors > 0;
   
 }
index 613cf30..b5e073e 100644 (file)
@@ -94,8 +94,8 @@ void _mc_cfg_cb_dot_output(const char *name, int pos) {
 mc_state_t mc_current_state = NULL;
 char mc_replay_mode = FALSE;
 double *mc_time = NULL;
 mc_state_t mc_current_state = NULL;
 char mc_replay_mode = FALSE;
 double *mc_time = NULL;
-mc_comparison_times_t mc_comp_times = NULL;
-double mc_snapshot_comparison_time;
+__thread mc_comparison_times_t mc_comp_times = NULL;
+__thread double mc_snapshot_comparison_time;
 mc_stats_t mc_stats = NULL;
 
 /* Safety */
 mc_stats_t mc_stats = NULL;
 
 /* Safety */
@@ -1325,10 +1325,8 @@ void MC_ignore_heap(void *address, size_t size){
   else
     xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor, &region);
 
   else
     xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor, &region);
 
-  MC_UNSET_RAW_MEM;
-
-  if(raw_mem_set)
-    MC_SET_RAW_MEM;
+  if(!raw_mem_set)
+    MC_UNSET_RAW_MEM;
 }
 
 void MC_remove_ignore_heap(void *address, size_t size){
 }
 
 void MC_remove_ignore_heap(void *address, size_t size){
@@ -1366,10 +1364,8 @@ void MC_remove_ignore_heap(void *address, size_t size){
     MC_remove_ignore_heap(address, size);
   }
 
     MC_remove_ignore_heap(address, size);
   }
 
-  MC_UNSET_RAW_MEM;
-  
-  if(raw_mem_set)
-    MC_SET_RAW_MEM;
+  if(!raw_mem_set)
+    MC_UNSET_RAW_MEM;
 
 }
 
 
 }
 
@@ -1443,10 +1439,8 @@ void MC_ignore_global_variable(const char *name){
     }
   }
 
     }
   }
 
-  MC_UNSET_RAW_MEM;
-
-  if(raw_mem_set)
-    MC_SET_RAW_MEM;
+  if(!raw_mem_set)
+    MC_UNSET_RAW_MEM;
 }
 
 void MC_ignore_local_variable(const char *var_name, const char *frame_name){
 }
 
 void MC_ignore_local_variable(const char *var_name, const char *frame_name){
@@ -1554,10 +1548,8 @@ void MC_ignore_local_variable(const char *var_name, const char *frame_name){
     }
   }
 
     }
   }
 
-  MC_UNSET_RAW_MEM;
-  
-  if(raw_mem_set)
-    MC_SET_RAW_MEM;
+  if(!raw_mem_set)
+    MC_UNSET_RAW_MEM;
 
 }
 
 
 }
 
@@ -1566,6 +1558,7 @@ void MC_new_stack_area(void *stack, char *name, void* context, size_t size){
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 
   MC_SET_RAW_MEM;
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 
   MC_SET_RAW_MEM;
+
   if(stacks_areas == NULL)
     stacks_areas = xbt_dynar_new(sizeof(stack_region_t), NULL);
   
   if(stacks_areas == NULL)
     stacks_areas = xbt_dynar_new(sizeof(stack_region_t), NULL);
   
@@ -1577,11 +1570,9 @@ void MC_new_stack_area(void *stack, char *name, void* context, size_t size){
   region->size = size;
   region->block = ((char*)stack - (char*)((xbt_mheap_t)std_heap)->heapbase) / BLOCKSIZE + 1;
   xbt_dynar_push(stacks_areas, &region);
   region->size = size;
   region->block = ((char*)stack - (char*)((xbt_mheap_t)std_heap)->heapbase) / BLOCKSIZE + 1;
   xbt_dynar_push(stacks_areas, &region);
-  
-  MC_UNSET_RAW_MEM;
 
 
-  if(raw_mem_set)
-    MC_SET_RAW_MEM;
+  if(!raw_mem_set)
+    MC_UNSET_RAW_MEM;
 }
 
 void MC_ignore(void *addr, size_t size){
 }
 
 void MC_ignore(void *addr, size_t size){
@@ -1724,6 +1715,9 @@ void MC_init(){
   MC_get_libsimgrid_plt_section();
   MC_get_binary_plt_section();
 
   MC_get_libsimgrid_plt_section();
   MC_get_binary_plt_section();
 
+   /* Init parmap */
+  parmap = xbt_parmap_mc_new(xbt_os_get_numcores(), XBT_PARMAP_DEFAULT);
+
   MC_UNSET_RAW_MEM;
 
    /* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */
   MC_UNSET_RAW_MEM;
 
    /* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */
@@ -1750,6 +1744,7 @@ void MC_init(){
   MC_ignore_global_variable("smx_current_context_key");
   MC_ignore_global_variable("sysv_maestro_context");
   MC_ignore_global_variable("counter"); /* Static variable used for tracing */
   MC_ignore_global_variable("smx_current_context_key");
   MC_ignore_global_variable("sysv_maestro_context");
   MC_ignore_global_variable("counter"); /* Static variable used for tracing */
 
   if(raw_mem_set)
     MC_SET_RAW_MEM;
 
   if(raw_mem_set)
     MC_SET_RAW_MEM;
index a360a24..66f17c5 100644 (file)
@@ -15,7 +15,7 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
 xbt_dynar_t acceptance_pairs;
 xbt_dynar_t visited_pairs;
 xbt_dynar_t successors;
 xbt_dynar_t acceptance_pairs;
 xbt_dynar_t visited_pairs;
 xbt_dynar_t successors;
-
+xbt_parmap_t parmap;
 
 /********* Static functions *********/
 
 
 /********* Static functions *********/
 
@@ -35,133 +35,114 @@ static xbt_dynar_t get_atomic_propositions_values(){
   return values;
 }
 
   return values;
 }
 
+static int get_search_interval(xbt_dynar_t all_pairs, mc_pair_t pair, int *min, int *max){
+
+  int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+
+  MC_SET_RAW_MEM;
+
+  int cursor = 0, previous_cursor, next_cursor;
+  mc_pair_t pair_test;
+  int start = 0;
+  int end = xbt_dynar_length(all_pairs) - 1;
+  
+  while(start <= end){
+    cursor = (start + end) / 2;
+    pair_test = (mc_pair_t)xbt_dynar_get_as(all_pairs, cursor, mc_pair_t);
+    if(pair_test->nb_processes < pair->nb_processes){
+      start = cursor + 1;
+    }else if(pair_test->nb_processes > pair->nb_processes){
+      end = cursor - 1;
+    }else{
+      if(pair_test->heap_bytes_used < pair->heap_bytes_used){
+        start = cursor +1;
+      }else if(pair_test->heap_bytes_used > pair->heap_bytes_used){
+        end = cursor - 1;
+      }else{
+        *min = *max = cursor;
+        previous_cursor = cursor - 1;
+        while(previous_cursor >= 0){
+          pair_test = (mc_pair_t)xbt_dynar_get_as(all_pairs, previous_cursor, mc_pair_t);
+          if(pair_test->nb_processes != pair->nb_processes || pair_test->heap_bytes_used != pair->heap_bytes_used)
+            break;
+          *min = previous_cursor;
+          previous_cursor--;
+        }
+        next_cursor = cursor + 1;
+        while(next_cursor < xbt_dynar_length(all_pairs)){
+          pair_test = (mc_pair_t)xbt_dynar_get_as(all_pairs, next_cursor, mc_pair_t);
+          if(pair_test->nb_processes != pair->nb_processes || pair_test->heap_bytes_used != pair->heap_bytes_used)
+            break;
+          *max = next_cursor;
+          next_cursor++;
+        }
+        if(!raw_mem_set)
+          MC_UNSET_RAW_MEM;
+        return -1;
+      }
+     }
+  }
+
+  if(!raw_mem_set)
+    MC_UNSET_RAW_MEM;
+
+  return cursor;
+}
+
 static int is_reached_acceptance_pair(mc_pair_t pair){
 
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 static int is_reached_acceptance_pair(mc_pair_t pair){
 
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+
+  MC_SET_RAW_MEM;
  
   if(xbt_dynar_is_empty(acceptance_pairs)){
 
  
   if(xbt_dynar_is_empty(acceptance_pairs)){
 
-    MC_SET_RAW_MEM;
     if(pair->graph_state->system_state == NULL){
       pair->graph_state->system_state = MC_take_snapshot();
       pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
     }
     xbt_dynar_push(acceptance_pairs, &pair); 
     if(pair->graph_state->system_state == NULL){
       pair->graph_state->system_state = MC_take_snapshot();
       pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
     }
     xbt_dynar_push(acceptance_pairs, &pair); 
-    MC_UNSET_RAW_MEM;
 
 
-    if(raw_mem_set)
-      MC_SET_RAW_MEM;
+    if(!raw_mem_set)
+      MC_UNSET_RAW_MEM;
 
     return -1;
 
   }else{
 
 
     return -1;
 
   }else{
 
-    MC_SET_RAW_MEM;
-
     if(pair->graph_state->system_state == NULL){
       pair->graph_state->system_state = MC_take_snapshot();
       pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
     }
 
     if(pair->graph_state->system_state == NULL){
       pair->graph_state->system_state = MC_take_snapshot();
       pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
     }
 
-    size_t current_bytes_used = pair->heap_bytes_used;
-    int current_nb_processes = pair->nb_processes;
-
-    unsigned int cursor = 0;
-    int previous_cursor = 0, next_cursor = 0;
-    int start = 0;
-    int end = xbt_dynar_length(acceptance_pairs) - 1;
-
-    mc_pair_t pair_test = NULL;
-    size_t bytes_used_test;
-    int nb_processes_test;
-    int same_processes_and_bytes_not_found = 1;
+    int min = -1, max = -1, index;
+    int res;
+    mc_pair_t pair_test;
+    
+    index = get_search_interval(acceptance_pairs, pair, &min, &max);
 
 
-    while(start <= end && same_processes_and_bytes_not_found){
-      cursor = (start + end) / 2;
-      pair_test = (mc_pair_t)xbt_dynar_get_as(acceptance_pairs, cursor, mc_pair_t);
-      bytes_used_test = pair_test->heap_bytes_used;
-      nb_processes_test = pair_test->nb_processes;
-      if(nb_processes_test < current_nb_processes)
-        start = cursor + 1;
-      else if(nb_processes_test > current_nb_processes)
-        end = cursor - 1; 
-      else if(nb_processes_test == current_nb_processes){
-        if(bytes_used_test < current_bytes_used)
-          start = cursor + 1;
-        else if(bytes_used_test > current_bytes_used)
-          end = cursor - 1;
-        else if(bytes_used_test == current_bytes_used){
-          same_processes_and_bytes_not_found = 0;
-          if(xbt_automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){
-            if(xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, pair->atomic_propositions) == 0){
-              XBT_DEBUG("Compare with state %d", pair_test->num);
-              if(snapshot_compare(pair->graph_state->system_state, pair_test->graph_state->system_state) == 0){
-                if(raw_mem_set)
-                  MC_SET_RAW_MEM;
-                else
-                  MC_UNSET_RAW_MEM;
-                return pair_test->num;
-              }
-            }
-          }
-          /* Search another pair with same number of bytes used in std_heap */
-          previous_cursor = cursor - 1;
-          while(previous_cursor >= 0){
-            pair_test = (mc_pair_t)xbt_dynar_get_as(acceptance_pairs, previous_cursor, mc_pair_t);
-            bytes_used_test = pair_test->heap_bytes_used;
-            if(bytes_used_test != current_bytes_used)
-              break;
-            if(xbt_automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){
-              if(xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, pair->atomic_propositions) == 0){  
-                XBT_DEBUG("Compare with state %d", pair_test->num);
-                if(snapshot_compare(pair->graph_state->system_state, pair_test->graph_state->system_state) == 0){
-                  if(raw_mem_set)
-                    MC_SET_RAW_MEM;
-                  else
-                    MC_UNSET_RAW_MEM;
-                  return pair_test->num;
-                }
-              }
-            }
-            previous_cursor--;
-          }
-          next_cursor = cursor + 1;
-          while(next_cursor < xbt_dynar_length(acceptance_pairs)){
-            pair_test = (mc_pair_t)xbt_dynar_get_as(acceptance_pairs, next_cursor, mc_pair_t);
-            bytes_used_test = pair_test->heap_bytes_used;
-            if(bytes_used_test != current_bytes_used)
-              break;
-            if(xbt_automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){
-              if(xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, pair->atomic_propositions) == 0){
-                XBT_DEBUG("Compare with state %d", pair_test->num);
-                if(snapshot_compare(pair->graph_state->system_state, pair_test->graph_state->system_state) == 0){
-                  if(raw_mem_set)
-                    MC_SET_RAW_MEM;
-                  else
-                    MC_UNSET_RAW_MEM;
-                  return pair_test->num;
-                }
-              }
-            }
-            next_cursor++;
-          }
-        }
+    if(min != -1 && max != -1){ /* Acceptance pair with same number of processes and same heap bytes used exists */
+      res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(acceptance_pairs, min), (max-min)+1, pair);
+      if(res != -1){
+        if(!raw_mem_set)
+          MC_UNSET_RAW_MEM;
+        return ((mc_pair_t)xbt_dynar_get_as(acceptance_pairs, (min+res)-1, mc_pair_t))->num;
+      }
+      xbt_dynar_insert_at(acceptance_pairs, min, &pair);
+    }else{
+      pair_test = (mc_pair_t)xbt_dynar_get_as(acceptance_pairs, index, mc_pair_t);
+      if(pair_test->nb_processes < pair->nb_processes){
+        xbt_dynar_insert_at(acceptance_pairs, index+1, &pair);
+      }else{
+        if(pair_test->heap_bytes_used < pair->heap_bytes_used)
+          xbt_dynar_insert_at(acceptance_pairs, index + 1, &pair);
+        else
+          xbt_dynar_insert_at(acceptance_pairs, index, &pair);
       }
     }
 
       }
     }
 
-    pair_test = (mc_pair_t)xbt_dynar_get_as(acceptance_pairs, cursor, mc_pair_t);
-    bytes_used_test = pair_test->heap_bytes_used;
-
-    if(bytes_used_test < current_bytes_used)
-      xbt_dynar_insert_at(acceptance_pairs, cursor + 1, &pair);
-    else
-      xbt_dynar_insert_at(acceptance_pairs, cursor, &pair);
-       
-    
-    MC_UNSET_RAW_MEM;
-
-    if(raw_mem_set)
-      MC_SET_RAW_MEM;
+    if(!raw_mem_set)
+      MC_UNSET_RAW_MEM;
     
     return -1;
     
     
     return -1;
     
@@ -174,20 +155,18 @@ static void set_acceptance_pair_reached(mc_pair_t pair){
 
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 
 
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 
+  MC_SET_RAW_MEM;
+
   if(xbt_dynar_is_empty(acceptance_pairs)){
 
   if(xbt_dynar_is_empty(acceptance_pairs)){
 
-     MC_SET_RAW_MEM;
      if(pair->graph_state->system_state == NULL){
        pair->graph_state->system_state = MC_take_snapshot();
        pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
      }
      xbt_dynar_push(acceptance_pairs, &pair); 
      if(pair->graph_state->system_state == NULL){
        pair->graph_state->system_state = MC_take_snapshot();
        pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
      }
      xbt_dynar_push(acceptance_pairs, &pair); 
-     MC_UNSET_RAW_MEM;
 
   }else{
 
 
   }else{
 
-    MC_SET_RAW_MEM;
-
     if(pair->graph_state->system_state == NULL){
       pair->graph_state->system_state = MC_take_snapshot();
       pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
     if(pair->graph_state->system_state == NULL){
       pair->graph_state->system_state = MC_take_snapshot();
       pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
@@ -196,7 +175,7 @@ static void set_acceptance_pair_reached(mc_pair_t pair){
     size_t current_bytes_used = pair->heap_bytes_used;
     int current_nb_processes = pair->nb_processes;
 
     size_t current_bytes_used = pair->heap_bytes_used;
     int current_nb_processes = pair->nb_processes;
 
-    unsigned int cursor = 0;
+    int cursor = 0;
     int start = 0;
     int end = xbt_dynar_length(acceptance_pairs) - 1;
 
     int start = 0;
     int end = xbt_dynar_length(acceptance_pairs) - 1;
 
@@ -226,19 +205,20 @@ static void set_acceptance_pair_reached(mc_pair_t pair){
     if(bytes_used_test < current_bytes_used)
       xbt_dynar_insert_at(acceptance_pairs, cursor + 1, &pair);
     else
     if(bytes_used_test < current_bytes_used)
       xbt_dynar_insert_at(acceptance_pairs, cursor + 1, &pair);
     else
-      xbt_dynar_insert_at(acceptance_pairs, cursor, &pair);
-    
-    MC_UNSET_RAW_MEM;
-    
+      xbt_dynar_insert_at(acceptance_pairs, cursor, &pair);    
   }
 
   }
 
-  if(raw_mem_set)
-    MC_SET_RAW_MEM;
+  if(!raw_mem_set)
+    MC_UNSET_RAW_MEM;
     
 }
 
 static void remove_acceptance_pair(mc_pair_t pair){
 
     
 }
 
 static void remove_acceptance_pair(mc_pair_t pair){
 
+  int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+
+  MC_SET_RAW_MEM;
+
   unsigned int cursor = 0;
   mc_pair_t pair_test;
   int pair_found = 0;
   unsigned int cursor = 0;
   mc_pair_t pair_test;
   int pair_found = 0;
@@ -263,6 +243,8 @@ static void remove_acceptance_pair(mc_pair_t pair){
     }
   }
 
     }
   }
 
+  if(!raw_mem_set)
+    MC_UNSET_RAW_MEM;
 }
 
 static int is_visited_pair(mc_pair_t pair){
 }
 
 static int is_visited_pair(mc_pair_t pair){
@@ -272,203 +254,94 @@ static int is_visited_pair(mc_pair_t pair){
 
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 
 
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 
+  MC_SET_RAW_MEM;
+
   if(xbt_dynar_is_empty(visited_pairs)){
 
   if(xbt_dynar_is_empty(visited_pairs)){
 
-    MC_SET_RAW_MEM;
     if(pair->graph_state->system_state == NULL)
       pair->graph_state->system_state = MC_take_snapshot();
     xbt_dynar_push(visited_pairs, &pair); 
     if(pair->graph_state->system_state == NULL)
       pair->graph_state->system_state = MC_take_snapshot();
     xbt_dynar_push(visited_pairs, &pair); 
-    MC_UNSET_RAW_MEM;
 
 
-    if(raw_mem_set)
-      MC_SET_RAW_MEM;
+    if(!raw_mem_set)
+      MC_UNSET_RAW_MEM;
 
     return -1;
 
   }else{
 
 
     return -1;
 
   }else{
 
-    MC_SET_RAW_MEM;
-
     if(pair->graph_state->system_state == NULL)
       pair->graph_state->system_state = MC_take_snapshot();
     if(pair->graph_state->system_state == NULL)
       pair->graph_state->system_state = MC_take_snapshot();
-    
-    size_t current_bytes_used = pair->heap_bytes_used;
-    int current_nb_processes = pair->nb_processes;
-
-    unsigned int cursor = 0;
-    int previous_cursor = 0, next_cursor = 0;
-    int start = 0;
-    int end = xbt_dynar_length(visited_pairs) - 1;
-
-    mc_pair_t pair_test = NULL;
-    size_t bytes_used_test;
-    int nb_processes_test;
-    int same_processes_and_bytes_not_found = 1;
 
 
-    while(start <= end && same_processes_and_bytes_not_found){
-      cursor = (start + end) / 2;
-      pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, cursor, mc_pair_t);
-      bytes_used_test = pair_test->heap_bytes_used;
-      nb_processes_test = pair_test->nb_processes;
-      if(nb_processes_test < current_nb_processes)
-        start = cursor + 1;
-      else if(nb_processes_test > current_nb_processes)
-        end = cursor - 1; 
-      else if(nb_processes_test == current_nb_processes){
-        if(bytes_used_test < current_bytes_used)
-          start = cursor + 1;
-        else if(bytes_used_test > current_bytes_used)
-          end = cursor - 1;
-        else if(bytes_used_test == current_bytes_used){
-          same_processes_and_bytes_not_found = 0;
-          if(xbt_automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){
-            if(xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, pair->atomic_propositions) == 0){
-              if(snapshot_compare(pair->graph_state->system_state, pair_test->graph_state->system_state) == 0){
-                if(pair_test->other_num == -1)
-                  pair->other_num = pair_test->num;
-                else
-                  pair->other_num = pair_test->other_num;
-                if(dot_output == NULL)
-                  XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", pair->num, pair_test->num);
-                else
-                  XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", pair->num, pair_test->num, pair->other_num);
-                xbt_dynar_remove_at(visited_pairs, cursor, NULL);
-                xbt_dynar_insert_at(visited_pairs, cursor, &pair);
-                pair_test->visited_removed = 1;
-                if(pair_test->stack_removed && pair_test->visited_removed){
-                  if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
-                    if(pair_test->acceptance_removed){ 
-                      MC_pair_delete(pair_test);
-                    }
-                  }else{
-                    MC_pair_delete(pair_test);
-                  }     
-                }
-                if(raw_mem_set)
-                  MC_SET_RAW_MEM;
-                else
-                  MC_UNSET_RAW_MEM;
-                return pair->other_num;
-              }
-            }
-          }
-          /* Search another pair with same number of bytes used in std_heap */
-          previous_cursor = cursor - 1;
-          while(previous_cursor >= 0){
-            pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, previous_cursor, mc_pair_t);
-            bytes_used_test = pair_test->heap_bytes_used;
-            if(bytes_used_test != current_bytes_used)
-              break;
-            if(xbt_automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){
-              if(xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, pair->atomic_propositions) == 0){  
-                if(snapshot_compare(pair->graph_state->system_state, pair_test->graph_state->system_state) == 0){
-                  if(pair_test->other_num == -1)
-                    pair->other_num = pair_test->num;
-                  else
-                    pair->other_num = pair_test->other_num;
-                  if(dot_output == NULL)
-                    XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", pair->num, pair_test->num);
-                  else
-                    XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", pair->num, pair_test->num, pair->other_num);
-                  xbt_dynar_remove_at(visited_pairs, previous_cursor, NULL);
-                  xbt_dynar_insert_at(visited_pairs, previous_cursor, &pair);
-                  pair_test->visited_removed = 1;
-                  if(pair_test->stack_removed && pair_test->visited_removed){
-                    if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
-                      if(pair_test->acceptance_removed){ 
-                        MC_pair_delete(pair_test);
-                      }
-                    }else{
-                      MC_pair_delete(pair_test);
-                    }     
-                  }
-                  if(raw_mem_set)
-                    MC_SET_RAW_MEM;
-                  else
-                    MC_UNSET_RAW_MEM;
-                  return pair->other_num;
-                }
-              }
-            }
-            previous_cursor--;
-          }
-          next_cursor = cursor + 1;
-          while(next_cursor < xbt_dynar_length(visited_pairs)){
-            pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, next_cursor, mc_pair_t);
-            bytes_used_test = pair_test->heap_bytes_used;
-            if(bytes_used_test != current_bytes_used)
-              break;
-            if(xbt_automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){
-              if(xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, pair->atomic_propositions) == 0){
-                if(snapshot_compare(pair->graph_state->system_state, pair_test->graph_state->system_state) == 0){
-                  if(pair_test->other_num == -1)
-                    pair->other_num = pair_test->num;
-                  else
-                    pair->other_num = pair_test->other_num;
-                  if(dot_output == NULL)
-                    XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", pair->num, pair_test->num);
-                  else
-                    XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", pair->num, pair_test->num, pair->other_num);
-                  xbt_dynar_remove_at(visited_pairs, next_cursor, NULL);
-                  xbt_dynar_insert_at(visited_pairs, next_cursor, &pair);
-                  pair_test->visited_removed = 1;
-                  if(pair_test->stack_removed && pair_test->visited_removed){
-                    if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
-                      if(pair_test->acceptance_removed){ 
-                        MC_pair_delete(pair_test);
-                      }
-                    }else{
-                      MC_pair_delete(pair_test);
-                    }     
-                  }
-                  if(raw_mem_set)
-                    MC_SET_RAW_MEM;
-                  else
-                    MC_UNSET_RAW_MEM;
-                  return pair->other_num;
-                }
-              }
+    int min = -1, max = -1, index;
+    int res;
+    mc_pair_t pair_test;
+
+    index = get_search_interval(visited_pairs, pair, &min, &max);
+
+    if(min != -1 && max != -1){ /* Visited pair with same number of processes and same heap bytes used exists */
+      res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_pairs, min), (max-min)+1, pair);
+      if(res != -1){
+        pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, (min+res)-1, mc_pair_t);
+        if(pair_test->other_num == -1)
+          pair->other_num = pair_test->num;
+        else
+          pair->other_num = pair_test->other_num;
+        if(dot_output == NULL)
+          XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", pair->num, pair_test->num);
+        else
+          XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", pair->num, pair_test->num, pair->other_num);
+        xbt_dynar_remove_at(visited_pairs, (min + res) - 1, NULL);
+        xbt_dynar_insert_at(visited_pairs, (min+res) - 1, &pair);
+        pair_test->visited_removed = 1;
+        if(pair_test->stack_removed && pair_test->visited_removed){
+          if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
+            if(pair_test->acceptance_removed){
+              MC_pair_delete(pair_test);
             }
             }
-            next_cursor++;
+          }else{
+            MC_pair_delete(pair_test);
           }
         }
           }
         }
+        if(!raw_mem_set)
+          MC_UNSET_RAW_MEM;
+        return pair->other_num;
+      }
+      xbt_dynar_insert_at(visited_pairs, min, &pair);
+    }else{
+      pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, index, mc_pair_t);
+      if(pair_test->nb_processes < pair->nb_processes){
+        xbt_dynar_insert_at(visited_pairs, index+1, &pair);
+      }else{
+        if(pair_test->heap_bytes_used < pair->heap_bytes_used)
+          xbt_dynar_insert_at(visited_pairs, index + 1, &pair);
+        else
+          xbt_dynar_insert_at(visited_pairs, index, &pair);
       }
     }
 
       }
     }
 
-    pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, cursor, mc_pair_t);
-    bytes_used_test = pair_test->heap_bytes_used;
-
-    if(bytes_used_test < current_bytes_used)
-      xbt_dynar_insert_at(visited_pairs, cursor + 1, &pair);
-    else
-      xbt_dynar_insert_at(visited_pairs, cursor, &pair);
-
     if(xbt_dynar_length(visited_pairs) > _sg_mc_visited){
       int min = mc_stats->expanded_states;
       unsigned int cursor2 = 0;
     if(xbt_dynar_length(visited_pairs) > _sg_mc_visited){
       int min = mc_stats->expanded_states;
       unsigned int cursor2 = 0;
-      unsigned int index = 0;
+      unsigned int index2 = 0;
       xbt_dynar_foreach(visited_pairs, cursor2, pair_test){
         if(pair_test->num < min){
           index = cursor2;
           min = pair_test->num;
         }
       }
       xbt_dynar_foreach(visited_pairs, cursor2, pair_test){
         if(pair_test->num < min){
           index = cursor2;
           min = pair_test->num;
         }
       }
-      xbt_dynar_remove_at(visited_pairs, index, &pair_test);
+      xbt_dynar_remove_at(visited_pairs, index2, &pair_test);
       pair_test->visited_removed = 1;
       if(pair_test->stack_removed && pair_test->acceptance_removed && pair_test->visited_removed)
         MC_pair_delete(pair_test);
       
     }
 
       pair_test->visited_removed = 1;
       if(pair_test->stack_removed && pair_test->acceptance_removed && pair_test->visited_removed)
         MC_pair_delete(pair_test);
       
     }
 
-    MC_UNSET_RAW_MEM;
-
-    if(raw_mem_set)
-      MC_SET_RAW_MEM;
+    if(!raw_mem_set)
+      MC_UNSET_RAW_MEM;
     
     return -1;
     
     return -1;
-    
+
   }
   }
 }
 
 static int MC_automaton_evaluate_label(xbt_automaton_exp_label_t l, xbt_dynar_t atomic_propositions_values){
 }
 
 static int MC_automaton_evaluate_label(xbt_automaton_exp_label_t l, xbt_dynar_t atomic_propositions_values){
@@ -625,7 +498,7 @@ void MC_ddfs(){
   /* Update current state in buchi automaton */
   _mc_property_automaton->current_state = current_pair->automaton_state;
 
   /* Update current state in buchi automaton */
   _mc_property_automaton->current_state = current_pair->automaton_state;
 
-  XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), current_pair->search_cycle);
+  XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d, interleave size %d)", xbt_fifo_size(mc_stack_liveness), current_pair->search_cycle, MC_state_interleave_size(current_pair->graph_state));
  
   mc_stats->visited_pairs++;
 
  
   mc_stats->visited_pairs++;
 
index 596e5eb..c417ede 100644 (file)
@@ -23,6 +23,7 @@
 #include "msg/msg.h"
 #include "msg/datatypes.h"
 #include "xbt/strbuff.h"
 #include "msg/msg.h"
 #include "msg/datatypes.h"
 #include "xbt/strbuff.h"
+#include "xbt/parmap.h"
 
 /****************************** Snapshots ***********************************/
 
 
 /****************************** Snapshots ***********************************/
 
@@ -75,6 +76,7 @@ extern xbt_dynar_t mc_checkpoint_ignore;
 extern double *mc_time;
 extern FILE *dot_output;
 extern const char* colors[13];
 extern double *mc_time;
 extern FILE *dot_output;
 extern const char* colors[13];
+extern xbt_parmap_t parmap;
 
 extern int user_max_depth_reached;
 
 
 extern int user_max_depth_reached;
 
@@ -249,10 +251,10 @@ typedef struct s_mc_comparison_times{
   double hash_local_variables_comparison_time;
 }s_mc_comparison_times_t, *mc_comparison_times_t;
 
   double hash_local_variables_comparison_time;
 }s_mc_comparison_times_t, *mc_comparison_times_t;
 
-extern mc_comparison_times_t mc_comp_times;
-extern double mc_snapshot_comparison_time;
+extern __thread mc_comparison_times_t mc_comp_times;
+extern __thread double mc_snapshot_comparison_time;
 
 
-int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2);
+int snapshot_compare(void *p1, void *p2);
 int SIMIX_pre_mc_compare_snapshots(smx_simcall_t simcall, mc_snapshot_t s1, mc_snapshot_t s2);
 void print_comparison_times(void);
 
 int SIMIX_pre_mc_compare_snapshots(smx_simcall_t simcall, mc_snapshot_t s1, mc_snapshot_t s2);
 void print_comparison_times(void);
 
index 2472c91..e522919 100644 (file)
@@ -169,7 +169,6 @@ void mfree(struct mdesc *mdp, void *ptr)
     /* Set size used in the fragment to -1 */
     mdp->heapinfo[block].busy_frag.frag_size[frag_nb] = -1;
     mdp->heapinfo[block].busy_frag.ignore[frag_nb] = 0;
     /* Set size used in the fragment to -1 */
     mdp->heapinfo[block].busy_frag.frag_size[frag_nb] = -1;
     mdp->heapinfo[block].busy_frag.ignore[frag_nb] = 0;
-    mdp->heapinfo[block].busy_frag.equal_to[frag_nb] = NULL;
 
 //    fprintf(stderr,"nfree:%zu capa:%d\n", mdp->heapinfo[block].busy_frag.nfree,(BLOCKSIZE >> type));
     if (mdp->heapinfo[block].busy_frag.nfree ==
 
 //    fprintf(stderr,"nfree:%zu capa:%d\n", mdp->heapinfo[block].busy_frag.nfree,(BLOCKSIZE >> type));
     if (mdp->heapinfo[block].busy_frag.nfree ==
@@ -181,7 +180,6 @@ void mfree(struct mdesc *mdp, void *ptr)
       mdp->heapinfo[block].type = 0;
       mdp->heapinfo[block].busy_block.size = 1;
       mdp->heapinfo[block].busy_block.busy_size = 0;
       mdp->heapinfo[block].type = 0;
       mdp->heapinfo[block].busy_block.size = 1;
       mdp->heapinfo[block].busy_block.busy_size = 0;
-      mdp->heapinfo[block].busy_block.equal_to = NULL;
             
       /* Keep the statistics accurate.  */
       mdp -> heapstats.chunks_used++;
             
       /* Keep the statistics accurate.  */
       mdp -> heapstats.chunks_used++;
index c501bcc..34f15e6 100644 (file)
@@ -129,10 +129,11 @@ static int compare_backtrace(int b1, int f1, int b2, int f2){
 /*********************************** Heap comparison ***********************************/
 /***************************************************************************************/
 
 /*********************************** Heap comparison ***********************************/
 /***************************************************************************************/
 
-void *s_heap = NULL, *heapbase1 = NULL, *heapbase2 = NULL;
-malloc_info *heapinfo1 = NULL, *heapinfo2 = NULL;
-size_t heaplimit = 0, heapsize1 = 0, heapsize2 = 0;
-xbt_dynar_t to_ignore1 = NULL, to_ignore2 = NULL;
+__thread void *s_heap = NULL, *heapbase1 = NULL, *heapbase2 = NULL;
+__thread malloc_info *heapinfo1 = NULL, *heapinfo2 = NULL;
+__thread size_t heaplimit = 0, heapsize1 = 0, heapsize2 = 0;
+__thread xbt_dynar_t to_ignore1 = NULL, to_ignore2 = NULL;
+__thread heap_area_t **equals_to1, **equals_to2;
 
 /*********************************** Free functions ************************************/
 
 
 /*********************************** Free functions ************************************/
 
@@ -246,40 +247,40 @@ static void match_equals(xbt_dynar_t list){
   xbt_dynar_foreach(list, cursor, current_pair){
 
     if(current_pair->fragment1 != -1){
   xbt_dynar_foreach(list, cursor, current_pair){
 
     if(current_pair->fragment1 != -1){
-      
-      if(heapinfo1[current_pair->block1].busy_frag.equal_to[current_pair->fragment1] != NULL){    
-        previous_area = heapinfo1[current_pair->block1].busy_frag.equal_to[current_pair->fragment1];
-        heap_area_free(heapinfo2[previous_area->block].busy_frag.equal_to[previous_area->fragment]);
-        heapinfo2[previous_area->block].busy_frag.equal_to[previous_area->fragment] = NULL;
-        heap_area_free(previous_area); 
+
+      if(equals_to1[current_pair->block1][current_pair->fragment1] != NULL){
+        previous_area = equals_to1[current_pair->block1][current_pair->fragment1];
+        heap_area_free(equals_to2[previous_area->block][previous_area->fragment]);
+        equals_to2[previous_area->block][previous_area->fragment] = NULL;
+        heap_area_free(previous_area);
       }
       }
-      if(heapinfo2[current_pair->block2].busy_frag.equal_to[current_pair->fragment2] != NULL){        
-        previous_area = heapinfo2[current_pair->block2].busy_frag.equal_to[current_pair->fragment2];
-        heap_area_free(heapinfo1[previous_area->block].busy_frag.equal_to[previous_area->fragment]);
-        heapinfo1[previous_area->block].busy_frag.equal_to[previous_area->fragment] = NULL;
+      if(equals_to2[current_pair->block2][current_pair->fragment2] != NULL){
+        previous_area = equals_to2[current_pair->block2][current_pair->fragment2];
+        heap_area_free(equals_to1[previous_area->block][previous_area->fragment]);
+        equals_to1[previous_area->block][previous_area->fragment] = NULL;
         heap_area_free(previous_area);
       }
 
         heap_area_free(previous_area);
       }
 
-      heapinfo1[current_pair->block1].busy_frag.equal_to[current_pair->fragment1] = new_heap_area(current_pair->block2, current_pair->fragment2);
-      heapinfo2[current_pair->block2].busy_frag.equal_to[current_pair->fragment2] = new_heap_area(current_pair->block1, current_pair->fragment1);
+      equals_to1[current_pair->block1][current_pair->fragment1] = new_heap_area(current_pair->block2, current_pair->fragment2);
+      equals_to2[current_pair->block2][current_pair->fragment2] = new_heap_area(current_pair->block1, current_pair->fragment1);
       
     }else{
 
       
     }else{
 
-      if(heapinfo1[current_pair->block1].busy_block.equal_to != NULL){
-        previous_area = heapinfo1[current_pair->block1].busy_block.equal_to;
-        heap_area_free(heapinfo2[previous_area->block].busy_block.equal_to);
-        heapinfo2[previous_area->block].busy_block.equal_to = NULL;
+      if(equals_to1[current_pair->block1][0] != NULL){
+        previous_area = equals_to1[current_pair->block1][0];
+        heap_area_free(equals_to2[previous_area->block][0]);
+        equals_to2[previous_area->block][0] = NULL;
         heap_area_free(previous_area);
       }
         heap_area_free(previous_area);
       }
-      if(heapinfo2[current_pair->block2].busy_block.equal_to != NULL){
-        previous_area = heapinfo2[current_pair->block2].busy_block.equal_to;
-        heap_area_free(heapinfo1[previous_area->block].busy_block.equal_to);
-        heapinfo1[previous_area->block].busy_block.equal_to = NULL;
+      if(equals_to2[current_pair->block2][0] != NULL){
+        previous_area = equals_to2[current_pair->block2][0];
+        heap_area_free(equals_to1[previous_area->block][0]);
+        equals_to1[previous_area->block][0] = NULL;
         heap_area_free(previous_area);
       }
 
         heap_area_free(previous_area);
       }
 
-      heapinfo1[current_pair->block1].busy_block.equal_to = new_heap_area(current_pair->block2, current_pair->fragment2);
-      heapinfo2[current_pair->block2].busy_block.equal_to = new_heap_area(current_pair->block1, current_pair->fragment1);
+      equals_to1[current_pair->block1][0] = new_heap_area(current_pair->block2, current_pair->fragment2);
+      equals_to2[current_pair->block2][0] = new_heap_area(current_pair->block1, current_pair->fragment1);
 
     }
 
 
     }
 
@@ -287,26 +288,27 @@ static void match_equals(xbt_dynar_t list){
 }
 
 static int equal_blocks(int b1, int b2){
 }
 
 static int equal_blocks(int b1, int b2){
-  if(heapinfo1[b1].busy_block.equal_to != NULL){
-    if(heapinfo2[b2].busy_block.equal_to != NULL){
-      if(((heap_area_t)(heapinfo1[b1].busy_block.equal_to))->block == b2 && ((heap_area_t)(heapinfo2[b2].busy_block.equal_to))->block == b1)
-        return 1;
-    }
-  }
+  
+  if(equals_to1[b1][0]->block == b2 && equals_to2[b2][0]->block == b1)
+    return 1;
+
   return 0;
 }
 
 static int equal_fragments(int b1, int f1, int b2, int f2){
   return 0;
 }
 
 static int equal_fragments(int b1, int f1, int b2, int f2){
-  if(heapinfo1[b1].busy_frag.equal_to[f1] != NULL){
-    if(heapinfo2[b2].busy_frag.equal_to[f2] != NULL){
-      if(((heap_area_t)(heapinfo1[b1].busy_frag.equal_to[f1]))->block == b2 && ((heap_area_t)(heapinfo2[b2].busy_frag.equal_to[f2]))->block == b1 && ((heap_area_t)(heapinfo1[b1].busy_frag.equal_to[f1]))->fragment == f2 && ((heap_area_t)(heapinfo2[b2].busy_frag.equal_to[f2]))->fragment == f1)
-        return 1;
-    }
-  }
+  
+  if(equals_to1[b1][f1]->block == b2 && equals_to1[b1][f1]->fragment == f2 && equals_to2[b2][f2]->block == b1 && equals_to2[b2][f2]->fragment == f1)
+    return 1;
+
   return 0;
 }
 
   return 0;
 }
 
-void init_heap_information(xbt_mheap_t heap1, xbt_mheap_t heap2, xbt_dynar_t i1, xbt_dynar_t i2){
+int init_heap_information(xbt_mheap_t heap1, xbt_mheap_t heap2, xbt_dynar_t i1, xbt_dynar_t i2){
+
+  if((((struct mdesc *)heap1)->heaplimit != ((struct mdesc *)heap2)->heaplimit) || ((((struct mdesc *)heap1)->heapsize != ((struct mdesc *)heap2)->heapsize) ))
+    return -1;
+
+  int i, j;
 
   heaplimit = ((struct mdesc *)heap1)->heaplimit;
 
 
   heaplimit = ((struct mdesc *)heap1)->heaplimit;
 
@@ -324,6 +326,21 @@ void init_heap_information(xbt_mheap_t heap1, xbt_mheap_t heap2, xbt_dynar_t i1,
   to_ignore1 = i1;
   to_ignore2 = i2;
 
   to_ignore1 = i1;
   to_ignore2 = i2;
 
+  equals_to1 = malloc(heaplimit * sizeof(heap_area_t *));
+  for(i=0; i<=heaplimit; i++){
+    equals_to1[i] = malloc(MAX_FRAGMENT_PER_BLOCK * sizeof(heap_area_t));
+    for(j=0; j<MAX_FRAGMENT_PER_BLOCK; j++)
+      equals_to1[i][j] = NULL;
+  }
+
+
+  equals_to2 = malloc(heaplimit * sizeof(heap_area_t *));
+  for(i=0; i<=heaplimit; i++){
+    equals_to2[i] = malloc(MAX_FRAGMENT_PER_BLOCK * sizeof(heap_area_t));
+    for(j=0; j<MAX_FRAGMENT_PER_BLOCK; j++)
+      equals_to2[i][j] = NULL;
+  }
+
   if(MC_is_active()){
     MC_ignore_global_variable("heaplimit");
     MC_ignore_global_variable("s_heap");
   if(MC_is_active()){
     MC_ignore_global_variable("heaplimit");
     MC_ignore_global_variable("s_heap");
@@ -335,65 +352,47 @@ void init_heap_information(xbt_mheap_t heap1, xbt_mheap_t heap2, xbt_dynar_t i1,
     MC_ignore_global_variable("heapsize2");
     MC_ignore_global_variable("to_ignore1");
     MC_ignore_global_variable("to_ignore2");
     MC_ignore_global_variable("heapsize2");
     MC_ignore_global_variable("to_ignore1");
     MC_ignore_global_variable("to_ignore2");
+    MC_ignore_global_variable("equals_to1");
+    MC_ignore_global_variable("equals_to2");
   }
 
   }
 
+  return 0;
+
 }
 
 void reset_heap_information(){
 
   size_t i = 0, j;
 
 }
 
 void reset_heap_information(){
 
   size_t i = 0, j;
 
-  while(i<=heaplimit){
-    if(heapinfo1[i].type == 0){
-      heap_area_free(heapinfo1[i].busy_block.equal_to);
-      heapinfo1[i].busy_block.equal_to = NULL;
-    }else if(heapinfo1[i].type > 0){
-      for(j=0; j < (size_t) (BLOCKSIZE >> heapinfo1[i].type); j++){
-        heap_area_free(heapinfo1[i].busy_frag.equal_to[j]);
-        heapinfo1[i].busy_frag.equal_to[j] = NULL;
-      }
-    }
-    i++; 
+  for(i=0; i<heaplimit; i++){
+    for(j=0; j<MAX_FRAGMENT_PER_BLOCK;j++){
+      heap_area_free(equals_to1[i][j]);
+      equals_to1[i][j] = NULL;
+      heap_area_free(equals_to2[i][j]);
+      equals_to2[i][j] = NULL;
+    }    
   }
 
   }
 
-  i = 0;
-
-  while(i<=heaplimit){
-    if(heapinfo2[i].type == 0){
-      heap_area_free(heapinfo2[i].busy_block.equal_to);
-      heapinfo2[i].busy_block.equal_to = NULL;
-    }else if(heapinfo2[i].type > 0){
-      for(j=0; j < (size_t) (BLOCKSIZE >> heapinfo2[i].type); j++){
-        heap_area_free(heapinfo2[i].busy_frag.equal_to[j]);
-        heapinfo2[i].busy_frag.equal_to[j] = NULL;
-      }
-    }
-    i++; 
-  }
+  free(equals_to1);
+  free(equals_to2);
 
   s_heap = NULL, heapbase1 = NULL, heapbase2 = NULL;
   heapinfo1 = NULL, heapinfo2 = NULL;
   heaplimit = 0, heapsize1 = 0, heapsize2 = 0;
   to_ignore1 = NULL, to_ignore2 = NULL;
 
   s_heap = NULL, heapbase1 = NULL, heapbase2 = NULL;
   heapinfo1 = NULL, heapinfo2 = NULL;
   heaplimit = 0, heapsize1 = 0, heapsize2 = 0;
   to_ignore1 = NULL, to_ignore2 = NULL;
+  equals_to1 = NULL, equals_to2 = NULL;
 
 }
 
 int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){
 
 
 }
 
 int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){
 
-  if(heap1 == NULL && heap1 == NULL){
+  if(heap1 == NULL && heap2 == NULL){
     XBT_DEBUG("Malloc descriptors null");
     return 0;
   }
 
     XBT_DEBUG("Malloc descriptors null");
     return 0;
   }
 
-  if(heap1->heaplimit != heap2->heaplimit){
-    XBT_DEBUG("Different limit of valid info table indices");
-    return 1;
-  }
-
   /* Start comparison */
   size_t i1, i2, j1, j2, k;
   /* Start comparison */
   size_t i1, i2, j1, j2, k;
-  size_t current_block = -1;    /* avoid "maybe uninitialized" warning */
-  size_t current_fragment;
   void *addr_block1, *addr_block2, *addr_frag1, *addr_frag2;
   int nb_diff1 = 0, nb_diff2 = 0;
 
   void *addr_block1, *addr_block2, *addr_frag1, *addr_frag2;
   int nb_diff1 = 0, nb_diff2 = 0;
 
@@ -407,8 +406,6 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){
 
   while(i1 <= heaplimit){
 
 
   while(i1 <= heaplimit){
 
-    current_block = i1;
-
     if(heapinfo1[i1].type == -1){ /* Free block */
       i1++;
       continue;
     if(heapinfo1[i1].type == -1){ /* Free block */
       i1++;
       continue;
@@ -420,14 +417,14 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){
       
       if(is_stack(addr_block1)){
         for(k=0; k < heapinfo1[i1].busy_block.size; k++)
       
       if(is_stack(addr_block1)){
         for(k=0; k < heapinfo1[i1].busy_block.size; k++)
-          heapinfo1[i1+k].busy_block.equal_to = new_heap_area(i1, -1);
+          equals_to1[i1+k][0] = new_heap_area(i1, -1);
         for(k=0; k < heapinfo2[i1].busy_block.size; k++)
         for(k=0; k < heapinfo2[i1].busy_block.size; k++)
-          heapinfo2[i1+k].busy_block.equal_to = new_heap_area(i1, -1);
-        i1 = i1 + heapinfo1[current_block].busy_block.size;
+          equals_to2[i1+k][0] = new_heap_area(i1, -1);
+        i1 += heapinfo1[i1].busy_block.size;
         continue;
       }
 
         continue;
       }
 
-      if(heapinfo1[i1].busy_block.equal_to != NULL){
+      if(equals_to1[i1][0] != NULL){
         i1++;
         continue;
       }
         i1++;
         continue;
       }
@@ -437,21 +434,21 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){
       res_compare = 0;
   
       /* Try first to associate to same block in the other heap */
       res_compare = 0;
   
       /* Try first to associate to same block in the other heap */
-      if(heapinfo2[current_block].type == heapinfo1[current_block].type){
+      if(heapinfo2[i1].type == heapinfo1[i1].type){
 
 
-        if(heapinfo2[current_block].busy_block.equal_to == NULL){  
-        
-          addr_block2 = ((void*) (((ADDR2UINT(current_block)) - 1) * BLOCKSIZE + (char*)((xbt_mheap_t)s_heap)->heapbase));
+        if(equals_to2[i1][0] == NULL){
+
+          addr_block2 = ((void*) (((ADDR2UINT(i1)) - 1) * BLOCKSIZE + (char*)((xbt_mheap_t)s_heap)->heapbase));
         
         
-          res_compare = compare_heap_area(addr_block1, addr_block2, NULL, NULL, NULL, NULL, 0); /*FIXME*/
+          res_compare = compare_heap_area(addr_block1, addr_block2, NULL, NULL, NULL, NULL, 0);
         
           if(res_compare == 0){
         
           if(res_compare == 0){
-            for(k=1; k < heapinfo2[current_block].busy_block.size; k++)
-              heapinfo2[current_block+k].busy_block.equal_to = new_heap_area(i1, -1);
-            for(k=1; k < heapinfo1[current_block].busy_block.size; k++)
-              heapinfo1[current_block+k].busy_block.equal_to = new_heap_area(i1, -1);
+            for(k=1; k < heapinfo2[i1].busy_block.size; k++)
+              equals_to2[i1+k][0] = new_heap_area(i1, -1);
+            for(k=1; k < heapinfo1[i1].busy_block.size; k++)
+              equals_to1[i1+k][0] = new_heap_area(i1, -1);
             equal = 1;
             equal = 1;
-            i1 = i1 + heapinfo1[current_block].busy_block.size;
+            i1 += heapinfo1[i1].busy_block.size;
           }
         
           xbt_dynar_reset(previous);
           }
         
           xbt_dynar_reset(previous);
@@ -464,7 +461,7 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){
 
         addr_block2 = ((void*) (((ADDR2UINT(i2)) - 1) * BLOCKSIZE + (char*)((xbt_mheap_t)s_heap)->heapbase));        
            
 
         addr_block2 = ((void*) (((ADDR2UINT(i2)) - 1) * BLOCKSIZE + (char*)((xbt_mheap_t)s_heap)->heapbase));        
            
-        if(i2 == current_block){
+        if(i2 == i1){
           i2++;
           continue;
         }
           i2++;
           continue;
         }
@@ -473,21 +470,21 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){
           i2++;
           continue;
         }
           i2++;
           continue;
         }
-
-        if(heapinfo2[i2].busy_block.equal_to != NULL){         
+    
+        if(equals_to2[i2][0] != NULL){  
           i2++;
           continue;
         }
           
           i2++;
           continue;
         }
           
-        res_compare = compare_heap_area(addr_block1, addr_block2, NULL, NULL, NULL, NULL, 0); /*FIXME */
+        res_compare = compare_heap_area(addr_block1, addr_block2, NULL, NULL, NULL, NULL, 0);
         
         if(res_compare == 0){
           for(k=1; k < heapinfo2[i2].busy_block.size; k++)
         
         if(res_compare == 0){
           for(k=1; k < heapinfo2[i2].busy_block.size; k++)
-            heapinfo2[i2+k].busy_block.equal_to = new_heap_area(i1, -1);
+            equals_to2[i2+k][0] = new_heap_area(i1, -1);
           for(k=1; k < heapinfo1[i1].busy_block.size; k++)
           for(k=1; k < heapinfo1[i1].busy_block.size; k++)
-            heapinfo1[i1+k].busy_block.equal_to = new_heap_area(i2, -1);
+            equals_to1[i1+k][0] = new_heap_area(i2, -1);
           equal = 1;
           equal = 1;
-          i1 = i1 + heapinfo1[i1].busy_block.size;
+          i1 += heapinfo1[i1].busy_block.size;
         }
 
         xbt_dynar_reset(previous);
         }
 
         xbt_dynar_reset(previous);
@@ -507,12 +504,10 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){
 
       for(j1=0; j1 < (size_t) (BLOCKSIZE >> heapinfo1[i1].type); j1++){
 
 
       for(j1=0; j1 < (size_t) (BLOCKSIZE >> heapinfo1[i1].type); j1++){
 
-        current_fragment = j1;
-
         if(heapinfo1[i1].busy_frag.frag_size[j1] == -1) /* Free fragment */
           continue;
 
         if(heapinfo1[i1].busy_frag.frag_size[j1] == -1) /* Free fragment */
           continue;
 
-        if(heapinfo1[i1].busy_frag.equal_to[j1] != NULL)
+        if(equals_to1[i1][j1] != NULL)
           continue;
 
         addr_frag1 = (void*) ((char *)addr_block1 + (j1 << heapinfo1[i1].type));
           continue;
 
         addr_frag1 = (void*) ((char *)addr_block1 + (j1 << heapinfo1[i1].type));
@@ -521,14 +516,14 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){
         equal = 0;
         
         /* Try first to associate to same fragment in the other heap */
         equal = 0;
         
         /* Try first to associate to same fragment in the other heap */
-        if(heapinfo2[current_block].type == heapinfo1[current_block].type){
+        if(heapinfo2[i1].type == heapinfo1[i1].type){
 
 
-          if(heapinfo2[current_block].busy_frag.equal_to[current_fragment] == NULL){  
-          
-            addr_block2 = ((void*) (((ADDR2UINT(current_block)) - 1) * BLOCKSIZE + (char*)((xbt_mheap_t)s_heap)->heapbase));
-            addr_frag2 = (void*) ((char *)addr_block2 + (current_fragment << ((xbt_mheap_t)s_heap)->heapinfo[current_block].type));
+          if(equals_to2[i1][j1] == NULL){
 
 
-            res_compare = compare_heap_area(addr_frag1, addr_frag2, NULL, NULL, NULL, NULL, 0); /*FIXME*/
+            addr_block2 = ((void*) (((ADDR2UINT(i1)) - 1) * BLOCKSIZE + (char*)((xbt_mheap_t)s_heap)->heapbase));
+            addr_frag2 = (void*) ((char *)addr_block2 + (j1 << ((xbt_mheap_t)s_heap)->heapinfo[i1].type));
+
+            res_compare = compare_heap_area(addr_frag1, addr_frag2, NULL, NULL, NULL, NULL, 0);
 
             if(res_compare == 0)
               equal = 1;
 
             if(res_compare == 0)
               equal = 1;
@@ -541,7 +536,6 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){
 
         while(i2 <= heaplimit && !equal){
 
 
         while(i2 <= heaplimit && !equal){
 
-          
           if(heapinfo2[i2].type <= 0){
             i2++;
             continue;
           if(heapinfo2[i2].type <= 0){
             i2++;
             continue;
@@ -549,16 +543,16 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){
 
           for(j2=0; j2 < (size_t) (BLOCKSIZE >> heapinfo2[i2].type); j2++){
 
 
           for(j2=0; j2 < (size_t) (BLOCKSIZE >> heapinfo2[i2].type); j2++){
 
-            if(i2 == current_block && j2 == current_fragment)
+            if(i2 == i1 && j2 == j1)
+              continue;
+           
+            if(equals_to2[i2][j2] != NULL)
               continue;
               continue;
-
-            if(heapinfo2[i2].busy_frag.equal_to[j2] != NULL)                
-              continue;            
                           
             addr_block2 = ((void*) (((ADDR2UINT(i2)) - 1) * BLOCKSIZE + (char*)((xbt_mheap_t)s_heap)->heapbase));
                           
             addr_block2 = ((void*) (((ADDR2UINT(i2)) - 1) * BLOCKSIZE + (char*)((xbt_mheap_t)s_heap)->heapbase));
-            addr_frag2 = (void*) ((char *)addr_block2 + (j2 << ((xbt_mheap_t)s_heap)->heapinfo[i2].type));
+            addr_frag2 = (void*) ((char *)addr_block2 + (j2 <<((xbt_mheap_t)s_heap)->heapinfo[i2].type));
 
 
-            res_compare = compare_heap_area(addr_frag1, addr_frag2, NULL, NULL, NULL, NULL, 0); /*FIXME*/
+            res_compare = compare_heap_area(addr_frag1, addr_frag2, NULL, NULL, NULL, NULL, 0);
             
             if(res_compare == 0){
               equal = 1;
             
             if(res_compare == 0){
               equal = 1;
@@ -574,8 +568,8 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){
 
         }
 
 
         }
 
-        if(heapinfo1[i1].busy_frag.equal_to[j1] == NULL){
-          XBT_DEBUG("Block %zu, fragment %zu not found (size_used = %zd, address = %p, ignore %d)\n", i1, j1, heapinfo1[i1].busy_frag.frag_size[j1], addr_frag1, heapinfo1[i1].busy_frag.ignore[j1]);
+        if(!equal){
+          XBT_DEBUG("Block %zu, fragment %zu not found (size_used = %zd, address = %p)\n", i1, j1, heapinfo1[i1].busy_frag.frag_size[j1], addr_frag1);
           i2 = heaplimit + 1;
           i1 = heaplimit + 1;
           nb_diff1++;
           i2 = heaplimit + 1;
           i1 = heaplimit + 1;
           nb_diff1++;
@@ -596,9 +590,9 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){
  
   while(i<=heaplimit){
     if(heapinfo1[i].type == 0){
  
   while(i<=heaplimit){
     if(heapinfo1[i].type == 0){
-      if(current_block == heaplimit){
+      if(i1 == heaplimit){
         if(heapinfo1[i].busy_block.busy_size > 0){
         if(heapinfo1[i].busy_block.busy_size > 0){
-          if(heapinfo1[i].busy_block.equal_to == NULL){
+          if(equals_to1[i][0] == NULL){            
             if(XBT_LOG_ISENABLED(mm_diff, xbt_log_priority_debug)){
               addr_block1 = ((void*) (((ADDR2UINT(i)) - 1) * BLOCKSIZE + (char*)heapbase1));
               XBT_DEBUG("Block %zu (%p) not found (size used = %zu)", i, addr_block1, heapinfo1[i].busy_block.busy_size);
             if(XBT_LOG_ISENABLED(mm_diff, xbt_log_priority_debug)){
               addr_block1 = ((void*) (((ADDR2UINT(i)) - 1) * BLOCKSIZE + (char*)heapbase1));
               XBT_DEBUG("Block %zu (%p) not found (size used = %zu)", i, addr_block1, heapinfo1[i].busy_block.busy_size);
@@ -613,9 +607,9 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){
       addr_block1 = ((void*) (((ADDR2UINT(i)) - 1) * BLOCKSIZE + (char*)heapbase1));
       real_addr_block1 =  ((void*) (((ADDR2UINT(i)) - 1) * BLOCKSIZE + (char*)((struct mdesc *)s_heap)->heapbase));
       for(j=0; j < (size_t) (BLOCKSIZE >> heapinfo1[i].type); j++){
       addr_block1 = ((void*) (((ADDR2UINT(i)) - 1) * BLOCKSIZE + (char*)heapbase1));
       real_addr_block1 =  ((void*) (((ADDR2UINT(i)) - 1) * BLOCKSIZE + (char*)((struct mdesc *)s_heap)->heapbase));
       for(j=0; j < (size_t) (BLOCKSIZE >> heapinfo1[i].type); j++){
-        if(current_block == heaplimit){
+        if(i1== heaplimit){
           if(heapinfo1[i].busy_frag.frag_size[j] > 0){
           if(heapinfo1[i].busy_frag.frag_size[j] > 0){
-            if(heapinfo1[i].busy_frag.equal_to[j] == NULL){
+            if(equals_to1[i][j] == NULL){
               if(XBT_LOG_ISENABLED(mm_diff, xbt_log_priority_debug)){
                 addr_frag1 = (void*) ((char *)addr_block1 + (j << heapinfo1[i].type));
                 real_addr_frag1 = (void*) ((char *)real_addr_block1 + (j << ((struct mdesc *)s_heap)->heapinfo[i].type));
               if(XBT_LOG_ISENABLED(mm_diff, xbt_log_priority_debug)){
                 addr_frag1 = (void*) ((char *)addr_block1 + (j << heapinfo1[i].type));
                 real_addr_frag1 = (void*) ((char *)real_addr_block1 + (j << ((struct mdesc *)s_heap)->heapinfo[i].type));
@@ -631,16 +625,16 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){
     i++; 
   }
 
     i++; 
   }
 
-  if(current_block == heaplimit)
+  if(i1 == heaplimit)
     XBT_DEBUG("Number of blocks/fragments not found in heap1 : %d", nb_diff1);
 
   i = 1;
 
   while(i<=heaplimit){
     if(heapinfo2[i].type == 0){
     XBT_DEBUG("Number of blocks/fragments not found in heap1 : %d", nb_diff1);
 
   i = 1;
 
   while(i<=heaplimit){
     if(heapinfo2[i].type == 0){
-      if(current_block == heaplimit){
+      if(i1 == heaplimit){
         if(heapinfo2[i].busy_block.busy_size > 0){
         if(heapinfo2[i].busy_block.busy_size > 0){
-          if(heapinfo2[i].busy_block.equal_to == NULL){
+          if(equals_to2[i][0] == NULL){
             if(XBT_LOG_ISENABLED(mm_diff, xbt_log_priority_debug)){
               addr_block2 = ((void*) (((ADDR2UINT(i)) - 1) * BLOCKSIZE + (char*)heapbase2));
               XBT_DEBUG("Block %zu (%p) not found (size used = %zu)", i, addr_block2, heapinfo2[i].busy_block.busy_size);
             if(XBT_LOG_ISENABLED(mm_diff, xbt_log_priority_debug)){
               addr_block2 = ((void*) (((ADDR2UINT(i)) - 1) * BLOCKSIZE + (char*)heapbase2));
               XBT_DEBUG("Block %zu (%p) not found (size used = %zu)", i, addr_block2, heapinfo2[i].busy_block.busy_size);
@@ -655,9 +649,9 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){
       addr_block2 = ((void*) (((ADDR2UINT(i)) - 1) * BLOCKSIZE + (char*)heapbase2));
       real_addr_block2 =  ((void*) (((ADDR2UINT(i)) - 1) * BLOCKSIZE + (char*)((struct mdesc *)s_heap)->heapbase));
       for(j=0; j < (size_t) (BLOCKSIZE >> heapinfo2[i].type); j++){
       addr_block2 = ((void*) (((ADDR2UINT(i)) - 1) * BLOCKSIZE + (char*)heapbase2));
       real_addr_block2 =  ((void*) (((ADDR2UINT(i)) - 1) * BLOCKSIZE + (char*)((struct mdesc *)s_heap)->heapbase));
       for(j=0; j < (size_t) (BLOCKSIZE >> heapinfo2[i].type); j++){
-        if(current_block == heaplimit){
+        if(i1 == heaplimit){
           if(heapinfo2[i].busy_frag.frag_size[j] > 0){
           if(heapinfo2[i].busy_frag.frag_size[j] > 0){
-            if(heapinfo2[i].busy_frag.equal_to[j] == NULL){
+            if(equals_to2[i][j] == NULL){
               if(XBT_LOG_ISENABLED(mm_diff, xbt_log_priority_debug)){
                 addr_frag2 = (void*) ((char *)addr_block2 + (j << heapinfo2[i].type));
                 real_addr_frag2 = (void*) ((char *)real_addr_block2 + (j << ((struct mdesc *)s_heap)->heapinfo[i].type));
               if(XBT_LOG_ISENABLED(mm_diff, xbt_log_priority_debug)){
                 addr_frag2 = (void*) ((char *)addr_block2 + (j << heapinfo2[i].type));
                 real_addr_frag2 = (void*) ((char *)real_addr_block2 + (j << ((struct mdesc *)s_heap)->heapinfo[i].type));
@@ -673,7 +667,7 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){
     i++; 
   }
 
     i++; 
   }
 
-  if(current_block == heaplimit)
+  if(i1 == heaplimit)
     XBT_DEBUG("Number of blocks/fragments not found in heap2 : %d", nb_diff2);
 
   xbt_dynar_free(&previous);
     XBT_DEBUG("Number of blocks/fragments not found in heap2 : %d", nb_diff2);
 
   xbt_dynar_free(&previous);
@@ -757,7 +751,7 @@ static int compare_heap_area_with_type(void *real_area1, void *real_area2, void
     if((check_ignore > 0) && ((ignore1 = heap_comparison_ignore_size(to_ignore1, real_area1)) > 0) && ((ignore2 = heap_comparison_ignore_size(to_ignore2, real_area2))  == ignore1))
       return 0;
     if(strcmp(type->name, "char") == 0){ /* String, hence random (arbitrary ?) size */
     if((check_ignore > 0) && ((ignore1 = heap_comparison_ignore_size(to_ignore1, real_area1)) > 0) && ((ignore2 = heap_comparison_ignore_size(to_ignore2, real_area2))  == ignore1))
       return 0;
     if(strcmp(type->name, "char") == 0){ /* String, hence random (arbitrary ?) size */
-      return (memcmp(area1, area2, area_size) != 0);
+      return  (memcmp(area1, area2, area_size) != 0);
     }else{
       if(area_size != -1 && type->size != area_size)
         return -1;
     }else{
       if(area_size != -1 && type->size != area_size)
         return -1;
@@ -821,7 +815,7 @@ static int compare_heap_area_with_type(void *real_area1, void *real_area2, void
         res = compare_heap_area_with_type((char *)real_area1 + (i*elm_size), (char *)real_area2 + (i*elm_size), (char *)area1 + (i*elm_size), (char *)area2 + (i*elm_size), previous, other_types, all_types, type->dw_type_id, type->size, check_ignore, pointer_level);
       else
         res = compare_heap_area_with_type((char *)real_area1 + (i*elm_size), (char *)real_area2 + (i*elm_size), (char *)area1 + (i*elm_size), (char *)area2 + (i*elm_size), previous, all_types, other_types, type->dw_type_id, type->size, check_ignore, pointer_level);
         res = compare_heap_area_with_type((char *)real_area1 + (i*elm_size), (char *)real_area2 + (i*elm_size), (char *)area1 + (i*elm_size), (char *)area2 + (i*elm_size), previous, other_types, all_types, type->dw_type_id, type->size, check_ignore, pointer_level);
       else
         res = compare_heap_area_with_type((char *)real_area1 + (i*elm_size), (char *)real_area2 + (i*elm_size), (char *)area1 + (i*elm_size), (char *)area2 + (i*elm_size), previous, all_types, other_types, type->dw_type_id, type->size, check_ignore, pointer_level);
-      if(res != 0)
+      if(res == 1)
         return res;
     }
     break;
         return res;
     }
     break;
@@ -840,7 +834,7 @@ static int compare_heap_area_with_type(void *real_area1, void *real_area2, void
             res =  compare_heap_area(addr_pointed1, addr_pointed2, previous, all_types, other_types, type->dw_type_id, pointer_level); 
           else
             res =  (addr_pointed1 != addr_pointed2);
             res =  compare_heap_area(addr_pointed1, addr_pointed2, previous, all_types, other_types, type->dw_type_id, pointer_level); 
           else
             res =  (addr_pointed1 != addr_pointed2);
-          if(res != 0)
+          if(res == 1)
             return res;
         }
       }else{
             return res;
         }
       }else{
@@ -870,7 +864,7 @@ static int compare_heap_area_with_type(void *real_area1, void *real_area2, void
             res = compare_heap_area_with_type((char *)real_area1 + (i*type->size), (char *)real_area2 + (i*type->size), (char *)area1 + (i*type->size), (char *)area2 + (i*type->size), previous, other_types, all_types, type_id, -1, check_ignore, 0); 
           else
             res = compare_heap_area_with_type((char *)real_area1 + (i*type->size), (char *)real_area2 + (i*type->size), (char *)area1 + (i*type->size), (char *)area2 + (i*type->size), previous, all_types, other_types, type_id, -1, check_ignore, 0); 
             res = compare_heap_area_with_type((char *)real_area1 + (i*type->size), (char *)real_area2 + (i*type->size), (char *)area1 + (i*type->size), (char *)area2 + (i*type->size), previous, other_types, all_types, type_id, -1, check_ignore, 0); 
           else
             res = compare_heap_area_with_type((char *)real_area1 + (i*type->size), (char *)real_area2 + (i*type->size), (char *)area1 + (i*type->size), (char *)area2 + (i*type->size), previous, all_types, other_types, type_id, -1, check_ignore, 0); 
-          if(res != 0)
+          if(res == 1)
             return res;
         }
       }else{
             return res;
         }
       }else{
@@ -883,7 +877,7 @@ static int compare_heap_area_with_type(void *real_area1, void *real_area2, void
           res = compare_heap_area_with_type((char *)real_area1 + member->offset, (char *)real_area2 + member->offset, (char *)area1 + member->offset, (char *)area2 + member->offset, previous, other_types, all_types, member->dw_type_id, -1, check_ignore, 0);
         else
           res = compare_heap_area_with_type((char *)real_area1 + member->offset, (char *)real_area2 + member->offset, (char *)area1 + member->offset, (char *)area2 + member->offset, previous, all_types, other_types, member->dw_type_id, -1, check_ignore, 0);  
           res = compare_heap_area_with_type((char *)real_area1 + member->offset, (char *)real_area2 + member->offset, (char *)area1 + member->offset, (char *)area2 + member->offset, previous, other_types, all_types, member->dw_type_id, -1, check_ignore, 0);
         else
           res = compare_heap_area_with_type((char *)real_area1 + member->offset, (char *)real_area2 + member->offset, (char *)area1 + member->offset, (char *)area2 + member->offset, previous, all_types, other_types, member->dw_type_id, -1, check_ignore, 0);  
-        if(res != 0)
+        if(res == 1)
           return res;        
       }
     }
           return res;        
       }
     }
@@ -913,6 +907,8 @@ int compare_heap_area(void *area1, void* area2, xbt_dynar_t previous, xbt_dict_t
 
   void *addr_block1, *addr_block2, *addr_frag1, *addr_frag2;
   void *area1_to_compare, *area2_to_compare;
 
   void *addr_block1, *addr_block2, *addr_frag1, *addr_frag2;
   void *area1_to_compare, *area2_to_compare;
+  dw_type_t type = NULL;
+  char *type_desc;
 
   int match_pairs = 0;
 
 
   int match_pairs = 0;
 
@@ -943,125 +939,123 @@ int compare_heap_area(void *area1, void* area2, xbt_dynar_t previous, xbt_dict_t
   addr_block1 = ((void*) (((ADDR2UINT(block1)) - 1) * BLOCKSIZE + (char*)heapbase1));
   addr_block2 = ((void*) (((ADDR2UINT(block2)) - 1) * BLOCKSIZE + (char*)heapbase2));
   
   addr_block1 = ((void*) (((ADDR2UINT(block1)) - 1) * BLOCKSIZE + (char*)heapbase1));
   addr_block2 = ((void*) (((ADDR2UINT(block2)) - 1) * BLOCKSIZE + (char*)heapbase2));
   
-  if(heapinfo1[block1].type == heapinfo2[block2].type){
-    
-    if(heapinfo1[block1].type == -1){ /* Free block */
-      if(match_pairs){
-        match_equals(previous);
-        xbt_dynar_free(&previous);
-      }
-      return 0;
+  if((heapinfo1[block1].type == -1) && (heapinfo2[block2].type == -1)){  /* Free block */
 
 
-    }else if(heapinfo1[block1].type == 0){ /* Complete block */
+    if(match_pairs){
+      match_equals(previous);
+      xbt_dynar_free(&previous);
+    }
+    return 0;
 
 
-      if(heapinfo1[block1].busy_block.equal_to != NULL && heapinfo2[block2].busy_block.equal_to != NULL){
-        if(equal_blocks(block1, block2)){
-          if(match_pairs){
-            match_equals(previous);
-            xbt_dynar_free(&previous);
-          }
-          return 0;
-        }
-      }
+  }else if((heapinfo1[block1].type == 0) && (heapinfo2[block2].type == 0)){ /* Complete block */
 
 
-      if(heapinfo1[block1].busy_block.size != heapinfo2[block2].busy_block.size){
+    if(equals_to1[block1][0] != NULL && equals_to2[block2][0] != NULL){
+      if(equal_blocks(block1, block2)){
         if(match_pairs){
         if(match_pairs){
+          match_equals(previous);
           xbt_dynar_free(&previous);
         }
           xbt_dynar_free(&previous);
         }
-        return 1;
+        return 0;
       }
       }
+    }
 
 
-      if(heapinfo1[block1].busy_block.busy_size != heapinfo2[block2].busy_block.busy_size){
-        if(match_pairs){
-          xbt_dynar_free(&previous);
+    if(type_id){
+      type = xbt_dict_get_or_null(all_types, type_id);
+      if(strcmp(type->name, "char") ==0){
+        if(area1 == area2)
+          return -1;
+      }
+      if(type->size == 0){
+        type_desc = get_type_description(all_types, type->name);
+        if(type_desc)
+          type = xbt_dict_get_or_null(all_types, type_desc);
+        else
+          type = xbt_dict_get_or_null(other_types, get_type_description(other_types, type->name));
+      }
+      if(strcmp(type->name, "s_smx_context") != 0){
+        if(type->size > 1){
+          if(heapinfo1[block1].busy_block.busy_size != type->size && heapinfo2[block2].busy_block.busy_size  != type->size)
+            return -1;
         }
         }
-        return 1;
       }
       }
+    }
 
 
-      if(!add_heap_area_pair(previous, block1, -1, block2, -1)){
-        if(match_pairs){
-          match_equals(previous);
-          xbt_dynar_free(&previous);
-        }
-        return 0;
+    if(heapinfo1[block1].busy_block.size != heapinfo2[block2].busy_block.size){
+      if(match_pairs){
+        xbt_dynar_free(&previous);
+      }
+      return 1;
+    }
+
+    if(heapinfo1[block1].busy_block.busy_size != heapinfo2[block2].busy_block.busy_size){
+      if(match_pairs){
+        xbt_dynar_free(&previous);
       }
       }
+      return 1;
+    }
+
+    if(!add_heap_area_pair(previous, block1, -1, block2, -1)){
+      if(match_pairs){
+        match_equals(previous);
+        xbt_dynar_free(&previous);
+      }
+      return 0;
+    }
  
  
-      size = heapinfo1[block1].busy_block.busy_size;
+    size = heapinfo1[block1].busy_block.busy_size;
 
 
-      if(size <= 0){
-        if(match_pairs){
-          match_equals(previous);
-          xbt_dynar_free(&previous);
-        }
-        return 0;
+    if(size <= 0){
+      if(match_pairs){
+        match_equals(previous);
+        xbt_dynar_free(&previous);
       }
       }
+      return 0;
+    }
 
 
-      frag1 = -1;
-      frag2 = -1;
+    frag1 = -1;
+    frag2 = -1;
 
 
-      area1_to_compare = addr_block1;
-      area2_to_compare = addr_block2;
+    area1_to_compare = addr_block1;
+    area2_to_compare = addr_block2;
 
 
-      if((heapinfo1[block1].busy_block.ignore > 0) && (heapinfo2[block2].busy_block.ignore == heapinfo1[block1].busy_block.ignore))
-        check_ignore = heapinfo1[block1].busy_block.ignore;
+    if((heapinfo1[block1].busy_block.ignore > 0) && (heapinfo2[block2].busy_block.ignore == heapinfo1[block1].busy_block.ignore))
+      check_ignore = heapinfo1[block1].busy_block.ignore;
       
       
-    }else{ /* Frgamented block */
+  }else if((heapinfo1[block1].type > 0) && (heapinfo2[block2].type > 0)){ /* Fragmented block */
 
 
-      frag1 = ((uintptr_t) (ADDR2UINT (area1) % (BLOCKSIZE))) >> heapinfo1[block1].type;
-      frag2 = ((uintptr_t) (ADDR2UINT (area2) % (BLOCKSIZE))) >> heapinfo2[block2].type;
+    frag1 = ((uintptr_t) (ADDR2UINT (area1) % (BLOCKSIZE))) >> heapinfo1[block1].type;
+    frag2 = ((uintptr_t) (ADDR2UINT (area2) % (BLOCKSIZE))) >> heapinfo2[block2].type;
       
       
-      addr_frag1 = (void*) ((char *)addr_block1 + (frag1 << heapinfo1[block1].type));
-      addr_frag2 = (void*) ((char *)addr_block2 + (frag2 << heapinfo2[block2].type));
+    addr_frag1 = (void*) ((char *)addr_block1 + (frag1 << heapinfo1[block1].type));
+    addr_frag2 = (void*) ((char *)addr_block2 + (frag2 << heapinfo2[block2].type));
       
       
-      area1_to_compare = addr_frag1;
-      area2_to_compare = addr_frag2;
-
-      if(heapinfo1[block1].busy_frag.equal_to[frag1] != NULL && heapinfo2[block2].busy_frag.equal_to[frag2] != NULL){
-        if(equal_fragments(block1, frag1, block2, frag2)){
-          if(match_pairs){
-            match_equals(previous);
-            xbt_dynar_free(&previous);
-          }
-          return 0;
-        }
-      }
+    area1_to_compare = addr_frag1;
+    area2_to_compare = addr_frag2;
 
 
-      if(heapinfo1[block1].busy_frag.frag_size[frag1] != heapinfo2[block2].busy_frag.frag_size[frag2]){
-        if(match_pairs){
-          xbt_dynar_free(&previous);
-        }
-        return 1;  
+    if(type_id){
+      type = xbt_dict_get_or_null(all_types, type_id);
+      if(strcmp(type->name, "char") ==0){
+        if(area1 == area2)
+          return -1;
       }
       }
-      
-      if(!add_heap_area_pair(previous, block1, frag1, block2, frag2)){
-        if(match_pairs){
-          match_equals(previous);
-          xbt_dynar_free(&previous);
+      if(type->size == 0 || type->type == e_dw_pointer_type){
+        if(!type->dw_type_id){
+          type_desc = get_type_description(all_types, type->name);
+          if(type_desc)
+            type = xbt_dict_get_or_null(all_types, type_desc);
+          else
+            type = xbt_dict_get_or_null(other_types, get_type_description(other_types, type->name));
+        }else{
+          type = xbt_dict_get_or_null(all_types, type->dw_type_id);
         }
         }
-        return 0;
       }
       }
-
-      size = heapinfo1[block1].busy_frag.frag_size[frag1];
-
-      if(size <= 0){
-        if(match_pairs){
-          match_equals(previous);
-          xbt_dynar_free(&previous);
-        }
-        return 0;
+      if(type->size > 1){
+        if(heapinfo1[block1].busy_frag.frag_size[frag1] != type->size || heapinfo2[block2].busy_frag.frag_size[frag2]  != type->size)
+          return -1;
       }
       }
-      
-      if((heapinfo1[block1].busy_frag.ignore[frag1] > 0) && ( heapinfo2[block2].busy_frag.ignore[frag2] == heapinfo1[block1].busy_frag.ignore[frag1]))
-        check_ignore = heapinfo1[block1].busy_frag.ignore[frag1];
-      
     }
 
     }
 
-  }else if((heapinfo1[block1].type > 0) && (heapinfo2[block2].type > 0)){
-
-    frag1 = ((uintptr_t) (ADDR2UINT (area1) % (BLOCKSIZE))) >> heapinfo1[block1].type;
-    frag2 = ((uintptr_t) (ADDR2UINT (area2) % (BLOCKSIZE))) >> heapinfo2[block2].type;
-
-    if(heapinfo1[block1].busy_frag.equal_to[frag1] != NULL || heapinfo2[block2].busy_frag.equal_to[frag2] != NULL){
+    if(equals_to1[block1][frag1] != NULL && equals_to2[block2][frag2] != NULL){
       if(equal_fragments(block1, frag1, block2, frag2)){
         if(match_pairs){
           match_equals(previous);
       if(equal_fragments(block1, frag1, block2, frag2)){
         if(match_pairs){
           match_equals(previous);
@@ -1075,9 +1069,9 @@ int compare_heap_area(void *area1, void* area2, xbt_dynar_t previous, xbt_dict_t
       if(match_pairs){
         xbt_dynar_free(&previous);
       }
       if(match_pairs){
         xbt_dynar_free(&previous);
       }
-      return 1;
+      return 1;  
     }
     }
-    
+      
     if(!add_heap_area_pair(previous, block1, frag1, block2, frag2)){
       if(match_pairs){
         match_equals(previous);
     if(!add_heap_area_pair(previous, block1, frag1, block2, frag2)){
       if(match_pairs){
         match_equals(previous);
@@ -1086,12 +1080,6 @@ int compare_heap_area(void *area1, void* area2, xbt_dynar_t previous, xbt_dict_t
       return 0;
     }
 
       return 0;
     }
 
-    addr_frag1 = (void*) ((char *)addr_block1 + (frag1 << heapinfo1[block1].type));
-    addr_frag2 = (void*) ((char *)addr_block2 + (frag2 << heapinfo2[block2].type));
-
-    area1_to_compare = addr_frag1;
-    area2_to_compare = addr_frag2;
-      
     size = heapinfo1[block1].busy_frag.frag_size[frag1];
 
     if(size <= 0){
     size = heapinfo1[block1].busy_frag.frag_size[frag1];
 
     if(size <= 0){
@@ -1101,17 +1089,19 @@ int compare_heap_area(void *area1, void* area2, xbt_dynar_t previous, xbt_dict_t
       }
       return 0;
     }
       }
       return 0;
     }
-
-    if((heapinfo1[block1].busy_frag.ignore[frag1] > 0) && (heapinfo2[block2].busy_frag.ignore[frag2] == heapinfo1[block1].busy_frag.ignore[frag1]))
-      check_ignore = heapinfo1[block1].busy_frag.ignore[frag1];   
+      
+    if((heapinfo1[block1].busy_frag.ignore[frag1] > 0) && ( heapinfo2[block2].busy_frag.ignore[frag2] == heapinfo1[block1].busy_frag.ignore[frag1]))
+      check_ignore = heapinfo1[block1].busy_frag.ignore[frag1];
     
   }else{
     
   }else{
+
     if(match_pairs){
       xbt_dynar_free(&previous);
     }
     return 1;
     if(match_pairs){
       xbt_dynar_free(&previous);
     }
     return 1;
-  }
 
 
+  }
+  
 
   /* Start comparison*/
   if(type_id != NULL){
 
   /* Start comparison*/
   if(type_id != NULL){
@@ -1123,11 +1113,11 @@ int compare_heap_area(void *area1, void* area2, xbt_dynar_t previous, xbt_dict_t
     }
   }else{
     res_compare = compare_heap_area_without_type(area1, area2, area1_to_compare, area2_to_compare, previous, all_types, other_types, size, check_ignore);
     }
   }else{
     res_compare = compare_heap_area_without_type(area1, area2, area1_to_compare, area2_to_compare, previous, all_types, other_types, size, check_ignore);
-      if(res_compare != 0){
-        if(match_pairs)
-          xbt_dynar_free(&previous);
-        return res_compare;
-      }
+    if(res_compare != 0){
+      if(match_pairs)
+        xbt_dynar_free(&previous);
+      return res_compare;
+    }
   }
 
   if(match_pairs){
   }
 
   if(match_pairs){
index 9e94017..71ddd56 100644 (file)
@@ -120,12 +120,10 @@ static void *register_morecore(struct mdesc *mdp, size_t size)
     for (it=0; it<BLOCKIFY(mdp->heapsize * sizeof(malloc_info)); it++){
       newinfo[BLOCK(oldinfo)+it].type = 0;
       newinfo[BLOCK(oldinfo)+it].busy_block.ignore = 0;
     for (it=0; it<BLOCKIFY(mdp->heapsize * sizeof(malloc_info)); it++){
       newinfo[BLOCK(oldinfo)+it].type = 0;
       newinfo[BLOCK(oldinfo)+it].busy_block.ignore = 0;
-      newinfo[BLOCK(oldinfo+it)].busy_block.equal_to = NULL;
     }
 
     newinfo[BLOCK(oldinfo)].busy_block.size = BLOCKIFY(mdp->heapsize * sizeof(malloc_info));
     newinfo[BLOCK(oldinfo)].busy_block.busy_size = size;
     }
 
     newinfo[BLOCK(oldinfo)].busy_block.size = BLOCKIFY(mdp->heapsize * sizeof(malloc_info));
     newinfo[BLOCK(oldinfo)].busy_block.busy_size = size;
-    //newinfo[BLOCK(oldinfo)].busy_block.bt_size = 0;// FIXME setup the backtrace
     mfree(mdp, (void *) oldinfo);
     mdp->heapsize = newsize;
   }
     mfree(mdp, (void *) oldinfo);
     mdp->heapsize = newsize;
   }
@@ -205,7 +203,6 @@ void *mmalloc_no_memset(xbt_mheap_t mdp, size_t size)
       /* Update our metadata about this fragment */
       candidate_info->busy_frag.frag_size[candidate_frag] = requested_size;
       candidate_info->busy_frag.ignore[candidate_frag] = 0;
       /* Update our metadata about this fragment */
       candidate_info->busy_frag.frag_size[candidate_frag] = requested_size;
       candidate_info->busy_frag.ignore[candidate_frag] = 0;
-      candidate_info->busy_frag.equal_to[candidate_frag] = NULL;
       //xbt_backtrace_no_malloc(candidate_info->busy_frag.bt[candidate_frag],XBT_BACKTRACE_SIZE);
       //xbt_libunwind_backtrace(candidate_info->busy_frag.bt[candidate_frag],XBT_BACKTRACE_SIZE);
 
       //xbt_backtrace_no_malloc(candidate_info->busy_frag.bt[candidate_frag],XBT_BACKTRACE_SIZE);
       //xbt_libunwind_backtrace(candidate_info->busy_frag.bt[candidate_frag],XBT_BACKTRACE_SIZE);
 
@@ -227,7 +224,6 @@ void *mmalloc_no_memset(xbt_mheap_t mdp, size_t size)
       for (i = 1; i < (size_t) (BLOCKSIZE >> log); ++i) {
         mdp->heapinfo[block].busy_frag.frag_size[i] = -1;
         mdp->heapinfo[block].busy_frag.ignore[i] = 0;
       for (i = 1; i < (size_t) (BLOCKSIZE >> log); ++i) {
         mdp->heapinfo[block].busy_frag.frag_size[i] = -1;
         mdp->heapinfo[block].busy_frag.ignore[i] = 0;
-        mdp->heapinfo[block].busy_frag.equal_to[i] = NULL;
       }
       mdp->heapinfo[block].busy_frag.nfree = i - 1;
       mdp->heapinfo[block].freehook.prev = NULL;
       }
       mdp->heapinfo[block].busy_frag.nfree = i - 1;
       mdp->heapinfo[block].freehook.prev = NULL;
@@ -238,7 +234,6 @@ void *mmalloc_no_memset(xbt_mheap_t mdp, size_t size)
       /* mark the fragment returned as busy */
       mdp->heapinfo[block].busy_frag.frag_size[0] = requested_size;
       mdp->heapinfo[block].busy_frag.ignore[0] = 0;
       /* mark the fragment returned as busy */
       mdp->heapinfo[block].busy_frag.frag_size[0] = requested_size;
       mdp->heapinfo[block].busy_frag.ignore[0] = 0;
-      mdp->heapinfo[block].busy_frag.equal_to[0] = NULL;
       //xbt_backtrace_no_malloc(mdp->heapinfo[block].busy_frag.bt[0],XBT_BACKTRACE_SIZE);
       //xbt_libunwind_backtrace(mdp->heapinfo[block].busy_frag.bt[0],XBT_BACKTRACE_SIZE);
       
       //xbt_backtrace_no_malloc(mdp->heapinfo[block].busy_frag.bt[0],XBT_BACKTRACE_SIZE);
       //xbt_libunwind_backtrace(mdp->heapinfo[block].busy_frag.bt[0],XBT_BACKTRACE_SIZE);
       
@@ -286,7 +281,6 @@ void *mmalloc_no_memset(xbt_mheap_t mdp, size_t size)
           mdp->heapinfo[block+it].type = 0;
           mdp->heapinfo[block+it].busy_block.busy_size = 0;
           mdp->heapinfo[block+it].busy_block.ignore = 0;
           mdp->heapinfo[block+it].type = 0;
           mdp->heapinfo[block+it].busy_block.busy_size = 0;
           mdp->heapinfo[block+it].busy_block.ignore = 0;
-          mdp->heapinfo[block+it].busy_block.equal_to = NULL;
         }
         mdp->heapinfo[block].busy_block.size = blocks;
         mdp->heapinfo[block].busy_block.busy_size = requested_size;
         }
         mdp->heapinfo[block].busy_block.size = blocks;
         mdp->heapinfo[block].busy_block.busy_size = requested_size;
@@ -328,7 +322,6 @@ void *mmalloc_no_memset(xbt_mheap_t mdp, size_t size)
       mdp->heapinfo[block+it].type = 0;
       mdp->heapinfo[block+it].busy_block.busy_size = 0;
       mdp->heapinfo[block+it].busy_block.ignore = 0;
       mdp->heapinfo[block+it].type = 0;
       mdp->heapinfo[block+it].busy_block.busy_size = 0;
       mdp->heapinfo[block+it].busy_block.ignore = 0;
-      mdp->heapinfo[block+it].busy_block.equal_to = NULL;
     }
     mdp->heapinfo[block].busy_block.size = blocks;
     mdp->heapinfo[block].busy_block.busy_size = requested_size; 
     }
     mdp->heapinfo[block].busy_block.size = blocks;
     mdp->heapinfo[block].busy_block.busy_size = requested_size; 
index 0623bff..f3e4d20 100644 (file)
@@ -157,7 +157,6 @@ typedef struct {
       ssize_t frag_size[MAX_FRAGMENT_PER_BLOCK];
       //void *bt[MAX_FRAGMENT_PER_BLOCK][XBT_BACKTRACE_SIZE]; /* Where it was malloced (or realloced lastly) */
       int ignore[MAX_FRAGMENT_PER_BLOCK];
       ssize_t frag_size[MAX_FRAGMENT_PER_BLOCK];
       //void *bt[MAX_FRAGMENT_PER_BLOCK][XBT_BACKTRACE_SIZE]; /* Where it was malloced (or realloced lastly) */
       int ignore[MAX_FRAGMENT_PER_BLOCK];
-      heap_area_t equal_to[MAX_FRAGMENT_PER_BLOCK];
     } busy_frag;
     struct {
       size_t size; /* Size (in blocks) of a large cluster.  */
     } busy_frag;
     struct {
       size_t size; /* Size (in blocks) of a large cluster.  */
@@ -165,7 +164,6 @@ typedef struct {
       //void *bt[XBT_BACKTRACE_SIZE]; /* Where it was malloced (or realloced lastly) */
       //int bt_size;
       int ignore;
       //void *bt[XBT_BACKTRACE_SIZE]; /* Where it was malloced (or realloced lastly) */
       //int bt_size;
       int ignore;
-      heap_area_t equal_to;
     } busy_block;
     /* Heap information for a free block (that may be the first of a free cluster).  */
     struct {
     } busy_block;
     /* Heap information for a free block (that may be the first of a free cluster).  */
     struct {
index 7cbe32c..8af2bcb 100644 (file)
@@ -85,7 +85,6 @@ void *mrealloc(xbt_mheap_t mdp, void *ptr, size_t size)
       for (it= block+blocks; it< mdp->heapinfo[block].busy_block.size ; it++){
         mdp->heapinfo[it].type = 0; // FIXME that should be useless, type should already be 0 here
         mdp->heapinfo[it].busy_block.ignore = 0;
       for (it= block+blocks; it< mdp->heapinfo[block].busy_block.size ; it++){
         mdp->heapinfo[it].type = 0; // FIXME that should be useless, type should already be 0 here
         mdp->heapinfo[it].busy_block.ignore = 0;
-        mdp->heapinfo[it].busy_block.equal_to = NULL;
       }
 
       mdp->heapinfo[block + blocks].busy_block.size
       }
 
       mdp->heapinfo[block + blocks].busy_block.size
@@ -95,7 +94,6 @@ void *mrealloc(xbt_mheap_t mdp, void *ptr, size_t size)
       mdp->heapinfo[block].busy_block.size = blocks;
       mdp->heapinfo[block].busy_block.busy_size = requested_size;
       mdp->heapinfo[block].busy_block.ignore = 0;
       mdp->heapinfo[block].busy_block.size = blocks;
       mdp->heapinfo[block].busy_block.busy_size = requested_size;
       mdp->heapinfo[block].busy_block.ignore = 0;
-      mdp->heapinfo[block].busy_block.equal_to = NULL;
 
       result = ptr;
     } else if (blocks == mdp->heapinfo[block].busy_block.size) {
 
       result = ptr;
     } else if (blocks == mdp->heapinfo[block].busy_block.size) {
@@ -104,7 +102,6 @@ void *mrealloc(xbt_mheap_t mdp, void *ptr, size_t size)
       result = ptr;
       mdp->heapinfo[block].busy_block.busy_size = requested_size;
       mdp->heapinfo[block].busy_block.ignore = 0;
       result = ptr;
       mdp->heapinfo[block].busy_block.busy_size = requested_size;
       mdp->heapinfo[block].busy_block.ignore = 0;
-      mdp->heapinfo[block].busy_block.equal_to = NULL;
 
     } else {
       /* Won't fit, so allocate a new region that will.
 
     } else {
       /* Won't fit, so allocate a new region that will.
@@ -137,7 +134,6 @@ void *mrealloc(xbt_mheap_t mdp, void *ptr, size_t size)
       int frag_nb = RESIDUAL(result, BLOCKSIZE) >> type;
       mdp->heapinfo[block].busy_frag.frag_size[frag_nb] = requested_size;
       mdp->heapinfo[block].busy_frag.ignore[frag_nb] = 0;
       int frag_nb = RESIDUAL(result, BLOCKSIZE) >> type;
       mdp->heapinfo[block].busy_frag.frag_size[frag_nb] = requested_size;
       mdp->heapinfo[block].busy_frag.ignore[frag_nb] = 0;
-      mdp->heapinfo[block].busy_frag.equal_to[frag_nb] = NULL;
 
     } else { /* fragment -> Either other fragment, or block */
       /* The new size is different; allocate a new space,
 
     } else { /* fragment -> Either other fragment, or block */
       /* The new size is different; allocate a new space,
index c7592a0..1a9e8e6 100644 (file)
@@ -53,6 +53,10 @@ static void xbt_parmap_busy_worker_signal(xbt_parmap_t parmap);
 static void xbt_parmap_busy_master_signal(xbt_parmap_t parmap);
 static void xbt_parmap_busy_worker_wait(xbt_parmap_t parmap, unsigned round);
 
 static void xbt_parmap_busy_master_signal(xbt_parmap_t parmap);
 static void xbt_parmap_busy_worker_wait(xbt_parmap_t parmap, unsigned round);
 
+#ifdef HAVE_MC
+static void xbt_parmap_mc_work(xbt_parmap_t parmap, int worker_id);
+static void *xbt_parmap_mc_worker_main(void *arg);
+#endif
 
 /**
  * \brief Parallel map structure
 
 /**
  * \brief Parallel map structure
@@ -67,6 +71,14 @@ typedef struct s_xbt_parmap {
   xbt_dynar_t data;                /**< parameters to pass to fun in parallel */
   unsigned int index;              /**< index of the next element of data to pick */
 
   xbt_dynar_t data;                /**< parameters to pass to fun in parallel */
   unsigned int index;              /**< index of the next element of data to pick */
 
+#ifdef HAVE_MC
+  int finish;
+  void* ref_snapshot;
+  int_f_pvoid_pvoid_t snapshot_compare;
+  unsigned int length;
+  void* mc_data;
+#endif
+
   /* posix only */
   xbt_os_cond_t ready_cond;
   xbt_os_mutex_t ready_mutex;
   /* posix only */
   xbt_os_cond_t ready_cond;
   xbt_os_mutex_t ready_mutex;
@@ -123,6 +135,40 @@ xbt_parmap_t xbt_parmap_new(unsigned int num_workers, e_xbt_parmap_mode_t mode)
   return parmap;
 }
 
   return parmap;
 }
 
+#ifdef HAVE_MC
+/**
+ * \brief Creates a parallel map object
+ * \param num_workers number of worker threads to create
+ * \param mode how to synchronize the worker threads
+ * \return the parmap created
+ */
+xbt_parmap_t xbt_parmap_mc_new(unsigned int num_workers, e_xbt_parmap_mode_t mode)
+{
+  unsigned int i;
+  xbt_os_thread_t worker = NULL;
+
+  XBT_DEBUG("Create new parmap (%u workers)", num_workers);
+
+  /* Initialize the thread pool data structure */
+  xbt_parmap_t parmap = xbt_new0(s_xbt_parmap_t, 1);
+
+  parmap->num_workers = num_workers;
+  parmap->status = XBT_PARMAP_WORK;
+  xbt_parmap_set_mode(parmap, mode);
+
+  /* Create the pool of worker threads */
+  xbt_parmap_thread_data_t data;
+  for (i = 1; i < num_workers; i++) {
+    data = xbt_new0(s_xbt_parmap_thread_data_t, 1);
+    data->parmap = parmap;
+    data->worker_id = i;
+    worker = xbt_os_thread_create(NULL, xbt_parmap_mc_worker_main, data, NULL);
+    xbt_os_thread_detach(worker);
+  }
+  return parmap;
+}
+#endif
+
 /**
  * \brief Destroys a parmap
  * \param parmap the parmap to destroy
 /**
  * \brief Destroys a parmap
  * \param parmap the parmap to destroy
@@ -261,8 +307,8 @@ static void *xbt_parmap_worker_main(void *arg)
   xbt_parmap_thread_data_t data = (xbt_parmap_thread_data_t) arg;
   xbt_parmap_t parmap = data->parmap;
   unsigned round = 0;
   xbt_parmap_thread_data_t data = (xbt_parmap_thread_data_t) arg;
   xbt_parmap_t parmap = data->parmap;
   unsigned round = 0;
-  smx_context_t context = SIMIX_context_new(NULL, 0, NULL, NULL, NULL);
-  SIMIX_context_set_current(context);
+  //  smx_context_t context = SIMIX_context_new(NULL, 0, NULL, NULL, NULL);
+  //SIMIX_context_set_current(context);
 
   XBT_DEBUG("New worker thread created");
 
 
   XBT_DEBUG("New worker thread created");
 
@@ -287,6 +333,89 @@ static void *xbt_parmap_worker_main(void *arg)
   }
 }
 
   }
 }
 
+#ifdef HAVE_MC
+
+/**
+ * \brief Applies a list of tasks in parallel.
+ * \param parmap a parallel map object
+ * \param fun the function to call in parallel
+ * \param data each element of this dynar will be passed as an argument to fun
+ */
+int xbt_parmap_mc_apply(xbt_parmap_t parmap, int_f_pvoid_pvoid_t fun, 
+                         void* data, unsigned int length,  void* ref_snapshot)
+{
+  /* Assign resources to worker threads */
+  parmap->snapshot_compare = fun;
+  parmap->mc_data = data;
+  parmap->index = 0;
+  parmap->finish = -1;
+  parmap->length = length;
+  parmap->ref_snapshot = ref_snapshot;
+  parmap->master_signal_f(parmap);
+  xbt_parmap_mc_work(parmap, 0);
+  parmap->master_wait_f(parmap);
+  XBT_DEBUG("Job done");
+  return parmap->finish;
+}
+
+static void xbt_parmap_mc_work(xbt_parmap_t parmap, int worker_id)
+{
+  unsigned int data_size = (parmap->length / parmap->num_workers) +
+    ((parmap->length % parmap->num_workers) ? 1 :0);
+  void* start = (char*)parmap->mc_data + (data_size*worker_id*sizeof(void*));
+  void* end = MIN((char *)start + data_size* sizeof(void*), (char*)parmap->mc_data + parmap->length*sizeof(void*));
+  
+  //XBT_CRITICAL("Worker %d : %p -> %p (%d)", worker_id, start, end, data_size);
+
+  while ( start < end && parmap->finish == -1) {
+    //XBT_CRITICAL("Starting with %p", start);
+    int res = parmap->snapshot_compare(*(void**)start, parmap->ref_snapshot);
+    start = (char *)start + sizeof(start);
+    if (!res){
+    
+      parmap->finish = ((char*)start - (char*)parmap->mc_data) / sizeof(void*);
+      //XBT_CRITICAL("Find good one %p (%p)", start, parmap->mc_data);
+      break;
+    }
+  }
+}
+
+/**
+ * \brief Main function of a worker thread.
+ * \param arg the parmap
+ */
+static void *xbt_parmap_mc_worker_main(void *arg)
+{
+  xbt_parmap_thread_data_t data = (xbt_parmap_thread_data_t) arg;
+  xbt_parmap_t parmap = data->parmap;
+  unsigned round = 0;
+  /* smx_context_t context = SIMIX_context_new(NULL, 0, NULL, NULL, NULL); */
+  /* SIMIX_context_set_current(context); */
+
+  XBT_DEBUG("New worker thread created");
+
+  /* Worker's main loop */
+  while (1) {
+    parmap->worker_wait_f(parmap, ++round);
+    if (parmap->status == XBT_PARMAP_WORK) {
+
+      XBT_DEBUG("Worker %d got a job", data->worker_id);
+
+      xbt_parmap_mc_work(parmap, data->worker_id);
+      parmap->worker_signal_f(parmap);
+
+      XBT_DEBUG("Worker %d has finished", data->worker_id);
+
+    /* We are destroying the parmap */
+    } else {
+      xbt_free(data);
+      parmap->worker_signal_f(parmap);
+      return NULL;
+    }
+  }
+}
+#endif
+
 #ifdef HAVE_FUTEX_H
 static void futex_wait(unsigned *uaddr, unsigned val)
 {
 #ifdef HAVE_FUTEX_H
 static void futex_wait(unsigned *uaddr, unsigned val)
 {