Logo AND Algorithmique Numérique Distribuée

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