src/mc/mc_global.c

   1 /* Copyright (c) 2008-2014. 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 <sys/mman.h>
  12 #include <libgen.h>
  13
  14 #include "simgrid/sg_config.h"
  15 #include "../surf/surf_private.h"
  16 #include "../simix/smx_private.h"
  17 #include "../xbt/mmalloc/mmprivate.h"
  18 #include "xbt/fifo.h"
  19 #include "mc_private.h"
  20 #include "xbt/automaton.h"
  21 #include "xbt/dict.h"
  22
  23 XBT_LOG_NEW_CATEGORY(mc, "All MC categories");
  24 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc,
  25                                 "Logging specific to MC (global)");
  26
  27 /* Configuration support */
  28 e_mc_reduce_t mc_reduce_kind = e_mc_reduce_unset;
  29
  30 int _sg_do_model_check = 0;
  31 int _sg_mc_checkpoint = 0;
  32 char *_sg_mc_property_file = NULL;
  33 int _sg_mc_timeout = 0;
  34 int _sg_mc_hash = 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 int _sg_mc_send_determinism = 0;
  40 int _sg_mc_safety = 0;
  41 int _sg_mc_liveness = 0;
  42
  43 int user_max_depth_reached = 0;
  44
  45 void _mc_cfg_cb_reduce(const char *name, int pos)
  46 {
  47   if (_sg_cfg_init_status && !_sg_do_model_check) {
  48     xbt_die
  49         ("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.");
  50   }
  51   char *val = xbt_cfg_get_string(_sg_cfg_set, name);
  52   if (!strcasecmp(val, "none")) {
  53     mc_reduce_kind = e_mc_reduce_none;
  54   } else if (!strcasecmp(val, "dpor")) {
  55     mc_reduce_kind = e_mc_reduce_dpor;
  56   } else {
  57     xbt_die("configuration option %s can only take 'none' or 'dpor' as a value",
  58             name);
  59   }
  60 }
  61
  62 void _mc_cfg_cb_checkpoint(const char *name, int pos)
  63 {
  64   if (_sg_cfg_init_status && !_sg_do_model_check) {
  65     xbt_die
  66         ("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.");
  67   }
  68   _sg_mc_checkpoint = xbt_cfg_get_int(_sg_cfg_set, name);
  69 }
  70
  71 void _mc_cfg_cb_property(const char *name, int pos)
  72 {
  73   if (_sg_cfg_init_status && !_sg_do_model_check) {
  74     xbt_die
  75         ("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.");
  76   }
  77   _sg_mc_property_file = xbt_cfg_get_string(_sg_cfg_set, name);
  78 }
  79
  80 void _mc_cfg_cb_timeout(const char *name, int pos)
  81 {
  82   if (_sg_cfg_init_status && !_sg_do_model_check) {
  83     xbt_die
  84         ("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.");
  85   }
  86   _sg_mc_timeout = xbt_cfg_get_boolean(_sg_cfg_set, name);
  87 }
  88
  89 void _mc_cfg_cb_hash(const char *name, int pos)
  90 {
  91   if (_sg_cfg_init_status && !_sg_do_model_check) {
  92     xbt_die
  93         ("You are specifying a value to enable/disable the use of global hash to speedup state comparaison, but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
  94   }
  95   _sg_mc_hash = xbt_cfg_get_boolean(_sg_cfg_set, name);
  96 }
  97
  98 void _mc_cfg_cb_max_depth(const char *name, int pos)
  99 {
 100   if (_sg_cfg_init_status && !_sg_do_model_check) {
 101     xbt_die
 102         ("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.");
 103   }
 104   _sg_mc_max_depth = xbt_cfg_get_int(_sg_cfg_set, name);
 105 }
 106
 107 void _mc_cfg_cb_visited(const char *name, int pos)
 108 {
 109   if (_sg_cfg_init_status && !_sg_do_model_check) {
 110     xbt_die
 111         ("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.");
 112   }
 113   _sg_mc_visited = xbt_cfg_get_int(_sg_cfg_set, name);
 114 }
 115
 116 void _mc_cfg_cb_dot_output(const char *name, int pos)
 117 {
 118   if (_sg_cfg_init_status && !_sg_do_model_check) {
 119     xbt_die
 120         ("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.");
 121   }
 122   _sg_mc_dot_output_file = xbt_cfg_get_string(_sg_cfg_set, name);
 123 }
 124
 125 void _mc_cfg_cb_comms_determinism(const char *name, int pos)
 126 {
 127   if (_sg_cfg_init_status && !_sg_do_model_check) {
 128     xbt_die
 129         ("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.");
 130   }
 131   _sg_mc_comms_determinism = xbt_cfg_get_boolean(_sg_cfg_set, name);
 132   mc_reduce_kind = e_mc_reduce_none;
 133 }
 134
 135 void _mc_cfg_cb_send_determinism(const char *name, int pos)
 136 {
 137   if (_sg_cfg_init_status && !_sg_do_model_check) {
 138     xbt_die
 139         ("You are specifying a value to enable/disable the detection of send-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.");
 140   }
 141   _sg_mc_send_determinism = xbt_cfg_get_boolean(_sg_cfg_set, name);
 142   mc_reduce_kind = e_mc_reduce_none;
 143 }
 144
 145 /* MC global data structures */
 146 mc_state_t mc_current_state = NULL;
 147 char mc_replay_mode = FALSE;
 148 double *mc_time = NULL;
 149 __thread mc_comparison_times_t mc_comp_times = NULL;
 150 __thread double mc_snapshot_comparison_time;
 151 mc_stats_t mc_stats = NULL;
 152 mc_global_t initial_global_state = NULL;
 153 xbt_fifo_t mc_stack = NULL;
 154
 155 /* Liveness */
 156 xbt_automaton_t _mc_property_automaton = NULL;
 157
 158 /* Variables */
 159 mc_object_info_t mc_libsimgrid_info = NULL;
 160 mc_object_info_t mc_binary_info = NULL;
 161
 162 mc_object_info_t mc_object_infos[2] = { NULL, NULL };
 163
 164 size_t mc_object_infos_size = 2;
 165
 166 /* Dot output */
 167 FILE *dot_output = NULL;
 168 const char *colors[13];
 169
 170
 171 /*******************************  Initialisation of MC *******************************/
 172 /*********************************************************************************/
 173
 174 static void MC_init_dot_output()
 175 {                               /* FIXME : more colors */
 176
 177   colors[0] = "blue";
 178   colors[1] = "red";
 179   colors[2] = "green3";
 180   colors[3] = "goldenrod";
 181   colors[4] = "brown";
 182   colors[5] = "purple";
 183   colors[6] = "magenta";
 184   colors[7] = "turquoise4";
 185   colors[8] = "gray25";
 186   colors[9] = "forestgreen";
 187   colors[10] = "hotpink";
 188   colors[11] = "lightblue";
 189   colors[12] = "tan";
 190
 191   dot_output = fopen(_sg_mc_dot_output_file, "w");
 192
 193   if (dot_output == NULL) {
 194     perror("Error open dot output file");
 195     xbt_abort();
 196   }
 197
 198   fprintf(dot_output,
 199           "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");
 200
 201 }
 202
 203 static void MC_init_debug_info(void)
 204 {
 205   XBT_INFO("Get debug information ...");
 206
 207   memory_map_t maps = MC_get_memory_map();
 208
 209   /* Get local variables for state equality detection */
 210   mc_binary_info = MC_find_object_info(maps, xbt_binary_name, 1);
 211   mc_object_infos[0] = mc_binary_info;
 212
 213   mc_libsimgrid_info = MC_find_object_info(maps, libsimgrid_path, 0);
 214   mc_object_infos[1] = mc_libsimgrid_info;
 215
 216   // Use information of the other objects:
 217   MC_post_process_object_info(mc_binary_info);
 218   MC_post_process_object_info(mc_libsimgrid_info);
 219
 220   MC_free_memory_map(maps);
 221   XBT_INFO("Get debug information done !");
 222 }
 223
 224
 225 void MC_init()
 226 {
 227
 228   int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
 229
 230   mc_time = xbt_new0(double, simix_process_maxpid);
 231
 232   /* Initialize the data structures that must be persistent across every
 233      iteration of the model-checker (in RAW memory) */
 234
 235   MC_SET_MC_HEAP;
 236
 237   mc_comp_times = xbt_new0(s_mc_comparison_times_t, 1);
 238
 239   /* Initialize statistics */
 240   mc_stats = xbt_new0(s_mc_stats_t, 1);
 241   mc_stats->state_size = 1;
 242
 243   MC_init_memory_map_info();
 244   MC_init_debug_info();         /* FIXME : get debug information only if liveness verification or visited state reduction */
 245
 246   if ((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0] != '\0'))
 247     MC_init_dot_output();
 248
 249   /* Init parmap */
 250   //parmap = xbt_parmap_mc_new(xbt_os_get_numcores(), XBT_PARMAP_DEFAULT);
 251
 252   MC_SET_STD_HEAP;
 253
 254   if (_sg_mc_visited > 0 || _sg_mc_liveness) {
 255     /* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */
 256     MC_ignore_local_variable("e", "*");
 257     MC_ignore_local_variable("__ex_cleanup", "*");
 258     MC_ignore_local_variable("__ex_mctx_en", "*");
 259     MC_ignore_local_variable("__ex_mctx_me", "*");
 260     MC_ignore_local_variable("__xbt_ex_ctx_ptr", "*");
 261     MC_ignore_local_variable("_log_ev", "*");
 262     MC_ignore_local_variable("_throw_ctx", "*");
 263     MC_ignore_local_variable("ctx", "*");
 264
 265     MC_ignore_local_variable("self", "simcall_BODY_mc_snapshot");
 266     MC_ignore_local_variable("next_context", "smx_ctx_sysv_suspend_serial");
 267     MC_ignore_local_variable("i", "smx_ctx_sysv_suspend_serial");
 268
 269     /* Ignore local variable about time used for tracing */
 270     MC_ignore_local_variable("start_time", "*");
 271
 272     MC_ignore_global_variable("compared_pointers");
 273     MC_ignore_global_variable("mc_comp_times");
 274     MC_ignore_global_variable("mc_snapshot_comparison_time");
 275     MC_ignore_global_variable("mc_time");
 276     MC_ignore_global_variable("smpi_current_rank");
 277     MC_ignore_global_variable("counter");       /* Static variable used for tracing */
 278     MC_ignore_global_variable("maestro_stack_start");
 279     MC_ignore_global_variable("maestro_stack_end");
 280     MC_ignore_global_variable("smx_total_comms");
 281     MC_ignore_global_variable("communications_pattern");
 282     MC_ignore_global_variable("initial_communications_pattern");
 283     MC_ignore_global_variable("incomplete_communications_pattern");
 284
 285     MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
 286
 287     smx_process_t process;
 288     xbt_swag_foreach(process, simix_global->process_list) {
 289       MC_ignore_heap(&(process->process_hookup),
 290                      sizeof(process->process_hookup));
 291                      }
 292   }
 293
 294   if (raw_mem_set)
 295     MC_SET_MC_HEAP;
 296
 297 }
 298
 299 /*******************************  Core of MC *******************************/
 300 /**************************************************************************/
 301
 302 static void MC_modelcheck_comm_determinism_init(void)
 303 {
 304
 305   int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
 306
 307   MC_init();
 308
 309   if (!mc_mem_set)
 310     MC_SET_MC_HEAP;
 311
 312   /* Create exploration stack */
 313   mc_stack = xbt_fifo_new();
 314
 315   MC_SET_STD_HEAP;
 316
 317   MC_pre_modelcheck_comm_determinism();
 318
 319   MC_SET_MC_HEAP;
 320   initial_global_state = xbt_new0(s_mc_global_t, 1);
 321   initial_global_state->snapshot = MC_take_snapshot(0);
 322   initial_global_state->initial_communications_pattern_done = 0;
 323   initial_global_state->comm_deterministic = 1;
 324   initial_global_state->send_deterministic = 1;
 325   MC_SET_STD_HEAP;
 326
 327   MC_modelcheck_comm_determinism();
 328
 329   if(mc_mem_set)
 330     MC_SET_MC_HEAP;
 331
 332 }
 333
 334 static void MC_modelcheck_safety_init(void)
 335 {
 336   int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
 337
 338   _sg_mc_safety = 1;
 339
 340   MC_init();
 341
 342   if (!mc_mem_set)
 343     MC_SET_MC_HEAP;
 344
 345   /* Create exploration stack */
 346   mc_stack = xbt_fifo_new();
 347
 348   MC_SET_STD_HEAP;
 349
 350   MC_pre_modelcheck_safety();
 351
 352   MC_SET_MC_HEAP;
 353   /* Save the initial state */
 354   initial_global_state = xbt_new0(s_mc_global_t, 1);
 355   initial_global_state->snapshot = MC_take_snapshot(0);
 356   MC_SET_STD_HEAP;
 357
 358   MC_modelcheck_safety();
 359
 360   if (mc_mem_set)
 361     MC_SET_MC_HEAP;
 362
 363   xbt_abort();
 364   //MC_exit();
 365 }
 366
 367 static void MC_modelcheck_liveness_init()
 368 {
 369
 370   int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
 371
 372   _sg_mc_liveness = 1;
 373
 374   MC_init();
 375
 376   if (!mc_mem_set)
 377     MC_SET_MC_HEAP;
 378
 379   /* Create exploration stack */
 380   mc_stack = xbt_fifo_new();
 381
 382   /* Create the initial state */
 383   initial_global_state = xbt_new0(s_mc_global_t, 1);
 384
 385   MC_SET_STD_HEAP;
 386
 387   MC_pre_modelcheck_liveness();
 388
 389   /* We're done */
 390   MC_print_statistics(mc_stats);
 391   xbt_free(mc_time);
 392
 393   if (mc_mem_set)
 394     MC_SET_MC_HEAP;
 395
 396 }
 397
 398 void MC_do_the_modelcheck_for_real()
 399 {
 400
 401   if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
 402     XBT_INFO("Check communication determinism");
 403     MC_modelcheck_comm_determinism_init();
 404   } else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0') {
 405     if (mc_reduce_kind == e_mc_reduce_unset)
 406       mc_reduce_kind = e_mc_reduce_dpor;
 407     XBT_INFO("Check a safety property");
 408     MC_modelcheck_safety_init();
 409   } else {
 410     if (mc_reduce_kind == e_mc_reduce_unset)
 411       mc_reduce_kind = e_mc_reduce_none;
 412     XBT_INFO("Check the liveness property %s", _sg_mc_property_file);
 413     MC_automaton_load(_sg_mc_property_file);
 414     MC_modelcheck_liveness_init();
 415   }
 416 }
 417
 418
 419 void MC_exit(void)
 420 {
 421   xbt_free(mc_time);
 422
 423   MC_memory_exit();
 424   //xbt_abort();
 425 }
 426
 427 int SIMIX_pre_mc_random(smx_simcall_t simcall, int min, int max)
 428 {
 429
 430   return simcall->mc_value;
 431 }
 432
 433
 434 int MC_random(int min, int max)
 435 {
 436   /*FIXME: return mc_current_state->executed_transition->random.value; */
 437   return simcall_mc_random(min, max);
 438 }
 439
 440 /**
 441  * \brief Schedules all the process that are ready to run
 442  */
 443 void MC_wait_for_requests(void)
 444 {
 445   smx_process_t process;
 446   smx_simcall_t req;
 447   unsigned int iter;
 448
 449   while (!xbt_dynar_is_empty(simix_global->process_to_run)) {
 450     SIMIX_process_runall();
 451     xbt_dynar_foreach(simix_global->process_that_ran, iter, process) {
 452       req = &process->simcall;
 453       if (req->call != SIMCALL_NONE && !MC_request_is_visible(req))
 454         SIMIX_simcall_pre(req, 0);
 455     }
 456   }
 457 }
 458
 459 int MC_deadlock_check()
 460 {
 461   int deadlock = FALSE;
 462   smx_process_t process;
 463   if (xbt_swag_size(simix_global->process_list)) {
 464     deadlock = TRUE;
 465     xbt_swag_foreach(process, simix_global->process_list) {
 466       if (process->simcall.call != SIMCALL_NONE
 467           && MC_request_is_enabled(&process->simcall)) {
 468         deadlock = FALSE;
 469         break;
 470       }
 471     }
 472   }
 473   return deadlock;
 474 }
 475
 476 /**
 477  * \brief Re-executes from the state at position start all the transitions indicated by
 478  *        a given model-checker stack.
 479  * \param stack The stack with the transitions to execute.
 480  * \param start Start index to begin the re-execution.
 481  */
 482 void MC_replay(xbt_fifo_t stack, int start)
 483 {
 484   int raw_mem = (mmalloc_get_current_heap() == mc_heap);
 485
 486   int value, i = 1, count = 1, call = 0, j;
 487   char *req_str;
 488   smx_simcall_t req = NULL, saved_req = NULL;
 489   xbt_fifo_item_t item, start_item;
 490   mc_state_t state;
 491   smx_process_t process = NULL;
 492   smx_action_t current_comm;
 493
 494   XBT_DEBUG("**** Begin Replay ****");
 495
 496   if (start == -1) {
 497     /* Restore the initial state */
 498     MC_restore_snapshot(initial_global_state->snapshot);
 499     /* At the moment of taking the snapshot the raw heap was set, so restoring
 500      * it will set it back again, we have to unset it to continue  */
 501     MC_SET_STD_HEAP;
 502   }
 503
 504   start_item = xbt_fifo_get_last_item(stack);
 505   if (start != -1) {
 506     while (i != start) {
 507       start_item = xbt_fifo_get_prev_item(start_item);
 508       i++;
 509     }
 510   }
 511
 512   MC_SET_MC_HEAP;
 513
 514   if (mc_reduce_kind == e_mc_reduce_dpor) {
 515     xbt_dict_reset(first_enabled_state);
 516     xbt_swag_foreach(process, simix_global->process_list) {
 517       if (MC_process_is_enabled(process)) {
 518         char *key = bprintf("%lu", process->pid);
 519         char *data = bprintf("%d", count);
 520         xbt_dict_set(first_enabled_state, key, data, NULL);
 521         xbt_free(key);
 522       }
 523     }
 524   }
 525
 526   if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
 527     for (j=0; j<simix_process_maxpid; j++) {
 528       xbt_dynar_reset((xbt_dynar_t)xbt_dynar_get_as(communications_pattern, j, xbt_dynar_t));
 529     }
 530     for (j=0; j<simix_process_maxpid; j++) {
 531       xbt_dynar_reset((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, j, xbt_dynar_t));
 532     }
 533   }
 534
 535   MC_SET_STD_HEAP;
 536
 537
 538   /* Traverse the stack from the state at position start and re-execute the transitions */
 539   for (item = start_item;
 540        item != xbt_fifo_get_first_item(stack);
 541        item = xbt_fifo_get_prev_item(item)) {
 542
 543     state = (mc_state_t) xbt_fifo_get_item_content(item);
 544     saved_req = MC_state_get_executed_request(state, &value);
 545
 546     if (mc_reduce_kind == e_mc_reduce_dpor) {
 547       MC_SET_MC_HEAP;
 548       char *key = bprintf("%lu", saved_req->issuer->pid);
 549       xbt_dict_remove(first_enabled_state, key);
 550       xbt_free(key);
 551       MC_SET_STD_HEAP;
 552     }
 553
 554     if (saved_req) {
 555       /* because we got a copy of the executed request, we have to fetch the
 556          real one, pointed by the request field of the issuer process */
 557       req = &saved_req->issuer->simcall;
 558
 559       /* Debug information */
 560       if (XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)) {
 561         req_str = MC_request_to_string(req, value);
 562         XBT_DEBUG("Replay: %s (%p)", req_str, state);
 563         xbt_free(req_str);
 564       }
 565
 566       /* TODO : handle test and testany simcalls */
 567       if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
 568         if (req->call == SIMCALL_COMM_ISEND)
 569           call = 1;
 570         else if (req->call == SIMCALL_COMM_IRECV)
 571           call = 2;
 572         else if (req->call == SIMCALL_COMM_WAIT)
 573           call = 3;
 574         else if (req->call == SIMCALL_COMM_WAITANY)
 575           call = 4;
 576       }
 577
 578       SIMIX_simcall_pre(req, value);
 579
 580       if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
 581         MC_SET_MC_HEAP;
 582         if (call == 1) { /* Send */
 583           get_comm_pattern(communications_pattern, req, call);
 584         } else if (call == 2) { /* Recv */
 585           get_comm_pattern(communications_pattern, req, call);
 586         } else if (call == 3) { /* Wait */
 587           current_comm = simcall_comm_wait__get__comm(req);
 588           if (current_comm->comm.refcount == 1)  /* First wait only must be considered */
 589             complete_comm_pattern(communications_pattern, current_comm);
 590         } else if (call == 4) { /* WaitAny */
 591           current_comm = xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value, smx_action_t);
 592           if (current_comm->comm.refcount == 1) /* First wait only must be considered */
 593             complete_comm_pattern(communications_pattern, current_comm);
 594         }
 595         MC_SET_STD_HEAP;
 596         call = 0;
 597       }
 598
 599
 600       MC_wait_for_requests();
 601
 602       count++;
 603
 604       if (mc_reduce_kind == e_mc_reduce_dpor) {
 605         MC_SET_MC_HEAP;
 606         /* Insert in dict all enabled processes */
 607         xbt_swag_foreach(process, simix_global->process_list) {
 608           if (MC_process_is_enabled(process) ) {
 609             char *key = bprintf("%lu", process->pid);
 610             if (xbt_dict_get_or_null(first_enabled_state, key) == NULL) {
 611               char *data = bprintf("%d", count);
 612               xbt_dict_set(first_enabled_state, key, data, NULL);
 613             }
 614             xbt_free(key);
 615           }
 616         }
 617         MC_SET_STD_HEAP;
 618       }
 619     }
 620
 621     /* Update statistics */
 622     mc_stats->visited_states++;
 623     mc_stats->executed_transitions++;
 624
 625   }
 626
 627   XBT_DEBUG("**** End Replay ****");
 628
 629   if (raw_mem)
 630     MC_SET_MC_HEAP;
 631   else
 632     MC_SET_STD_HEAP;
 633
 634
 635 }
 636
 637 void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
 638 {
 639
 640   initial_global_state->raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
 641
 642   int value;
 643   char *req_str;
 644   smx_simcall_t req = NULL, saved_req = NULL;
 645   xbt_fifo_item_t item;
 646   mc_state_t state;
 647   mc_pair_t pair;
 648   int depth = 1;
 649
 650   XBT_DEBUG("**** Begin Replay ****");
 651
 652   /* Restore the initial state */
 653   MC_restore_snapshot(initial_global_state->snapshot);
 654
 655   /* At the moment of taking the snapshot the raw heap was set, so restoring
 656    * it will set it back again, we have to unset it to continue  */
 657   if (!initial_global_state->raw_mem_set)
 658     MC_SET_STD_HEAP;
 659
 660   if (all_stack) {
 661
 662     item = xbt_fifo_get_last_item(stack);
 663
 664     while (depth <= xbt_fifo_size(stack)) {
 665
 666       pair = (mc_pair_t) xbt_fifo_get_item_content(item);
 667       state = (mc_state_t) pair->graph_state;
 668
 669       if (pair->requests > 0) {
 670
 671         saved_req = MC_state_get_executed_request(state, &value);
 672         //XBT_DEBUG("SavedReq->call %u", saved_req->call);
 673
 674         if (saved_req != NULL) {
 675           /* because we got a copy of the executed request, we have to fetch the
 676              real one, pointed by the request field of the issuer process */
 677           req = &saved_req->issuer->simcall;
 678           //XBT_DEBUG("Req->call %u", req->call);
 679
 680           /* Debug information */
 681           if (XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)) {
 682             req_str = MC_request_to_string(req, value);
 683             XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
 684             xbt_free(req_str);
 685           }
 686
 687         }
 688
 689         SIMIX_simcall_pre(req, value);
 690         MC_wait_for_requests();
 691       }
 692
 693       depth++;
 694
 695       /* Update statistics */
 696       mc_stats->visited_pairs++;
 697       mc_stats->executed_transitions++;
 698
 699       item = xbt_fifo_get_prev_item(item);
 700     }
 701
 702   } else {
 703
 704     /* Traverse the stack from the initial state and re-execute the transitions */
 705     for (item = xbt_fifo_get_last_item(stack);
 706          item != xbt_fifo_get_first_item(stack);
 707          item = xbt_fifo_get_prev_item(item)) {
 708
 709       pair = (mc_pair_t) xbt_fifo_get_item_content(item);
 710       state = (mc_state_t) pair->graph_state;
 711
 712       if (pair->requests > 0) {
 713
 714         saved_req = MC_state_get_executed_request(state, &value);
 715         //XBT_DEBUG("SavedReq->call %u", saved_req->call);
 716
 717         if (saved_req != NULL) {
 718           /* because we got a copy of the executed request, we have to fetch the
 719              real one, pointed by the request field of the issuer process */
 720           req = &saved_req->issuer->simcall;
 721           //XBT_DEBUG("Req->call %u", req->call);
 722
 723           /* Debug information */
 724           if (XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)) {
 725             req_str = MC_request_to_string(req, value);
 726             XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
 727             xbt_free(req_str);
 728           }
 729
 730         }
 731
 732         SIMIX_simcall_pre(req, value);
 733         MC_wait_for_requests();
 734       }
 735
 736       depth++;
 737
 738       /* Update statistics */
 739       mc_stats->visited_pairs++;
 740       mc_stats->executed_transitions++;
 741     }
 742   }
 743
 744   XBT_DEBUG("**** End Replay ****");
 745
 746   if (initial_global_state->raw_mem_set)
 747     MC_SET_MC_HEAP;
 748   else
 749     MC_SET_STD_HEAP;
 750
 751 }
 752
 753 /**
 754  * \brief Dumps the contents of a model-checker's stack and shows the actual
 755  *        execution trace
 756  * \param stack The stack to dump
 757  */
 758 void MC_dump_stack_safety(xbt_fifo_t stack)
 759 {
 760
 761   int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
 762
 763   MC_show_stack_safety(stack);
 764
 765   if (!_sg_mc_checkpoint) {
 766
 767     mc_state_t state;
 768
 769     MC_SET_MC_HEAP;
 770     while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
 771       MC_state_delete(state);
 772     MC_SET_STD_HEAP;
 773
 774   }
 775
 776   if (raw_mem_set)
 777     MC_SET_MC_HEAP;
 778   else
 779     MC_SET_STD_HEAP;
 780
 781 }
 782
 783
 784 void MC_show_stack_safety(xbt_fifo_t stack)
 785 {
 786
 787   int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
 788
 789   MC_SET_MC_HEAP;
 790
 791   int value;
 792   mc_state_t state;
 793   xbt_fifo_item_t item;
 794   smx_simcall_t req;
 795   char *req_str = NULL;
 796
 797   for (item = xbt_fifo_get_last_item(stack);
 798        (item ? (state = (mc_state_t) (xbt_fifo_get_item_content(item)))
 799         : (NULL)); item = xbt_fifo_get_prev_item(item)) {
 800     req = MC_state_get_executed_request(state, &value);
 801     if (req) {
 802       req_str = MC_request_to_string(req, value);
 803       XBT_INFO("%s", req_str);
 804       xbt_free(req_str);
 805     }
 806   }
 807
 808   if (!raw_mem_set)
 809     MC_SET_STD_HEAP;
 810 }
 811
 812 void MC_show_deadlock(smx_simcall_t req)
 813 {
 814   /*char *req_str = NULL; */
 815   XBT_INFO("**************************");
 816   XBT_INFO("*** DEAD-LOCK DETECTED ***");
 817   XBT_INFO("**************************");
 818   XBT_INFO("Locked request:");
 819   /*req_str = MC_request_to_string(req);
 820      XBT_INFO("%s", req_str);
 821      xbt_free(req_str); */
 822   XBT_INFO("Counter-example execution trace:");
 823   MC_dump_stack_safety(mc_stack);
 824   MC_print_statistics(mc_stats);
 825 }
 826
 827
 828 void MC_show_stack_liveness(xbt_fifo_t stack)
 829 {
 830   int value;
 831   mc_pair_t pair;
 832   xbt_fifo_item_t item;
 833   smx_simcall_t req;
 834   char *req_str = NULL;
 835
 836   for (item = xbt_fifo_get_last_item(stack);
 837        (item ? (pair = (mc_pair_t) (xbt_fifo_get_item_content(item)))
 838         : (NULL)); item = xbt_fifo_get_prev_item(item)) {
 839     req = MC_state_get_executed_request(pair->graph_state, &value);
 840     if (req) {
 841       if (pair->requests > 0) {
 842         req_str = MC_request_to_string(req, value);
 843         XBT_INFO("%s", req_str);
 844         xbt_free(req_str);
 845       } else {
 846         XBT_INFO("End of system requests but evolution in Büchi automaton");
 847       }
 848     }
 849   }
 850 }
 851
 852 void MC_dump_stack_liveness(xbt_fifo_t stack)
 853 {
 854
 855   int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
 856
 857   mc_pair_t pair;
 858
 859   MC_SET_MC_HEAP;
 860   while ((pair = (mc_pair_t) xbt_fifo_pop(stack)) != NULL)
 861     MC_pair_delete(pair);
 862   MC_SET_STD_HEAP;
 863
 864   if (raw_mem_set)
 865     MC_SET_MC_HEAP;
 866
 867 }
 868
 869
 870 void MC_print_statistics(mc_stats_t stats)
 871 {
 872   if (stats->expanded_pairs == 0) {
 873     XBT_INFO("Expanded states = %lu", stats->expanded_states);
 874     XBT_INFO("Visited states = %lu", stats->visited_states);
 875   } else {
 876     XBT_INFO("Expanded pairs = %lu", stats->expanded_pairs);
 877     XBT_INFO("Visited pairs = %lu", stats->visited_pairs);
 878   }
 879   XBT_INFO("Executed transitions = %lu", stats->executed_transitions);
 880   MC_SET_MC_HEAP;
 881   if ((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0] != '\0')) {
 882     fprintf(dot_output, "}\n");
 883     fclose(dot_output);
 884   }
 885   if (initial_global_state != NULL) {
 886     if (_sg_mc_comms_determinism)
 887       XBT_INFO("Communication-deterministic : %s",
 888                !initial_global_state->comm_deterministic ? "No" : "Yes");
 889     if (_sg_mc_send_determinism)
 890       XBT_INFO("Send-deterministic : %s",
 891                !initial_global_state->send_deterministic ? "No" : "Yes");
 892   }
 893   MC_SET_STD_HEAP;
 894 }
 895
 896 void MC_assert(int prop)
 897 {
 898   if (MC_is_active() && !prop) {
 899     XBT_INFO("**************************");
 900     XBT_INFO("*** PROPERTY NOT VALID ***");
 901     XBT_INFO("**************************");
 902     XBT_INFO("Counter-example execution trace:");
 903     MC_dump_stack_safety(mc_stack);
 904     MC_print_statistics(mc_stats);
 905     xbt_abort();
 906   }
 907 }
 908
 909 void MC_cut(void)
 910 {
 911   user_max_depth_reached = 1;
 912 }
 913
 914 void MC_process_clock_add(smx_process_t process, double amount)
 915 {
 916   mc_time[process->pid] += amount;
 917 }
 918
 919 double MC_process_clock_get(smx_process_t process)
 920 {
 921   if (mc_time) {
 922     if (process != NULL)
 923       return mc_time[process->pid];
 924     else
 925       return -1;
 926   } else {
 927     return 0;
 928   }
 929 }
 930
 931 void MC_automaton_load(const char *file)
 932 {
 933
 934   int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
 935
 936   MC_SET_MC_HEAP;
 937
 938   if (_mc_property_automaton == NULL)
 939     _mc_property_automaton = xbt_automaton_new();
 940
 941   xbt_automaton_load(_mc_property_automaton, file);
 942
 943   MC_SET_STD_HEAP;
 944
 945   if (raw_mem_set)
 946     MC_SET_MC_HEAP;
 947
 948 }
 949
 950 void MC_automaton_new_propositional_symbol(const char *id, void *fct)
 951 {
 952
 953   int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
 954
 955   MC_SET_MC_HEAP;
 956
 957   if (_mc_property_automaton == NULL)
 958     _mc_property_automaton = xbt_automaton_new();
 959
 960   xbt_automaton_propositional_symbol_new(_mc_property_automaton, id, fct);
 961
 962   MC_SET_STD_HEAP;
 963
 964   if (raw_mem_set)
 965     MC_SET_MC_HEAP;
 966
 967 }