Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
[mc] Do not execute MCer code in MCed mode in MC_remove_ignore_heap()
[simgrid.git] / src / mc / mc_request.cpp
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 <assert.h>
8
9 #include "mc_request.h"
10 #include "mc_safety.h"
11 #include "mc_private.h"
12 #include "mc_smx.h"
13
14 extern "C" {
15
16 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_request, mc,
17                                 "Logging specific to MC (request)");
18
19 static char *pointer_to_string(void *pointer);
20 static char *buff_size_to_string(size_t size);
21
22 // Those are MC_state_get_internal_request(state)
23 int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2)
24 {
25   if (mc_reduce_kind == e_mc_reduce_none)
26     return TRUE;
27
28   if (r1->issuer == r2->issuer)
29     return FALSE;
30
31   /* Wait with timeout transitions are not considered by the independance theorem, thus we consider them as dependant with all other transitions */
32   if ((r1->call == SIMCALL_COMM_WAIT && simcall_comm_wait__get__timeout(r1) > 0)
33       || (r2->call == SIMCALL_COMM_WAIT
34           && simcall_comm_wait__get__timeout(r2) > 0))
35     return TRUE;
36
37   if (r1->call == SIMCALL_COMM_ISEND && r2->call == SIMCALL_COMM_IRECV)
38     return FALSE;
39
40   if (r1->call == SIMCALL_COMM_IRECV && r2->call == SIMCALL_COMM_ISEND)
41     return FALSE;
42
43   // Those are internal requests, we do not need indirection
44   // because those objects are copies:
45   smx_synchro_t synchro1 = NULL, synchro2 = NULL;
46   if (r1->call == SIMCALL_COMM_WAIT) {
47     synchro1 = simcall_comm_wait__get__comm(r1);
48   }
49   if (r2->call == SIMCALL_COMM_WAIT) {
50     synchro2 = simcall_comm_wait__get__comm(r2);
51   }
52   if (r1->call == SIMCALL_COMM_TEST) {
53     synchro1 = simcall_comm_test__get__comm(r1);
54   }
55   if (r2->call == SIMCALL_COMM_TEST) {
56     synchro2 = simcall_comm_test__get__comm(r2);
57   }
58
59   if ((r1->call == SIMCALL_COMM_ISEND || r1->call == SIMCALL_COMM_IRECV)
60       && r2->call == SIMCALL_COMM_WAIT) {
61
62     smx_rdv_t rdv =
63         r1->call ==
64         SIMCALL_COMM_ISEND ? simcall_comm_isend__get__rdv(r1) :
65         simcall_comm_irecv__get__rdv(r1);
66
67     if (rdv != synchro2->comm.rdv_cpy
68         && simcall_comm_wait__get__timeout(r2) <= 0)
69       return FALSE;
70
71     if ((r1->issuer != synchro2->comm.src_proc)
72         && (r1->issuer != synchro2->comm.dst_proc)
73         && simcall_comm_wait__get__timeout(r2) <= 0)
74       return FALSE;
75
76     if ((r1->call == SIMCALL_COMM_ISEND)
77         && (synchro2->comm.type == SIMIX_COMM_SEND)
78         && (synchro2->comm.src_buff !=
79             simcall_comm_isend__get__src_buff(r1))
80         && simcall_comm_wait__get__timeout(r2) <= 0)
81       return FALSE;
82
83     if ((r1->call == SIMCALL_COMM_IRECV)
84         && (synchro2->comm.type == SIMIX_COMM_RECEIVE)
85         && (synchro2->comm.dst_buff != simcall_comm_irecv__get__dst_buff(r1))
86         && simcall_comm_wait__get__timeout(r2) <= 0)
87       return FALSE;
88   }
89
90   if ((r2->call == SIMCALL_COMM_ISEND || r2->call == SIMCALL_COMM_IRECV)
91       && r1->call == SIMCALL_COMM_WAIT) {
92
93     smx_rdv_t rdv =
94         r2->call ==
95         SIMCALL_COMM_ISEND ? simcall_comm_isend__get__rdv(r2) :
96         simcall_comm_irecv__get__rdv(r2);
97
98     if (rdv != synchro1->comm.rdv_cpy
99         && simcall_comm_wait__get__timeout(r1) <= 0)
100       return FALSE;
101
102     if ((r2->issuer != synchro1->comm.src_proc)
103         && (r2->issuer != synchro1->comm.dst_proc)
104         && simcall_comm_wait__get__timeout(r1) <= 0)
105       return FALSE;
106
107     if ((r2->call == SIMCALL_COMM_ISEND)
108         && (synchro1->comm.type == SIMIX_COMM_SEND)
109         && (synchro1->comm.src_buff !=
110             simcall_comm_isend__get__src_buff(r2))
111         && simcall_comm_wait__get__timeout(r1) <= 0)
112       return FALSE;
113
114     if ((r2->call == SIMCALL_COMM_IRECV)
115         && (synchro1->comm.type == SIMIX_COMM_RECEIVE)
116         && (synchro1->comm.dst_buff !=
117             simcall_comm_irecv__get__dst_buff(r2))
118         && simcall_comm_wait__get__timeout(r1) <= 0)
119       return FALSE;
120   }
121
122   /* FIXME: the following rule assumes that the result of the
123    * isend/irecv call is not stored in a buffer used in the
124    * test call. */
125   /*if(   (r1->call == SIMCALL_COMM_ISEND || r1->call == SIMCALL_COMM_IRECV)
126      &&  r2->call == SIMCALL_COMM_TEST)
127      return FALSE; */
128
129   /* FIXME: the following rule assumes that the result of the
130    * isend/irecv call is not stored in a buffer used in the
131    * test call.*/
132   /*if(   (r2->call == SIMCALL_COMM_ISEND || r2->call == SIMCALL_COMM_IRECV)
133      && r1->call == SIMCALL_COMM_TEST)
134      return FALSE; */
135
136   if (r1->call == SIMCALL_COMM_ISEND && r2->call == SIMCALL_COMM_ISEND
137       && simcall_comm_isend__get__rdv(r1) != simcall_comm_isend__get__rdv(r2))
138     return FALSE;
139
140   if (r1->call == SIMCALL_COMM_IRECV && r2->call == SIMCALL_COMM_IRECV
141       && simcall_comm_irecv__get__rdv(r1) != simcall_comm_irecv__get__rdv(r2))
142     return FALSE;
143
144   if (r1->call == SIMCALL_COMM_WAIT
145       && (r2->call == SIMCALL_COMM_WAIT || r2->call == SIMCALL_COMM_TEST)
146       && (synchro1->comm.src_proc == NULL || synchro1->comm.dst_proc == NULL))
147     return FALSE;
148
149   if (r2->call == SIMCALL_COMM_WAIT
150       && (r1->call == SIMCALL_COMM_WAIT || r1->call == SIMCALL_COMM_TEST)
151       && (synchro2->comm.src_proc == NULL || synchro2->comm.dst_proc == NULL))
152       return FALSE;
153
154   if (r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_WAIT
155       && synchro1->comm.src_buff == synchro2->comm.src_buff
156       && synchro2->comm.dst_buff == synchro2->comm.dst_buff)
157     return FALSE;
158
159   if (r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_WAIT
160       && synchro1->comm.src_buff != NULL
161       && synchro1->comm.dst_buff != NULL
162       && synchro2->comm.src_buff != NULL
163       && synchro2->comm.dst_buff != NULL
164       && synchro1->comm.dst_buff != synchro2->comm.src_buff
165       && synchro1->comm.dst_buff != synchro2->comm.dst_buff
166       && synchro2->comm.dst_buff != synchro1->comm.src_buff)
167     return FALSE;
168
169   if (r1->call == SIMCALL_COMM_TEST &&
170       (simcall_comm_test__get__comm(r1) == NULL
171        || synchro1->comm.src_buff == NULL
172        || synchro1->comm.dst_buff == NULL))
173     return FALSE;
174
175   if (r2->call == SIMCALL_COMM_TEST &&
176       (simcall_comm_test__get__comm(r2) == NULL
177        || synchro2->comm.src_buff == NULL
178        || synchro2->comm.dst_buff == NULL))
179     return FALSE;
180
181   if (r1->call == SIMCALL_COMM_TEST && r2->call == SIMCALL_COMM_WAIT
182       && synchro1->comm.src_buff == synchro2->comm.src_buff
183       && synchro1->comm.dst_buff == synchro2->comm.dst_buff)
184     return FALSE;
185
186   if (r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_TEST
187       && synchro1->comm.src_buff == synchro2->comm.src_buff
188       && synchro1->comm.dst_buff == synchro2->comm.dst_buff)
189     return FALSE;
190
191   if (r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_TEST
192       && synchro1->comm.src_buff != NULL
193       && synchro1->comm.dst_buff != NULL
194       && synchro2->comm.src_buff != NULL
195       && synchro2->comm.dst_buff != NULL
196       && synchro1->comm.dst_buff != synchro2->comm.src_buff
197       && synchro1->comm.dst_buff != synchro2->comm.dst_buff
198       && synchro2->comm.dst_buff != synchro1->comm.src_buff)
199     return FALSE;
200
201   if (r1->call == SIMCALL_COMM_TEST && r2->call == SIMCALL_COMM_WAIT
202       && synchro1->comm.src_buff != NULL
203       && synchro1->comm.dst_buff != NULL
204       && synchro2->comm.src_buff != NULL
205       && synchro2->comm.dst_buff != NULL
206       && synchro1->comm.dst_buff != synchro2->comm.src_buff
207       && synchro1->comm.dst_buff != synchro2->comm.dst_buff
208       && synchro2->comm.dst_buff != synchro1->comm.src_buff)
209     return FALSE;
210
211   return TRUE;
212 }
213
214 static char *pointer_to_string(void *pointer)
215 {
216
217   if (XBT_LOG_ISENABLED(mc_request, xbt_log_priority_verbose))
218     return bprintf("%p", pointer);
219
220   return xbt_strdup("(verbose only)");
221 }
222
223 static char *buff_size_to_string(size_t buff_size)
224 {
225
226   if (XBT_LOG_ISENABLED(mc_request, xbt_log_priority_verbose))
227     return bprintf("%zu", buff_size);
228
229   return xbt_strdup("(verbose only)");
230 }
231
232
233 char *MC_request_to_string(smx_simcall_t req, int value, e_mc_request_type_t request_type)
234 {
235   bool use_remote_comm = false;
236   switch(request_type) {
237   case MC_REQUEST_SIMIX:
238     use_remote_comm = true;
239     break;
240   case MC_REQUEST_EXECUTED:
241   case MC_REQUEST_INTERNAL:
242     use_remote_comm = false;
243     break;
244   }
245
246   const char* type = NULL;
247   char *args = NULL;
248
249   smx_process_t issuer = MC_smx_simcall_get_issuer(req);
250
251   switch (req->call) {
252
253   case SIMCALL_COMM_ISEND: {
254     type = "iSend";
255     char* p = pointer_to_string(simcall_comm_isend__get__src_buff(req));
256     char* bs = buff_size_to_string(simcall_comm_isend__get__src_buff_size(req));
257     if (issuer->smx_host)
258       args =
259           bprintf("src=(%lu)%s (%s), buff=%s, size=%s", issuer->pid,
260                   MC_smx_process_get_host_name(issuer),
261                   MC_smx_process_get_name(issuer),
262                   p, bs);
263     else
264       args =
265           bprintf("src=(%lu)%s, buff=%s, size=%s", issuer->pid,
266                   MC_smx_process_get_name(issuer), p, bs);
267     xbt_free(bs);
268     xbt_free(p);
269     break;
270   }
271
272   case SIMCALL_COMM_IRECV: {
273     size_t* remote_size = simcall_comm_irecv__get__dst_buff_size(req);
274
275     // size_t size = size_pointer ? *size_pointer : 0;
276     size_t size = 0;
277     if (remote_size)
278       MC_process_read_simple(&mc_model_checker->process(), &size,
279         remote_size, sizeof(size));
280
281     type = "iRecv";
282     char* p = pointer_to_string(simcall_comm_irecv__get__dst_buff(req));
283     char* bs = buff_size_to_string(size);
284     if (issuer->smx_host)
285       args =
286           bprintf("dst=(%lu)%s (%s), buff=%s, size=%s", issuer->pid,
287                   MC_smx_process_get_host_name(issuer),
288                   MC_smx_process_get_name(issuer),
289                   p, bs);
290     else
291       args =
292           bprintf("dst=(%lu)%s, buff=%s, size=%s", issuer->pid,
293                   MC_smx_process_get_name(issuer),
294                   p, bs);
295     xbt_free(bs);
296     xbt_free(p);
297     break;
298   }
299
300   case SIMCALL_COMM_WAIT: {
301     smx_synchro_t remote_act = simcall_comm_wait__get__comm(req);
302     char* p;
303     if (value == -1) {
304       type = "WaitTimeout";
305       p = pointer_to_string(remote_act);
306       args = bprintf("comm=%s", p);
307     } else {
308       type = "Wait";
309       p = pointer_to_string(remote_act);
310
311       s_smx_synchro_t synchro;
312       smx_synchro_t act;
313       if (use_remote_comm) {
314         MC_process_read_simple(&mc_model_checker->process(), &synchro,
315           remote_act, sizeof(synchro));
316         act = &synchro;
317       } else
318         act = remote_act;
319
320       smx_process_t src_proc = MC_smx_resolve_process(act->comm.src_proc);
321       smx_process_t dst_proc = MC_smx_resolve_process(act->comm.dst_proc);
322       args = bprintf("comm=%s [(%lu)%s (%s)-> (%lu)%s (%s)]", p,
323                      src_proc ? src_proc->pid : 0,
324                      src_proc ? MC_smx_process_get_host_name(src_proc) : "",
325                      src_proc ? MC_smx_process_get_name(src_proc) : "",
326                      dst_proc ? dst_proc->pid : 0,
327                      dst_proc ? MC_smx_process_get_host_name(dst_proc) : "",
328                      dst_proc ? MC_smx_process_get_name(dst_proc) : "");
329     }
330     xbt_free(p);
331     break;
332   }
333
334   case SIMCALL_COMM_TEST: {
335     smx_synchro_t remote_act = simcall_comm_test__get__comm(req);
336     s_smx_synchro_t synchro;
337       smx_synchro_t act;
338       if (use_remote_comm) {
339         MC_process_read_simple(&mc_model_checker->process(), &synchro,
340           remote_act, sizeof(synchro));
341         act = &synchro;
342       } else
343         act = remote_act;
344
345     char* p;
346     if (act->comm.src_proc == NULL || act->comm.dst_proc == NULL) {
347       type = "Test FALSE";
348       p = pointer_to_string(remote_act);
349       args = bprintf("comm=%s", p);
350     } else {
351       type = "Test TRUE";
352       p = pointer_to_string(remote_act);
353
354       smx_process_t src_proc = MC_smx_resolve_process(act->comm.src_proc);
355       smx_process_t dst_proc = MC_smx_resolve_process(act->comm.dst_proc);
356       args = bprintf("comm=%s [(%lu)%s (%s) -> (%lu)%s (%s)]", p,
357                      src_proc->pid,
358                      MC_smx_process_get_name(src_proc),
359                      MC_smx_process_get_host_name(src_proc),
360                      dst_proc->pid,
361                      MC_smx_process_get_name(dst_proc),
362                      MC_smx_process_get_host_name(dst_proc));
363     }
364     xbt_free(p);
365     break;
366   }
367
368   case SIMCALL_COMM_WAITANY: {
369     type = "WaitAny";
370     s_xbt_dynar_t comms;
371     MC_process_read_simple(&mc_model_checker->process(),
372       &comms,  simcall_comm_waitany__get__comms(req), sizeof(comms));
373     if (!xbt_dynar_is_empty(&comms)) {
374       smx_synchro_t remote_sync;
375       MC_process_read_dynar_element(&mc_model_checker->process(),
376         &remote_sync, simcall_comm_waitany__get__comms(req), value,
377         sizeof(remote_sync));
378       char* p = pointer_to_string(remote_sync);
379       args = bprintf("comm=%s (%d of %lu)",
380         p, value + 1, xbt_dynar_length(&comms));
381       xbt_free(p);
382     } else {
383       args = bprintf("comm at idx %d", value);
384     }
385     break;
386   }
387
388   case SIMCALL_COMM_TESTANY:
389     if (value == -1) {
390       type = "TestAny FALSE";
391       args = xbt_strdup("-");
392     } else {
393       type = "TestAny";
394       args =
395           bprintf("(%d of %lu)", value + 1,
396                   MC_process_read_dynar_length(&mc_model_checker->process(),
397                     simcall_comm_testany__get__comms(req)));
398     }
399     break;
400
401   case SIMCALL_MUTEX_LOCK: {
402     type = "Mutex LOCK";
403
404     s_smx_mutex_t mutex;
405     MC_process_read_simple(&mc_model_checker->process(), &mutex,
406       simcall_mutex_lock__get__mutex(req), sizeof(mutex));
407     s_xbt_swag_t mutex_sleeping;
408     MC_process_read_simple(&mc_model_checker->process(), &mutex_sleeping,
409       mutex.sleeping, sizeof(mutex_sleeping));
410
411     args = bprintf("locked = %d, owner = %d, sleeping = %d",
412       mutex.locked,
413       mutex.owner != NULL ? (int) MC_smx_resolve_process(mutex.owner)->pid : -1,
414       mutex_sleeping.count);
415     break;
416   }
417
418   case SIMCALL_MC_SNAPSHOT:
419     type = "MC_SNAPSHOT";
420     args = NULL;
421     break;
422
423   case SIMCALL_MC_COMPARE_SNAPSHOTS:
424     type = "MC_COMPARE_SNAPSHOTS";
425     args = NULL;
426     break;
427
428   case SIMCALL_MC_RANDOM:
429     type = "MC_RANDOM";
430     args = bprintf("%d", value);
431     break;
432
433   default:
434     THROW_UNIMPLEMENTED;
435   }
436
437   char* str;
438   if (args != NULL) {
439     str =
440         bprintf("[(%lu)%s (%s)] %s(%s)", issuer->pid,
441                 MC_smx_process_get_host_name(issuer),
442                 MC_smx_process_get_name(issuer),
443                 type, args);
444   } else {
445     str =
446         bprintf("[(%lu)%s (%s)] %s ", issuer->pid,
447                 MC_smx_process_get_host_name(issuer),
448                 MC_smx_process_get_name(issuer),
449                 type);
450   }
451   xbt_free(args);
452   return str;
453 }
454
455 unsigned int MC_request_testany_fail(smx_simcall_t req)
456 {
457   // Remote xbt_dynar_foreach on simcall_comm_testany__get__comms(req).
458
459   // Read the dynar:
460   s_xbt_dynar_t comms;
461   MC_process_read_simple(&mc_model_checker->process(),
462     &comms, simcall_comm_testany__get__comms(req), sizeof(comms));
463
464   // Read ther dynar buffer:
465   size_t buffer_size = comms.elmsize * comms.used;
466   char buffer[buffer_size];
467   MC_process_read_simple(&mc_model_checker->process(),
468     buffer, comms.data, buffer_size);
469
470   // Iterate over the elements:
471   assert(comms.elmsize == sizeof(smx_synchro_t));
472   unsigned cursor;
473   for (cursor=0; cursor != comms.used; ++cursor) {
474
475     // Get the element:
476     smx_synchro_t remote_action;
477     memcpy(&remote_action, buffer + comms.elmsize * cursor, sizeof(remote_action));
478
479     // Dereference the pointer:
480     s_smx_synchro_t action;
481     MC_process_read_simple(&mc_model_checker->process(),
482       &action, remote_action, sizeof(action));
483
484     // Finally so something useful about it:
485     if (action.comm.src_proc && action.comm.dst_proc)
486       return FALSE;
487   }
488
489   return TRUE;
490 }
491
492 int MC_request_is_enabled_by_idx(smx_simcall_t req, unsigned int idx)
493 {
494   smx_synchro_t remote_act = NULL;
495   switch (req->call) {
496
497   case SIMCALL_COMM_WAIT:
498     /* FIXME: check also that src and dst processes are not suspended */
499     remote_act = simcall_comm_wait__get__comm(req);
500     break;
501
502   case SIMCALL_COMM_WAITANY: {
503     MC_process_read_dynar_element(
504       &mc_model_checker->process(), &remote_act, simcall_comm_waitany__get__comms(req),
505       idx, sizeof(remote_act));
506     }
507     break;
508
509   case SIMCALL_COMM_TESTANY: {
510     MC_process_read_dynar_element(
511       &mc_model_checker->process(), &remote_act, simcall_comm_testany__get__comms(req),
512       idx, sizeof(remote_act));
513     }
514     break;
515
516   default:
517     return TRUE;
518   }
519
520   s_smx_synchro_t synchro;
521   MC_process_read_simple(&mc_model_checker->process(),
522     &synchro, remote_act, sizeof(synchro));
523   return synchro.comm.src_proc && synchro.comm.dst_proc;
524 }
525
526 int MC_process_is_enabled(smx_process_t process)
527 {
528   return MC_request_is_enabled(&process->simcall);
529 }
530
531 char *MC_request_get_dot_output(smx_simcall_t req, int value)
532 {
533   char *label = NULL;
534
535   const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
536
537   switch (req->call) {
538   case SIMCALL_COMM_ISEND:
539     if (issuer->smx_host)
540       label =
541           bprintf("[(%lu)%s] iSend", issuer->pid,
542                   MC_smx_process_get_host_name(issuer));
543     else
544       label = bprintf("[(%lu)] iSend", issuer->pid);
545     break;
546
547   case SIMCALL_COMM_IRECV:
548     if (issuer->smx_host)
549       label =
550           bprintf("[(%lu)%s] iRecv", issuer->pid,
551                   MC_smx_process_get_host_name(issuer));
552     else
553       label = bprintf("[(%lu)] iRecv", issuer->pid);
554     break;
555
556   case SIMCALL_COMM_WAIT: {
557     if (value == -1) {
558       if (issuer->smx_host)
559         label =
560             bprintf("[(%lu)%s] WaitTimeout", issuer->pid,
561                     MC_smx_process_get_host_name(issuer));
562       else
563         label = bprintf("[(%lu)] WaitTimeout", issuer->pid);
564     } else {
565       smx_synchro_t remote_act = simcall_comm_wait__get__comm(req);
566       s_smx_synchro_t synchro;
567       MC_process_read_simple(&mc_model_checker->process(), &synchro,
568         remote_act, sizeof(synchro));
569
570       smx_process_t src_proc = MC_smx_resolve_process(synchro.comm.src_proc);
571       smx_process_t dst_proc = MC_smx_resolve_process(synchro.comm.dst_proc);
572       if (issuer->smx_host)
573         label =
574             bprintf("[(%lu)%s] Wait [(%lu)->(%lu)]", issuer->pid,
575                     MC_smx_process_get_host_name(issuer),
576                     src_proc ? src_proc->pid : 0,
577                     dst_proc ? dst_proc->pid : 0);
578       else
579         label =
580             bprintf("[(%lu)] Wait [(%lu)->(%lu)]", issuer->pid,
581                     src_proc ? src_proc->pid : 0,
582                     dst_proc ? dst_proc->pid : 0);
583     }
584     break;
585   }
586
587   case SIMCALL_COMM_TEST: {
588     smx_synchro_t remote_act = simcall_comm_test__get__comm(req);
589     s_smx_synchro_t synchro;
590     MC_process_read_simple(&mc_model_checker->process(), &synchro,
591       remote_act, sizeof(synchro));
592     if (synchro.comm.src_proc == NULL || synchro.comm.dst_proc == NULL) {
593       if (issuer->smx_host)
594         label =
595             bprintf("[(%lu)%s] Test FALSE", issuer->pid,
596                     MC_smx_process_get_host_name(issuer));
597       else
598         label = bprintf("[(%lu)] Test FALSE", issuer->pid);
599     } else {
600       if (issuer->smx_host)
601         label =
602             bprintf("[(%lu)%s] Test TRUE", issuer->pid,
603                     MC_smx_process_get_host_name(issuer));
604       else
605         label = bprintf("[(%lu)] Test TRUE", issuer->pid);
606     }
607     break;
608   }
609
610   case SIMCALL_COMM_WAITANY: {
611     unsigned long comms_size = MC_process_read_dynar_length(
612       &mc_model_checker->process(), simcall_comm_waitany__get__comms(req));
613     if (issuer->smx_host)
614       label =
615           bprintf("[(%lu)%s] WaitAny [%d of %lu]", issuer->pid,
616                   MC_smx_process_get_host_name(issuer), value + 1,
617                   comms_size);
618     else
619       label =
620           bprintf("[(%lu)] WaitAny [%d of %lu]", issuer->pid, value + 1,
621                   comms_size);
622     break;
623   }
624
625   case SIMCALL_COMM_TESTANY:
626     if (value == -1) {
627       if (issuer->smx_host)
628         label =
629             bprintf("[(%lu)%s] TestAny FALSE", issuer->pid,
630                     MC_smx_process_get_host_name(issuer));
631       else
632         label = bprintf("[(%lu)] TestAny FALSE", issuer->pid);
633     } else {
634       if (issuer->smx_host)
635         label =
636             bprintf("[(%lu)%s] TestAny TRUE [%d of %lu]", issuer->pid,
637                     MC_smx_process_get_host_name(issuer), value + 1,
638                     xbt_dynar_length(simcall_comm_testany__get__comms(req)));
639       else
640         label =
641             bprintf("[(%lu)] TestAny TRUE [%d of %lu]", issuer->pid,
642                     value + 1,
643                     xbt_dynar_length(simcall_comm_testany__get__comms(req)));
644     }
645     break;
646
647   case SIMCALL_MUTEX_LOCK:
648     label = bprintf("[(%lu)] Mutex LOCK", req->issuer->pid);
649     break;
650
651   case SIMCALL_MC_RANDOM:
652     if (issuer->smx_host)
653       label =
654           bprintf("[(%lu)%s] MC_RANDOM (%d)", issuer->pid,
655                   MC_smx_process_get_host_name(issuer), value);
656     else
657       label = bprintf("[(%lu)] MC_RANDOM (%d)", issuer->pid, value);
658     break;
659
660   case SIMCALL_MC_SNAPSHOT:
661     if (issuer->smx_host)
662       label =
663           bprintf("[(%lu)%s] MC_SNAPSHOT", issuer->pid,
664                   MC_smx_process_get_host_name(issuer));
665     else
666       label = bprintf("[(%lu)] MC_SNAPSHOT", issuer->pid);
667     break;
668
669   case SIMCALL_MC_COMPARE_SNAPSHOTS:
670     if (issuer->smx_host)
671       label =
672           bprintf("[(%lu)%s] MC_COMPARE_SNAPSHOTS", issuer->pid,
673                   MC_smx_process_get_host_name(issuer));
674     else
675       label = bprintf("[(%lu)] MC_COMPARE_SNAPSHOTS", issuer->pid);
676     break;
677
678   default:
679     THROW_UNIMPLEMENTED;
680   }
681
682   char* str =
683       bprintf("label = \"%s\", color = %s, fontcolor = %s", label,
684               colors[issuer->pid - 1], colors[issuer->pid - 1]);
685   xbt_free(label);
686   return str;
687
688 }
689
690 }