src/mc/CommunicationDeterminismChecker.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 <cstdint>
   8
   9 #include <xbt/dynar.h>
  10 #include <xbt/dynar.hpp>
  11 #include <xbt/fifo.h>
  12 #include <xbt/log.h>
  13 #include <xbt/sysdep.h>
  14
  15 #include "src/mc/mc_state.h"
  16 #include "src/mc/mc_comm_pattern.h"
  17 #include "src/mc/mc_request.h"
  18 #include "src/mc/mc_safety.h"
  19 #include "src/mc/mc_private.h"
  20 #include "src/mc/mc_record.h"
  21 #include "src/mc/mc_smx.h"
  22 #include "src/mc/Client.hpp"
  23 #include "src/mc/CommunicationDeterminismChecker.hpp"
  24 #include "src/mc/mc_exit.h"
  25
  26 using simgrid::mc::remote;
  27
  28 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_comm_determinism, mc,
  29                                 "Logging specific to MC communication determinism detection");
  30
  31 /********** Global variables **********/
  32
  33 xbt_dynar_t initial_communications_pattern;
  34 xbt_dynar_t incomplete_communications_pattern;
  35
  36 /********** Static functions ***********/
  37
  38 static e_mc_comm_pattern_difference_t compare_comm_pattern(mc_comm_pattern_t comm1, mc_comm_pattern_t comm2) {
  39   if(comm1->type != comm2->type)
  40     return TYPE_DIFF;
  41   if (strcmp(comm1->rdv, comm2->rdv) != 0)
  42     return RDV_DIFF;
  43   if (comm1->src_proc != comm2->src_proc)
  44     return SRC_PROC_DIFF;
  45   if (comm1->dst_proc != comm2->dst_proc)
  46     return DST_PROC_DIFF;
  47   if (comm1->tag != comm2->tag)
  48     return TAG_DIFF;
  49   if (comm1->data_size != comm2->data_size)
  50     return DATA_SIZE_DIFF;
  51   if(comm1->data == nullptr && comm2->data == NULL)
  52     return NONE_DIFF;
  53   if(comm1->data != nullptr && comm2->data !=NULL) {
  54     if (!memcmp(comm1->data, comm2->data, comm1->data_size))
  55       return NONE_DIFF;
  56     return DATA_DIFF;
  57   } else
  58     return DATA_DIFF;
  59   return NONE_DIFF;
  60 }
  61
  62 static char* print_determinism_result(e_mc_comm_pattern_difference_t diff, int process, mc_comm_pattern_t comm, unsigned int cursor) {
  63   char *type, *res;
  64
  65   if(comm->type == SIMIX_COMM_SEND)
  66     type = bprintf("The send communications pattern of the process %d is different!", process - 1);
  67   else
  68     type = bprintf("The recv communications pattern of the process %d is different!", process - 1);
  69
  70   switch(diff) {
  71   case TYPE_DIFF:
  72     res = bprintf("%s Different type for communication #%d", type, cursor);
  73     break;
  74   case RDV_DIFF:
  75     res = bprintf("%s Different rdv for communication #%d", type, cursor);
  76     break;
  77   case TAG_DIFF:
  78     res = bprintf("%s Different tag for communication #%d", type, cursor);
  79     break;
  80   case SRC_PROC_DIFF:
  81       res = bprintf("%s Different source for communication #%d", type, cursor);
  82     break;
  83   case DST_PROC_DIFF:
  84       res = bprintf("%s Different destination for communication #%d", type, cursor);
  85     break;
  86   case DATA_SIZE_DIFF:
  87     res = bprintf("%s\n Different data size for communication #%d", type, cursor);
  88     break;
  89   case DATA_DIFF:
  90     res = bprintf("%s\n Different data for communication #%d", type, cursor);
  91     break;
  92   default:
  93     res = nullptr;
  94     break;
  95   }
  96
  97   return res;
  98 }
  99
 100 static void update_comm_pattern(mc_comm_pattern_t comm_pattern, smx_synchro_t comm_addr)
 101 {
 102   s_smx_synchro_t comm;
 103   mc_model_checker->process().read(&comm, remote(comm_addr));
 104
 105   smx_process_t src_proc = MC_smx_resolve_process(comm.comm.src_proc);
 106   smx_process_t dst_proc = MC_smx_resolve_process(comm.comm.dst_proc);
 107   comm_pattern->src_proc = src_proc->pid;
 108   comm_pattern->dst_proc = dst_proc->pid;
 109   comm_pattern->src_host = MC_smx_process_get_host_name(src_proc);
 110   comm_pattern->dst_host = MC_smx_process_get_host_name(dst_proc);
 111   if (comm_pattern->data_size == -1 && comm.comm.src_buff != nullptr) {
 112     size_t buff_size;
 113     mc_model_checker->process().read(
 114       &buff_size, remote(comm.comm.dst_buff_size));
 115     comm_pattern->data_size = buff_size;
 116     comm_pattern->data = xbt_malloc0(comm_pattern->data_size);
 117     mc_model_checker->process().read_bytes(
 118       comm_pattern->data, comm_pattern->data_size,
 119       remote(comm.comm.src_buff));
 120   }
 121 }
 122
 123 static void deterministic_comm_pattern(int process, mc_comm_pattern_t comm, int backtracking) {
 124
 125   mc_list_comm_pattern_t list =
 126     xbt_dynar_get_as(initial_communications_pattern, process, mc_list_comm_pattern_t);
 127
 128   if(!backtracking){
 129     mc_comm_pattern_t initial_comm =
 130       xbt_dynar_get_as(list->list, list->index_comm, mc_comm_pattern_t);
 131     e_mc_comm_pattern_difference_t diff =
 132       compare_comm_pattern(initial_comm, comm);
 133
 134     if (diff != NONE_DIFF) {
 135       if (comm->type == SIMIX_COMM_SEND){
 136         simgrid::mc::initial_global_state->send_deterministic = 0;
 137         if(simgrid::mc::initial_global_state->send_diff != nullptr)
 138           xbt_free(simgrid::mc::initial_global_state->send_diff);
 139         simgrid::mc::initial_global_state->send_diff = print_determinism_result(diff, process, comm, list->index_comm + 1);
 140       }else{
 141         simgrid::mc::initial_global_state->recv_deterministic = 0;
 142         if(simgrid::mc::initial_global_state->recv_diff != nullptr)
 143           xbt_free(simgrid::mc::initial_global_state->recv_diff);
 144         simgrid::mc::initial_global_state->recv_diff = print_determinism_result(diff, process, comm, list->index_comm + 1);
 145       }
 146       if(_sg_mc_send_determinism && !simgrid::mc::initial_global_state->send_deterministic){
 147         XBT_INFO("*********************************************************");
 148         XBT_INFO("***** Non-send-deterministic communications pattern *****");
 149         XBT_INFO("*********************************************************");
 150         XBT_INFO("%s", simgrid::mc::initial_global_state->send_diff);
 151         xbt_free(simgrid::mc::initial_global_state->send_diff);
 152         simgrid::mc::initial_global_state->send_diff = nullptr;
 153         MC_print_statistics(mc_stats);
 154         mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
 155       }else if(_sg_mc_comms_determinism
 156           && (!simgrid::mc::initial_global_state->send_deterministic
 157             && !simgrid::mc::initial_global_state->recv_deterministic)) {
 158         XBT_INFO("****************************************************");
 159         XBT_INFO("***** Non-deterministic communications pattern *****");
 160         XBT_INFO("****************************************************");
 161         XBT_INFO("%s", simgrid::mc::initial_global_state->send_diff);
 162         XBT_INFO("%s", simgrid::mc::initial_global_state->recv_diff);
 163         xbt_free(simgrid::mc::initial_global_state->send_diff);
 164         simgrid::mc::initial_global_state->send_diff = nullptr;
 165         xbt_free(simgrid::mc::initial_global_state->recv_diff);
 166         simgrid::mc::initial_global_state->recv_diff = nullptr;
 167         MC_print_statistics(mc_stats);
 168         mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
 169       }
 170     }
 171   }
 172
 173   MC_comm_pattern_free(comm);
 174
 175 }
 176
 177 /********** Non Static functions ***********/
 178
 179 void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking)
 180 {
 181   const smx_process_t issuer = MC_smx_simcall_get_issuer(request);
 182   mc_list_comm_pattern_t initial_pattern = xbt_dynar_get_as(
 183     initial_communications_pattern, issuer->pid, mc_list_comm_pattern_t);
 184   xbt_dynar_t incomplete_pattern = xbt_dynar_get_as(
 185     incomplete_communications_pattern, issuer->pid, xbt_dynar_t);
 186
 187   mc_comm_pattern_t pattern = xbt_new0(s_mc_comm_pattern_t, 1);
 188   pattern->data_size = -1;
 189   pattern->data = nullptr;
 190   pattern->index =
 191     initial_pattern->index_comm + xbt_dynar_length(incomplete_pattern);
 192
 193   if (call_type == MC_CALL_TYPE_SEND) {
 194     /* Create comm pattern */
 195     pattern->type = SIMIX_COMM_SEND;
 196     pattern->comm_addr = simcall_comm_isend__get__result(request);
 197
 198     s_smx_synchro_t synchro = mc_model_checker->process().read<s_smx_synchro_t>(
 199       (std::uint64_t) pattern->comm_addr);
 200
 201     char* remote_name = mc_model_checker->process().read<char*>(
 202       (std::uint64_t)(synchro.comm.rdv ? &synchro.comm.rdv->name : &synchro.comm.rdv_cpy->name));
 203     pattern->rdv = mc_model_checker->process().read_string(remote_name);
 204     pattern->src_proc = MC_smx_resolve_process(synchro.comm.src_proc)->pid;
 205     pattern->src_host = MC_smx_process_get_host_name(issuer);
 206
 207     struct s_smpi_mpi_request mpi_request =
 208       mc_model_checker->process().read<s_smpi_mpi_request>(
 209         (std::uint64_t) simcall_comm_isend__get__data(request));
 210     pattern->tag = mpi_request.tag;
 211
 212     if(synchro.comm.src_buff != nullptr){
 213       pattern->data_size = synchro.comm.src_buff_size;
 214       pattern->data = xbt_malloc0(pattern->data_size);
 215       mc_model_checker->process().read_bytes(
 216         pattern->data, pattern->data_size, remote(synchro.comm.src_buff));
 217     }
 218     if(mpi_request.detached){
 219       if (!simgrid::mc::initial_global_state->initial_communications_pattern_done) {
 220         /* Store comm pattern */
 221         xbt_dynar_push(
 222           xbt_dynar_get_as(
 223             initial_communications_pattern, pattern->src_proc, mc_list_comm_pattern_t
 224           )->list,
 225           &pattern);
 226       } else {
 227         /* Evaluate comm determinism */
 228         deterministic_comm_pattern(pattern->src_proc, pattern, backtracking);
 229         xbt_dynar_get_as(
 230           initial_communications_pattern, pattern->src_proc, mc_list_comm_pattern_t
 231         )->index_comm++;
 232       }
 233       return;
 234     }
 235   } else if (call_type == MC_CALL_TYPE_RECV) {
 236     pattern->type = SIMIX_COMM_RECEIVE;
 237     pattern->comm_addr = simcall_comm_irecv__get__result(request);
 238
 239     struct s_smpi_mpi_request mpi_request;
 240     mc_model_checker->process().read(
 241       &mpi_request, remote((struct s_smpi_mpi_request*)simcall_comm_irecv__get__data(request)));
 242     pattern->tag = mpi_request.tag;
 243
 244     s_smx_synchro_t synchro;
 245     mc_model_checker->process().read(&synchro, remote(pattern->comm_addr));
 246
 247     char* remote_name;
 248     mc_model_checker->process().read(&remote_name,
 249       remote(synchro.comm.rdv ? &synchro.comm.rdv->name : &synchro.comm.rdv_cpy->name));
 250     pattern->rdv = mc_model_checker->process().read_string(remote_name);
 251     pattern->dst_proc = MC_smx_resolve_process(synchro.comm.dst_proc)->pid;
 252     pattern->dst_host = MC_smx_process_get_host_name(issuer);
 253   } else
 254     xbt_die("Unexpected call_type %i", (int) call_type);
 255
 256   xbt_dynar_push(
 257     xbt_dynar_get_as(incomplete_communications_pattern, issuer->pid, xbt_dynar_t),
 258     &pattern);
 259
 260   XBT_DEBUG("Insert incomplete comm pattern %p for process %lu", pattern, issuer->pid);
 261 }
 262
 263 void MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigned int issuer, int backtracking) {
 264   mc_comm_pattern_t current_comm_pattern;
 265   unsigned int cursor = 0;
 266   mc_comm_pattern_t comm_pattern;
 267   int completed = 0;
 268
 269   /* Complete comm pattern */
 270   xbt_dynar_foreach(xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t), cursor, current_comm_pattern)
 271     if (current_comm_pattern->comm_addr == comm_addr) {
 272       update_comm_pattern(current_comm_pattern, comm_addr);
 273       completed = 1;
 274       xbt_dynar_remove_at(
 275         xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t),
 276         cursor, &comm_pattern);
 277       XBT_DEBUG("Remove incomplete comm pattern for process %u at cursor %u", issuer, cursor);
 278       break;
 279     }
 280
 281   if(!completed)
 282     xbt_die("Corresponding communication not found!");
 283
 284   mc_list_comm_pattern_t pattern = xbt_dynar_get_as(
 285     initial_communications_pattern, issuer, mc_list_comm_pattern_t);
 286
 287   if (!simgrid::mc::initial_global_state->initial_communications_pattern_done)
 288     /* Store comm pattern */
 289     xbt_dynar_push(pattern->list, &comm_pattern);
 290   else {
 291     /* Evaluate comm determinism */
 292     deterministic_comm_pattern(issuer, comm_pattern, backtracking);
 293     pattern->index_comm++;
 294   }
 295 }
 296
 297
 298 /************************ Main algorithm ************************/
 299
 300 namespace simgrid {
 301 namespace mc {
 302
 303 CommunicationDeterminismChecker::CommunicationDeterminismChecker(Session& session)
 304   : Checker(session)
 305 {
 306
 307 }
 308
 309 CommunicationDeterminismChecker::~CommunicationDeterminismChecker()
 310 {
 311
 312 }
 313
 314 // TODO, deduplicate with SafetyChecker
 315 RecordTrace CommunicationDeterminismChecker::getRecordTrace() // override
 316 {
 317   RecordTrace res;
 318
 319   xbt_fifo_item_t start = xbt_fifo_get_last_item(mc_stack);
 320   for (xbt_fifo_item_t item = start; item; item = xbt_fifo_get_prev_item(item)) {
 321
 322     // Find (pid, value):
 323     simgrid::mc::State* state = (simgrid::mc::State*) xbt_fifo_get_item_content(item);
 324     int value = 0;
 325     smx_simcall_t saved_req = MC_state_get_executed_request(state, &value);
 326     const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
 327     const int pid = issuer->pid;
 328
 329     res.push_back(RecordTraceElement(pid, value));
 330   }
 331
 332   return std::move(res);
 333 }
 334
 335 // TODO, deduplicate with SafetyChecker
 336 std::vector<std::string> CommunicationDeterminismChecker::getTextualTrace() // override
 337 {
 338   std::vector<std::string> res;
 339   for (xbt_fifo_item_t item = xbt_fifo_get_last_item(mc_stack);
 340        item; item = xbt_fifo_get_prev_item(item)) {
 341     simgrid::mc::State* state = (simgrid::mc::State*)xbt_fifo_get_item_content(item);
 342     int value;
 343     smx_simcall_t req = MC_state_get_executed_request(state, &value);
 344     if (req) {
 345       char* req_str = simgrid::mc::request_to_string(
 346         req, value, simgrid::mc::RequestType::executed);
 347       res.push_back(req_str);
 348       xbt_free(req_str);
 349     }
 350   }
 351   return std::move(res);
 352 }
 353
 354 void CommunicationDeterminismChecker::prepare()
 355 {
 356   simgrid::mc::State* initial_state = nullptr;
 357   int i;
 358   const int maxpid = MC_smx_get_maxpid();
 359
 360   simgrid::mc::visited_states.clear();
 361
 362   // Create initial_communications_pattern elements:
 363   initial_communications_pattern = xbt_dynar_new(sizeof(mc_list_comm_pattern_t), MC_list_comm_pattern_free_voidp);
 364   for (i=0; i < maxpid; i++){
 365     mc_list_comm_pattern_t process_list_pattern = xbt_new0(s_mc_list_comm_pattern_t, 1);
 366     process_list_pattern->list = xbt_dynar_new(sizeof(mc_comm_pattern_t), MC_comm_pattern_free_voidp);
 367     process_list_pattern->index_comm = 0;
 368     xbt_dynar_insert_at(initial_communications_pattern, i, &process_list_pattern);
 369   }
 370
 371   // Create incomplete_communications_pattern elements:
 372   incomplete_communications_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp);
 373   for (i=0; i < maxpid; i++){
 374     xbt_dynar_t process_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), nullptr);
 375     xbt_dynar_insert_at(incomplete_communications_pattern, i, &process_pattern);
 376   }
 377
 378   initial_state = MC_state_new();
 379
 380   XBT_DEBUG("********* Start communication determinism verification *********");
 381
 382   /* Wait for requests (schedules processes) */
 383   mc_model_checker->wait_for_requests();
 384
 385   /* Get an enabled process and insert it in the interleave set of the initial state */
 386   for (auto& p : mc_model_checker->process().simix_processes())
 387     if (simgrid::mc::process_is_enabled(&p.copy))
 388       MC_state_interleave_process(initial_state, &p.copy);
 389
 390   xbt_fifo_unshift(mc_stack, initial_state);
 391 }
 392
 393 static inline
 394 bool all_communications_are_finished()
 395 {
 396   for (size_t current_process = 1; current_process < MC_smx_get_maxpid(); current_process++) {
 397     xbt_dynar_t pattern = xbt_dynar_get_as(
 398       incomplete_communications_pattern, current_process, xbt_dynar_t);
 399     if (!xbt_dynar_is_empty(pattern)) {
 400       XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
 401       return false;
 402     }
 403   }
 404   return true;
 405 }
 406
 407 int CommunicationDeterminismChecker::main(void)
 408 {
 409
 410   char *req_str = nullptr;
 411   int value;
 412   std::unique_ptr<simgrid::mc::VisitedState> visited_state = nullptr;
 413   smx_simcall_t req = nullptr;
 414   simgrid::mc::State* state = nullptr;
 415   simgrid::mc::State* next_state = nullptr;
 416
 417   while (xbt_fifo_size(mc_stack) > 0) {
 418
 419     /* Get current state */
 420     state = (simgrid::mc::State*) xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
 421
 422     XBT_DEBUG("**************************************************");
 423     XBT_DEBUG("Exploration depth = %d (state = %d, interleaved processes = %d)",
 424               xbt_fifo_size(mc_stack), state->num,
 425               MC_state_interleave_size(state));
 426
 427     /* Update statistics */
 428     mc_stats->visited_states++;
 429
 430     if ((xbt_fifo_size(mc_stack) <= _sg_mc_max_depth)
 431         && (req = MC_state_get_request(state, &value))
 432         && (visited_state == nullptr)) {
 433
 434       req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
 435       XBT_DEBUG("Execute: %s", req_str);
 436       xbt_free(req_str);
 437
 438       if (dot_output != nullptr)
 439         req_str = simgrid::mc::request_get_dot_output(req, value);
 440
 441       MC_state_set_executed_request(state, req, value);
 442       mc_stats->executed_transitions++;
 443
 444       /* TODO : handle test and testany simcalls */
 445       e_mc_call_type_t call = MC_CALL_TYPE_NONE;
 446       if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
 447         call = MC_get_call_type(req);
 448
 449       /* Answer the request */
 450       simgrid::mc::handle_simcall(req, value);    /* After this call req is no longer useful */
 451
 452       if(!initial_global_state->initial_communications_pattern_done)
 453         MC_handle_comm_pattern(call, req, value, initial_communications_pattern, 0);
 454       else
 455         MC_handle_comm_pattern(call, req, value, nullptr, 0);
 456
 457       /* Wait for requests (schedules processes) */
 458       mc_model_checker->wait_for_requests();
 459
 460       /* Create the new expanded state */
 461       next_state = MC_state_new();
 462
 463       /* If comm determinism verification, we cannot stop the exploration if
 464          some communications are not finished (at least, data are transfered).
 465          These communications  are incomplete and they cannot be analyzed and
 466          compared with the initial pattern. */
 467       bool compare_snapshots = all_communications_are_finished()
 468         && initial_global_state->initial_communications_pattern_done;
 469
 470       if (_sg_mc_visited == 0 || (visited_state = simgrid::mc::is_visited_state(next_state, compare_snapshots)) == nullptr) {
 471
 472         /* Get enabled processes and insert them in the interleave set of the next state */
 473         for (auto& p : mc_model_checker->process().simix_processes())
 474           if (simgrid::mc::process_is_enabled(&p.copy))
 475             MC_state_interleave_process(next_state, &p.copy);
 476
 477         if (dot_output != nullptr)
 478           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,  next_state->num, req_str);
 479
 480       } else if (dot_output != nullptr)
 481         fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
 482           state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
 483
 484       xbt_fifo_unshift(mc_stack, next_state);
 485
 486       if (dot_output != nullptr)
 487         xbt_free(req_str);
 488
 489     } else {
 490
 491       if (xbt_fifo_size(mc_stack) > _sg_mc_max_depth)
 492         XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 493       else if (visited_state != nullptr)
 494         XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.", visited_state->other_num == -1 ? visited_state->num : visited_state->other_num);
 495       else
 496         XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack));
 497
 498       if (!initial_global_state->initial_communications_pattern_done)
 499         initial_global_state->initial_communications_pattern_done = 1;
 500
 501       /* Trash the current state, no longer needed */
 502       xbt_fifo_shift(mc_stack);
 503       MC_state_delete(state, !state->in_visited_states ? 1 : 0);
 504       XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
 505
 506       visited_state = nullptr;
 507
 508       /* Check for deadlocks */
 509       if (mc_model_checker->checkDeadlock()) {
 510         MC_show_deadlock();
 511         return SIMGRID_MC_EXIT_DEADLOCK;
 512       }
 513
 514       while ((state = (simgrid::mc::State*) xbt_fifo_shift(mc_stack)) != nullptr)
 515         if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
 516           /* We found a back-tracking point, let's loop */
 517           XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
 518           xbt_fifo_unshift(mc_stack, state);
 519
 520           MC_replay(mc_stack);
 521
 522           XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack));
 523
 524           break;
 525         } else {
 526           XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
 527           MC_state_delete(state, !state->in_visited_states ? 1 : 0);
 528         }
 529
 530     }
 531   }
 532
 533   MC_print_statistics(mc_stats);
 534   return SIMGRID_MC_EXIT_SUCCESS;
 535 }
 536
 537 int CommunicationDeterminismChecker::run()
 538 {
 539   XBT_INFO("Check communication determinism");
 540   mc_model_checker->wait_for_requests();
 541
 542   if (mc_mode == MC_MODE_CLIENT)
 543     // This will move somehwere else:
 544     simgrid::mc::Client::get()->handleMessages();
 545
 546   /* Create exploration stack */
 547   mc_stack = xbt_fifo_new();
 548
 549   this->prepare();
 550
 551   initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
 552   initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
 553   initial_global_state->initial_communications_pattern_done = 0;
 554   initial_global_state->recv_deterministic = 1;
 555   initial_global_state->send_deterministic = 1;
 556   initial_global_state->recv_diff = nullptr;
 557   initial_global_state->send_diff = nullptr;
 558
 559   int res = this->main();
 560   initial_global_state = nullptr;
 561   return res;
 562 }
 563
 564 }
 565 }