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