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