Logo AND Algorithmique Numérique Distribuée

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