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