src/mc/mc_request.cpp

   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 extern "C" {
  15
  16 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_request, mc,
  17                                 "Logging specific to MC (request)");
  18
  19 static char *pointer_to_string(void *pointer);
  20 static char *buff_size_to_string(size_t size);
  21
  22 // Those are MC_state_get_internal_request(state)
  23 int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2)
  24 {
  25   if (mc_reduce_kind == e_mc_reduce_none)
  26     return TRUE;
  27
  28   if (r1->issuer == r2->issuer)
  29     return FALSE;
  30
  31   /* Wait with timeout transitions are not considered by the independance theorem, thus we consider them as dependant with all other transitions */
  32   if ((r1->call == SIMCALL_COMM_WAIT && simcall_comm_wait__get__timeout(r1) > 0)
  33       || (r2->call == SIMCALL_COMM_WAIT
  34           && simcall_comm_wait__get__timeout(r2) > 0))
  35     return TRUE;
  36
  37   if (r1->call == SIMCALL_COMM_ISEND && r2->call == SIMCALL_COMM_IRECV)
  38     return FALSE;
  39
  40   if (r1->call == SIMCALL_COMM_IRECV && r2->call == SIMCALL_COMM_ISEND)
  41     return FALSE;
  42
  43   // Those are internal requests, we do not need indirection
  44   // because those objects are copies:
  45   smx_synchro_t synchro1 = NULL, synchro2 = NULL;
  46   if (r1->call == SIMCALL_COMM_WAIT) {
  47     synchro1 = simcall_comm_wait__get__comm(r1);
  48   }
  49   if (r2->call == SIMCALL_COMM_WAIT) {
  50     synchro2 = simcall_comm_wait__get__comm(r2);
  51   }
  52   if (r1->call == SIMCALL_COMM_TEST) {
  53     synchro1 = simcall_comm_test__get__comm(r1);
  54   }
  55   if (r2->call == SIMCALL_COMM_TEST) {
  56     synchro2 = simcall_comm_test__get__comm(r2);
  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, e_mc_request_type_t request_type)
 234 {
 235   bool use_remote_comm = true;
 236   switch(request_type) {
 237   case MC_REQUEST_SIMIX:
 238     use_remote_comm = true;
 239     break;
 240   case MC_REQUEST_EXECUTED:
 241   case MC_REQUEST_INTERNAL:
 242     use_remote_comm = false;
 243     break;
 244   }
 245
 246   const char* type = NULL;
 247   char *args = NULL;
 248
 249   smx_process_t issuer = MC_smx_simcall_get_issuer(req);
 250
 251   switch (req->call) {
 252
 253   case SIMCALL_COMM_ISEND: {
 254     type = "iSend";
 255     char* p = pointer_to_string(simcall_comm_isend__get__src_buff(req));
 256     char* bs = buff_size_to_string(simcall_comm_isend__get__src_buff_size(req));
 257     if (issuer->smx_host)
 258       args =
 259           bprintf("src=(%lu)%s (%s), buff=%s, size=%s", issuer->pid,
 260                   MC_smx_process_get_host_name(issuer),
 261                   MC_smx_process_get_name(issuer),
 262                   p, bs);
 263     else
 264       args =
 265           bprintf("src=(%lu)%s, buff=%s, size=%s", issuer->pid,
 266                   MC_smx_process_get_name(issuer), p, bs);
 267     xbt_free(bs);
 268     xbt_free(p);
 269     break;
 270   }
 271
 272   case SIMCALL_COMM_IRECV: {
 273     size_t* remote_size = simcall_comm_irecv__get__dst_buff_size(req);
 274
 275     // size_t size = size_pointer ? *size_pointer : 0;
 276     size_t size = 0;
 277     if (remote_size)
 278       MC_process_read_simple(&mc_model_checker->process(), &size,
 279         remote_size, sizeof(size));
 280
 281     type = "iRecv";
 282     char* p = pointer_to_string(simcall_comm_irecv__get__dst_buff(req));
 283     char* bs = buff_size_to_string(size);
 284     if (issuer->smx_host)
 285       args =
 286           bprintf("dst=(%lu)%s (%s), buff=%s, size=%s", issuer->pid,
 287                   MC_smx_process_get_host_name(issuer),
 288                   MC_smx_process_get_name(issuer),
 289                   p, bs);
 290     else
 291       args =
 292           bprintf("dst=(%lu)%s, buff=%s, size=%s", issuer->pid,
 293                   MC_smx_process_get_name(issuer),
 294                   p, bs);
 295     xbt_free(bs);
 296     xbt_free(p);
 297     break;
 298   }
 299
 300   case SIMCALL_COMM_WAIT: {
 301     smx_synchro_t remote_act = simcall_comm_wait__get__comm(req);
 302     char* p;
 303     if (value == -1) {
 304       type = "WaitTimeout";
 305       p = pointer_to_string(remote_act);
 306       args = bprintf("comm=%s", p);
 307     } else {
 308       type = "Wait";
 309       p = pointer_to_string(remote_act);
 310
 311       s_smx_synchro_t synchro;
 312       smx_synchro_t act;
 313       if (use_remote_comm) {
 314         MC_process_read_simple(&mc_model_checker->process(), &synchro,
 315           remote_act, sizeof(synchro));
 316         act = &synchro;
 317       } else
 318         act = remote_act;
 319
 320       smx_process_t src_proc = MC_smx_resolve_process(act->comm.src_proc);
 321       smx_process_t dst_proc = MC_smx_resolve_process(act->comm.dst_proc);
 322       args = bprintf("comm=%s [(%lu)%s (%s)-> (%lu)%s (%s)]", p,
 323                      src_proc ? src_proc->pid : 0,
 324                      src_proc ? MC_smx_process_get_host_name(src_proc) : "",
 325                      src_proc ? MC_smx_process_get_name(src_proc) : "",
 326                      dst_proc ? dst_proc->pid : 0,
 327                      dst_proc ? MC_smx_process_get_host_name(dst_proc) : "",
 328                      dst_proc ? MC_smx_process_get_name(dst_proc) : "");
 329     }
 330     xbt_free(p);
 331     break;
 332   }
 333
 334   case SIMCALL_COMM_TEST: {
 335     smx_synchro_t remote_act = simcall_comm_test__get__comm(req);
 336     s_smx_synchro_t synchro;
 337       smx_synchro_t act;
 338       if (use_remote_comm) {
 339         MC_process_read_simple(&mc_model_checker->process(), &synchro,
 340           remote_act, sizeof(synchro));
 341         act = &synchro;
 342       } else
 343         act = remote_act;
 344
 345     char* p;
 346     if (act->comm.src_proc == NULL || act->comm.dst_proc == NULL) {
 347       type = "Test FALSE";
 348       p = pointer_to_string(remote_act);
 349       args = bprintf("comm=%s", p);
 350     } else {
 351       type = "Test TRUE";
 352       p = pointer_to_string(remote_act);
 353
 354       smx_process_t src_proc = MC_smx_resolve_process(act->comm.src_proc);
 355       smx_process_t dst_proc = MC_smx_resolve_process(act->comm.dst_proc);
 356       args = bprintf("comm=%s [(%lu)%s (%s) -> (%lu)%s (%s)]", p,
 357                      src_proc->pid,
 358                      MC_smx_process_get_name(src_proc),
 359                      MC_smx_process_get_host_name(src_proc),
 360                      dst_proc->pid,
 361                      MC_smx_process_get_name(dst_proc),
 362                      MC_smx_process_get_host_name(dst_proc));
 363     }
 364     xbt_free(p);
 365     break;
 366   }
 367
 368   case SIMCALL_COMM_WAITANY: {
 369     type = "WaitAny";
 370     s_xbt_dynar_t comms;
 371     MC_process_read_simple(&mc_model_checker->process(),
 372       &comms,  simcall_comm_waitany__get__comms(req), sizeof(comms));
 373     if (!xbt_dynar_is_empty(&comms)) {
 374       smx_synchro_t remote_sync;
 375       MC_process_read_dynar_element(&mc_model_checker->process(),
 376         &remote_sync, simcall_comm_waitany__get__comms(req), value,
 377         sizeof(remote_sync));
 378       char* p = pointer_to_string(remote_sync);
 379       args = bprintf("comm=%s (%d of %lu)",
 380         p, value + 1, xbt_dynar_length(&comms));
 381       xbt_free(p);
 382     } else {
 383       args = bprintf("comm at idx %d", value);
 384     }
 385     break;
 386   }
 387
 388   case SIMCALL_COMM_TESTANY:
 389     if (value == -1) {
 390       type = "TestAny FALSE";
 391       args = xbt_strdup("-");
 392     } else {
 393       type = "TestAny";
 394       args =
 395           bprintf("(%d of %lu)", value + 1,
 396                   MC_process_read_dynar_length(&mc_model_checker->process(),
 397                     simcall_comm_testany__get__comms(req)));
 398     }
 399     break;
 400
 401   case SIMCALL_MUTEX_LOCK: {
 402     type = "Mutex LOCK";
 403
 404     s_smx_mutex_t mutex;
 405     MC_process_read_simple(&mc_model_checker->process(), &mutex,
 406       simcall_mutex_lock__get__mutex(req), sizeof(mutex));
 407     s_xbt_swag_t mutex_sleeping;
 408     MC_process_read_simple(&mc_model_checker->process(), &mutex_sleeping,
 409       mutex.sleeping, sizeof(mutex_sleeping));
 410
 411     args = bprintf("locked = %d, owner = %d, sleeping = %d",
 412       mutex.locked,
 413       mutex.owner != NULL ? (int) MC_smx_resolve_process(mutex.owner)->pid : -1,
 414       mutex_sleeping.count);
 415     break;
 416   }
 417
 418   case SIMCALL_MC_SNAPSHOT:
 419     type = "MC_SNAPSHOT";
 420     args = NULL;
 421     break;
 422
 423   case SIMCALL_MC_COMPARE_SNAPSHOTS:
 424     type = "MC_COMPARE_SNAPSHOTS";
 425     args = NULL;
 426     break;
 427
 428   case SIMCALL_MC_RANDOM:
 429     type = "MC_RANDOM";
 430     args = bprintf("%d", value);
 431     break;
 432
 433   default:
 434     THROW_UNIMPLEMENTED;
 435   }
 436
 437   char* str;
 438   if (args != NULL) {
 439     str =
 440         bprintf("[(%lu)%s (%s)] %s(%s)", issuer->pid,
 441                 MC_smx_process_get_host_name(issuer),
 442                 MC_smx_process_get_name(issuer),
 443                 type, args);
 444   } else {
 445     str =
 446         bprintf("[(%lu)%s (%s)] %s ", issuer->pid,
 447                 MC_smx_process_get_host_name(issuer),
 448                 MC_smx_process_get_name(issuer),
 449                 type);
 450   }
 451   xbt_free(args);
 452   return str;
 453 }
 454
 455 unsigned int MC_request_testany_fail(smx_simcall_t req)
 456 {
 457   // Remote xbt_dynar_foreach on simcall_comm_testany__get__comms(req).
 458
 459   // Read the dynar:
 460   s_xbt_dynar_t comms;
 461   MC_process_read_simple(&mc_model_checker->process(),
 462     &comms, simcall_comm_testany__get__comms(req), sizeof(comms));
 463
 464   // Read ther dynar buffer:
 465   size_t buffer_size = comms.elmsize * comms.used;
 466   char buffer[buffer_size];
 467   MC_process_read_simple(&mc_model_checker->process(),
 468     buffer, comms.data, buffer_size);
 469
 470   // Iterate over the elements:
 471   assert(comms.elmsize == sizeof(smx_synchro_t));
 472   unsigned cursor;
 473   for (cursor=0; cursor != comms.used; ++cursor) {
 474
 475     // Get the element:
 476     smx_synchro_t remote_action = NULL;
 477     memcpy(&remote_action, buffer + comms.elmsize * cursor, sizeof(remote_action));
 478
 479     // Dereference the pointer:
 480     s_smx_synchro_t action;
 481     MC_process_read_simple(&mc_model_checker->process(),
 482       &action, remote_action, sizeof(action));
 483
 484     // Finally so something useful about it:
 485     if (action.comm.src_proc && action.comm.dst_proc)
 486       return FALSE;
 487   }
 488
 489   return TRUE;
 490 }
 491
 492 int MC_request_is_enabled_by_idx(smx_simcall_t req, unsigned int idx)
 493 {
 494   smx_synchro_t remote_act = NULL;
 495   switch (req->call) {
 496
 497   case SIMCALL_COMM_WAIT:
 498     /* FIXME: check also that src and dst processes are not suspended */
 499     remote_act = simcall_comm_wait__get__comm(req);
 500     break;
 501
 502   case SIMCALL_COMM_WAITANY: {
 503     MC_process_read_dynar_element(
 504       &mc_model_checker->process(), &remote_act, simcall_comm_waitany__get__comms(req),
 505       idx, sizeof(remote_act));
 506     }
 507     break;
 508
 509   case SIMCALL_COMM_TESTANY: {
 510     MC_process_read_dynar_element(
 511       &mc_model_checker->process(), &remote_act, simcall_comm_testany__get__comms(req),
 512       idx, sizeof(remote_act));
 513     }
 514     break;
 515
 516   default:
 517     return TRUE;
 518   }
 519
 520   s_smx_synchro_t synchro;
 521   MC_process_read_simple(&mc_model_checker->process(),
 522     &synchro, remote_act, sizeof(synchro));
 523   return synchro.comm.src_proc && synchro.comm.dst_proc;
 524 }
 525
 526 int MC_process_is_enabled(smx_process_t process)
 527 {
 528   return MC_request_is_enabled(&process->simcall);
 529 }
 530
 531 char *MC_request_get_dot_output(smx_simcall_t req, int value)
 532 {
 533   char *label = NULL;
 534
 535   const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
 536
 537   switch (req->call) {
 538   case SIMCALL_COMM_ISEND:
 539     if (issuer->smx_host)
 540       label =
 541           bprintf("[(%lu)%s] iSend", issuer->pid,
 542                   MC_smx_process_get_host_name(issuer));
 543     else
 544       label = bprintf("[(%lu)] iSend", issuer->pid);
 545     break;
 546
 547   case SIMCALL_COMM_IRECV:
 548     if (issuer->smx_host)
 549       label =
 550           bprintf("[(%lu)%s] iRecv", issuer->pid,
 551                   MC_smx_process_get_host_name(issuer));
 552     else
 553       label = bprintf("[(%lu)] iRecv", issuer->pid);
 554     break;
 555
 556   case SIMCALL_COMM_WAIT: {
 557     if (value == -1) {
 558       if (issuer->smx_host)
 559         label =
 560             bprintf("[(%lu)%s] WaitTimeout", issuer->pid,
 561                     MC_smx_process_get_host_name(issuer));
 562       else
 563         label = bprintf("[(%lu)] WaitTimeout", issuer->pid);
 564     } else {
 565       smx_synchro_t remote_act = simcall_comm_wait__get__comm(req);
 566       s_smx_synchro_t synchro;
 567       MC_process_read_simple(&mc_model_checker->process(), &synchro,
 568         remote_act, sizeof(synchro));
 569
 570       smx_process_t src_proc = MC_smx_resolve_process(synchro.comm.src_proc);
 571       smx_process_t dst_proc = MC_smx_resolve_process(synchro.comm.dst_proc);
 572       if (issuer->smx_host)
 573         label =
 574             bprintf("[(%lu)%s] Wait [(%lu)->(%lu)]", issuer->pid,
 575                     MC_smx_process_get_host_name(issuer),
 576                     src_proc ? src_proc->pid : 0,
 577                     dst_proc ? dst_proc->pid : 0);
 578       else
 579         label =
 580             bprintf("[(%lu)] Wait [(%lu)->(%lu)]", issuer->pid,
 581                     src_proc ? src_proc->pid : 0,
 582                     dst_proc ? dst_proc->pid : 0);
 583     }
 584     break;
 585   }
 586
 587   case SIMCALL_COMM_TEST: {
 588     smx_synchro_t remote_act = simcall_comm_test__get__comm(req);
 589     s_smx_synchro_t synchro;
 590     MC_process_read_simple(&mc_model_checker->process(), &synchro,
 591       remote_act, sizeof(synchro));
 592     if (synchro.comm.src_proc == NULL || synchro.comm.dst_proc == NULL) {
 593       if (issuer->smx_host)
 594         label =
 595             bprintf("[(%lu)%s] Test FALSE", issuer->pid,
 596                     MC_smx_process_get_host_name(issuer));
 597       else
 598         label = bprintf("[(%lu)] Test FALSE", issuer->pid);
 599     } else {
 600       if (issuer->smx_host)
 601         label =
 602             bprintf("[(%lu)%s] Test TRUE", issuer->pid,
 603                     MC_smx_process_get_host_name(issuer));
 604       else
 605         label = bprintf("[(%lu)] Test TRUE", issuer->pid);
 606     }
 607     break;
 608   }
 609
 610   case SIMCALL_COMM_WAITANY: {
 611     unsigned long comms_size = MC_process_read_dynar_length(
 612       &mc_model_checker->process(), simcall_comm_waitany__get__comms(req));
 613     if (issuer->smx_host)
 614       label =
 615           bprintf("[(%lu)%s] WaitAny [%d of %lu]", issuer->pid,
 616                   MC_smx_process_get_host_name(issuer), value + 1,
 617                   comms_size);
 618     else
 619       label =
 620           bprintf("[(%lu)] WaitAny [%d of %lu]", issuer->pid, value + 1,
 621                   comms_size);
 622     break;
 623   }
 624
 625   case SIMCALL_COMM_TESTANY:
 626     if (value == -1) {
 627       if (issuer->smx_host)
 628         label =
 629             bprintf("[(%lu)%s] TestAny FALSE", issuer->pid,
 630                     MC_smx_process_get_host_name(issuer));
 631       else
 632         label = bprintf("[(%lu)] TestAny FALSE", issuer->pid);
 633     } else {
 634       if (issuer->smx_host)
 635         label =
 636             bprintf("[(%lu)%s] TestAny TRUE [%d of %lu]", issuer->pid,
 637                     MC_smx_process_get_host_name(issuer), value + 1,
 638                     xbt_dynar_length(simcall_comm_testany__get__comms(req)));
 639       else
 640         label =
 641             bprintf("[(%lu)] TestAny TRUE [%d of %lu]", issuer->pid,
 642                     value + 1,
 643                     xbt_dynar_length(simcall_comm_testany__get__comms(req)));
 644     }
 645     break;
 646
 647   case SIMCALL_MUTEX_LOCK:
 648     label = bprintf("[(%lu)] Mutex LOCK", req->issuer->pid);
 649     break;
 650
 651   case SIMCALL_MC_RANDOM:
 652     if (issuer->smx_host)
 653       label =
 654           bprintf("[(%lu)%s] MC_RANDOM (%d)", issuer->pid,
 655                   MC_smx_process_get_host_name(issuer), value);
 656     else
 657       label = bprintf("[(%lu)] MC_RANDOM (%d)", issuer->pid, value);
 658     break;
 659
 660   case SIMCALL_MC_SNAPSHOT:
 661     if (issuer->smx_host)
 662       label =
 663           bprintf("[(%lu)%s] MC_SNAPSHOT", issuer->pid,
 664                   MC_smx_process_get_host_name(issuer));
 665     else
 666       label = bprintf("[(%lu)] MC_SNAPSHOT", issuer->pid);
 667     break;
 668
 669   case SIMCALL_MC_COMPARE_SNAPSHOTS:
 670     if (issuer->smx_host)
 671       label =
 672           bprintf("[(%lu)%s] MC_COMPARE_SNAPSHOTS", issuer->pid,
 673                   MC_smx_process_get_host_name(issuer));
 674     else
 675       label = bprintf("[(%lu)] MC_COMPARE_SNAPSHOTS", issuer->pid);
 676     break;
 677
 678   default:
 679     THROW_UNIMPLEMENTED;
 680   }
 681
 682   char* str =
 683       bprintf("label = \"%s\", color = %s, fontcolor = %s", label,
 684               colors[issuer->pid - 1], colors[issuer->pid - 1]);
 685   xbt_free(label);
 686   return str;
 687
 688 }
 689
 690 }