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, *str = NULL, *p = NULL, *bs = NULL;
 237   smx_synchro_t act = NULL;
 238   smx_mutex_t mutex = NULL;
 239   size_t size = 0;
 240
 241   smx_process_t issuer = MC_smx_simcall_get_issuer(req);
 242
 243   switch (req->call) {
 244   case SIMCALL_COMM_ISEND:
 245     type = "iSend";
 246     p = pointer_to_string(simcall_comm_isend__get__src_buff(req));
 247     bs = buff_size_to_string(simcall_comm_isend__get__src_buff_size(req));
 248     if (issuer->smx_host)
 249       args =
 250           bprintf("src=(%lu)%s (%s), buff=%s, size=%s", issuer->pid,
 251                   MC_smx_process_get_host_name(issuer),
 252                   MC_smx_process_get_name(issuer),
 253                   p, bs);
 254     else
 255       args =
 256           bprintf("src=(%lu)%s, buff=%s, size=%s", issuer->pid,
 257                   MC_smx_process_get_name(issuer), p, bs);
 258     break;
 259   case SIMCALL_COMM_IRECV:
 260     // TODO, REMOTE(*simcall_comm_irecv__get__dst_buff_size(req))
 261     size =
 262         simcall_comm_irecv__get__dst_buff_size(req) ?
 263         *simcall_comm_irecv__get__dst_buff_size(req) : 0;
 264     type = "iRecv";
 265     p = pointer_to_string(simcall_comm_irecv__get__dst_buff(req));
 266     bs = buff_size_to_string(size);
 267     if (issuer->smx_host)
 268       args =
 269           bprintf("dst=(%lu)%s (%s), buff=%s, size=%s", issuer->pid,
 270                   MC_smx_process_get_host_name(issuer),
 271                   MC_smx_process_get_name(issuer),
 272                   p, bs);
 273     else
 274       args =
 275           bprintf("dst=(%lu)%s, buff=%s, size=%s", issuer->pid,
 276                   MC_smx_process_get_name(issuer),
 277                   p, bs);
 278     break;
 279   case SIMCALL_COMM_WAIT:
 280     act = simcall_comm_wait__get__comm(req);
 281     if (value == -1) {
 282       type = "WaitTimeout";
 283       p = pointer_to_string(act);
 284       args = bprintf("comm=%s", p);
 285     } else {
 286       type = "Wait";
 287       p = pointer_to_string(act);
 288       // TODO, fix remote access to comm
 289       smx_process_t src_proc = MC_smx_resolve_process(act->comm.src_proc);
 290       smx_process_t dst_proc = MC_smx_resolve_process(act->comm.dst_proc);
 291       args = bprintf("comm=%s [(%lu)%s (%s)-> (%lu)%s (%s)]", p,
 292                      src_proc ? src_proc->pid : 0,
 293                      src_proc ? MC_smx_process_get_host_name(src_proc) : "",
 294                      src_proc ? MC_smx_process_get_name(src_proc) : "",
 295                      dst_proc ? dst_proc->pid : 0,
 296                      dst_proc ? MC_smx_process_get_host_name(dst_proc) : "",
 297                      dst_proc ? MC_smx_process_get_name(dst_proc) : "");
 298     }
 299     break;
 300   case SIMCALL_COMM_TEST:
 301     act = simcall_comm_test__get__comm(req);
 302     if (act->comm.src_proc == NULL || act->comm.dst_proc == NULL) {
 303       type = "Test FALSE";
 304       p = pointer_to_string(act);
 305       args = bprintf("comm=%s", p);
 306     } else {
 307       type = "Test TRUE";
 308       p = pointer_to_string(act);
 309       // TODO, get process, get process name
 310       smx_process_t src_proc = MC_smx_resolve_process(act->comm.src_proc);
 311       smx_process_t dst_proc = MC_smx_resolve_process(act->comm.dst_proc);
 312       args = bprintf("comm=%s [(%lu)%s (%s) -> (%lu)%s (%s)]", p,
 313                      src_proc->pid,
 314                      MC_smx_process_get_name(src_proc),
 315                      MC_smx_process_get_host_name(src_proc),
 316                      dst_proc->pid,
 317                      MC_smx_process_get_name(dst_proc),
 318                      MC_smx_process_get_host_name(dst_proc));
 319     }
 320     break;
 321
 322   case SIMCALL_COMM_WAITANY:
 323     type = "WaitAny";
 324     if (!xbt_dynar_is_empty(simcall_comm_waitany__get__comms(req))) {
 325       p = pointer_to_string(xbt_dynar_get_as
 326                             (simcall_comm_waitany__get__comms(req), value,
 327                              smx_synchro_t));
 328       args =
 329           bprintf("comm=%s (%d of %lu)", p, value + 1,
 330                   xbt_dynar_length(simcall_comm_waitany__get__comms(req)));
 331     } else {
 332       args = bprintf("comm at idx %d", value);
 333     }
 334     break;
 335
 336   case SIMCALL_COMM_TESTANY:
 337     if (value == -1) {
 338       type = "TestAny FALSE";
 339       args = xbt_strdup("-");
 340     } else {
 341       type = "TestAny";
 342       args =
 343           bprintf("(%d of %lu)", value + 1,
 344                   xbt_dynar_length(simcall_comm_testany__get__comms(req)));
 345     }
 346     break;
 347
 348   case SIMCALL_MUTEX_LOCK:
 349     mutex = simcall_mutex_lock__get__mutex(req);
 350     type = "Mutex LOCK";
 351     args = bprintf("locked = %d, owner = %d, sleeping = %d", mutex->locked, mutex->owner != NULL ? (int)mutex->owner->pid : -1, xbt_swag_size(mutex->sleeping));
 352     break;
 353
 354   case SIMCALL_MC_SNAPSHOT:
 355     type = "MC_SNAPSHOT";
 356     args = NULL;
 357     break;
 358
 359   case SIMCALL_MC_COMPARE_SNAPSHOTS:
 360     type = "MC_COMPARE_SNAPSHOTS";
 361     args = NULL;
 362     break;
 363
 364   case SIMCALL_MC_RANDOM:
 365     type = "MC_RANDOM";
 366     args = bprintf("%d", value);
 367     break;
 368
 369   default:
 370     THROW_UNIMPLEMENTED;
 371   }
 372
 373   if (args != NULL) {
 374     // FIXME, get process name
 375     str =
 376         bprintf("[(%lu)%s (%s)] %s(%s)", issuer->pid,
 377                 MC_smx_process_get_host_name(issuer),
 378                 MC_smx_process_get_name(issuer),
 379                 type, args);
 380   } else {
 381     // FIXME, get process name
 382     str =
 383         bprintf("[(%lu)%s (%s)] %s ", issuer->pid,
 384                 MC_smx_process_get_host_name(issuer),
 385                 MC_smx_process_get_name(issuer),
 386                 type);
 387   }
 388
 389   xbt_free(args);
 390   xbt_free(p);
 391   xbt_free(bs);
 392   return str;
 393 }
 394
 395 unsigned int MC_request_testany_fail(smx_simcall_t req)
 396 {
 397   unsigned int cursor;
 398   smx_synchro_t action;
 399
 400   xbt_dynar_foreach(simcall_comm_testany__get__comms(req), cursor, action) {
 401     // FIXME, remote access to comm object
 402     if (action->comm.src_proc && action->comm.dst_proc)
 403       return FALSE;
 404   }
 405
 406   return TRUE;
 407 }
 408
 409 int MC_request_is_enabled_by_idx(smx_simcall_t req, unsigned int idx)
 410 {
 411   smx_synchro_t act;
 412
 413   // FIXME, remote access to comm object
 414
 415   switch (req->call) {
 416
 417   case SIMCALL_COMM_WAIT:
 418     /* FIXME: check also that src and dst processes are not suspended */
 419     act = simcall_comm_wait__get__comm(req);
 420     return (act->comm.src_proc && act->comm.dst_proc);
 421     break;
 422
 423   case SIMCALL_COMM_WAITANY:
 424     act =
 425         xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), idx,
 426                          smx_synchro_t);
 427     return (act->comm.src_proc && act->comm.dst_proc);
 428     break;
 429
 430   case SIMCALL_COMM_TESTANY:
 431     act =
 432         xbt_dynar_get_as(simcall_comm_testany__get__comms(req), idx,
 433                          smx_synchro_t);
 434     return (act->comm.src_proc && act->comm.dst_proc);
 435     break;
 436
 437   default:
 438     return TRUE;
 439   }
 440 }
 441
 442 int MC_process_is_enabled(smx_process_t process)
 443 {
 444   return MC_request_is_enabled(&process->simcall);
 445 }
 446
 447 char *MC_request_get_dot_output(smx_simcall_t req, int value)
 448 {
 449   char *str = NULL, *label = NULL;
 450   smx_synchro_t act = NULL;
 451
 452   const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
 453
 454   switch (req->call) {
 455   case SIMCALL_COMM_ISEND:
 456     if (issuer->smx_host)
 457       label =
 458           bprintf("[(%lu)%s] iSend", issuer->pid,
 459                   MC_smx_process_get_host_name(issuer));
 460     else
 461       label = bprintf("[(%lu)] iSend", issuer->pid);
 462     break;
 463
 464   case SIMCALL_COMM_IRECV:
 465     if (issuer->smx_host)
 466       label =
 467           bprintf("[(%lu)%s] iRecv", issuer->pid,
 468                   MC_smx_process_get_host_name(issuer));
 469     else
 470       label = bprintf("[(%lu)] iRecv", issuer->pid);
 471     break;
 472
 473   case SIMCALL_COMM_WAIT:
 474     act = simcall_comm_wait__get__comm(req);
 475     if (value == -1) {
 476       if (issuer->smx_host)
 477         label =
 478             bprintf("[(%lu)%s] WaitTimeout", issuer->pid,
 479                     MC_smx_process_get_host_name(issuer));
 480       else
 481         label = bprintf("[(%lu)] WaitTimeout", issuer->pid);
 482     } else {
 483       // FIXME, remote access to act->comm
 484       smx_process_t src_proc = MC_smx_resolve_process(act->comm.src_proc);
 485       smx_process_t dst_proc = MC_smx_resolve_process(act->comm.dst_proc);
 486       if (issuer->smx_host)
 487         label =
 488             bprintf("[(%lu)%s] Wait [(%lu)->(%lu)]", issuer->pid,
 489                     MC_smx_process_get_host_name(issuer),
 490                     src_proc ? src_proc->pid : 0,
 491                     dst_proc ? dst_proc->pid : 0);
 492       else
 493         label =
 494             bprintf("[(%lu)] Wait [(%lu)->(%lu)]", issuer->pid,
 495                     src_proc ? src_proc->pid : 0,
 496                     dst_proc ? dst_proc->pid : 0);
 497     }
 498     break;
 499
 500   case SIMCALL_COMM_TEST:
 501     act = simcall_comm_test__get__comm(req);
 502     if (act->comm.src_proc == NULL || act->comm.dst_proc == NULL) {
 503       if (issuer->smx_host)
 504         label =
 505             bprintf("[(%lu)%s] Test FALSE", issuer->pid,
 506                     MC_smx_process_get_host_name(issuer));
 507       else
 508         label = bprintf("[(%lu)] Test FALSE", issuer->pid);
 509     } else {
 510       if (issuer->smx_host)
 511         label =
 512             bprintf("[(%lu)%s] Test TRUE", issuer->pid,
 513                     MC_smx_process_get_host_name(issuer));
 514       else
 515         label = bprintf("[(%lu)] Test TRUE", issuer->pid);
 516     }
 517     break;
 518
 519   case SIMCALL_COMM_WAITANY:
 520     if (issuer->smx_host)
 521       label =
 522           bprintf("[(%lu)%s] WaitAny [%d of %lu]", issuer->pid,
 523                   MC_smx_process_get_host_name(issuer), value + 1,
 524                   xbt_dynar_length(simcall_comm_waitany__get__comms(req)));
 525     else
 526       label =
 527           bprintf("[(%lu)] WaitAny [%d of %lu]", issuer->pid, value + 1,
 528                   xbt_dynar_length(simcall_comm_waitany__get__comms(req)));
 529     break;
 530
 531   case SIMCALL_COMM_TESTANY:
 532     if (value == -1) {
 533       if (issuer->smx_host)
 534         label =
 535             bprintf("[(%lu)%s] TestAny FALSE", issuer->pid,
 536                     MC_smx_process_get_host_name(issuer));
 537       else
 538         label = bprintf("[(%lu)] TestAny FALSE", issuer->pid);
 539     } else {
 540       if (issuer->smx_host)
 541         label =
 542             bprintf("[(%lu)%s] TestAny TRUE [%d of %lu]", issuer->pid,
 543                     MC_smx_process_get_host_name(issuer), value + 1,
 544                     xbt_dynar_length(simcall_comm_testany__get__comms(req)));
 545       else
 546         label =
 547             bprintf("[(%lu)] TestAny TRUE [%d of %lu]", issuer->pid,
 548                     value + 1,
 549                     xbt_dynar_length(simcall_comm_testany__get__comms(req)));
 550     }
 551     break;
 552
 553   case SIMCALL_MUTEX_LOCK:
 554     label = bprintf("[(%lu)] Mutex LOCK", req->issuer->pid);
 555     break;
 556
 557   case SIMCALL_MC_RANDOM:
 558     if (issuer->smx_host)
 559       label =
 560           bprintf("[(%lu)%s] MC_RANDOM (%d)", issuer->pid,
 561                   MC_smx_process_get_host_name(issuer), value);
 562     else
 563       label = bprintf("[(%lu)] MC_RANDOM (%d)", issuer->pid, value);
 564     break;
 565
 566   case SIMCALL_MC_SNAPSHOT:
 567     if (issuer->smx_host)
 568       label =
 569           bprintf("[(%lu)%s] MC_SNAPSHOT", issuer->pid,
 570                   MC_smx_process_get_host_name(issuer));
 571     else
 572       label = bprintf("[(%lu)] MC_SNAPSHOT", issuer->pid);
 573     break;
 574
 575   case SIMCALL_MC_COMPARE_SNAPSHOTS:
 576     if (issuer->smx_host)
 577       label =
 578           bprintf("[(%lu)%s] MC_COMPARE_SNAPSHOTS", issuer->pid,
 579                   MC_smx_process_get_host_name(issuer));
 580     else
 581       label = bprintf("[(%lu)] MC_COMPARE_SNAPSHOTS", issuer->pid);
 582     break;
 583
 584   default:
 585     THROW_UNIMPLEMENTED;
 586   }
 587
 588   str =
 589       bprintf("label = \"%s\", color = %s, fontcolor = %s", label,
 590               colors[issuer->pid - 1], colors[issuer->pid - 1]);
 591   xbt_free(label);
 592   return str;
 593
 594 }