src/mc/mc_request.cpp

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