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 "mc_request.h"
   8 #include "mc_safety.h"
   9 #include "mc_private.h"
  10 #include "mc_smx.h"
  11
  12 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_request, mc,
  13                                 "Logging specific to MC (request)");
  14
  15 static char *pointer_to_string(void *pointer);
  16 static char *buff_size_to_string(size_t size);
  17
  18 int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2)
  19 {
  20   if (mc_reduce_kind == e_mc_reduce_none)
  21     return TRUE;
  22
  23   if (r1->issuer == r2->issuer)
  24     return FALSE;
  25
  26   /* Wait with timeout transitions are not considered by the independance theorem, thus we consider them as dependant with all other transitions */
  27   if ((r1->call == SIMCALL_COMM_WAIT && simcall_comm_wait__get__timeout(r1) > 0)
  28       || (r2->call == SIMCALL_COMM_WAIT
  29           && simcall_comm_wait__get__timeout(r2) > 0))
  30     return TRUE;
  31
  32   if (r1->call == SIMCALL_COMM_ISEND && r2->call == SIMCALL_COMM_IRECV)
  33     return FALSE;
  34
  35   if (r1->call == SIMCALL_COMM_IRECV && r2->call == SIMCALL_COMM_ISEND)
  36     return FALSE;
  37
  38   // Read object from MCed memory:
  39   s_smx_synchro_t synchro1, synchro2;
  40   if (r1->call == SIMCALL_COMM_WAIT) {
  41     MC_process_read_simple(&mc_model_checker->process, &synchro1,
  42       simcall_comm_wait__get__comm(r1), sizeof(synchro1));
  43   }
  44   if (r2->call == SIMCALL_COMM_WAIT) {
  45     MC_process_read_simple(&mc_model_checker->process, &synchro2,
  46       simcall_comm_wait__get__comm(r2), sizeof(synchro2));
  47   }
  48   if (r1->call == SIMCALL_COMM_TEST) {
  49     MC_process_read_simple(&mc_model_checker->process, &synchro1,
  50       simcall_comm_test__get__comm(r1), sizeof(synchro1));
  51   }
  52   if (r2->call == SIMCALL_COMM_TEST) {
  53     MC_process_read_simple(&mc_model_checker->process, &synchro2,
  54       simcall_comm_test__get__comm(r2), sizeof(synchro2));
  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     // FIXME, remote access to comm object
  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)
 234 {
 235   const char* type = NULL;
 236   char *args = NULL;
 237
 238   smx_process_t issuer = MC_smx_simcall_get_issuer(req);
 239
 240   switch (req->call) {
 241
 242   case SIMCALL_COMM_ISEND: {
 243     type = "iSend";
 244     char* p = pointer_to_string(simcall_comm_isend__get__src_buff(req));
 245     char* bs = buff_size_to_string(simcall_comm_isend__get__src_buff_size(req));
 246     if (issuer->smx_host)
 247       args =
 248           bprintf("src=(%lu)%s (%s), buff=%s, size=%s", issuer->pid,
 249                   MC_smx_process_get_host_name(issuer),
 250                   MC_smx_process_get_name(issuer),
 251                   p, bs);
 252     else
 253       args =
 254           bprintf("src=(%lu)%s, buff=%s, size=%s", issuer->pid,
 255                   MC_smx_process_get_name(issuer), p, bs);
 256     xbt_free(bs);
 257     xbt_free(p);
 258     break;
 259   }
 260
 261   case SIMCALL_COMM_IRECV: {
 262     size_t* remote_size = simcall_comm_irecv__get__dst_buff_size(req);
 263
 264     // size_t size = size_pointer ? *size_pointer : 0;
 265     size_t size = 0;
 266     if (remote_size)
 267       MC_process_read_simple(&mc_model_checker->process, &size,
 268         remote_size, sizeof(size));
 269
 270     type = "iRecv";
 271     char* p = pointer_to_string(simcall_comm_irecv__get__dst_buff(req));
 272     char* bs = buff_size_to_string(size);
 273     if (issuer->smx_host)
 274       args =
 275           bprintf("dst=(%lu)%s (%s), buff=%s, size=%s", issuer->pid,
 276                   MC_smx_process_get_host_name(issuer),
 277                   MC_smx_process_get_name(issuer),
 278                   p, bs);
 279     else
 280       args =
 281           bprintf("dst=(%lu)%s, buff=%s, size=%s", issuer->pid,
 282                   MC_smx_process_get_name(issuer),
 283                   p, bs);
 284     xbt_free(bs);
 285     xbt_free(p);
 286     break;
 287   }
 288
 289   case SIMCALL_COMM_WAIT: {
 290     smx_synchro_t remote_act = simcall_comm_wait__get__comm(req);
 291     char* p;
 292     if (value == -1) {
 293       type = "WaitTimeout";
 294       p = pointer_to_string(remote_act);
 295       args = bprintf("comm=%s", p);
 296     } else {
 297       type = "Wait";
 298       p = pointer_to_string(remote_act);
 299
 300       s_smx_synchro_t synchro;
 301       MC_process_read_simple(&mc_model_checker->process, &synchro,
 302         remote_act, sizeof(synchro));
 303
 304       smx_process_t src_proc = MC_smx_resolve_process(synchro.comm.src_proc);
 305       smx_process_t dst_proc = MC_smx_resolve_process(synchro.comm.dst_proc);
 306       args = bprintf("comm=%s [(%lu)%s (%s)-> (%lu)%s (%s)]", p,
 307                      src_proc ? src_proc->pid : 0,
 308                      src_proc ? MC_smx_process_get_host_name(src_proc) : "",
 309                      src_proc ? MC_smx_process_get_name(src_proc) : "",
 310                      dst_proc ? dst_proc->pid : 0,
 311                      dst_proc ? MC_smx_process_get_host_name(dst_proc) : "",
 312                      dst_proc ? MC_smx_process_get_name(dst_proc) : "");
 313     }
 314     xbt_free(p);
 315     break;
 316   }
 317
 318   case SIMCALL_COMM_TEST: {
 319     smx_synchro_t remote_act = simcall_comm_test__get__comm(req);
 320     s_smx_synchro_t synchro;
 321     MC_process_read_simple(&mc_model_checker->process, &synchro,
 322       remote_act, sizeof(synchro));
 323
 324     char* p;
 325     if (synchro.comm.src_proc == NULL || synchro.comm.dst_proc == NULL) {
 326       type = "Test FALSE";
 327       p = pointer_to_string(remote_act);
 328       args = bprintf("comm=%s", p);
 329     } else {
 330       type = "Test TRUE";
 331       p = pointer_to_string(remote_act);
 332
 333       smx_process_t src_proc = MC_smx_resolve_process(synchro.comm.src_proc);
 334       smx_process_t dst_proc = MC_smx_resolve_process(synchro.comm.dst_proc);
 335       args = bprintf("comm=%s [(%lu)%s (%s) -> (%lu)%s (%s)]", p,
 336                      src_proc->pid,
 337                      MC_smx_process_get_name(src_proc),
 338                      MC_smx_process_get_host_name(src_proc),
 339                      dst_proc->pid,
 340                      MC_smx_process_get_name(dst_proc),
 341                      MC_smx_process_get_host_name(dst_proc));
 342     }
 343     xbt_free(p);
 344     break;
 345   }
 346
 347   case SIMCALL_COMM_WAITANY: {
 348     type = "WaitAny";
 349     s_xbt_dynar_t comms;
 350     MC_process_read_simple(&mc_model_checker->process,
 351       &comms,  simcall_comm_waitany__get__comms(req), sizeof(comms));
 352     if (!xbt_dynar_is_empty(&comms)) {
 353       smx_synchro_t remote_sync;
 354       MC_process_read_dynar_element(&mc_model_checker->process,
 355         &remote_sync, simcall_comm_waitany__get__comms(req), value);
 356       char* p = pointer_to_string(remote_sync);
 357       args = bprintf("comm=%s (%d of %lu)",
 358         p, value + 1, xbt_dynar_length(&comms));
 359       xbt_free(p);
 360     } else {
 361       args = bprintf("comm at idx %d", value);
 362     }
 363     break;
 364   }
 365
 366   case SIMCALL_COMM_TESTANY:
 367     if (value == -1) {
 368       type = "TestAny FALSE";
 369       args = xbt_strdup("-");
 370     } else {
 371       type = "TestAny";
 372       args =
 373           bprintf("(%d of %lu)", value + 1,
 374                   MC_process_read_dynar_length(&mc_model_checker->process,
 375                     simcall_comm_testany__get__comms(req)));
 376     }
 377     break;
 378
 379   case SIMCALL_MUTEX_LOCK: {
 380     type = "Mutex LOCK";
 381
 382     s_smx_mutex_t mutex;
 383     MC_process_read_simple(&mc_model_checker->process, &mutex,
 384       simcall_mutex_lock__get__mutex(req), sizeof(mutex));
 385     s_xbt_swag_t mutex_sleeping;
 386     MC_process_read_simple(&mc_model_checker->process, &mutex_sleeping,
 387       mutex.sleeping, sizeof(mutex_sleeping));
 388
 389     args = bprintf("locked = %d, owner = %d, sleeping = %d",
 390       mutex.locked,
 391       mutex.owner != NULL ? (int) MC_smx_resolve_process(mutex.owner)->pid : -1,
 392       mutex_sleeping.count);
 393     break;
 394   }
 395
 396   case SIMCALL_MC_SNAPSHOT:
 397     type = "MC_SNAPSHOT";
 398     args = NULL;
 399     break;
 400
 401   case SIMCALL_MC_COMPARE_SNAPSHOTS:
 402     type = "MC_COMPARE_SNAPSHOTS";
 403     args = NULL;
 404     break;
 405
 406   case SIMCALL_MC_RANDOM:
 407     type = "MC_RANDOM";
 408     args = bprintf("%d", value);
 409     break;
 410
 411   default:
 412     THROW_UNIMPLEMENTED;
 413   }
 414
 415   char* str;
 416   if (args != NULL) {
 417     str =
 418         bprintf("[(%lu)%s (%s)] %s(%s)", issuer->pid,
 419                 MC_smx_process_get_host_name(issuer),
 420                 MC_smx_process_get_name(issuer),
 421                 type, args);
 422   } else {
 423     // FIXME, get process name
 424     str =
 425         bprintf("[(%lu)%s (%s)] %s ", issuer->pid,
 426                 MC_smx_process_get_host_name(issuer),
 427                 MC_smx_process_get_name(issuer),
 428                 type);
 429   }
 430   xbt_free(args);
 431   return str;
 432 }
 433
 434 unsigned int MC_request_testany_fail(smx_simcall_t req)
 435 {
 436   unsigned int cursor;
 437   smx_synchro_t action;
 438
 439   xbt_dynar_foreach(simcall_comm_testany__get__comms(req), cursor, action) {
 440     // FIXME, remote access to comm object
 441     if (action->comm.src_proc && action->comm.dst_proc)
 442       return FALSE;
 443   }
 444
 445   return TRUE;
 446 }
 447
 448 int MC_request_is_enabled_by_idx(smx_simcall_t req, unsigned int idx)
 449 {
 450   smx_synchro_t remote_act = NULL;
 451   switch (req->call) {
 452
 453   case SIMCALL_COMM_WAIT:
 454     /* FIXME: check also that src and dst processes are not suspended */
 455     remote_act = simcall_comm_wait__get__comm(req);
 456     break;
 457
 458   case SIMCALL_COMM_WAITANY: {
 459     smx_synchro_t act;
 460     MC_process_read_dynar_element(
 461       &mc_model_checker->process, &act, simcall_comm_waitany__get__comms(req),
 462       idx);
 463     }
 464     break;
 465
 466   case SIMCALL_COMM_TESTANY: {
 467     s_smx_synchro_t act;
 468     MC_process_read_dynar_element(
 469       &mc_model_checker->process, &act, simcall_comm_testany__get__comms(req),
 470       idx);
 471     }
 472     break;
 473
 474   default:
 475     return TRUE;
 476   }
 477
 478   s_smx_synchro_t synchro;
 479   MC_process_read_simple(&mc_model_checker->process,
 480     &synchro, remote_act, sizeof(synchro));
 481   return synchro.comm.src_proc && synchro.comm.dst_proc;
 482 }
 483
 484 int MC_process_is_enabled(smx_process_t process)
 485 {
 486   return MC_request_is_enabled(&process->simcall);
 487 }
 488
 489 char *MC_request_get_dot_output(smx_simcall_t req, int value)
 490 {
 491   char *label = NULL;
 492
 493   const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
 494
 495   switch (req->call) {
 496   case SIMCALL_COMM_ISEND:
 497     if (issuer->smx_host)
 498       label =
 499           bprintf("[(%lu)%s] iSend", issuer->pid,
 500                   MC_smx_process_get_host_name(issuer));
 501     else
 502       label = bprintf("[(%lu)] iSend", issuer->pid);
 503     break;
 504
 505   case SIMCALL_COMM_IRECV:
 506     if (issuer->smx_host)
 507       label =
 508           bprintf("[(%lu)%s] iRecv", issuer->pid,
 509                   MC_smx_process_get_host_name(issuer));
 510     else
 511       label = bprintf("[(%lu)] iRecv", issuer->pid);
 512     break;
 513
 514   case SIMCALL_COMM_WAIT: {
 515     if (value == -1) {
 516       if (issuer->smx_host)
 517         label =
 518             bprintf("[(%lu)%s] WaitTimeout", issuer->pid,
 519                     MC_smx_process_get_host_name(issuer));
 520       else
 521         label = bprintf("[(%lu)] WaitTimeout", issuer->pid);
 522     } else {
 523       smx_synchro_t remote_act = simcall_comm_wait__get__comm(req);
 524       s_smx_synchro_t synchro;
 525       MC_process_read_simple(&mc_model_checker->process, &synchro,
 526         remote_act, sizeof(synchro));
 527
 528       smx_process_t src_proc = MC_smx_resolve_process(synchro.comm.src_proc);
 529       smx_process_t dst_proc = MC_smx_resolve_process(synchro.comm.dst_proc);
 530       if (issuer->smx_host)
 531         label =
 532             bprintf("[(%lu)%s] Wait [(%lu)->(%lu)]", issuer->pid,
 533                     MC_smx_process_get_host_name(issuer),
 534                     src_proc ? src_proc->pid : 0,
 535                     dst_proc ? dst_proc->pid : 0);
 536       else
 537         label =
 538             bprintf("[(%lu)] Wait [(%lu)->(%lu)]", issuer->pid,
 539                     src_proc ? src_proc->pid : 0,
 540                     dst_proc ? dst_proc->pid : 0);
 541     }
 542     break;
 543   }
 544
 545   case SIMCALL_COMM_TEST: {
 546     smx_synchro_t remote_act = simcall_comm_test__get__comm(req);
 547     s_smx_synchro_t synchro;
 548     MC_process_read_simple(&mc_model_checker->process, &synchro,
 549       remote_act, sizeof(synchro));
 550     if (synchro.comm.src_proc == NULL || synchro.comm.dst_proc == NULL) {
 551       if (issuer->smx_host)
 552         label =
 553             bprintf("[(%lu)%s] Test FALSE", issuer->pid,
 554                     MC_smx_process_get_host_name(issuer));
 555       else
 556         label = bprintf("[(%lu)] Test FALSE", issuer->pid);
 557     } else {
 558       if (issuer->smx_host)
 559         label =
 560             bprintf("[(%lu)%s] Test TRUE", issuer->pid,
 561                     MC_smx_process_get_host_name(issuer));
 562       else
 563         label = bprintf("[(%lu)] Test TRUE", issuer->pid);
 564     }
 565     break;
 566   }
 567
 568   case SIMCALL_COMM_WAITANY: {
 569     unsigned long comms_size = MC_process_read_dynar_length(
 570       &mc_model_checker->process, simcall_comm_waitany__get__comms(req));
 571     if (issuer->smx_host)
 572       label =
 573           bprintf("[(%lu)%s] WaitAny [%d of %lu]", issuer->pid,
 574                   MC_smx_process_get_host_name(issuer), value + 1,
 575                   comms_size);
 576     else
 577       label =
 578           bprintf("[(%lu)] WaitAny [%d of %lu]", issuer->pid, value + 1,
 579                   comms_size);
 580     break;
 581   }
 582
 583   case SIMCALL_COMM_TESTANY:
 584     if (value == -1) {
 585       if (issuer->smx_host)
 586         label =
 587             bprintf("[(%lu)%s] TestAny FALSE", issuer->pid,
 588                     MC_smx_process_get_host_name(issuer));
 589       else
 590         label = bprintf("[(%lu)] TestAny FALSE", issuer->pid);
 591     } else {
 592       if (issuer->smx_host)
 593         label =
 594             bprintf("[(%lu)%s] TestAny TRUE [%d of %lu]", issuer->pid,
 595                     MC_smx_process_get_host_name(issuer), value + 1,
 596                     xbt_dynar_length(simcall_comm_testany__get__comms(req)));
 597       else
 598         label =
 599             bprintf("[(%lu)] TestAny TRUE [%d of %lu]", issuer->pid,
 600                     value + 1,
 601                     xbt_dynar_length(simcall_comm_testany__get__comms(req)));
 602     }
 603     break;
 604
 605   case SIMCALL_MUTEX_LOCK:
 606     label = bprintf("[(%lu)] Mutex LOCK", req->issuer->pid);
 607     break;
 608
 609   case SIMCALL_MC_RANDOM:
 610     if (issuer->smx_host)
 611       label =
 612           bprintf("[(%lu)%s] MC_RANDOM (%d)", issuer->pid,
 613                   MC_smx_process_get_host_name(issuer), value);
 614     else
 615       label = bprintf("[(%lu)] MC_RANDOM (%d)", issuer->pid, value);
 616     break;
 617
 618   case SIMCALL_MC_SNAPSHOT:
 619     if (issuer->smx_host)
 620       label =
 621           bprintf("[(%lu)%s] MC_SNAPSHOT", issuer->pid,
 622                   MC_smx_process_get_host_name(issuer));
 623     else
 624       label = bprintf("[(%lu)] MC_SNAPSHOT", issuer->pid);
 625     break;
 626
 627   case SIMCALL_MC_COMPARE_SNAPSHOTS:
 628     if (issuer->smx_host)
 629       label =
 630           bprintf("[(%lu)%s] MC_COMPARE_SNAPSHOTS", issuer->pid,
 631                   MC_smx_process_get_host_name(issuer));
 632     else
 633       label = bprintf("[(%lu)] MC_COMPARE_SNAPSHOTS", issuer->pid);
 634     break;
 635
 636   default:
 637     THROW_UNIMPLEMENTED;
 638   }
 639
 640   char* str =
 641       bprintf("label = \"%s\", color = %s, fontcolor = %s", label,
 642               colors[issuer->pid - 1], colors[issuer->pid - 1]);
 643   xbt_free(label);
 644   return str;
 645
 646 }