Logo AND Algorithmique Numérique Distribuée

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