src/mc/mc_request.cpp

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