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