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