Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : minor fix
[simgrid.git] / src / mc / mc_global.c
1 /* Copyright (c) 2008-2013. The SimGrid Team.
2  * All rights reserved.                                                     */
3
4 /* This program is free software; you can redistribute it and/or modify it
5  * under the terms of the license (GNU LGPL) which comes with this package. */
6
7 #include <unistd.h>
8 #include <sys/types.h>
9 #include <sys/wait.h>
10 #include <sys/time.h>
11 #include <libgen.h>
12
13 #include "simgrid/sg_config.h"
14 #include "../surf/surf_private.h"
15 #include "../simix/smx_private.h"
16 #include "../xbt/mmalloc/mmprivate.h"
17 #include "xbt/fifo.h"
18 #include "mc_private.h"
19 #include "xbt/automaton.h"
20 #include "xbt/dict.h"
21
22 static void MC_post_process_types(mc_object_info_t info);
23
24 XBT_LOG_NEW_CATEGORY(mc, "All MC categories");
25 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc,
26                                 "Logging specific to MC (global)");
27
28 /* Configuration support */
29 e_mc_reduce_t mc_reduce_kind=e_mc_reduce_unset;
30
31 int _sg_do_model_check = 0;
32 int _sg_mc_checkpoint=0;
33 char* _sg_mc_property_file=NULL;
34 int _sg_mc_timeout=0;
35 int _sg_mc_max_depth=1000;
36 int _sg_mc_visited=0;
37 char *_sg_mc_dot_output_file = NULL;
38 int _sg_mc_comms_determinism=0;
39
40 int user_max_depth_reached = 0;
41
42 void _mc_cfg_cb_reduce(const char *name, int pos) {
43   if (_sg_cfg_init_status && !_sg_do_model_check) {
44     xbt_die("You are specifying a reduction strategy after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
45   }
46   char *val= xbt_cfg_get_string(_sg_cfg_set, name);
47   if (!strcasecmp(val,"none")) {
48     mc_reduce_kind = e_mc_reduce_none;
49   } else if (!strcasecmp(val,"dpor")) {
50     mc_reduce_kind = e_mc_reduce_dpor;
51   } else {
52     xbt_die("configuration option %s can only take 'none' or 'dpor' as a value",name);
53   }
54 }
55
56 void _mc_cfg_cb_checkpoint(const char *name, int pos) {
57   if (_sg_cfg_init_status && !_sg_do_model_check) {
58     xbt_die("You are specifying a checkpointing value after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
59   }
60   _sg_mc_checkpoint = xbt_cfg_get_int(_sg_cfg_set, name);
61 }
62 void _mc_cfg_cb_property(const char *name, int pos) {
63   if (_sg_cfg_init_status && !_sg_do_model_check) {
64     xbt_die("You are specifying a property after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
65   }
66   _sg_mc_property_file= xbt_cfg_get_string(_sg_cfg_set, name);
67 }
68
69 void _mc_cfg_cb_timeout(const char *name, int pos) {
70   if (_sg_cfg_init_status && !_sg_do_model_check) {
71     xbt_die("You are specifying a value to enable/disable timeout for wait requests after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
72   }
73   _sg_mc_timeout= xbt_cfg_get_boolean(_sg_cfg_set, name);
74 }
75
76 void _mc_cfg_cb_max_depth(const char *name, int pos) {
77   if (_sg_cfg_init_status && !_sg_do_model_check) {
78     xbt_die("You are specifying a max depth value after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
79   }
80   _sg_mc_max_depth= xbt_cfg_get_int(_sg_cfg_set, name);
81 }
82
83 void _mc_cfg_cb_visited(const char *name, int pos) {
84   if (_sg_cfg_init_status && !_sg_do_model_check) {
85     xbt_die("You are specifying a number of stored visited states after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
86   }
87   _sg_mc_visited= xbt_cfg_get_int(_sg_cfg_set, name);
88 }
89
90 void _mc_cfg_cb_dot_output(const char *name, int pos) {
91   if (_sg_cfg_init_status && !_sg_do_model_check) {
92     xbt_die("You are specifying a file name for a dot output of graph state after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
93   }
94   _sg_mc_dot_output_file= xbt_cfg_get_string(_sg_cfg_set, name);
95 }
96
97 void _mc_cfg_cb_comms_determinism(const char *name, int pos) {
98   if (_sg_cfg_init_status && !_sg_do_model_check) {
99     xbt_die("You are specifying a value to enable/disable the detection of determinism in the communications schemes after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
100   }
101   _sg_mc_comms_determinism= xbt_cfg_get_boolean(_sg_cfg_set, name);
102 }
103
104 /* MC global data structures */
105 mc_state_t mc_current_state = NULL;
106 char mc_replay_mode = FALSE;
107 double *mc_time = NULL;
108 __thread mc_comparison_times_t mc_comp_times = NULL;
109 __thread double mc_snapshot_comparison_time;
110 mc_stats_t mc_stats = NULL;
111
112 /* Safety */
113 xbt_fifo_t mc_stack_safety = NULL;
114 mc_global_t initial_state_safety = NULL;
115
116 /* Liveness */
117 xbt_fifo_t mc_stack_liveness = NULL;
118 mc_global_t initial_state_liveness = NULL;
119 int compare;
120
121 xbt_automaton_t _mc_property_automaton = NULL;
122
123 /* Variables */
124 mc_object_info_t mc_libsimgrid_info = NULL;
125 mc_object_info_t mc_binary_info = NULL;
126
127 /* Ignore mechanism */
128 xbt_dynar_t mc_stack_comparison_ignore;
129 xbt_dynar_t mc_data_bss_comparison_ignore;
130 extern xbt_dynar_t mc_heap_comparison_ignore;
131 extern xbt_dynar_t stacks_areas;
132
133 /* Dot output */
134 FILE *dot_output = NULL;
135 const char* colors[13];
136
137
138 /*******************************  DWARF Information *******************************/
139 /**********************************************************************************/
140
141 /************************** Free functions *************************/
142
143 static void dw_location_free(dw_location_t l){
144   if(l){
145     if(l->type == e_dw_loclist)
146       xbt_dynar_free(&(l->location.loclist));
147     else if(l->type == e_dw_compose)
148       xbt_dynar_free(&(l->location.compose));
149     else if(l->type == e_dw_arithmetic)
150       xbt_free(l->location.arithmetic);
151   
152     xbt_free(l);
153   }
154 }
155
156 static void dw_location_entry_free(dw_location_entry_t e){
157   dw_location_free(e->location);
158   xbt_free(e);
159 }
160
161 void dw_type_free(dw_type_t t){
162   xbt_free(t->name);
163   xbt_free(t->dw_type_id);
164   xbt_dynar_free(&(t->members));
165   xbt_free(t);
166 }
167
168 static void dw_type_free_voidp(void *t){
169   dw_type_free((dw_type_t) * (void **) t);
170 }
171
172 void dw_variable_free(dw_variable_t v){
173   if(v){
174     xbt_free(v->name);
175     xbt_free(v->type_origin);
176     if(!v->global)
177       dw_location_free(v->address.location);
178     xbt_free(v);
179   }
180 }
181
182 void dw_variable_free_voidp(void *t){
183   dw_variable_free((dw_variable_t) * (void **) t);
184 }
185
186 // object_info
187
188 mc_object_info_t MC_new_object_info(void) {
189   mc_object_info_t res = xbt_new(s_mc_object_info_t, 1);
190   res->file_name = NULL;
191   res->start_text = NULL;
192   res->start_data = NULL;
193   res->start_bss = NULL;
194   res->local_variables = xbt_dict_new_homogeneous(NULL);
195   res->global_variables = xbt_dynar_new(sizeof(dw_variable_t), dw_variable_free_voidp);
196   res->types = xbt_dict_new_homogeneous(NULL);
197   return res;
198 }
199
200 void MC_free_object_info(mc_object_info_t* info) {
201   xbt_free(&(*info)->file_name);
202   xbt_dict_free(&(*info)->local_variables);
203   xbt_dynar_free(&(*info)->global_variables);
204   xbt_dict_free(&(*info)->types);
205   xbt_free(info);
206   *info = NULL;
207 }
208
209 /*************************************************************************/
210
211 static dw_location_t MC_dwarf_get_location(xbt_dict_t location_list, char *expr){
212
213   dw_location_t loc = xbt_new0(s_dw_location_t, 1);
214
215   if(location_list != NULL){
216     
217     char *key = bprintf("%d", (int)strtoul(expr, NULL, 16));
218     loc->type = e_dw_loclist;
219     loc->location.loclist =  (xbt_dynar_t)xbt_dict_get_or_null(location_list, key);
220     if(loc->location.loclist == NULL)
221       XBT_INFO("Key not found in loclist");
222     xbt_free(key);
223     return loc;
224
225   }else{
226
227     int cursor = 0;
228     char *tok = NULL, *tok2 = NULL; 
229     
230     xbt_dynar_t tokens1 = xbt_str_split(expr, ";");
231     xbt_dynar_t tokens2;
232
233     loc->type = e_dw_compose;
234     loc->location.compose = xbt_dynar_new(sizeof(dw_location_t), NULL);
235
236     while(cursor < xbt_dynar_length(tokens1)){
237
238       tok = xbt_dynar_get_as(tokens1, cursor, char*);
239       tokens2 = xbt_str_split(tok, " ");
240       tok2 = xbt_dynar_get_as(tokens2, 0, char*);
241       
242       if(strncmp(tok2, "DW_OP_reg", 9) == 0){
243         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
244         new_element->type = e_dw_register;
245         new_element->location.reg = atoi(strtok(tok2, "DW_OP_reg"));
246         xbt_dynar_push(loc->location.compose, &new_element);     
247       }else if(strcmp(tok2, "DW_OP_fbreg:") == 0){
248         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
249         new_element->type = e_dw_fbregister_op;
250         new_element->location.fbreg_op = atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*));
251         xbt_dynar_push(loc->location.compose, &new_element);
252       }else if(strncmp(tok2, "DW_OP_breg", 10) == 0){
253         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
254         new_element->type = e_dw_bregister_op;
255         new_element->location.breg_op.reg = atoi(strtok(tok2, "DW_OP_breg"));
256         new_element->location.breg_op.offset = atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*));
257         xbt_dynar_push(loc->location.compose, &new_element);
258       }else if(strncmp(tok2, "DW_OP_lit", 9) == 0){
259         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
260         new_element->type = e_dw_lit;
261         new_element->location.lit = atoi(strtok(tok2, "DW_OP_lit"));
262         xbt_dynar_push(loc->location.compose, &new_element);
263       }else if(strcmp(tok2, "DW_OP_piece:") == 0){
264         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
265         new_element->type = e_dw_piece;
266         new_element->location.piece = atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*));
267         xbt_dynar_push(loc->location.compose, &new_element);
268       }else if(strcmp(tok2, "DW_OP_plus_uconst:") == 0){
269         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
270         new_element->type = e_dw_plus_uconst;
271         new_element->location.plus_uconst = atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char *));
272         xbt_dynar_push(loc->location.compose, &new_element);
273       }else if(strcmp(tok, "DW_OP_abs") == 0 || 
274                strcmp(tok, "DW_OP_and") == 0 ||
275                strcmp(tok, "DW_OP_div") == 0 ||
276                strcmp(tok, "DW_OP_minus") == 0 ||
277                strcmp(tok, "DW_OP_mod") == 0 ||
278                strcmp(tok, "DW_OP_mul") == 0 ||
279                strcmp(tok, "DW_OP_neg") == 0 ||
280                strcmp(tok, "DW_OP_not") == 0 ||
281                strcmp(tok, "DW_OP_or") == 0 ||
282                strcmp(tok, "DW_OP_plus") == 0){               
283         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
284         new_element->type = e_dw_arithmetic;
285         new_element->location.arithmetic = strdup(strtok(tok2, "DW_OP_"));
286         xbt_dynar_push(loc->location.compose, &new_element);
287       }else if(strcmp(tok, "DW_OP_stack_value") == 0){
288       }else if(strcmp(tok2, "DW_OP_deref_size:") == 0){
289         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
290         new_element->type = e_dw_deref;
291         new_element->location.deref_size = (unsigned int short) atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*));
292         xbt_dynar_push(loc->location.compose, &new_element);
293       }else if(strcmp(tok, "DW_OP_deref") == 0){
294         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
295         new_element->type = e_dw_deref;
296         new_element->location.deref_size = sizeof(void *);
297         xbt_dynar_push(loc->location.compose, &new_element);
298       }else if(strcmp(tok2, "DW_OP_constu:") == 0){
299         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
300         new_element->type = e_dw_uconstant;
301         new_element->location.uconstant.bytes = 1;
302         new_element->location.uconstant.value = (unsigned long int)(atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*)));
303         xbt_dynar_push(loc->location.compose, &new_element);
304       }else if(strcmp(tok2, "DW_OP_consts:") == 0){
305         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
306         new_element->type = e_dw_sconstant;
307         new_element->location.sconstant.bytes = 1;
308         new_element->location.sconstant.value = (long int)(atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*)));
309         xbt_dynar_push(loc->location.compose, &new_element);
310       }else if(strcmp(tok2, "DW_OP_const1u:") == 0 ||
311                strcmp(tok2, "DW_OP_const2u:") == 0 ||
312                strcmp(tok2, "DW_OP_const4u:") == 0 ||
313                strcmp(tok2, "DW_OP_const8u:") == 0){
314         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
315         new_element->type = e_dw_uconstant;
316         new_element->location.uconstant.bytes = tok2[11] - '0';
317         new_element->location.uconstant.value = (unsigned long int)(atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*)));
318         xbt_dynar_push(loc->location.compose, &new_element);
319       }else if(strcmp(tok, "DW_OP_const1s") == 0 ||
320                strcmp(tok, "DW_OP_const2s") == 0 ||
321                strcmp(tok, "DW_OP_const4s") == 0 ||
322                strcmp(tok, "DW_OP_const8s") == 0){
323         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
324         new_element->type = e_dw_sconstant;
325         new_element->location.sconstant.bytes = tok2[11] - '0';
326         new_element->location.sconstant.value = (long int)(atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*)));
327         xbt_dynar_push(loc->location.compose, &new_element);
328       }else{
329         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
330         new_element->type = e_dw_unsupported;
331         xbt_dynar_push(loc->location.compose, &new_element);
332       }
333
334       cursor++;
335       xbt_dynar_free(&tokens2);
336
337     }
338     
339     xbt_dynar_free(&tokens1);
340
341     return loc;
342     
343   }
344
345 }
346
347
348 /** \brief Finds a frame (DW_TAG_subprogram) from an DWARF offset in the rangd of this subprogram
349  *
350  * The offset can be an offset of a child DW_TAG_variable.
351  */
352 static dw_frame_t MC_dwarf_get_frame_by_offset(xbt_dict_t all_variables, unsigned long int offset){
353
354   xbt_dict_cursor_t cursor = NULL;
355   char *name;
356   dw_frame_t res;
357
358   xbt_dict_foreach(all_variables, cursor, name, res) {
359     if(offset >= res->start && offset < res->end){
360       xbt_dict_cursor_free(&cursor);
361       return res;
362     }
363   }
364
365   xbt_dict_cursor_free(&cursor);
366   return NULL;
367   
368 }
369
370 static dw_variable_t MC_dwarf_get_variable_by_name(dw_frame_t frame, char *var){
371
372   unsigned int cursor = 0;
373   dw_variable_t current_var;
374
375   xbt_dynar_foreach(frame->variables, cursor, current_var){
376     if(strcmp(var, current_var->name) == 0)
377       return current_var;
378   }
379
380   return NULL;
381 }
382
383 static int MC_dwarf_get_variable_index(xbt_dynar_t variables, char* var, void *address){
384
385   if(xbt_dynar_is_empty(variables))
386     return 0;
387
388   unsigned int cursor = 0;
389   int start = 0;
390   int end = xbt_dynar_length(variables) - 1;
391   dw_variable_t var_test = NULL;
392
393   while(start <= end){
394     cursor = (start + end) / 2;
395     var_test = (dw_variable_t)xbt_dynar_get_as(variables, cursor, dw_variable_t);
396     if(strcmp(var_test->name, var) < 0){
397       start = cursor + 1;
398     }else if(strcmp(var_test->name, var) > 0){
399       end = cursor - 1;
400     }else{
401       if(address){ /* global variable */
402         if(var_test->address.address == address)
403           return -1;
404         if(var_test->address.address > address)
405           end = cursor - 1;
406         else
407           start = cursor + 1;
408       }else{ /* local variable */
409         return -1;
410       }
411     }
412   }
413
414   if(strcmp(var_test->name, var) == 0){
415     if(address && var_test->address.address < address)
416       return cursor+1;
417     else
418       return cursor;
419   }else if(strcmp(var_test->name, var) < 0)
420     return cursor+1;
421   else
422     return cursor;
423
424 }
425
426 void MC_dwarf_register_global_variable(mc_object_info_t info, dw_variable_t variable) {
427   int index = MC_dwarf_get_variable_index(info->global_variables, variable->name, variable->address.address);
428   if (index != -1)
429     xbt_dynar_insert_at(info->global_variables, index, &variable);
430   // TODO, else ?
431 }
432
433 void MC_dwarf_register_non_global_variable(mc_object_info_t info, dw_frame_t frame, dw_variable_t variable) {
434   xbt_assert(frame, "Frame is NULL");
435   int index = MC_dwarf_get_variable_index(frame->variables, variable->name, NULL);
436   if (index != -1)
437     xbt_dynar_insert_at(frame->variables, index, &variable);
438   // TODO, else ?
439 }
440
441 void MC_dwarf_register_variable(mc_object_info_t info, dw_frame_t frame, dw_variable_t variable) {
442   if(variable->global)
443     MC_dwarf_register_global_variable(info, variable);
444   else if(frame==NULL)
445     xbt_die("No frame for this local variable");
446   else
447     MC_dwarf_register_non_global_variable(info, frame, variable);
448 }
449
450 static void MC_post_process_array_size(mc_object_info_t info, dw_type_t type) {
451   xbt_assert(type->dw_type_id, "No base type for array <%p>%s", type->id, type->name);
452   dw_type_t subtype = xbt_dict_get_or_null(info->types, type->dw_type_id);
453   xbt_assert(subtype, "Unkown base type <%s> for array <%p>%s", type->dw_type_id, type->id, type->name);
454   if(subtype->type==DW_TAG_array_type && type->byte_size==0) {
455           MC_post_process_array_size(info, subtype);
456   }
457   type->byte_size = type->element_count*subtype->byte_size;
458 }
459
460 static void MC_post_process_types(mc_object_info_t info) {
461   xbt_dict_cursor_t cursor;
462   char *origin;
463   dw_type_t type;
464   xbt_dict_foreach(info->types, cursor, origin, type){
465     if(type->type==DW_TAG_array_type && type->byte_size==0)
466       MC_post_process_array_size(info, type);
467   }
468 }
469
470 /*******************************  Ignore mechanism *******************************/
471 /*********************************************************************************/
472
473 xbt_dynar_t mc_checkpoint_ignore;
474
475 typedef struct s_mc_stack_ignore_variable{
476   char *var_name;
477   char *frame;
478 }s_mc_stack_ignore_variable_t, *mc_stack_ignore_variable_t;
479
480 typedef struct s_mc_data_bss_ignore_variable{
481   char *name;
482 }s_mc_data_bss_ignore_variable_t, *mc_data_bss_ignore_variable_t;
483
484 /**************************** Free functions ******************************/
485
486 static void stack_ignore_variable_free(mc_stack_ignore_variable_t v){
487   xbt_free(v->var_name);
488   xbt_free(v->frame);
489   xbt_free(v);
490 }
491
492 static void stack_ignore_variable_free_voidp(void *v){
493   stack_ignore_variable_free((mc_stack_ignore_variable_t) * (void **) v);
494 }
495
496 void heap_ignore_region_free(mc_heap_ignore_region_t r){
497   xbt_free(r);
498 }
499
500 void heap_ignore_region_free_voidp(void *r){
501   heap_ignore_region_free((mc_heap_ignore_region_t) * (void **) r);
502 }
503
504 static void data_bss_ignore_variable_free(mc_data_bss_ignore_variable_t v){
505   xbt_free(v->name);
506   xbt_free(v);
507 }
508
509 static void data_bss_ignore_variable_free_voidp(void *v){
510   data_bss_ignore_variable_free((mc_data_bss_ignore_variable_t) * (void **) v);
511 }
512
513 static void checkpoint_ignore_region_free(mc_checkpoint_ignore_region_t r){
514   xbt_free(r);
515 }
516
517 static void checkpoint_ignore_region_free_voidp(void *r){
518   checkpoint_ignore_region_free((mc_checkpoint_ignore_region_t) * (void **) r);
519 }
520
521 /***********************************************************************/
522
523 void MC_ignore_heap(void *address, size_t size){
524
525   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
526
527   MC_SET_RAW_MEM;
528
529   mc_heap_ignore_region_t region = NULL;
530   region = xbt_new0(s_mc_heap_ignore_region_t, 1);
531   region->address = address;
532   region->size = size;
533   
534   region->block = ((char*)address - (char*)((xbt_mheap_t)std_heap)->heapbase) / BLOCKSIZE + 1;
535   
536   if(((xbt_mheap_t)std_heap)->heapinfo[region->block].type == 0){
537     region->fragment = -1;
538     ((xbt_mheap_t)std_heap)->heapinfo[region->block].busy_block.ignore++;
539   }else{
540     region->fragment = ((uintptr_t) (ADDR2UINT (address) % (BLOCKSIZE))) >> ((xbt_mheap_t)std_heap)->heapinfo[region->block].type;
541     ((xbt_mheap_t)std_heap)->heapinfo[region->block].busy_frag.ignore[region->fragment]++;
542   }
543   
544   if(mc_heap_comparison_ignore == NULL){
545     mc_heap_comparison_ignore = xbt_dynar_new(sizeof(mc_heap_ignore_region_t), heap_ignore_region_free_voidp);
546     xbt_dynar_push(mc_heap_comparison_ignore, &region);
547     if(!raw_mem_set)
548       MC_UNSET_RAW_MEM;
549     return;
550   }
551
552   unsigned int cursor = 0;
553   mc_heap_ignore_region_t current_region = NULL;
554   int start = 0;
555   int end = xbt_dynar_length(mc_heap_comparison_ignore) - 1;
556   
557   while(start <= end){
558     cursor = (start + end) / 2;
559     current_region = (mc_heap_ignore_region_t)xbt_dynar_get_as(mc_heap_comparison_ignore, cursor, mc_heap_ignore_region_t);
560     if(current_region->address == address){
561       heap_ignore_region_free(region);
562       if(!raw_mem_set)
563         MC_UNSET_RAW_MEM;
564       return;
565     }else if(current_region->address < address){
566       start = cursor + 1;
567     }else{
568       end = cursor - 1;
569     }   
570   }
571
572   if(current_region->address < address)
573     xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor + 1, &region);
574   else
575     xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor, &region);
576
577   if(!raw_mem_set)
578     MC_UNSET_RAW_MEM;
579 }
580
581 void MC_remove_ignore_heap(void *address, size_t size){
582
583   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
584
585   MC_SET_RAW_MEM;
586
587   unsigned int cursor = 0;
588   int start = 0;
589   int end = xbt_dynar_length(mc_heap_comparison_ignore) - 1;
590   mc_heap_ignore_region_t region;
591   int ignore_found = 0;
592
593   while(start <= end){
594     cursor = (start + end) / 2;
595     region = (mc_heap_ignore_region_t)xbt_dynar_get_as(mc_heap_comparison_ignore, cursor, mc_heap_ignore_region_t);
596     if(region->address == address){
597       ignore_found = 1;
598       break;
599     }else if(region->address < address){
600       start = cursor + 1;
601     }else{
602       if((char * )region->address <= ((char *)address + size)){
603         ignore_found = 1;
604         break;
605       }else{
606         end = cursor - 1;   
607       }
608     }
609   }
610   
611   if(ignore_found == 1){
612     xbt_dynar_remove_at(mc_heap_comparison_ignore, cursor, NULL);
613     MC_remove_ignore_heap(address, size);
614   }
615
616   if(!raw_mem_set)
617     MC_UNSET_RAW_MEM;
618
619 }
620
621 void MC_ignore_global_variable(const char *name){
622
623   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
624
625   MC_SET_RAW_MEM;
626
627   if(mc_libsimgrid_info){
628
629     unsigned int cursor = 0;
630     dw_variable_t current_var;
631     int start = 0;
632     int end = xbt_dynar_length(mc_libsimgrid_info->global_variables) - 1;
633
634     while(start <= end){
635       cursor = (start + end) /2;
636       current_var = (dw_variable_t)xbt_dynar_get_as(mc_libsimgrid_info->global_variables, cursor, dw_variable_t);
637       if(strcmp(current_var->name, name) == 0){
638         xbt_dynar_remove_at(mc_libsimgrid_info->global_variables, cursor, NULL);
639         start = 0;
640         end = xbt_dynar_length(mc_libsimgrid_info->global_variables) - 1;
641       }else if(strcmp(current_var->name, name) < 0){
642         start = cursor + 1;
643       }else{
644         end = cursor - 1;
645       } 
646     }
647    
648   }else{
649
650     if(mc_data_bss_comparison_ignore == NULL)
651       mc_data_bss_comparison_ignore = xbt_dynar_new(sizeof(mc_data_bss_ignore_variable_t), data_bss_ignore_variable_free_voidp);
652
653     mc_data_bss_ignore_variable_t var = NULL;
654     var = xbt_new0(s_mc_data_bss_ignore_variable_t, 1);
655     var->name = strdup(name);
656
657     if(xbt_dynar_is_empty(mc_data_bss_comparison_ignore)){
658
659       xbt_dynar_insert_at(mc_data_bss_comparison_ignore, 0, &var);
660
661     }else{
662     
663       unsigned int cursor = 0;
664       int start = 0;
665       int end = xbt_dynar_length(mc_data_bss_comparison_ignore) - 1;
666       mc_data_bss_ignore_variable_t current_var = NULL;
667
668       while(start <= end){
669         cursor = (start + end) / 2;
670         current_var = (mc_data_bss_ignore_variable_t)xbt_dynar_get_as(mc_data_bss_comparison_ignore, cursor, mc_data_bss_ignore_variable_t);
671         if(strcmp(current_var->name, name) == 0){
672           data_bss_ignore_variable_free(var);
673           if(!raw_mem_set)
674             MC_UNSET_RAW_MEM;
675           return;
676         }else if(strcmp(current_var->name, name) < 0){
677           start = cursor + 1;
678         }else{
679           end = cursor - 1;
680         }
681       }
682
683       if(strcmp(current_var->name, name) < 0)
684         xbt_dynar_insert_at(mc_data_bss_comparison_ignore, cursor + 1, &var);
685       else
686         xbt_dynar_insert_at(mc_data_bss_comparison_ignore, cursor, &var);
687
688     }
689   }
690
691   if(!raw_mem_set)
692     MC_UNSET_RAW_MEM;
693 }
694
695 void MC_ignore_local_variable(const char *var_name, const char *frame_name){
696   
697   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
698
699   MC_SET_RAW_MEM;
700
701   if(mc_libsimgrid_info){
702     unsigned int cursor = 0;
703     dw_variable_t current_var;
704     int start, end;
705     if(strcmp(frame_name, "*") == 0){ /* Remove variable in all frames */
706       xbt_dict_cursor_t dict_cursor;
707       char *current_frame_name;
708       dw_frame_t frame;
709       xbt_dict_foreach(mc_libsimgrid_info->local_variables, dict_cursor, current_frame_name, frame){
710         start = 0;
711         end = xbt_dynar_length(frame->variables) - 1;
712         while(start <= end){
713           cursor = (start + end) / 2;
714           current_var = (dw_variable_t)xbt_dynar_get_as(frame->variables, cursor, dw_variable_t); 
715           if(strcmp(current_var->name, var_name) == 0){
716             xbt_dynar_remove_at(frame->variables, cursor, NULL);
717             start = 0;
718             end = xbt_dynar_length(frame->variables) - 1;
719           }else if(strcmp(current_var->name, var_name) < 0){
720             start = cursor + 1;
721           }else{
722             end = cursor - 1;
723           } 
724         }
725       }
726        xbt_dict_foreach(mc_binary_info->local_variables, dict_cursor, current_frame_name, frame){
727         start = 0;
728         end = xbt_dynar_length(frame->variables) - 1;
729         while(start <= end){
730           cursor = (start + end) / 2;
731           current_var = (dw_variable_t)xbt_dynar_get_as(frame->variables, cursor, dw_variable_t); 
732           if(strcmp(current_var->name, var_name) == 0){
733             xbt_dynar_remove_at(frame->variables, cursor, NULL);
734             start = 0;
735             end = xbt_dynar_length(frame->variables) - 1;
736           }else if(strcmp(current_var->name, var_name) < 0){
737             start = cursor + 1;
738           }else{
739             end = cursor - 1;
740           } 
741         }
742       }
743     }else{
744       xbt_dynar_t variables_list = ((dw_frame_t)xbt_dict_get_or_null(
745                                       mc_libsimgrid_info->local_variables, frame_name))->variables;
746       start = 0;
747       end = xbt_dynar_length(variables_list) - 1;
748       while(start <= end){
749         cursor = (start + end) / 2;
750         current_var = (dw_variable_t)xbt_dynar_get_as(variables_list, cursor, dw_variable_t);
751         if(strcmp(current_var->name, var_name) == 0){
752           xbt_dynar_remove_at(variables_list, cursor, NULL);
753           start = 0;
754           end = xbt_dynar_length(variables_list) - 1;
755         }else if(strcmp(current_var->name, var_name) < 0){
756           start = cursor + 1;
757         }else{
758           end = cursor - 1;
759         } 
760       }
761     } 
762   }else{
763
764     if(mc_stack_comparison_ignore == NULL)
765       mc_stack_comparison_ignore = xbt_dynar_new(sizeof(mc_stack_ignore_variable_t), stack_ignore_variable_free_voidp);
766   
767     mc_stack_ignore_variable_t var = NULL;
768     var = xbt_new0(s_mc_stack_ignore_variable_t, 1);
769     var->var_name = strdup(var_name);
770     var->frame = strdup(frame_name);
771   
772     if(xbt_dynar_is_empty(mc_stack_comparison_ignore)){
773
774       xbt_dynar_insert_at(mc_stack_comparison_ignore, 0, &var);
775
776     }else{
777     
778       unsigned int cursor = 0;
779       int start = 0;
780       int end = xbt_dynar_length(mc_stack_comparison_ignore) - 1;
781       mc_stack_ignore_variable_t current_var = NULL;
782
783       while(start <= end){
784         cursor = (start + end) / 2;
785         current_var = (mc_stack_ignore_variable_t)xbt_dynar_get_as(mc_stack_comparison_ignore, cursor, mc_stack_ignore_variable_t);
786         if(strcmp(current_var->frame, frame_name) == 0){
787           if(strcmp(current_var->var_name, var_name) == 0){
788             stack_ignore_variable_free(var);
789             if(!raw_mem_set)
790               MC_UNSET_RAW_MEM;
791             return;
792           }else if(strcmp(current_var->var_name, var_name) < 0){
793             start = cursor + 1;
794           }else{
795             end = cursor - 1;
796           }
797         }else if(strcmp(current_var->frame, frame_name) < 0){
798           start = cursor + 1;
799         }else{
800           end = cursor - 1;
801         }
802       }
803
804       if(strcmp(current_var->frame, frame_name) == 0){
805         if(strcmp(current_var->var_name, var_name) < 0){
806           xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor + 1, &var);
807         }else{
808           xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor, &var);
809         }
810       }else if(strcmp(current_var->frame, frame_name) < 0){
811         xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor + 1, &var);
812       }else{
813         xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor, &var);
814       }
815     }
816   }
817
818   if(!raw_mem_set)
819     MC_UNSET_RAW_MEM;
820
821 }
822
823 void MC_new_stack_area(void *stack, char *name, void* context, size_t size){
824
825   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
826
827   MC_SET_RAW_MEM;
828
829   if(stacks_areas == NULL)
830     stacks_areas = xbt_dynar_new(sizeof(stack_region_t), NULL);
831   
832   stack_region_t region = NULL;
833   region = xbt_new0(s_stack_region_t, 1);
834   region->address = stack;
835   region->process_name = strdup(name);
836   region->context = context;
837   region->size = size;
838   region->block = ((char*)stack - (char*)((xbt_mheap_t)std_heap)->heapbase) / BLOCKSIZE + 1;
839   xbt_dynar_push(stacks_areas, &region);
840
841   if(!raw_mem_set)
842     MC_UNSET_RAW_MEM;
843 }
844
845 void MC_ignore(void *addr, size_t size){
846
847   int raw_mem_set= (mmalloc_get_current_heap() == raw_heap);
848
849   MC_SET_RAW_MEM;
850
851   if(mc_checkpoint_ignore == NULL)
852     mc_checkpoint_ignore = xbt_dynar_new(sizeof(mc_checkpoint_ignore_region_t), checkpoint_ignore_region_free_voidp);
853
854   mc_checkpoint_ignore_region_t region = xbt_new0(s_mc_checkpoint_ignore_region_t, 1);
855   region->addr = addr;
856   region->size = size;
857
858   if(xbt_dynar_is_empty(mc_checkpoint_ignore)){
859     xbt_dynar_push(mc_checkpoint_ignore, &region);
860   }else{
861      
862     unsigned int cursor = 0;
863     int start = 0;
864     int end = xbt_dynar_length(mc_checkpoint_ignore) -1;
865     mc_checkpoint_ignore_region_t current_region = NULL;
866
867     while(start <= end){
868       cursor = (start + end) / 2;
869       current_region = (mc_checkpoint_ignore_region_t)xbt_dynar_get_as(mc_checkpoint_ignore, cursor, mc_checkpoint_ignore_region_t);
870       if(current_region->addr == addr){
871         if(current_region->size == size){
872           checkpoint_ignore_region_free(region);
873           if(!raw_mem_set)
874             MC_UNSET_RAW_MEM;
875           return;
876         }else if(current_region->size < size){
877           start = cursor + 1;
878         }else{
879           end = cursor - 1;
880         }
881       }else if(current_region->addr < addr){
882           start = cursor + 1;
883       }else{
884         end = cursor - 1;
885       }
886     }
887
888      if(current_region->addr == addr){
889        if(current_region->size < size){
890         xbt_dynar_insert_at(mc_checkpoint_ignore, cursor + 1, &region);
891       }else{
892         xbt_dynar_insert_at(mc_checkpoint_ignore, cursor, &region);
893       }
894     }else if(current_region->addr < addr){
895        xbt_dynar_insert_at(mc_checkpoint_ignore, cursor + 1, &region);
896     }else{
897        xbt_dynar_insert_at(mc_checkpoint_ignore, cursor, &region);
898     }
899   }
900
901   if(!raw_mem_set)
902     MC_UNSET_RAW_MEM;
903 }
904
905 /*******************************  Initialisation of MC *******************************/
906 /*********************************************************************************/
907
908 static void MC_dump_ignored_local_variables(void){
909
910   if(mc_stack_comparison_ignore == NULL || xbt_dynar_is_empty(mc_stack_comparison_ignore))
911     return;
912
913   unsigned int cursor = 0;
914   mc_stack_ignore_variable_t current_var;
915
916   xbt_dynar_foreach(mc_stack_comparison_ignore, cursor, current_var){
917     MC_ignore_local_variable(current_var->var_name, current_var->frame);
918   }
919
920   xbt_dynar_free(&mc_stack_comparison_ignore);
921   mc_stack_comparison_ignore = NULL;
922  
923 }
924
925 static void MC_dump_ignored_global_variables(void){
926
927   if(mc_data_bss_comparison_ignore == NULL || xbt_dynar_is_empty(mc_data_bss_comparison_ignore))
928     return;
929
930   unsigned int cursor = 0;
931   mc_data_bss_ignore_variable_t current_var;
932
933   xbt_dynar_foreach(mc_data_bss_comparison_ignore, cursor, current_var){
934     MC_ignore_global_variable(current_var->name);
935   } 
936
937   xbt_dynar_free(&mc_data_bss_comparison_ignore);
938   mc_data_bss_comparison_ignore = NULL;
939
940 }
941
942 static void MC_init_debug_info();
943 static void MC_init_debug_info() {
944   XBT_INFO("Get debug information ...");
945
946   memory_map_t maps = MC_get_memory_map();
947
948   /* Get local variables for state equality detection */
949   mc_binary_info = MC_find_object_info(maps, xbt_binary_name);
950   mc_libsimgrid_info = MC_find_object_info(maps, libsimgrid_path);
951
952   MC_free_memory_map(maps);
953   XBT_INFO("Get debug information done !");
954 }
955
956 void MC_init(){
957
958   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
959
960   compare = 0;
961
962   /* Initialize the data structures that must be persistent across every
963      iteration of the model-checker (in RAW memory) */
964
965   MC_SET_RAW_MEM;
966
967   MC_init_memory_map_info();
968   MC_init_debug_info();
969
970   /* Remove variables ignored before getting list of variables */
971   MC_dump_ignored_local_variables();
972   MC_dump_ignored_global_variables();
973
974    /* Init parmap */
975   parmap = xbt_parmap_mc_new(xbt_os_get_numcores(), XBT_PARMAP_DEFAULT);
976
977   MC_UNSET_RAW_MEM;
978
979    /* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */
980   MC_ignore_local_variable("e", "*");
981   MC_ignore_local_variable("__ex_cleanup", "*");
982   MC_ignore_local_variable("__ex_mctx_en", "*");
983   MC_ignore_local_variable("__ex_mctx_me", "*");
984   MC_ignore_local_variable("__xbt_ex_ctx_ptr", "*");
985   MC_ignore_local_variable("_log_ev", "*");
986   MC_ignore_local_variable("_throw_ctx", "*");
987   MC_ignore_local_variable("ctx", "*");
988
989   MC_ignore_local_variable("next_context", "smx_ctx_sysv_suspend_serial");
990   MC_ignore_local_variable("i", "smx_ctx_sysv_suspend_serial");
991
992   /* Ignore local variable about time used for tracing */
993   MC_ignore_local_variable("start_time", "*"); 
994
995   MC_ignore_global_variable("mc_comp_times");
996   MC_ignore_global_variable("mc_snapshot_comparison_time"); 
997   MC_ignore_global_variable("mc_time");
998   MC_ignore_global_variable("smpi_current_rank");
999   MC_ignore_global_variable("counter"); /* Static variable used for tracing */
1000   MC_ignore_global_variable("maestro_stack_start");
1001   MC_ignore_global_variable("maestro_stack_end");
1002
1003   MC_ignore_heap(&(simix_global->process_to_run), sizeof(simix_global->process_to_run));
1004   MC_ignore_heap(&(simix_global->process_that_ran), sizeof(simix_global->process_that_ran));
1005   MC_ignore_heap(simix_global->process_to_run, sizeof(*(simix_global->process_to_run)));
1006   MC_ignore_heap(simix_global->process_that_ran, sizeof(*(simix_global->process_that_ran)));
1007   
1008   smx_process_t process;
1009   xbt_swag_foreach(process, simix_global->process_list){
1010     MC_ignore_heap(&(process->process_hookup), sizeof(process->process_hookup));
1011   }
1012
1013   if(raw_mem_set)
1014     MC_SET_RAW_MEM;
1015
1016 }
1017
1018 static void MC_init_dot_output(){ /* FIXME : more colors */
1019
1020   colors[0] = "blue";
1021   colors[1] = "red";
1022   colors[2] = "green3";
1023   colors[3] = "goldenrod";
1024   colors[4] = "brown";
1025   colors[5] = "purple";
1026   colors[6] = "magenta";
1027   colors[7] = "turquoise4";
1028   colors[8] = "gray25";
1029   colors[9] = "forestgreen";
1030   colors[10] = "hotpink";
1031   colors[11] = "lightblue";
1032   colors[12] = "tan";
1033
1034   dot_output = fopen(_sg_mc_dot_output_file, "w");
1035   
1036   if(dot_output == NULL){
1037     perror("Error open dot output file");
1038     xbt_abort();
1039   }
1040
1041   fprintf(dot_output, "digraph graphname{\n fixedsize=true; rankdir=TB; ranksep=.25; edge [fontsize=12]; node [fontsize=10, shape=circle,width=.5 ]; graph [resolution=20, fontsize=10];\n");
1042
1043 }
1044
1045 /*******************************  Core of MC *******************************/
1046 /**************************************************************************/
1047
1048 void MC_do_the_modelcheck_for_real() {
1049
1050   MC_SET_RAW_MEM;
1051   mc_comp_times = xbt_new0(s_mc_comparison_times_t, 1);
1052   MC_UNSET_RAW_MEM;
1053   
1054   if (!_sg_mc_property_file || _sg_mc_property_file[0]=='\0') {
1055     if (mc_reduce_kind==e_mc_reduce_unset)
1056       mc_reduce_kind=e_mc_reduce_dpor;
1057
1058     XBT_INFO("Check a safety property");
1059     MC_modelcheck_safety();
1060
1061   } else  {
1062
1063     if (mc_reduce_kind==e_mc_reduce_unset)
1064       mc_reduce_kind=e_mc_reduce_none;
1065
1066     XBT_INFO("Check the liveness property %s",_sg_mc_property_file);
1067     MC_automaton_load(_sg_mc_property_file);
1068     MC_modelcheck_liveness();
1069   }
1070 }
1071
1072 void MC_modelcheck_safety(void)
1073 {
1074   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1075
1076   /* Check if MC is already initialized */
1077   if (initial_state_safety)
1078     return;
1079
1080   mc_time = xbt_new0(double, simix_process_maxpid);
1081
1082   /* mc_time refers to clock for each process -> ignore it for heap comparison */  
1083   MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
1084
1085   /* Initialize the data structures that must be persistent across every
1086      iteration of the model-checker (in RAW memory) */
1087   
1088   MC_SET_RAW_MEM;
1089
1090   /* Initialize statistics */
1091   mc_stats = xbt_new0(s_mc_stats_t, 1);
1092   mc_stats->state_size = 1;
1093
1094   /* Create exploration stack */
1095   mc_stack_safety = xbt_fifo_new();
1096
1097   if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0'))
1098     MC_init_dot_output();
1099
1100   MC_UNSET_RAW_MEM;
1101
1102   if(_sg_mc_visited > 0){
1103     MC_init();
1104   }else{
1105     MC_SET_RAW_MEM;
1106     MC_init_memory_map_info();
1107     MC_init_debug_info();
1108     MC_UNSET_RAW_MEM;
1109   }
1110
1111   MC_dpor_init();
1112
1113   MC_SET_RAW_MEM;
1114   /* Save the initial state */
1115   initial_state_safety = xbt_new0(s_mc_global_t, 1);
1116   initial_state_safety->snapshot = MC_take_snapshot(0);
1117   initial_state_safety->initial_communications_pattern_done = 0;
1118   initial_state_safety->comm_deterministic = 1;
1119   initial_state_safety->send_deterministic = 1;
1120   MC_UNSET_RAW_MEM;
1121
1122   MC_dpor();
1123
1124   if(raw_mem_set)
1125     MC_SET_RAW_MEM;
1126
1127   xbt_abort();
1128   //MC_exit();
1129 }
1130
1131 void MC_modelcheck_liveness(){
1132
1133   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1134
1135   MC_init();
1136
1137   mc_time = xbt_new0(double, simix_process_maxpid);
1138
1139   /* mc_time refers to clock for each process -> ignore it for heap comparison */  
1140   MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
1141  
1142   MC_SET_RAW_MEM;
1143  
1144   /* Initialize statistics */
1145   mc_stats = xbt_new0(s_mc_stats_t, 1);
1146   mc_stats->state_size = 1;
1147
1148   /* Create exploration stack */
1149   mc_stack_liveness = xbt_fifo_new();
1150
1151   /* Create the initial state */
1152   initial_state_liveness = xbt_new0(s_mc_global_t, 1);
1153
1154   if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0'))
1155     MC_init_dot_output();
1156   
1157   MC_UNSET_RAW_MEM;
1158
1159   MC_ddfs_init();
1160
1161   /* We're done */
1162   MC_print_statistics(mc_stats);
1163   xbt_free(mc_time);
1164
1165   if(raw_mem_set)
1166     MC_SET_RAW_MEM;
1167
1168 }
1169
1170
1171 void MC_exit(void)
1172 {
1173   xbt_free(mc_time);
1174
1175   MC_memory_exit();
1176   //xbt_abort();
1177 }
1178
1179 int SIMIX_pre_mc_random(smx_simcall_t simcall, int min, int max){
1180
1181   return simcall->mc_value;
1182 }
1183
1184
1185 int MC_random(int min, int max)
1186 {
1187   /*FIXME: return mc_current_state->executed_transition->random.value;*/
1188   return simcall_mc_random(min, max);
1189 }
1190
1191 /**
1192  * \brief Schedules all the process that are ready to run
1193  */
1194 void MC_wait_for_requests(void)
1195 {
1196   smx_process_t process;
1197   smx_simcall_t req;
1198   unsigned int iter;
1199
1200   while (!xbt_dynar_is_empty(simix_global->process_to_run)) {
1201     SIMIX_process_runall();
1202     xbt_dynar_foreach(simix_global->process_that_ran, iter, process) {
1203       req = &process->simcall;
1204       if (req->call != SIMCALL_NONE && !MC_request_is_visible(req))
1205         SIMIX_simcall_pre(req, 0);
1206     }
1207   }
1208 }
1209
1210 int MC_deadlock_check()
1211 {
1212   int deadlock = FALSE;
1213   smx_process_t process;
1214   if(xbt_swag_size(simix_global->process_list)){
1215     deadlock = TRUE;
1216     xbt_swag_foreach(process, simix_global->process_list){
1217       if(process->simcall.call != SIMCALL_NONE
1218          && MC_request_is_enabled(&process->simcall)){
1219         deadlock = FALSE;
1220         break;
1221       }
1222     }
1223   }
1224   return deadlock;
1225 }
1226
1227 /**
1228  * \brief Re-executes from the state at position start all the transitions indicated by
1229  *        a given model-checker stack.
1230  * \param stack The stack with the transitions to execute.
1231  * \param start Start index to begin the re-execution.
1232  */
1233 void MC_replay(xbt_fifo_t stack, int start)
1234 {
1235   int raw_mem = (mmalloc_get_current_heap() == raw_heap);
1236
1237   int value, i = 1, count = 1;
1238   char *req_str;
1239   smx_simcall_t req = NULL, saved_req = NULL;
1240   xbt_fifo_item_t item, start_item;
1241   mc_state_t state;
1242   smx_process_t process = NULL;
1243   int comm_pattern = 0;
1244
1245   XBT_DEBUG("**** Begin Replay ****");
1246
1247   if(start == -1){
1248     /* Restore the initial state */
1249     MC_restore_snapshot(initial_state_safety->snapshot);
1250     /* At the moment of taking the snapshot the raw heap was set, so restoring
1251      * it will set it back again, we have to unset it to continue  */
1252     MC_UNSET_RAW_MEM;
1253   }
1254
1255   start_item = xbt_fifo_get_last_item(stack);
1256   if(start != -1){
1257     while (i != start){
1258       start_item = xbt_fifo_get_prev_item(start_item);
1259       i++;
1260     }
1261   }
1262
1263   MC_SET_RAW_MEM;
1264   xbt_dict_reset(first_enabled_state);
1265   xbt_swag_foreach(process, simix_global->process_list){
1266     if(MC_process_is_enabled(process)){
1267       char *key = bprintf("%lu", process->pid);
1268       char *data = bprintf("%d", count);
1269       xbt_dict_set(first_enabled_state, key, data, NULL);
1270       xbt_free(key);
1271     }
1272   }
1273   if(_sg_mc_comms_determinism)
1274     xbt_dynar_reset(communications_pattern);
1275   MC_UNSET_RAW_MEM;
1276   
1277
1278   /* Traverse the stack from the state at position start and re-execute the transitions */
1279   for (item = start_item;
1280        item != xbt_fifo_get_first_item(stack);
1281        item = xbt_fifo_get_prev_item(item)) {
1282
1283     state = (mc_state_t) xbt_fifo_get_item_content(item);
1284     saved_req = MC_state_get_executed_request(state, &value);
1285    
1286     MC_SET_RAW_MEM;
1287     char *key = bprintf("%lu", saved_req->issuer->pid);
1288     xbt_dict_remove(first_enabled_state, key); 
1289     xbt_free(key);
1290     MC_UNSET_RAW_MEM;
1291    
1292     if(saved_req){
1293       /* because we got a copy of the executed request, we have to fetch the  
1294          real one, pointed by the request field of the issuer process */
1295       req = &saved_req->issuer->simcall;
1296
1297       /* Debug information */
1298       if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
1299         req_str = MC_request_to_string(req, value);
1300         XBT_DEBUG("Replay: %s (%p)", req_str, state);
1301         xbt_free(req_str);
1302       }
1303     }
1304
1305     if(_sg_mc_comms_determinism){
1306       if(req->call == SIMCALL_COMM_ISEND)
1307         comm_pattern = 1;
1308       else if(req->call == SIMCALL_COMM_IRECV)
1309       comm_pattern = 2;
1310     }
1311
1312     SIMIX_simcall_pre(req, value);
1313
1314     if(_sg_mc_comms_determinism){
1315       MC_SET_RAW_MEM;
1316       if(comm_pattern != 0){
1317         get_comm_pattern(communications_pattern, req, comm_pattern);
1318       }
1319       MC_UNSET_RAW_MEM;
1320       comm_pattern = 0;
1321     }
1322     
1323     MC_wait_for_requests();
1324
1325     count++;
1326
1327     MC_SET_RAW_MEM;
1328     /* Insert in dict all enabled processes */
1329     xbt_swag_foreach(process, simix_global->process_list){
1330       if(MC_process_is_enabled(process) /*&& !MC_state_process_is_done(state, process)*/){
1331         char *key = bprintf("%lu", process->pid);
1332         if(xbt_dict_get_or_null(first_enabled_state, key) == NULL){
1333           char *data = bprintf("%d", count);
1334           xbt_dict_set(first_enabled_state, key, data, NULL);
1335         }
1336         xbt_free(key);
1337       }
1338     }
1339     MC_UNSET_RAW_MEM;
1340          
1341     /* Update statistics */
1342     mc_stats->visited_states++;
1343     mc_stats->executed_transitions++;
1344
1345   }
1346
1347   XBT_DEBUG("**** End Replay ****");
1348
1349   if(raw_mem)
1350     MC_SET_RAW_MEM;
1351   else
1352     MC_UNSET_RAW_MEM;
1353   
1354
1355 }
1356
1357 void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
1358 {
1359
1360   initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1361
1362   int value;
1363   char *req_str;
1364   smx_simcall_t req = NULL, saved_req = NULL;
1365   xbt_fifo_item_t item;
1366   mc_state_t state;
1367   mc_pair_t pair;
1368   int depth = 1;
1369
1370   XBT_DEBUG("**** Begin Replay ****");
1371
1372   /* Restore the initial state */
1373   MC_restore_snapshot(initial_state_liveness->snapshot);
1374
1375   /* At the moment of taking the snapshot the raw heap was set, so restoring
1376    * it will set it back again, we have to unset it to continue  */
1377   if(!initial_state_liveness->raw_mem_set)
1378     MC_UNSET_RAW_MEM;
1379
1380   if(all_stack){
1381
1382     item = xbt_fifo_get_last_item(stack);
1383
1384     while(depth <= xbt_fifo_size(stack)){
1385
1386       pair = (mc_pair_t) xbt_fifo_get_item_content(item);
1387       state = (mc_state_t) pair->graph_state;
1388
1389       if(pair->requests > 0){
1390    
1391         saved_req = MC_state_get_executed_request(state, &value);
1392         //XBT_DEBUG("SavedReq->call %u", saved_req->call);
1393       
1394         if(saved_req != NULL){
1395           /* because we got a copy of the executed request, we have to fetch the  
1396              real one, pointed by the request field of the issuer process */
1397           req = &saved_req->issuer->simcall;
1398           //XBT_DEBUG("Req->call %u", req->call);
1399   
1400           /* Debug information */
1401           if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
1402             req_str = MC_request_to_string(req, value);
1403             XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
1404             xbt_free(req_str);
1405           }
1406   
1407         }
1408  
1409         SIMIX_simcall_pre(req, value);
1410         MC_wait_for_requests();
1411       }
1412
1413       depth++;
1414     
1415       /* Update statistics */
1416       mc_stats->visited_pairs++;
1417       mc_stats->executed_transitions++;
1418
1419       item = xbt_fifo_get_prev_item(item);
1420     }
1421
1422   }else{
1423
1424     /* Traverse the stack from the initial state and re-execute the transitions */
1425     for (item = xbt_fifo_get_last_item(stack);
1426          item != xbt_fifo_get_first_item(stack);
1427          item = xbt_fifo_get_prev_item(item)) {
1428
1429       pair = (mc_pair_t) xbt_fifo_get_item_content(item);
1430       state = (mc_state_t) pair->graph_state;
1431
1432       if(pair->requests > 0){
1433    
1434         saved_req = MC_state_get_executed_request(state, &value);
1435         //XBT_DEBUG("SavedReq->call %u", saved_req->call);
1436       
1437         if(saved_req != NULL){
1438           /* because we got a copy of the executed request, we have to fetch the  
1439              real one, pointed by the request field of the issuer process */
1440           req = &saved_req->issuer->simcall;
1441           //XBT_DEBUG("Req->call %u", req->call);
1442   
1443           /* Debug information */
1444           if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
1445             req_str = MC_request_to_string(req, value);
1446             XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
1447             xbt_free(req_str);
1448           }
1449   
1450         }
1451  
1452         SIMIX_simcall_pre(req, value);
1453         MC_wait_for_requests();
1454       }
1455
1456       depth++;
1457     
1458       /* Update statistics */
1459       mc_stats->visited_pairs++;
1460       mc_stats->executed_transitions++;
1461     }
1462   }  
1463
1464   XBT_DEBUG("**** End Replay ****");
1465
1466   if(initial_state_liveness->raw_mem_set)
1467     MC_SET_RAW_MEM;
1468   else
1469     MC_UNSET_RAW_MEM;
1470   
1471 }
1472
1473 /**
1474  * \brief Dumps the contents of a model-checker's stack and shows the actual
1475  *        execution trace
1476  * \param stack The stack to dump
1477  */
1478 void MC_dump_stack_safety(xbt_fifo_t stack)
1479 {
1480   
1481   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1482
1483   MC_show_stack_safety(stack);
1484
1485   if(!_sg_mc_checkpoint){
1486
1487     mc_state_t state;
1488
1489     MC_SET_RAW_MEM;
1490     while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
1491       MC_state_delete(state);
1492     MC_UNSET_RAW_MEM;
1493
1494   }
1495
1496   if(raw_mem_set)
1497     MC_SET_RAW_MEM;
1498   else
1499     MC_UNSET_RAW_MEM;
1500   
1501 }
1502
1503
1504 void MC_show_stack_safety(xbt_fifo_t stack)
1505 {
1506
1507   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1508
1509   MC_SET_RAW_MEM;
1510
1511   int value;
1512   mc_state_t state;
1513   xbt_fifo_item_t item;
1514   smx_simcall_t req;
1515   char *req_str = NULL;
1516   
1517   for (item = xbt_fifo_get_last_item(stack);
1518        (item ? (state = (mc_state_t) (xbt_fifo_get_item_content(item)))
1519         : (NULL)); item = xbt_fifo_get_prev_item(item)) {
1520     req = MC_state_get_executed_request(state, &value);
1521     if(req){
1522       req_str = MC_request_to_string(req, value);
1523       XBT_INFO("%s", req_str);
1524       xbt_free(req_str);
1525     }
1526   }
1527
1528   if(!raw_mem_set)
1529     MC_UNSET_RAW_MEM;
1530 }
1531
1532 void MC_show_deadlock(smx_simcall_t req)
1533 {
1534   /*char *req_str = NULL;*/
1535   XBT_INFO("**************************");
1536   XBT_INFO("*** DEAD-LOCK DETECTED ***");
1537   XBT_INFO("**************************");
1538   XBT_INFO("Locked request:");
1539   /*req_str = MC_request_to_string(req);
1540     XBT_INFO("%s", req_str);
1541     xbt_free(req_str);*/
1542   XBT_INFO("Counter-example execution trace:");
1543   MC_dump_stack_safety(mc_stack_safety);
1544   MC_print_statistics(mc_stats);
1545 }
1546
1547
1548 void MC_show_stack_liveness(xbt_fifo_t stack){
1549   int value;
1550   mc_pair_t pair;
1551   xbt_fifo_item_t item;
1552   smx_simcall_t req;
1553   char *req_str = NULL;
1554   
1555   for (item = xbt_fifo_get_last_item(stack);
1556        (item ? (pair = (mc_pair_t) (xbt_fifo_get_item_content(item)))
1557         : (NULL)); item = xbt_fifo_get_prev_item(item)) {
1558     req = MC_state_get_executed_request(pair->graph_state, &value);
1559     if(req){
1560       if(pair->requests>0){
1561         req_str = MC_request_to_string(req, value);
1562         XBT_INFO("%s", req_str);
1563         xbt_free(req_str);
1564       }else{
1565         XBT_INFO("End of system requests but evolution in B├╝chi automaton");
1566       }
1567     }
1568   }
1569 }
1570
1571 void MC_dump_stack_liveness(xbt_fifo_t stack){
1572
1573   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1574
1575   mc_pair_t pair;
1576
1577   MC_SET_RAW_MEM;
1578   while ((pair = (mc_pair_t) xbt_fifo_pop(stack)) != NULL)
1579     MC_pair_delete(pair);
1580   MC_UNSET_RAW_MEM;
1581
1582   if(raw_mem_set)
1583     MC_SET_RAW_MEM;
1584
1585 }
1586
1587
1588 void MC_print_statistics(mc_stats_t stats)
1589 {
1590   if(stats->expanded_pairs == 0){
1591     XBT_INFO("Expanded states = %lu", stats->expanded_states);
1592     XBT_INFO("Visited states = %lu", stats->visited_states);
1593   }else{
1594     XBT_INFO("Expanded pairs = %lu", stats->expanded_pairs);
1595     XBT_INFO("Visited pairs = %lu", stats->visited_pairs);
1596   }
1597   XBT_INFO("Executed transitions = %lu", stats->executed_transitions);
1598   MC_SET_RAW_MEM;
1599   if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0')){
1600     fprintf(dot_output, "}\n");
1601     fclose(dot_output);
1602   }
1603   if(initial_state_safety != NULL && _sg_mc_comms_determinism){
1604     XBT_INFO("Communication-deterministic : %s", !initial_state_safety->comm_deterministic ? "No" : "Yes");
1605     XBT_INFO("Send-deterministic : %s", !initial_state_safety->send_deterministic ? "No" : "Yes");
1606   }
1607   MC_UNSET_RAW_MEM;
1608 }
1609
1610 void MC_assert(int prop)
1611 {
1612   if (MC_is_active() && !prop){
1613     XBT_INFO("**************************");
1614     XBT_INFO("*** PROPERTY NOT VALID ***");
1615     XBT_INFO("**************************");
1616     XBT_INFO("Counter-example execution trace:");
1617     MC_dump_stack_safety(mc_stack_safety);
1618     MC_print_statistics(mc_stats);
1619     xbt_abort();
1620   }
1621 }
1622
1623 void MC_cut(void){
1624   user_max_depth_reached = 1;
1625 }
1626
1627 void MC_process_clock_add(smx_process_t process, double amount)
1628 {
1629   mc_time[process->pid] += amount;
1630 }
1631
1632 double MC_process_clock_get(smx_process_t process)
1633 {
1634   if(mc_time){
1635     if(process != NULL)
1636       return mc_time[process->pid];
1637     else 
1638       return -1;
1639   }else{
1640     return 0;
1641   }
1642 }
1643
1644 void MC_automaton_load(const char *file){
1645
1646   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1647
1648   MC_SET_RAW_MEM;
1649
1650   if (_mc_property_automaton == NULL)
1651     _mc_property_automaton = xbt_automaton_new();
1652   
1653   xbt_automaton_load(_mc_property_automaton,file);
1654
1655   MC_UNSET_RAW_MEM;
1656
1657   if(raw_mem_set)
1658     MC_SET_RAW_MEM;
1659
1660 }
1661
1662 void MC_automaton_new_propositional_symbol(const char* id, void* fct) {
1663
1664   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1665
1666   MC_SET_RAW_MEM;
1667
1668   if (_mc_property_automaton == NULL)
1669     _mc_property_automaton = xbt_automaton_new();
1670
1671   xbt_automaton_propositional_symbol_new(_mc_property_automaton,id,fct);
1672
1673   MC_UNSET_RAW_MEM;
1674
1675   if(raw_mem_set)
1676     MC_SET_RAW_MEM;
1677   
1678 }
1679
1680
1681