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