Logo AND Algorithmique Numérique Distribuée

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