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