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