src/mc/mc_global.cpp

   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 <assert.h>
   8 #include <string.h>
   9 #include <stdint.h>
  10
  11 #include "mc_base.h"
  12
  13 #ifndef _XBT_WIN32
  14 #include <unistd.h>
  15 #include <sys/wait.h>
  16 #include <sys/time.h>
  17 #endif
  18
  19 #include "simgrid/sg_config.h"
  20 #include "../surf/surf_private.h"
  21 #include "../simix/smx_private.h"
  22 #include "xbt/fifo.h"
  23 #include "xbt/automaton.h"
  24 #include "xbt/dict.h"
  25 #include "mc_record.h"
  26
  27 #ifdef HAVE_MC
  28 #include "mc_server.h"
  29 #include <libunwind.h>
  30 #include <xbt/mmalloc.h>
  31 #include "../xbt/mmalloc/mmprivate.h"
  32 #include "mc_object_info.h"
  33 #include "mc_comm_pattern.h"
  34 #include "mc_request.h"
  35 #include "mc_safety.h"
  36 #include "mc_memory_map.h"
  37 #include "mc_snapshot.h"
  38 #include "mc_liveness.h"
  39 #include "mc_private.h"
  40 #include "mc_unw.h"
  41 #include "mc_smx.h"
  42 #endif
  43 #include "mc_record.h"
  44 #include "mc_protocol.h"
  45 #include "mc_client.h"
  46
  47 extern "C" {
  48
  49 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc,
  50                                 "Logging specific to MC (global)");
  51
  52 e_mc_mode_t mc_mode;
  53
  54 double *mc_time = NULL;
  55
  56 #ifdef HAVE_MC
  57 int user_max_depth_reached = 0;
  58
  59 /* MC global data structures */
  60 mc_state_t mc_current_state = NULL;
  61 char mc_replay_mode = FALSE;
  62
  63 __thread mc_comparison_times_t mc_comp_times = NULL;
  64 __thread double mc_snapshot_comparison_time;
  65 mc_stats_t mc_stats = NULL;
  66 mc_global_t initial_global_state = NULL;
  67 xbt_fifo_t mc_stack = NULL;
  68
  69 /* Liveness */
  70 xbt_automaton_t _mc_property_automaton = NULL;
  71
  72 /* Dot output */
  73 FILE *dot_output = NULL;
  74 const char *colors[13];
  75
  76
  77 /*******************************  Initialisation of MC *******************************/
  78 /*********************************************************************************/
  79
  80 static void MC_init_dot_output()
  81 {                               /* FIXME : more colors */
  82
  83   colors[0] = "blue";
  84   colors[1] = "red";
  85   colors[2] = "green3";
  86   colors[3] = "goldenrod";
  87   colors[4] = "brown";
  88   colors[5] = "purple";
  89   colors[6] = "magenta";
  90   colors[7] = "turquoise4";
  91   colors[8] = "gray25";
  92   colors[9] = "forestgreen";
  93   colors[10] = "hotpink";
  94   colors[11] = "lightblue";
  95   colors[12] = "tan";
  96
  97   dot_output = fopen(_sg_mc_dot_output_file, "w");
  98
  99   if (dot_output == NULL) {
 100     perror("Error open dot output file");
 101     xbt_abort();
 102   }
 103
 104   fprintf(dot_output,
 105           "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");
 106
 107 }
 108
 109 static void MC_init_mode(void)
 110 {
 111   if (mc_mode == MC_MODE_NONE) {
 112     if (getenv(MC_ENV_SOCKET_FD)) {
 113       mc_mode = MC_MODE_CLIENT;
 114     } else {
 115       mc_mode = MC_MODE_STANDALONE;
 116     }
 117   }
 118 }
 119
 120 #ifdef HAVE_MC
 121 void MC_init()
 122 {
 123   MC_init_pid(getpid(), -1);
 124 }
 125
 126 void MC_init_pid(pid_t pid, int socket)
 127 {
 128   /* Initialize the data structures that must be persistent across every
 129      iteration of the model-checker (in RAW memory) */
 130
 131   xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
 132   mc_model_checker = MC_model_checker_new(pid, socket);
 133
 134   // It's not useful anymore:
 135   if (0 && mc_mode == MC_MODE_SERVER) {
 136     unsigned long maxpid;
 137     MC_process_read_variable(&mc_model_checker->process, "simix_process_maxpid",
 138       &maxpid, sizeof(maxpid));
 139     simix_process_maxpid = maxpid;
 140   }
 141
 142   mmalloc_set_current_heap(std_heap);
 143   mc_time = xbt_new0(double, MC_smx_get_maxpid());
 144   mmalloc_set_current_heap(mc_heap);
 145
 146   mc_comp_times = xbt_new0(s_mc_comparison_times_t, 1);
 147
 148   /* Initialize statistics */
 149   mc_stats = xbt_new0(s_mc_stats_t, 1);
 150   mc_stats->state_size = 1;
 151
 152   if ((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0] != '\0'))
 153     MC_init_dot_output();
 154
 155   /* Init parmap */
 156   //parmap = xbt_parmap_mc_new(xbt_os_get_numcores(), XBT_PARMAP_DEFAULT);
 157
 158   MC_SET_STD_HEAP;
 159
 160   if (_sg_mc_visited > 0 || _sg_mc_liveness  || _sg_mc_termination || mc_mode == MC_MODE_SERVER) {
 161     /* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */
 162     MC_ignore_local_variable("e", "*");
 163     MC_ignore_local_variable("__ex_cleanup", "*");
 164     MC_ignore_local_variable("__ex_mctx_en", "*");
 165     MC_ignore_local_variable("__ex_mctx_me", "*");
 166     MC_ignore_local_variable("__xbt_ex_ctx_ptr", "*");
 167     MC_ignore_local_variable("_log_ev", "*");
 168     MC_ignore_local_variable("_throw_ctx", "*");
 169     MC_ignore_local_variable("ctx", "*");
 170
 171     MC_ignore_local_variable("self", "simcall_BODY_mc_snapshot");
 172     MC_ignore_local_variable("next_cont"
 173       "ext", "smx_ctx_sysv_suspend_serial");
 174     MC_ignore_local_variable("i", "smx_ctx_sysv_suspend_serial");
 175
 176     /* Ignore local variable about time used for tracing */
 177     MC_ignore_local_variable("start_time", "*");
 178
 179     /* Main MC state: */
 180     MC_ignore_global_variable("mc_model_checker");
 181     MC_ignore_global_variable("initial_communications_pattern");
 182     MC_ignore_global_variable("incomplete_communications_pattern");
 183     MC_ignore_global_variable("nb_comm_pattern");
 184
 185     /* MC __thread variables: */
 186     MC_ignore_global_variable("mc_diff_info");
 187     MC_ignore_global_variable("mc_comp_times");
 188     MC_ignore_global_variable("mc_snapshot_comparison_time");
 189
 190     /* This MC state is used in MC replay as well: */
 191     MC_ignore_global_variable("mc_time");
 192
 193     /* Static variable used for tracing */
 194     MC_ignore_global_variable("counter");
 195
 196     /* SIMIX */
 197     MC_ignore_global_variable("smx_total_comms");
 198
 199     if (mc_mode == MC_MODE_STANDALONE || mc_mode == MC_MODE_CLIENT) {
 200       /* Those requests are handled on the client side and propagated by message
 201        * to the server: */
 202
 203       MC_ignore_heap(mc_time, MC_smx_get_maxpid() * sizeof(double));
 204
 205       smx_process_t process;
 206       xbt_swag_foreach(process, simix_global->process_list) {
 207         MC_ignore_heap(&(process->process_hookup), sizeof(process->process_hookup));
 208       }
 209     }
 210
 211   }
 212
 213   mmalloc_set_current_heap(heap);
 214 }
 215 #endif
 216
 217 /*******************************  Core of MC *******************************/
 218 /**************************************************************************/
 219
 220 void MC_do_the_modelcheck_for_real()
 221 {
 222   MC_init_mode();
 223
 224   switch(mc_mode) {
 225   default:
 226     xbt_die("Unexpected mc mode");
 227     break;
 228   case MC_MODE_CLIENT:
 229     MC_init();
 230     MC_client_main_loop();
 231     return;
 232   case MC_MODE_SERVER:
 233     break;
 234   case MC_MODE_STANDALONE:
 235     MC_init();
 236     break;
 237   }
 238
 239   if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
 240     XBT_INFO("Check communication determinism");
 241     mc_reduce_kind = e_mc_reduce_none;
 242     MC_wait_for_requests();
 243     MC_modelcheck_comm_determinism();
 244   }
 245
 246   else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0') {
 247     if(_sg_mc_termination)
 248       mc_reduce_kind = e_mc_reduce_none;
 249     else if (mc_reduce_kind == e_mc_reduce_unset)
 250       mc_reduce_kind = e_mc_reduce_dpor;
 251     _sg_mc_safety = 1;
 252     if (_sg_mc_termination)
 253       XBT_INFO("Check non progressive cycles");
 254     else
 255       XBT_INFO("Check a safety property");
 256     MC_wait_for_requests();
 257     MC_modelcheck_safety();
 258   }
 259
 260   else {
 261     if (mc_reduce_kind == e_mc_reduce_unset)
 262       mc_reduce_kind = e_mc_reduce_none;
 263     XBT_INFO("Check the liveness property %s", _sg_mc_property_file);
 264     MC_automaton_load(_sg_mc_property_file);
 265     MC_wait_for_requests();
 266     MC_modelcheck_liveness();
 267   }
 268
 269 }
 270
 271
 272 void MC_exit(void)
 273 {
 274   xbt_free(mc_time);
 275
 276   MC_memory_exit();
 277   //xbt_abort();
 278 }
 279
 280 #ifdef HAVE_MC
 281 int MC_deadlock_check()
 282 {
 283   if (mc_mode == MC_MODE_SERVER) {
 284     int res;
 285     if ((res = MC_protocol_send_simple_message(mc_model_checker->process.socket,
 286       MC_MESSAGE_DEADLOCK_CHECK)))
 287       xbt_die("Could not check deadlock state");
 288     s_mc_int_message_t message;
 289     ssize_t s = MC_receive_message(mc_model_checker->process.socket, &message, sizeof(message), 0);
 290     if (s == -1)
 291       xbt_die("Could not receive message");
 292     else if (s != sizeof(message) || message.type != MC_MESSAGE_DEADLOCK_CHECK_REPLY) {
 293       xbt_die("%s received unexpected message %s (%i, size=%i) "
 294         "expected MC_MESSAGE_DEADLOCK_CHECK_REPLY (%i, size=%i)",
 295         MC_mode_name(mc_mode),
 296         MC_message_type_name(message.type), (int) message.type, (int) s,
 297         (int) MC_MESSAGE_DEADLOCK_CHECK_REPLY, (int) sizeof(message)
 298         );
 299     }
 300     else
 301       return message.value;
 302   }
 303
 304   int deadlock = FALSE;
 305   smx_process_t process;
 306   if (xbt_swag_size(simix_global->process_list)) {
 307     deadlock = TRUE;
 308     MC_EACH_SIMIX_PROCESS(process,
 309       if (MC_process_is_enabled(process)) {
 310         deadlock = FALSE;
 311         break;
 312       }
 313     );
 314   }
 315   return deadlock;
 316 }
 317 #endif
 318
 319 /**
 320  * \brief Re-executes from the state at position start all the transitions indicated by
 321  *        a given model-checker stack.
 322  * \param stack The stack with the transitions to execute.
 323  * \param start Start index to begin the re-execution.
 324  */
 325 void MC_replay(xbt_fifo_t stack)
 326 {
 327   xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
 328
 329   int value, count = 1;
 330   char *req_str;
 331   smx_simcall_t req = NULL, saved_req = NULL;
 332   xbt_fifo_item_t item, start_item;
 333   mc_state_t state;
 334
 335   XBT_DEBUG("**** Begin Replay ****");
 336
 337   /* Intermediate backtracking */
 338   if(_sg_mc_checkpoint > 0 || _sg_mc_termination || _sg_mc_visited > 0) {
 339     start_item = xbt_fifo_get_first_item(stack);
 340     state = (mc_state_t)xbt_fifo_get_item_content(start_item);
 341     if(state->system_state){
 342       MC_restore_snapshot(state->system_state);
 343       if(_sg_mc_comms_determinism || _sg_mc_send_determinism)
 344         MC_restore_communications_pattern(state);
 345       MC_SET_STD_HEAP;
 346       return;
 347     }
 348   }
 349
 350
 351   /* Restore the initial state */
 352   MC_restore_snapshot(initial_global_state->snapshot);
 353   /* At the moment of taking the snapshot the raw heap was set, so restoring
 354    * it will set it back again, we have to unset it to continue  */
 355   MC_SET_STD_HEAP;
 356
 357   start_item = xbt_fifo_get_last_item(stack);
 358
 359   MC_SET_MC_HEAP;
 360
 361   if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
 362     // int n = xbt_dynar_length(incomplete_communications_pattern);
 363     unsigned n = MC_smx_get_maxpid();
 364     assert(n == xbt_dynar_length(incomplete_communications_pattern));
 365     assert(n == xbt_dynar_length(initial_communications_pattern));
 366     for (unsigned j=0; j < n ; j++) {
 367       xbt_dynar_reset((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, j, xbt_dynar_t));
 368       xbt_dynar_get_as(initial_communications_pattern, j, mc_list_comm_pattern_t)->index_comm = 0;
 369     }
 370   }
 371
 372   MC_SET_STD_HEAP;
 373
 374   /* Traverse the stack from the state at position start and re-execute the transitions */
 375   for (item = start_item;
 376        item != xbt_fifo_get_first_item(stack);
 377        item = xbt_fifo_get_prev_item(item)) {
 378
 379     state = (mc_state_t) xbt_fifo_get_item_content(item);
 380     saved_req = MC_state_get_executed_request(state, &value);
 381
 382     if (saved_req) {
 383       /* because we got a copy of the executed request, we have to fetch the
 384          real one, pointed by the request field of the issuer process */
 385
 386       const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
 387       req = &issuer->simcall;
 388
 389       /* Debug information */
 390       if (XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)) {
 391         req_str = MC_request_to_string(req, value, MC_REQUEST_SIMIX);
 392         XBT_DEBUG("Replay: %s (%p)", req_str, state);
 393         xbt_free(req_str);
 394       }
 395
 396       /* TODO : handle test and testany simcalls */
 397       e_mc_call_type_t call = MC_CALL_TYPE_NONE;
 398       if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
 399         call = MC_get_call_type(req);
 400
 401       MC_simcall_handle(req, value);
 402
 403       MC_SET_MC_HEAP;
 404       if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
 405         MC_handle_comm_pattern(call, req, value, NULL, 1);
 406       MC_SET_STD_HEAP;
 407
 408       MC_wait_for_requests();
 409
 410       count++;
 411     }
 412
 413     /* Update statistics */
 414     mc_stats->visited_states++;
 415     mc_stats->executed_transitions++;
 416
 417   }
 418
 419   XBT_DEBUG("**** End Replay ****");
 420   mmalloc_set_current_heap(heap);
 421 }
 422
 423 void MC_replay_liveness(xbt_fifo_t stack)
 424 {
 425
 426   initial_global_state->raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
 427
 428   xbt_fifo_item_t item;
 429   mc_pair_t pair = NULL;
 430   mc_state_t state = NULL;
 431   smx_simcall_t req = NULL, saved_req = NULL;
 432   int value, depth = 1;
 433   char *req_str;
 434
 435   XBT_DEBUG("**** Begin Replay ****");
 436
 437   /* Intermediate backtracking */
 438   if(_sg_mc_checkpoint > 0) {
 439     item = xbt_fifo_get_first_item(stack);
 440     pair = (mc_pair_t) xbt_fifo_get_item_content(item);
 441     if(pair->graph_state->system_state){
 442       MC_restore_snapshot(pair->graph_state->system_state);
 443       MC_SET_STD_HEAP;
 444       return;
 445     }
 446   }
 447
 448   /* Restore the initial state */
 449   MC_restore_snapshot(initial_global_state->snapshot);
 450
 451   /* At the moment of taking the snapshot the raw heap was set, so restoring
 452    * it will set it back again, we have to unset it to continue  */
 453   if (!initial_global_state->raw_mem_set)
 454     MC_SET_STD_HEAP;
 455
 456     /* Traverse the stack from the initial state and re-execute the transitions */
 457     for (item = xbt_fifo_get_last_item(stack);
 458          item != xbt_fifo_get_first_item(stack);
 459          item = xbt_fifo_get_prev_item(item)) {
 460
 461       pair = (mc_pair_t) xbt_fifo_get_item_content(item);
 462
 463       state = (mc_state_t) pair->graph_state;
 464
 465       if (pair->exploration_started) {
 466
 467         saved_req = MC_state_get_executed_request(state, &value);
 468
 469         if (saved_req != NULL) {
 470           /* because we got a copy of the executed request, we have to fetch the
 471              real one, pointed by the request field of the issuer process */
 472           const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
 473           req = &issuer->simcall;
 474
 475           /* Debug information */
 476           if (XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)) {
 477             req_str = MC_request_to_string(req, value, MC_REQUEST_SIMIX);
 478             XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
 479             xbt_free(req_str);
 480           }
 481
 482         }
 483
 484         MC_simcall_handle(req, value);
 485         MC_wait_for_requests();
 486       }
 487
 488       /* Update statistics */
 489       mc_stats->visited_pairs++;
 490       mc_stats->executed_transitions++;
 491
 492       depth++;
 493
 494     }
 495
 496   XBT_DEBUG("**** End Replay ****");
 497
 498   if (initial_global_state->raw_mem_set)
 499     MC_SET_MC_HEAP;
 500   else
 501     MC_SET_STD_HEAP;
 502
 503 }
 504
 505 /**
 506  * \brief Dumps the contents of a model-checker's stack and shows the actual
 507  *        execution trace
 508  * \param stack The stack to dump
 509  */
 510 void MC_dump_stack_safety(xbt_fifo_t stack)
 511 {
 512   xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
 513
 514   MC_show_stack_safety(stack);
 515
 516   mc_state_t state;
 517
 518   MC_SET_MC_HEAP;
 519   while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
 520     MC_state_delete(state, !state->in_visited_states ? 1 : 0);
 521   mmalloc_set_current_heap(heap);
 522 }
 523
 524
 525 void MC_show_stack_safety(xbt_fifo_t stack)
 526 {
 527   xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
 528
 529   int value;
 530   mc_state_t state;
 531   xbt_fifo_item_t item;
 532   smx_simcall_t req;
 533   char *req_str = NULL;
 534
 535   for (item = xbt_fifo_get_last_item(stack);
 536        (item ? (state = (mc_state_t) (xbt_fifo_get_item_content(item)))
 537         : (NULL)); item = xbt_fifo_get_prev_item(item)) {
 538     req = MC_state_get_executed_request(state, &value);
 539     if (req) {
 540       req_str = MC_request_to_string(req, value, MC_REQUEST_EXECUTED);
 541       XBT_INFO("%s", req_str);
 542       xbt_free(req_str);
 543     }
 544   }
 545
 546   mmalloc_set_current_heap(heap);
 547 }
 548
 549 void MC_show_deadlock(smx_simcall_t req)
 550 {
 551   /*char *req_str = NULL; */
 552   XBT_INFO("**************************");
 553   XBT_INFO("*** DEAD-LOCK DETECTED ***");
 554   XBT_INFO("**************************");
 555   XBT_INFO("Locked request:");
 556   /*req_str = MC_request_to_string(req);
 557      XBT_INFO("%s", req_str);
 558      xbt_free(req_str); */
 559   XBT_INFO("Counter-example execution trace:");
 560   MC_dump_stack_safety(mc_stack);
 561   MC_print_statistics(mc_stats);
 562 }
 563
 564 void MC_show_non_termination(void){
 565   XBT_INFO("******************************************");
 566   XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
 567   XBT_INFO("******************************************");
 568   XBT_INFO("Counter-example execution trace:");
 569   MC_dump_stack_safety(mc_stack);
 570   MC_print_statistics(mc_stats);
 571 }
 572
 573
 574 void MC_show_stack_liveness(xbt_fifo_t stack)
 575 {
 576   int value;
 577   mc_pair_t pair;
 578   xbt_fifo_item_t item;
 579   smx_simcall_t req;
 580   char *req_str = NULL;
 581
 582   for (item = xbt_fifo_get_last_item(stack);
 583        (item ? (pair = (mc_pair_t) (xbt_fifo_get_item_content(item))) : (NULL));
 584        item = xbt_fifo_get_prev_item(item)) {
 585     req = MC_state_get_executed_request(pair->graph_state, &value);
 586     if (req && req->call != SIMCALL_NONE) {
 587       req_str = MC_request_to_string(req, value, MC_REQUEST_EXECUTED);
 588       XBT_INFO("%s", req_str);
 589       xbt_free(req_str);
 590     }
 591   }
 592 }
 593
 594
 595 void MC_dump_stack_liveness(xbt_fifo_t stack)
 596 {
 597   xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
 598   mc_pair_t pair;
 599   while ((pair = (mc_pair_t) xbt_fifo_pop(stack)) != NULL)
 600     MC_pair_delete(pair);
 601   mmalloc_set_current_heap(heap);
 602 }
 603
 604 void MC_print_statistics(mc_stats_t stats)
 605 {
 606   if(_sg_mc_comms_determinism) {
 607     if (!initial_global_state->recv_deterministic && initial_global_state->send_deterministic){
 608       XBT_INFO("******************************************************");
 609       XBT_INFO("**** Only-send-deterministic communication pattern ****");
 610       XBT_INFO("******************************************************");
 611       XBT_INFO("%s", initial_global_state->recv_diff);
 612     }else if(!initial_global_state->send_deterministic && initial_global_state->recv_deterministic) {
 613       XBT_INFO("******************************************************");
 614       XBT_INFO("**** Only-recv-deterministic communication pattern ****");
 615       XBT_INFO("******************************************************");
 616       XBT_INFO("%s", initial_global_state->send_diff);
 617     }
 618   }
 619
 620   if (stats->expanded_pairs == 0) {
 621     XBT_INFO("Expanded states = %lu", stats->expanded_states);
 622     XBT_INFO("Visited states = %lu", stats->visited_states);
 623   } else {
 624     XBT_INFO("Expanded pairs = %lu", stats->expanded_pairs);
 625     XBT_INFO("Visited pairs = %lu", stats->visited_pairs);
 626   }
 627   XBT_INFO("Executed transitions = %lu", stats->executed_transitions);
 628   xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
 629   if ((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0] != '\0')) {
 630     fprintf(dot_output, "}\n");
 631     fclose(dot_output);
 632   }
 633   if (initial_global_state != NULL && (_sg_mc_comms_determinism || _sg_mc_send_determinism)) {
 634     XBT_INFO("Send-deterministic : %s", !initial_global_state->send_deterministic ? "No" : "Yes");
 635     if (_sg_mc_comms_determinism)
 636       XBT_INFO("Recv-deterministic : %s", !initial_global_state->recv_deterministic ? "No" : "Yes");
 637   }
 638   mmalloc_set_current_heap(heap);
 639 }
 640
 641 void MC_automaton_load(const char *file)
 642 {
 643   xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
 644
 645   if (_mc_property_automaton == NULL)
 646     _mc_property_automaton = xbt_automaton_new();
 647
 648   xbt_automaton_load(_mc_property_automaton, file);
 649   mmalloc_set_current_heap(heap);
 650 }
 651
 652 static void register_symbol(xbt_automaton_propositional_symbol_t symbol)
 653 {
 654   if (mc_mode != MC_MODE_CLIENT)
 655     return;
 656   s_mc_register_symbol_message_t message;
 657   message.type = MC_MESSAGE_REGISTER_SYMBOL;
 658   const char* name = xbt_automaton_propositional_symbol_get_name(symbol);
 659   if (strlen(name) + 1 > sizeof(message.name))
 660     xbt_die("Symbol is too long");
 661   strncpy(message.name, name, sizeof(message.name));
 662   message.callback = xbt_automaton_propositional_symbol_get_callback(symbol);
 663   message.data = xbt_automaton_propositional_symbol_get_data(symbol);
 664   MC_client_send_message(&message, sizeof(message));
 665 }
 666
 667 void MC_automaton_new_propositional_symbol(const char *id, int(*fct)(void))
 668 {
 669   xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
 670
 671   if (_mc_property_automaton == NULL)
 672     _mc_property_automaton = xbt_automaton_new();
 673
 674   xbt_automaton_propositional_symbol_t symbol = xbt_automaton_propositional_symbol_new(_mc_property_automaton, id, fct);
 675   register_symbol(symbol);
 676   mmalloc_set_current_heap(heap);
 677 }
 678
 679 void MC_automaton_new_propositional_symbol_pointer(const char *id, int* value)
 680 {
 681   xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
 682   if (_mc_property_automaton == NULL)
 683     _mc_property_automaton = xbt_automaton_new();
 684   xbt_automaton_propositional_symbol_t symbol = xbt_automaton_propositional_symbol_new_pointer(_mc_property_automaton, id, value);
 685   register_symbol(symbol);
 686   mmalloc_set_current_heap(heap);
 687 }
 688
 689 void MC_automaton_new_propositional_symbol_callback(const char* id,
 690   xbt_automaton_propositional_symbol_callback_type callback,
 691   void* data, xbt_automaton_propositional_symbol_free_function_type free_function)
 692 {
 693   xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
 694   if (_mc_property_automaton == NULL)
 695     _mc_property_automaton = xbt_automaton_new();
 696   xbt_automaton_propositional_symbol_t symbol = xbt_automaton_propositional_symbol_new_callback(
 697     _mc_property_automaton, id, callback, data, free_function);
 698   register_symbol(symbol);
 699   mmalloc_set_current_heap(heap);
 700 }
 701
 702 // TODO, fix cross-process access (this function is not used)
 703 void MC_dump_stacks(FILE* file)
 704 {
 705   xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
 706
 707   int nstack = 0;
 708   stack_region_t current_stack;
 709   unsigned cursor;
 710   xbt_dynar_foreach(stacks_areas, cursor, current_stack) {
 711     unw_context_t * context = (unw_context_t *)current_stack->context;
 712     fprintf(file, "Stack %i:\n", nstack);
 713
 714     int nframe = 0;
 715     char buffer[100];
 716     unw_cursor_t c;
 717     unw_init_local (&c, context);
 718     unw_word_t off;
 719     do {
 720       const char * name = !unw_get_proc_name(&c, buffer, 100, &off) ? buffer : "?";
 721 #if defined(__x86_64__)
 722       unw_word_t rip = 0;
 723       unw_word_t rsp = 0;
 724       unw_get_reg(&c, UNW_X86_64_RIP, &rip);
 725       unw_get_reg(&c, UNW_X86_64_RSP, &rsp);
 726       fprintf(file, "  %i: %s (RIP=0x%" PRIx64 " RSP=0x%" PRIx64 ")\n",
 727         nframe, name, rip, rsp);
 728 #else
 729       fprintf(file, "  %i: %s\n", nframe, name);
 730 #endif
 731       ++nframe;
 732     } while(unw_step(&c));
 733
 734     ++nstack;
 735   }
 736   mmalloc_set_current_heap(heap);
 737 }
 738 #endif
 739
 740 double MC_process_clock_get(smx_process_t process)
 741 {
 742   if (mc_time) {
 743     if (process != NULL)
 744       return mc_time[process->pid];
 745     else
 746       return -1;
 747   } else {
 748     return 0;
 749   }
 750 }
 751
 752 void MC_process_clock_add(smx_process_t process, double amount)
 753 {
 754   mc_time[process->pid] += amount;
 755 }
 756
 757 #ifdef HAVE_MC
 758 void MC_report_assertion_error(void)
 759 {
 760   XBT_INFO("**************************");
 761   XBT_INFO("*** PROPERTY NOT VALID ***");
 762   XBT_INFO("**************************");
 763   XBT_INFO("Counter-example execution trace:");
 764   MC_record_dump_path(mc_stack);
 765   MC_dump_stack_safety(mc_stack);
 766   MC_print_statistics(mc_stats);
 767 }
 768 #endif
 769
 770 }