src/mc/checker/CommunicationDeterminismChecker.cpp

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