Logo AND Algorithmique Numérique Distribuée

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