Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : parallel comparison of system states for liveness model-checking
[simgrid.git] / src / mc / mc_compare.c
1 /* Copyright (c) 2012-2013 Da SimGrid Team. All rights reserved.            */
2
3 /* This program is free software; you can redistribute it and/or modify it
4  * under the terms of the license (GNU LGPL) which comes with this package. */
5
6 #include "mc_private.h"
7
8 #include "xbt/mmalloc.h"
9
10 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_compare, mc,
11                                 "Logging specific to mc_compare");
12
13 typedef struct s_pointers_pair{
14   void *p1;
15   void *p2;
16 }s_pointers_pair_t, *pointers_pair_t;
17
18 __thread xbt_dynar_t compared_pointers;
19
20 /************************** Free functions ****************************/
21 /********************************************************************/
22
23 static void stack_region_free(stack_region_t s){
24   if(s){
25     xbt_free(s->process_name);
26     xbt_free(s);
27   }
28 }
29
30 static void stack_region_free_voidp(void *s){
31   stack_region_free((stack_region_t) * (void **) s);
32 }
33
34 static void pointers_pair_free(pointers_pair_t p){
35   xbt_free(p);
36 }
37
38 static void pointers_pair_free_voidp(void *p){
39   pointers_pair_free((pointers_pair_t) * (void **)p);
40 }
41
42 /************************** Snapshot comparison *******************************/
43 /******************************************************************************/
44
45 static int already_compared_pointers(void *p1, void *p2){
46
47   if(xbt_dynar_is_empty(compared_pointers))
48     return -1;
49
50   unsigned int cursor = 0;
51   int start = 0;
52   int end = xbt_dynar_length(compared_pointers) - 1;
53   pointers_pair_t pair;
54
55   while(start <= end){
56     cursor = (start + end) / 2;
57     pair = (pointers_pair_t)xbt_dynar_get_as(compared_pointers, cursor, pointers_pair_t);
58     if(pair->p1 == p1){
59       if(pair->p2 == p2)
60         return 0;
61       else if(pair->p2 < p2)
62         start = cursor + 1;
63       else
64         end = cursor - 1;
65     }else if(pair->p1 < p1){
66       start = cursor + 1;
67     }else{
68       end = cursor - 1 ;
69     }
70   }
71
72   return -1;
73
74 }
75
76 static void add_compared_pointers(void *p1, void *p2){
77
78   pointers_pair_t new_pair = xbt_new0(s_pointers_pair_t, 1);
79   new_pair->p1 = p1;
80   new_pair->p2 = p2;
81   
82   if(xbt_dynar_is_empty(compared_pointers)){
83     xbt_dynar_push(compared_pointers, &new_pair);
84     return;
85   }
86
87   unsigned int cursor = 0;
88   int start = 0;
89   int end = xbt_dynar_length(compared_pointers) - 1;
90   pointers_pair_t pair = NULL;
91
92   while(start <= end){
93     cursor = (start + end) / 2;
94     pair = (pointers_pair_t)xbt_dynar_get_as(compared_pointers, cursor, pointers_pair_t);
95     if(pair->p1 == p1){
96       if(pair->p2 == p2){
97         pointers_pair_free(new_pair);
98         return;
99       }else if(pair->p2 < p2)
100         start = cursor + 1;
101       else
102         end = cursor - 1;
103     }else if(pair->p1 < p1){
104       start = cursor + 1;
105     }else{
106       end = cursor - 1 ;
107     }
108   }
109
110   if(pair->p1 == p1){
111     if(pair->p2 < p2)
112       xbt_dynar_insert_at(compared_pointers, cursor + 1, &new_pair);
113     else
114       xbt_dynar_insert_at(compared_pointers, cursor, &new_pair); 
115   }else{
116     if(pair->p1 < p1)
117       xbt_dynar_insert_at(compared_pointers, cursor + 1, &new_pair);
118     else
119       xbt_dynar_insert_at(compared_pointers, cursor, &new_pair);   
120   }
121
122 }
123
124 static int compare_areas_with_type(void *area1, void *area2, xbt_dict_t types, xbt_dict_t other_types, char *type_id, int region_size, int region_type, void *start_data, int pointer_level){
125
126   dw_type_t type = xbt_dict_get_or_null(types, type_id);;
127   unsigned int cursor = 0;
128   dw_type_t member, subtype, subsubtype;
129   int elm_size, i, res, switch_types = 0;
130   void *addr_pointed1, *addr_pointed2;
131   int pointed_area_size1, pointed_area_size2;
132
133   switch(type->type){
134   case e_dw_base_type:
135   case e_dw_enumeration_type:
136   case e_dw_union_type:
137     return (memcmp(area1, area2, type->size) != 0);
138     break;
139   case e_dw_typedef:
140   case e_dw_volatile_type:
141     return compare_areas_with_type(area1, area2, types, other_types, type->dw_type_id, region_size, region_type, start_data, pointer_level);
142     break;
143   case e_dw_const_type: /* Const variable cannot be modified */
144     return -1;
145     break;
146   case e_dw_array_type:
147     subtype = xbt_dict_get_or_null(types, type->dw_type_id);
148     switch(subtype->type){
149     case e_dw_base_type:
150     case e_dw_enumeration_type:
151     case e_dw_pointer_type:
152     case e_dw_structure_type:
153     case e_dw_union_type:
154       if(subtype->size == 0){ /*declaration of the type, need the complete description */
155         subtype = xbt_dict_get_or_null(types, get_type_description(types, subtype->name));
156         if(subtype == NULL){
157           subtype = xbt_dict_get_or_null(other_types, get_type_description(other_types, subtype->name));
158           switch_types = 1;
159         }
160       }
161       elm_size = subtype->size;
162       break;
163     case e_dw_typedef:
164     case e_dw_volatile_type:
165       subsubtype = xbt_dict_get_or_null(types, subtype->dw_type_id);
166       if(subsubtype->size == 0){ /*declaration of the type, need the complete description */
167         subsubtype = xbt_dict_get_or_null(types, get_type_description(types, subsubtype->name));
168         if(subsubtype == NULL){
169           subsubtype = xbt_dict_get_or_null(other_types, get_type_description(other_types, subsubtype->name));
170           switch_types = 1;
171         }
172       }
173       elm_size = subsubtype->size;
174       break;
175     default : 
176       return 0;
177       break;
178     }
179     for(i=0; i<type->size; i++){
180       if(switch_types)
181         res = compare_areas_with_type((char *)area1 + (i*elm_size), (char *)area2 + (i*elm_size), other_types, types, type->dw_type_id, region_size, region_type, start_data, pointer_level);
182       else
183         res = compare_areas_with_type((char *)area1 + (i*elm_size), (char *)area2 + (i*elm_size), types, other_types, type->dw_type_id, region_size, region_type, start_data, pointer_level);
184       if(res != 0)
185         return res;
186     }
187     break;
188   case e_dw_pointer_type: 
189     if(type->dw_type_id && ((dw_type_t)xbt_dict_get_or_null(types, type->dw_type_id))->type == e_dw_subroutine_type){
190       addr_pointed1 = *((void **)(area1)); 
191       addr_pointed2 = *((void **)(area2));
192       return (addr_pointed1 != addr_pointed2);
193     }else{
194       addr_pointed1 = *((void **)(area1)); 
195       addr_pointed2 = *((void **)(area2));
196       
197       if((addr_pointed1 == addr_pointed2) && ((pointed_area_size1 = get_pointed_area_size(addr_pointed1, 1)) != (pointed_area_size2 = get_pointed_area_size(addr_pointed2, 2))))
198         return -1;
199       if(addr_pointed1 == NULL && addr_pointed2 == NULL)
200         return 0;
201       if(already_compared_pointers(addr_pointed1, addr_pointed2) != -1)
202         return 0;
203       add_compared_pointers(addr_pointed1, addr_pointed2);
204
205       pointer_level++;
206       
207       if(addr_pointed1 > std_heap && (char *)addr_pointed1 < (char*) std_heap + STD_HEAP_SIZE && addr_pointed2 > std_heap && (char *)addr_pointed2 < (char*) std_heap + STD_HEAP_SIZE){
208         return compare_heap_area(addr_pointed1, addr_pointed2, NULL, types, other_types, type->dw_type_id, pointer_level); 
209       }else if(addr_pointed1 > start_data && (char*)addr_pointed1 <= (char *)start_data + region_size && addr_pointed2 > start_data && (char*)addr_pointed2 <= (char *)start_data + region_size){
210         if(type->dw_type_id == NULL)
211           return  (addr_pointed1 != addr_pointed2);
212         else
213           return compare_areas_with_type(addr_pointed1, addr_pointed2, types, other_types, type->dw_type_id, region_size, region_type, start_data, pointer_level); 
214       }else{
215         return  (addr_pointed1 != addr_pointed2);
216       }
217     }
218     break;
219   case e_dw_structure_type:
220     xbt_dynar_foreach(type->members, cursor, member){
221       res = compare_areas_with_type((char *)area1 + member->offset, (char *)area2 + member->offset, types, other_types, member->dw_type_id, region_size, region_type, start_data, pointer_level);
222       if(res == 1)
223         return res;
224     }
225     break;
226   case e_dw_subroutine_type:
227     return -1;
228     break;
229   default:
230     XBT_VERB("Unknown case : %d", type->type);
231     break;
232   }
233   
234   return 0;
235 }
236
237 static int compare_global_variables(int region_type, mc_mem_region_t r1, mc_mem_region_t r2){
238
239   if(!compared_pointers){
240     compared_pointers = xbt_dynar_new(sizeof(pointers_pair_t), pointers_pair_free_voidp);
241     MC_ignore_global_variable("compared_pointers");
242   }else{
243     xbt_dynar_reset(compared_pointers);
244   }
245
246   xbt_dynar_t variables;
247   xbt_dict_t types, other_types;
248   int res;
249   unsigned int cursor = 0;
250   dw_variable_t current_var;
251   size_t offset;
252   void *start_data;
253
254   if(region_type == 2){
255     variables = mc_global_variables_binary;
256     types = mc_variables_type_binary;
257     other_types = mc_variables_type_libsimgrid;
258     start_data = start_data_binary;
259   }else{
260     variables = mc_global_variables_libsimgrid;
261     types = mc_variables_type_libsimgrid;
262     other_types = mc_variables_type_binary;
263     start_data = start_data_libsimgrid;
264   }
265
266   xbt_dynar_foreach(variables, cursor, current_var){
267
268     if(region_type == 2)
269       offset = (char *)current_var->address.address - (char *)start_data_binary;
270     else
271       offset = (char *)current_var->address.address - (char *)start_data_libsimgrid;
272
273     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);
274     if(res == 1){
275       XBT_VERB("Global variable %s is different between snapshots", current_var->name);
276       xbt_dynar_free(&compared_pointers);
277       compared_pointers = NULL;
278       return 1;
279     }
280
281   }
282
283   xbt_dynar_free(&compared_pointers);
284   compared_pointers = NULL;
285
286   return 0;
287
288 }
289
290 static int compare_local_variables(mc_snapshot_stack_t stack1, mc_snapshot_stack_t stack2, void *heap1, void *heap2){
291
292   if(!compared_pointers){
293     compared_pointers = xbt_dynar_new(sizeof(pointers_pair_t), pointers_pair_free_voidp);
294     MC_ignore_global_variable("compared_pointers");
295   }else{
296     xbt_dynar_reset(compared_pointers);
297   }
298
299   if(xbt_dynar_length(stack1->local_variables) != xbt_dynar_length(stack2->local_variables)){
300     XBT_VERB("Different number of local variables");
301     xbt_dynar_free(&compared_pointers);
302     compared_pointers = NULL;
303     return 1;
304   }else{
305     unsigned int cursor = 0;
306     local_variable_t current_var1, current_var2;
307     int offset1, offset2, res;
308     while(cursor < xbt_dynar_length(stack1->local_variables)){
309       current_var1 = (local_variable_t)xbt_dynar_get_as(stack1->local_variables, cursor, local_variable_t);
310       current_var2 = (local_variable_t)xbt_dynar_get_as(stack2->local_variables, cursor, local_variable_t);
311       if(strcmp(current_var1->name, current_var2->name) != 0 || strcmp(current_var1->frame, current_var2->frame) != 0 || current_var1->ip != current_var2->ip){
312         xbt_dynar_free(&compared_pointers);
313         return 1;
314       }
315       offset1 = (char *)current_var1->address - (char *)std_heap;
316       offset2 = (char *)current_var2->address - (char *)std_heap;
317       if(current_var1->region == 1)
318         res = compare_areas_with_type( (char *)heap1 + offset1, (char *)heap2 + offset2, mc_variables_type_libsimgrid, mc_variables_type_binary, current_var1->type, 0, 1, start_data_libsimgrid, 0l);
319       else
320         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);
321       if(res == 1){
322         XBT_VERB("Local variable %s in frame %s  is different between snapshots", current_var1->name, current_var1->frame);
323         xbt_dynar_free(&compared_pointers);
324         compared_pointers = NULL;
325         return res;
326       }
327       cursor++;
328     }
329     xbt_dynar_free(&compared_pointers);
330     compared_pointers = NULL;
331     return 0;
332   }
333 }
334
335 int snapshot_compare(void *p1, void *p2){
336
337   mc_snapshot_t s1 = ((mc_pair_t)p1)->graph_state->system_state;
338   mc_snapshot_t s2 = ((mc_pair_t)p2)->graph_state->system_state;
339
340   int errors = 0;
341   int res_init;
342
343   xbt_os_timer_t global_timer = xbt_os_timer_new();
344   xbt_os_timer_t timer = xbt_os_timer_new();
345
346   xbt_os_walltimer_start(global_timer);
347
348   #ifdef MC_DEBUG
349     xbt_os_walltimer_start(timer);
350   #endif
351
352   /* Compare size of stacks */
353   int i = 0;
354   size_t size_used1, size_used2;
355   int is_diff = 0;
356   while(i < xbt_dynar_length(s1->stacks)){
357     size_used1 = s1->stack_sizes[i];
358     size_used2 = s2->stack_sizes[i];
359     if(size_used1 != size_used2){
360     #ifdef MC_DEBUG
361       if(is_diff == 0){
362         xbt_os_walltimer_stop(timer);
363         mc_comp_times->stacks_sizes_comparison_time = xbt_os_timer_elapsed(timer);
364       }
365       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);
366       errors++;
367       is_diff = 1;
368     #else
369       #ifdef MC_VERBOSE
370       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);
371       #endif
372
373       xbt_os_walltimer_stop(timer);
374       xbt_os_timer_free(timer);
375       xbt_os_walltimer_stop(global_timer);
376       mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
377       xbt_os_timer_free(global_timer);
378
379       return 1;
380     #endif  
381     }
382     i++;
383   }
384
385   #ifdef MC_DEBUG
386     if(is_diff == 0)
387       xbt_os_walltimer_stop(timer);
388     xbt_os_walltimer_start(timer);
389   #endif
390
391   /* Compare hash of global variables */
392   if(s1->hash_global != NULL && s2->hash_global != NULL){
393     if(strcmp(s1->hash_global, s2->hash_global) != 0){
394       #ifdef MC_DEBUG
395         xbt_os_walltimer_stop(timer);
396         mc_comp_times->hash_global_variables_comparison_time = xbt_os_timer_elapsed(timer);
397         XBT_DEBUG("Different hash of global variables : %s - %s", s1->hash_global, s2->hash_global); 
398         errors++; 
399       #else
400         #ifdef MC_VERBOSE
401           XBT_VERB("Different hash of global variables : %s - %s", s1->hash_global, s2->hash_global); 
402         #endif
403
404         xbt_os_walltimer_stop(timer);
405         xbt_os_timer_free(timer);
406         xbt_os_walltimer_stop(global_timer);
407         mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
408         xbt_os_timer_free(global_timer);
409
410         return 1;
411       #endif
412     }
413   }
414
415   #ifdef MC_DEBUG
416     xbt_os_walltimer_start(timer);
417   #endif
418
419   /* Compare hash of local variables */
420   if(s1->hash_local != NULL && s2->hash_local != NULL){
421     if(strcmp(s1->hash_local, s2->hash_local) != 0){
422       #ifdef MC_DEBUG
423         xbt_os_walltimer_stop(timer);
424         mc_comp_times->hash_local_variables_comparison_time = xbt_os_timer_elapsed(timer);
425         XBT_DEBUG("Different hash of local variables : %s - %s", s1->hash_local, s2->hash_local); 
426         errors++; 
427       #else
428         #ifdef MC_VERBOSE
429           XBT_VERB("Different hash of local variables : %s - %s", s1->hash_local, s2->hash_local); 
430         #endif
431
432         xbt_os_walltimer_stop(timer);
433         xbt_os_timer_free(timer);
434         xbt_os_walltimer_stop(global_timer);
435         mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
436         xbt_os_timer_free(global_timer);
437
438         return 1;
439       #endif
440     }
441   }
442
443   #ifdef MC_DEBUG
444     xbt_os_walltimer_start(timer);
445   #endif
446
447   /* Init heap information used in heap comparison algorithm */
448   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);
449   if(res_init == -1){
450      #ifdef MC_DEBUG
451     XBT_DEBUG("(%d - %d) Different heap information", ((mc_pair_t)p1)->num, ((mc_pair_t)p2)->num); 
452         errors++; 
453       #else
454         #ifdef MC_VERBOSE
455         XBT_VERB("(%d - %d) Different heap information", ((mc_pair_t)p1)->num, ((mc_pair_t)p2)->num); 
456         #endif
457
458         xbt_os_walltimer_stop(global_timer);
459         mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
460         xbt_os_timer_free(global_timer);
461
462         return 1;
463       #endif
464   }
465
466   #ifdef MC_DEBUG
467     xbt_os_walltimer_start(timer);
468   #endif
469
470   /* Stacks comparison */
471   unsigned int  cursor = 0;
472   int diff_local = 0;
473   is_diff = 0;
474   mc_snapshot_stack_t stack1, stack2;
475     
476   while(cursor < xbt_dynar_length(s1->stacks)){
477     stack1 = (mc_snapshot_stack_t)xbt_dynar_get_as(s1->stacks, cursor, mc_snapshot_stack_t);
478     stack2 = (mc_snapshot_stack_t)xbt_dynar_get_as(s2->stacks, cursor, mc_snapshot_stack_t);
479     diff_local = compare_local_variables(stack1, stack2, s1->regions[0]->data, s2->regions[0]->data);
480     if(diff_local > 0){
481       #ifdef MC_DEBUG
482         if(is_diff == 0){
483           xbt_os_walltimer_stop(timer);
484           mc_comp_times->stacks_comparison_time = xbt_os_timer_elapsed(timer);
485         }
486         XBT_DEBUG("(%d - %d) Different local variables between stacks %d", ((mc_pair_t)p1)->num, ((mc_pair_t)p2)->num, cursor + 1);
487         errors++;
488         is_diff = 1;
489       #else
490         
491         #ifdef MC_VERBOSE
492         XBT_VERB("(%d - %d) Different local variables between stacks %d", ((mc_pair_t)p1)->num, ((mc_pair_t)p2)->num, cursor + 1);
493         #endif
494           
495         reset_heap_information();
496         xbt_os_walltimer_stop(timer);
497         xbt_os_timer_free(timer);
498         xbt_os_walltimer_stop(global_timer);
499         mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
500         xbt_os_timer_free(global_timer);
501  
502         return 1;
503       #endif
504     }
505     cursor++;
506   }
507
508   #ifdef MC_DEBUG
509     if(is_diff == 0)
510       xbt_os_walltimer_stop(timer);
511     xbt_os_walltimer_start(timer);
512   #endif
513
514   /* Compare binary global variables */
515   is_diff = compare_global_variables(2, s1->regions[2], s2->regions[2]);
516   if(is_diff != 0){
517     #ifdef MC_DEBUG
518       xbt_os_walltimer_stop(timer);
519       mc_comp_times->binary_global_variables_comparison_time = xbt_os_timer_elapsed(timer);
520       XBT_DEBUG("(%d - %d) Different global variables in binary", ((mc_pair_t)p1)->num, ((mc_pair_t)p2)->num);
521       errors++;
522     #else
523       #ifdef MC_VERBOSE
524       XBT_VERB("(%d - %d) Different global variables in binary", ((mc_pair_t)p1)->num, ((mc_pair_t)p2)->num);
525       #endif
526
527       reset_heap_information();
528       xbt_os_walltimer_stop(timer);
529       xbt_os_timer_free(timer);
530       xbt_os_walltimer_stop(global_timer);
531       mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
532       xbt_os_timer_free(global_timer);
533
534       return 1;
535     #endif
536   }
537
538   #ifdef MC_DEBUG
539     if(is_diff == 0)
540       xbt_os_walltimer_stop(timer);
541     xbt_os_walltimer_start(timer);
542   #endif
543
544   /* Compare libsimgrid global variables */
545   is_diff = compare_global_variables(1, s1->regions[1], s2->regions[1]);
546   if(is_diff != 0){
547     #ifdef MC_DEBUG
548       xbt_os_walltimer_stop(timer);
549       mc_comp_times->libsimgrid_global_variables_comparison_time = xbt_os_timer_elapsed(timer);
550       XBT_DEBUG("(%d - %d) Different global variables in libsimgrid", ((mc_pair_t)p1)->num, ((mc_pair_t)p2)->num);
551       errors++;
552     #else
553       #ifdef MC_VERBOSE
554       XBT_VERB("(%d - %d) Different global variables in libsimgrid", ((mc_pair_t)p1)->num, ((mc_pair_t)p2)->num);
555       #endif
556         
557       reset_heap_information();
558       xbt_os_walltimer_stop(timer);
559       xbt_os_timer_free(timer);
560       xbt_os_walltimer_stop(global_timer);
561       mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
562       xbt_os_timer_free(global_timer);
563
564       return 1;
565     #endif
566   }
567
568   #ifdef MC_DEBUG
569     xbt_os_walltimer_start(timer);
570   #endif
571
572   /* Compare heap */
573   if(mmalloc_compare_heap((xbt_mheap_t)s1->regions[0]->data, (xbt_mheap_t)s2->regions[0]->data) > 0){
574
575     #ifdef MC_DEBUG
576       xbt_os_walltimer_stop(timer);
577       mc_comp_times->heap_comparison_time = xbt_os_timer_elapsed(timer); 
578       XBT_DEBUG("(%d - %d) Different heap (mmalloc_compare)", ((mc_pair_t)p1)->num, ((mc_pair_t)p2)->num);
579       errors++;
580     #else
581  
582       #ifdef MC_VERBOSE
583       XBT_VERB("(%d - %d) Different heap (mmalloc_compare)", ((mc_pair_t)p1)->num, ((mc_pair_t)p2)->num);
584       #endif
585        
586       reset_heap_information();
587       xbt_os_walltimer_stop(timer);
588       xbt_os_timer_free(timer);
589       xbt_os_walltimer_stop(global_timer);
590       mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
591       xbt_os_timer_free(global_timer);
592
593       return 1;
594     #endif
595   }else{
596     #ifdef MC_DEBUG
597       xbt_os_walltimer_stop(timer);
598     #endif
599   }
600
601   reset_heap_information();
602   
603   xbt_os_walltimer_stop(timer);
604   xbt_os_timer_free(timer);
605
606   #ifdef MC_VERBOSE
607     xbt_os_walltimer_stop(global_timer);
608     mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
609   #endif
610
611   xbt_os_timer_free(global_timer);
612
613   #ifdef MC_DEBUG
614     print_comparison_times();
615   #endif
616
617   return errors > 0;
618   
619 }
620
621 /***************************** Statistics *****************************/
622 /*******************************************************************/
623
624 void print_comparison_times(){
625   XBT_DEBUG("*** Comparison times ***");
626   XBT_DEBUG("- Nb processes : %f", mc_comp_times->nb_processes_comparison_time);
627   XBT_DEBUG("- Nb bytes used : %f", mc_comp_times->bytes_used_comparison_time);
628   XBT_DEBUG("- Stacks sizes : %f", mc_comp_times->stacks_sizes_comparison_time);
629   XBT_DEBUG("- Binary global variables : %f", mc_comp_times->binary_global_variables_comparison_time);
630   XBT_DEBUG("- Libsimgrid global variables : %f", mc_comp_times->libsimgrid_global_variables_comparison_time);
631   XBT_DEBUG("- Heap : %f", mc_comp_times->heap_comparison_time);
632   XBT_DEBUG("- Stacks : %f", mc_comp_times->stacks_comparison_time);
633 }
634
635 /**************************** MC snapshot compare simcall **************************/
636 /***********************************************************************************/
637
638 int SIMIX_pre_mc_compare_snapshots(smx_simcall_t simcall,
639                                    mc_snapshot_t s1, mc_snapshot_t s2){
640   return snapshot_compare(s1, s2);
641 }
642
643 int MC_compare_snapshots(void *s1, void *s2){
644   
645   MC_ignore_local_variable("self", "simcall_BODY_mc_snapshot");
646   return simcall_mc_compare_snapshots(s1, s2);
647
648 }