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