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       char* p = pointer_to_string(remote_sync);
 357       args = bprintf("comm=%s (%d of %lu)",
 358         p, value + 1, xbt_dynar_length(&comms));
 359       xbt_free(p);
 360     } else {
 361       args = bprintf("comm at idx %d", value);
 362     }
 363     break;
 364   }
 365
 366   case SIMCALL_COMM_TESTANY:
 367     if (value == -1) {
 368       type = "TestAny FALSE";
 369       args = xbt_strdup("-");
 370     } else {
 371       type = "TestAny";
 372       args =
 373           bprintf("(%d of %lu)", value + 1,
 374                   MC_process_read_dynar_length(&mc_model_checker->process,
 375                     simcall_comm_testany__get__comms(req)));
 376     }
 377     break;
 378
 379   case SIMCALL_MUTEX_LOCK: {
 380     type = "Mutex LOCK";
 381
 382     s_smx_mutex_t mutex;
 383     MC_process_read_simple(&mc_model_checker->process, &mutex,
 384       simcall_mutex_lock__get__mutex(req), sizeof(mutex));
 385     s_xbt_swag_t mutex_sleeping;
 386     MC_process_read_simple(&mc_model_checker->process, &mutex_sleeping,
 387       mutex.sleeping, sizeof(mutex_sleeping));
 388
 389     args = bprintf("locked = %d, owner = %d, sleeping = %d",
 390       mutex.locked,
 391       mutex.owner != NULL ? (int) MC_smx_resolve_process(mutex.owner)->pid : -1,
 392       mutex_sleeping.count);
 393     break;
 394   }
 395
 396   case SIMCALL_MC_SNAPSHOT:
 397     type = "MC_SNAPSHOT";
 398     args = NULL;
 399     break;
 400
 401   case SIMCALL_MC_COMPARE_SNAPSHOTS:
 402     type = "MC_COMPARE_SNAPSHOTS";
 403     args = NULL;
 404     break;
 405
 406   case SIMCALL_MC_RANDOM:
 407     type = "MC_RANDOM";
 408     args = bprintf("%d", value);
 409     break;
 410
 411   default:
 412     THROW_UNIMPLEMENTED;
 413   }
 414
 415   char* str;
 416   if (args != NULL) {
 417     str =
 418         bprintf("[(%lu)%s (%s)] %s(%s)", issuer->pid,
 419                 MC_smx_process_get_host_name(issuer),
 420                 MC_smx_process_get_name(issuer),
 421                 type, args);
 422   } else {
 423     str =
 424         bprintf("[(%lu)%s (%s)] %s ", issuer->pid,
 425                 MC_smx_process_get_host_name(issuer),
 426                 MC_smx_process_get_name(issuer),
 427                 type);
 428   }
 429   xbt_free(args);
 430   return str;
 431 }
 432
 433 unsigned int MC_request_testany_fail(smx_simcall_t req)
 434 {
 435   // Remote xbt_dynar_foreach on simcall_comm_testany__get__comms(req).
 436
 437   // Read the dynar:
 438   s_xbt_dynar_t comms;
 439   MC_process_read_simple(&mc_model_checker->process,
 440     &comms, simcall_comm_testany__get__comms(req), sizeof(comms));
 441
 442   // Read ther dynar buffer:
 443   size_t buffer_size = comms.elmsize * comms.used;
 444   char buffer[buffer_size];
 445   MC_process_read_simple(&mc_model_checker->process,
 446     buffer, comms.data, buffer_size);
 447
 448   // Iterate over the elements:
 449   assert(comms.elmsize == sizeof(smx_synchro_t));
 450   unsigned cursor;
 451   for (cursor=0; cursor != comms.used; ++cursor) {
 452
 453     // Get the element:
 454     smx_synchro_t remote_action;
 455     memcpy(buffer + comms.elmsize * cursor, &remote_action, sizeof(remote_action));
 456
 457     // Dereference the pointer:
 458     s_smx_synchro_t action;
 459     MC_process_read_simple(&mc_model_checker->process,
 460       &action, remote_action, sizeof(action));
 461
 462     // Finally so something useful about it:
 463     if (action.comm.src_proc && action.comm.dst_proc)
 464       return FALSE;
 465   }
 466
 467   return TRUE;
 468 }
 469
 470 int MC_request_is_enabled_by_idx(smx_simcall_t req, unsigned int idx)
 471 {
 472   smx_synchro_t remote_act = NULL;
 473   switch (req->call) {
 474
 475   case SIMCALL_COMM_WAIT:
 476     /* FIXME: check also that src and dst processes are not suspended */
 477     remote_act = simcall_comm_wait__get__comm(req);
 478     break;
 479
 480   case SIMCALL_COMM_WAITANY: {
 481     smx_synchro_t act;
 482     MC_process_read_dynar_element(
 483       &mc_model_checker->process, &act, simcall_comm_waitany__get__comms(req),
 484       idx);
 485     }
 486     break;
 487
 488   case SIMCALL_COMM_TESTANY: {
 489     s_smx_synchro_t act;
 490     MC_process_read_dynar_element(
 491       &mc_model_checker->process, &act, simcall_comm_testany__get__comms(req),
 492       idx);
 493     }
 494     break;
 495
 496   default:
 497     return TRUE;
 498   }
 499
 500   s_smx_synchro_t synchro;
 501   MC_process_read_simple(&mc_model_checker->process,
 502     &synchro, remote_act, sizeof(synchro));
 503   return synchro.comm.src_proc && synchro.comm.dst_proc;
 504 }
 505
 506 int MC_process_is_enabled(smx_process_t process)
 507 {
 508   return MC_request_is_enabled(&process->simcall);
 509 }
 510
 511 char *MC_request_get_dot_output(smx_simcall_t req, int value)
 512 {
 513   char *label = NULL;
 514
 515   const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
 516
 517   switch (req->call) {
 518   case SIMCALL_COMM_ISEND:
 519     if (issuer->smx_host)
 520       label =
 521           bprintf("[(%lu)%s] iSend", issuer->pid,
 522                   MC_smx_process_get_host_name(issuer));
 523     else
 524       label = bprintf("[(%lu)] iSend", issuer->pid);
 525     break;
 526
 527   case SIMCALL_COMM_IRECV:
 528     if (issuer->smx_host)
 529       label =
 530           bprintf("[(%lu)%s] iRecv", issuer->pid,
 531                   MC_smx_process_get_host_name(issuer));
 532     else
 533       label = bprintf("[(%lu)] iRecv", issuer->pid);
 534     break;
 535
 536   case SIMCALL_COMM_WAIT: {
 537     if (value == -1) {
 538       if (issuer->smx_host)
 539         label =
 540             bprintf("[(%lu)%s] WaitTimeout", issuer->pid,
 541                     MC_smx_process_get_host_name(issuer));
 542       else
 543         label = bprintf("[(%lu)] WaitTimeout", issuer->pid);
 544     } else {
 545       smx_synchro_t remote_act = simcall_comm_wait__get__comm(req);
 546       s_smx_synchro_t synchro;
 547       MC_process_read_simple(&mc_model_checker->process, &synchro,
 548         remote_act, sizeof(synchro));
 549
 550       smx_process_t src_proc = MC_smx_resolve_process(synchro.comm.src_proc);
 551       smx_process_t dst_proc = MC_smx_resolve_process(synchro.comm.dst_proc);
 552       if (issuer->smx_host)
 553         label =
 554             bprintf("[(%lu)%s] Wait [(%lu)->(%lu)]", issuer->pid,
 555                     MC_smx_process_get_host_name(issuer),
 556                     src_proc ? src_proc->pid : 0,
 557                     dst_proc ? dst_proc->pid : 0);
 558       else
 559         label =
 560             bprintf("[(%lu)] Wait [(%lu)->(%lu)]", issuer->pid,
 561                     src_proc ? src_proc->pid : 0,
 562                     dst_proc ? dst_proc->pid : 0);
 563     }
 564     break;
 565   }
 566
 567   case SIMCALL_COMM_TEST: {
 568     smx_synchro_t remote_act = simcall_comm_test__get__comm(req);
 569     s_smx_synchro_t synchro;
 570     MC_process_read_simple(&mc_model_checker->process, &synchro,
 571       remote_act, sizeof(synchro));
 572     if (synchro.comm.src_proc == NULL || synchro.comm.dst_proc == NULL) {
 573       if (issuer->smx_host)
 574         label =
 575             bprintf("[(%lu)%s] Test FALSE", issuer->pid,
 576                     MC_smx_process_get_host_name(issuer));
 577       else
 578         label = bprintf("[(%lu)] Test FALSE", issuer->pid);
 579     } else {
 580       if (issuer->smx_host)
 581         label =
 582             bprintf("[(%lu)%s] Test TRUE", issuer->pid,
 583                     MC_smx_process_get_host_name(issuer));
 584       else
 585         label = bprintf("[(%lu)] Test TRUE", issuer->pid);
 586     }
 587     break;
 588   }
 589
 590   case SIMCALL_COMM_WAITANY: {
 591     unsigned long comms_size = MC_process_read_dynar_length(
 592       &mc_model_checker->process, simcall_comm_waitany__get__comms(req));
 593     if (issuer->smx_host)
 594       label =
 595           bprintf("[(%lu)%s] WaitAny [%d of %lu]", issuer->pid,
 596                   MC_smx_process_get_host_name(issuer), value + 1,
 597                   comms_size);
 598     else
 599       label =
 600           bprintf("[(%lu)] WaitAny [%d of %lu]", issuer->pid, value + 1,
 601                   comms_size);
 602     break;
 603   }
 604
 605   case SIMCALL_COMM_TESTANY:
 606     if (value == -1) {
 607       if (issuer->smx_host)
 608         label =
 609             bprintf("[(%lu)%s] TestAny FALSE", issuer->pid,
 610                     MC_smx_process_get_host_name(issuer));
 611       else
 612         label = bprintf("[(%lu)] TestAny FALSE", issuer->pid);
 613     } else {
 614       if (issuer->smx_host)
 615         label =
 616             bprintf("[(%lu)%s] TestAny TRUE [%d of %lu]", issuer->pid,
 617                     MC_smx_process_get_host_name(issuer), value + 1,
 618                     xbt_dynar_length(simcall_comm_testany__get__comms(req)));
 619       else
 620         label =
 621             bprintf("[(%lu)] TestAny TRUE [%d of %lu]", issuer->pid,
 622                     value + 1,
 623                     xbt_dynar_length(simcall_comm_testany__get__comms(req)));
 624     }
 625     break;
 626
 627   case SIMCALL_MUTEX_LOCK:
 628     label = bprintf("[(%lu)] Mutex LOCK", req->issuer->pid);
 629     break;
 630
 631   case SIMCALL_MC_RANDOM:
 632     if (issuer->smx_host)
 633       label =
 634           bprintf("[(%lu)%s] MC_RANDOM (%d)", issuer->pid,
 635                   MC_smx_process_get_host_name(issuer), value);
 636     else
 637       label = bprintf("[(%lu)] MC_RANDOM (%d)", issuer->pid, value);
 638     break;
 639
 640   case SIMCALL_MC_SNAPSHOT:
 641     if (issuer->smx_host)
 642       label =
 643           bprintf("[(%lu)%s] MC_SNAPSHOT", issuer->pid,
 644                   MC_smx_process_get_host_name(issuer));
 645     else
 646       label = bprintf("[(%lu)] MC_SNAPSHOT", issuer->pid);
 647     break;
 648
 649   case SIMCALL_MC_COMPARE_SNAPSHOTS:
 650     if (issuer->smx_host)
 651       label =
 652           bprintf("[(%lu)%s] MC_COMPARE_SNAPSHOTS", issuer->pid,
 653                   MC_smx_process_get_host_name(issuer));
 654     else
 655       label = bprintf("[(%lu)] MC_COMPARE_SNAPSHOTS", issuer->pid);
 656     break;
 657
 658   default:
 659     THROW_UNIMPLEMENTED;
 660   }
 661
 662   char* str =
 663       bprintf("label = \"%s\", color = %s, fontcolor = %s", label,
 664               colors[issuer->pid - 1], colors[issuer->pid - 1]);
 665   xbt_free(label);
 666   return str;
 667
 668 }