Logo AND Algorithmique Numérique Distribuée

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