src/mc/mc_request.c

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