src/mc/checker/CommunicationDeterminismChecker.cpp

   1 /* Copyright (c) 2008-2022. 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 "src/mc/checker/CommunicationDeterminismChecker.hpp"
   7 #include "src/kernel/activity/MailboxImpl.hpp"
   8 #include "src/mc/Session.hpp"
   9 #include "src/mc/mc_config.hpp"
  10 #include "src/mc/mc_exit.hpp"
  11 #include "src/mc/mc_private.hpp"
  12
  13 #include <cstdint>
  14
  15 using api = simgrid::mc::Api;
  16
  17 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_comm_determinism, mc, "Logging specific to MC communication determinism detection");
  18
  19 namespace simgrid {
  20 namespace mc {
  21
  22 enum class CallType { NONE, SEND, RECV, WAIT, WAITANY };
  23 enum class CommPatternDifference { NONE, TYPE, RDV, TAG, SRC_PROC, DST_PROC, DATA_SIZE, DATA };
  24
  25 struct PatternCommunicationList {
  26   unsigned int index_comm = 0;
  27   std::vector<std::unique_ptr<simgrid::mc::PatternCommunication>> list;
  28 };
  29
  30 static inline simgrid::mc::CallType MC_get_call_type(const s_smx_simcall* req)
  31 {
  32   using simgrid::mc::CallType;
  33   using simgrid::simix::Simcall;
  34   switch (req->call_) {
  35     case Simcall::COMM_ISEND:
  36       return CallType::SEND;
  37     case Simcall::COMM_IRECV:
  38       return CallType::RECV;
  39     case Simcall::COMM_WAIT:
  40       return CallType::WAIT;
  41     case Simcall::COMM_WAITANY:
  42       return CallType::WAITANY;
  43     default:
  44       return CallType::NONE;
  45   }
  46 }
  47
  48 /********** Checker extension **********/
  49
  50 struct CommDetExtension {
  51   static simgrid::xbt::Extension<simgrid::mc::Checker, CommDetExtension> EXTENSION_ID;
  52
  53   CommDetExtension()
  54   {
  55     const unsigned long maxpid = api::get().get_maxpid();
  56
  57     initial_communications_pattern.resize(maxpid);
  58     incomplete_communications_pattern.resize(maxpid);
  59   }
  60
  61   std::vector<simgrid::mc::PatternCommunicationList> initial_communications_pattern;
  62   std::vector<std::vector<simgrid::mc::PatternCommunication*>> incomplete_communications_pattern;
  63
  64   bool initial_communications_pattern_done = false;
  65   bool recv_deterministic                  = true;
  66   bool send_deterministic                  = true;
  67   std::string send_diff;
  68   std::string recv_diff;
  69
  70   void restore_communications_pattern(simgrid::mc::State* state);
  71   void deterministic_comm_pattern(aid_t process, const PatternCommunication* comm, bool backtracking);
  72   void get_comm_pattern(smx_simcall_t request, CallType call_type, bool backtracking);
  73   void complete_comm_pattern(RemotePtr<kernel::activity::CommImpl> const& comm_addr, aid_t issuer, bool backtracking);
  74   void handle_comm_pattern(simgrid::mc::CallType call_type, smx_simcall_t req, int value, bool backtracking);
  75 };
  76 simgrid::xbt::Extension<simgrid::mc::Checker, CommDetExtension> CommDetExtension::EXTENSION_ID;
  77 /********** State Extension ***********/
  78
  79 class StateCommDet {
  80   CommDetExtension* checker_;
  81
  82 public:
  83   std::vector<std::vector<simgrid::mc::PatternCommunication>> incomplete_comm_pattern_;
  84   std::vector<unsigned> communication_indices_;
  85
  86   static simgrid::xbt::Extension<simgrid::mc::State, StateCommDet> EXTENSION_ID;
  87   explicit StateCommDet(CommDetExtension* checker) : checker_(checker)
  88   {
  89     copy_incomplete_comm_pattern();
  90     copy_index_comm_pattern();
  91   }
  92
  93   void copy_incomplete_comm_pattern()
  94   {
  95     incomplete_comm_pattern_.clear();
  96     const unsigned long maxpid = api::get().get_maxpid();
  97     for (unsigned long i = 0; i < maxpid; i++) {
  98       std::vector<simgrid::mc::PatternCommunication> res;
  99       for (auto const& comm : checker_->incomplete_communications_pattern[i])
 100         res.push_back(comm->dup());
 101       incomplete_comm_pattern_.push_back(std::move(res));
 102     }
 103   }
 104
 105   void copy_index_comm_pattern()
 106   {
 107     communication_indices_.clear();
 108     for (auto const& list_process_comm : checker_->initial_communications_pattern)
 109       this->communication_indices_.push_back(list_process_comm.index_comm);
 110   }
 111 };
 112 simgrid::xbt::Extension<simgrid::mc::State, StateCommDet> StateCommDet::EXTENSION_ID;
 113
 114 static simgrid::mc::CommPatternDifference compare_comm_pattern(const simgrid::mc::PatternCommunication* comm1,
 115                                                                const simgrid::mc::PatternCommunication* comm2)
 116 {
 117   using simgrid::mc::CommPatternDifference;
 118   if (comm1->type != comm2->type)
 119     return CommPatternDifference::TYPE;
 120   if (comm1->rdv != comm2->rdv)
 121     return CommPatternDifference::RDV;
 122   if (comm1->src_proc != comm2->src_proc)
 123     return CommPatternDifference::SRC_PROC;
 124   if (comm1->dst_proc != comm2->dst_proc)
 125     return CommPatternDifference::DST_PROC;
 126   if (comm1->tag != comm2->tag)
 127     return CommPatternDifference::TAG;
 128   if (comm1->data.size() != comm2->data.size())
 129     return CommPatternDifference::DATA_SIZE;
 130   if (comm1->data != comm2->data)
 131     return CommPatternDifference::DATA;
 132   return CommPatternDifference::NONE;
 133 }
 134
 135 static void patterns_copy(std::vector<simgrid::mc::PatternCommunication*>& dest,
 136                              std::vector<simgrid::mc::PatternCommunication> const& source)
 137 {
 138   dest.clear();
 139   for (simgrid::mc::PatternCommunication const& comm : source) {
 140     auto* copy_comm = new simgrid::mc::PatternCommunication(comm.dup());
 141     dest.push_back(copy_comm);
 142   }
 143 }
 144
 145 void CommDetExtension::restore_communications_pattern(simgrid::mc::State* state)
 146 {
 147   for (size_t i = 0; i < initial_communications_pattern.size(); i++)
 148     initial_communications_pattern[i].index_comm =
 149         state->extension<simgrid::mc::StateCommDet>()->communication_indices_[i];
 150
 151   const unsigned long maxpid = api::get().get_maxpid();
 152   for (unsigned long i = 0; i < maxpid; i++)
 153     patterns_copy(incomplete_communications_pattern[i],
 154                   state->extension<simgrid::mc::StateCommDet>()->incomplete_comm_pattern_[i]);
 155 }
 156
 157 std::string print_determinism_result(simgrid::mc::CommPatternDifference diff, aid_t process,
 158                                      const simgrid::mc::PatternCommunication* comm, unsigned int cursor)
 159 {
 160   std::string type;
 161   std::string res;
 162
 163   if (comm->type == simgrid::mc::PatternCommunicationType::send)
 164     type = xbt::string_printf("The send communications pattern of the process %ld is different!", process - 1);
 165   else
 166     type = xbt::string_printf("The recv communications pattern of the process %ld is different!", process - 1);
 167
 168   using simgrid::mc::CommPatternDifference;
 169   switch (diff) {
 170     case CommPatternDifference::TYPE:
 171       res = xbt::string_printf("%s Different type for communication #%u", type.c_str(), cursor);
 172       break;
 173     case CommPatternDifference::RDV:
 174       res = xbt::string_printf("%s Different rdv for communication #%u", type.c_str(), cursor);
 175       break;
 176     case CommPatternDifference::TAG:
 177       res = xbt::string_printf("%s Different tag for communication #%u", type.c_str(), cursor);
 178       break;
 179     case CommPatternDifference::SRC_PROC:
 180       res = xbt::string_printf("%s Different source for communication #%u", type.c_str(), cursor);
 181       break;
 182     case CommPatternDifference::DST_PROC:
 183       res = xbt::string_printf("%s Different destination for communication #%u", type.c_str(), cursor);
 184       break;
 185     case CommPatternDifference::DATA_SIZE:
 186       res = xbt::string_printf("%s Different data size for communication #%u", type.c_str(), cursor);
 187       break;
 188     case CommPatternDifference::DATA:
 189       res = xbt::string_printf("%s Different data for communication #%u", type.c_str(), cursor);
 190       break;
 191     default:
 192       res = "";
 193       break;
 194   }
 195
 196   return res;
 197 }
 198
 199 static void update_comm_pattern(simgrid::mc::PatternCommunication* comm_pattern,
 200                                 simgrid::mc::RemotePtr<simgrid::kernel::activity::CommImpl> const& comm_addr)
 201 {
 202   auto src_proc = api::get().get_src_actor(comm_addr);
 203   auto dst_proc = api::get().get_dst_actor(comm_addr);
 204   comm_pattern->src_proc = src_proc->get_pid();
 205   comm_pattern->dst_proc = dst_proc->get_pid();
 206
 207   if (comm_pattern->data.empty()) {
 208     comm_pattern->data = api::get().get_pattern_comm_data(comm_addr);
 209   }
 210 }
 211
 212 void CommDetExtension::deterministic_comm_pattern(aid_t process, const PatternCommunication* comm, bool backtracking)
 213 {
 214   if (not backtracking) {
 215     PatternCommunicationList& list = initial_communications_pattern[process];
 216     CommPatternDifference diff     = compare_comm_pattern(list.list[list.index_comm].get(), comm);
 217
 218     if (diff != CommPatternDifference::NONE) {
 219       if (comm->type == PatternCommunicationType::send) {
 220         send_deterministic = false;
 221         send_diff = print_determinism_result(diff, process, comm, list.index_comm + 1);
 222       } else {
 223         recv_deterministic = false;
 224         recv_diff = print_determinism_result(diff, process, comm, list.index_comm + 1);
 225       }
 226       if (_sg_mc_send_determinism && not send_deterministic) {
 227         XBT_INFO("*********************************************************");
 228         XBT_INFO("***** Non-send-deterministic communications pattern *****");
 229         XBT_INFO("*********************************************************");
 230         XBT_INFO("%s", send_diff.c_str());
 231         api::get().log_state();
 232         api::get().mc_exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
 233       } else if (_sg_mc_comms_determinism && (not send_deterministic && not recv_deterministic)) {
 234         XBT_INFO("****************************************************");
 235         XBT_INFO("***** Non-deterministic communications pattern *****");
 236         XBT_INFO("****************************************************");
 237         if (not send_diff.empty())
 238           XBT_INFO("%s", send_diff.c_str());
 239         if (not recv_diff.empty())
 240           XBT_INFO("%s", recv_diff.c_str());
 241         api::get().log_state();
 242         api::get().mc_exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
 243       }
 244     }
 245   }
 246 }
 247
 248 /********** Non Static functions ***********/
 249
 250 void CommDetExtension::get_comm_pattern(smx_simcall_t request, CallType call_type, bool backtracking)
 251 {
 252   const smx_actor_t issuer                                     = api::get().simcall_get_issuer(request);
 253   const mc::PatternCommunicationList& initial_pattern          = initial_communications_pattern[issuer->get_pid()];
 254   const std::vector<PatternCommunication*>& incomplete_pattern = incomplete_communications_pattern[issuer->get_pid()];
 255
 256   auto pattern   = std::make_unique<PatternCommunication>();
 257   pattern->index = initial_pattern.index_comm + incomplete_pattern.size();
 258
 259   if (call_type == CallType::SEND) {
 260     /* Create comm pattern */
 261     pattern->type      = PatternCommunicationType::send;
 262     pattern->comm_addr = api::get().get_comm_isend_raw_addr(request);
 263     pattern->rdv       = api::get().get_pattern_comm_rdv(pattern->comm_addr);
 264     pattern->src_proc  = api::get().get_pattern_comm_src_proc(pattern->comm_addr);
 265
 266 #if HAVE_SMPI
 267     pattern->tag = api::get().get_smpi_request_tag(request, simgrid::simix::Simcall::COMM_ISEND);
 268 #endif
 269     pattern->data = api::get().get_pattern_comm_data(pattern->comm_addr);
 270
 271 #if HAVE_SMPI
 272     auto send_detached = api::get().check_send_request_detached(request);
 273     if (send_detached) {
 274       if (initial_communications_pattern_done) {
 275         /* Evaluate comm determinism */
 276         deterministic_comm_pattern(pattern->src_proc, pattern.get(), backtracking);
 277         initial_communications_pattern[pattern->src_proc].index_comm++;
 278       } else {
 279         /* Store comm pattern */
 280         initial_communications_pattern[pattern->src_proc].list.push_back(std::move(pattern));
 281       }
 282       return;
 283     }
 284 #endif
 285   } else if (call_type == CallType::RECV) {
 286     pattern->type = PatternCommunicationType::receive;
 287     pattern->comm_addr = api::get().get_comm_isend_raw_addr(request);
 288
 289 #if HAVE_SMPI
 290     pattern->tag = api::get().get_smpi_request_tag(request, simgrid::simix::Simcall::COMM_IRECV);
 291 #endif
 292     pattern->rdv = api::get().get_pattern_comm_rdv(pattern->comm_addr);
 293     pattern->dst_proc = api::get().get_pattern_comm_dst_proc(pattern->comm_addr);
 294   } else
 295     xbt_die("Unexpected call_type %i", (int)call_type);
 296
 297   XBT_DEBUG("Insert incomplete comm pattern %p for process %ld", pattern.get(), issuer->get_pid());
 298   incomplete_communications_pattern[issuer->get_pid()].push_back(pattern.release());
 299 }
 300
 301 void CommDetExtension::complete_comm_pattern(RemotePtr<kernel::activity::CommImpl> const& comm_addr, aid_t issuer,
 302                                              bool backtracking)
 303 {
 304   /* Complete comm pattern */
 305   std::vector<PatternCommunication*>& incomplete_pattern = incomplete_communications_pattern[issuer];
 306   auto current_comm_pattern =
 307       std::find_if(begin(incomplete_pattern), end(incomplete_pattern),
 308                    [&comm_addr](const PatternCommunication* comm) { return (comm->comm_addr == comm_addr); });
 309   xbt_assert(current_comm_pattern != std::end(incomplete_pattern), "Corresponding communication not found!");
 310
 311   update_comm_pattern(*current_comm_pattern, comm_addr);
 312   std::unique_ptr<PatternCommunication> comm_pattern(*current_comm_pattern);
 313   XBT_DEBUG("Remove incomplete comm pattern for process %ld at cursor %zd", issuer,
 314             std::distance(begin(incomplete_pattern), current_comm_pattern));
 315   incomplete_pattern.erase(current_comm_pattern);
 316
 317   if (initial_communications_pattern_done) {
 318     /* Evaluate comm determinism */
 319     deterministic_comm_pattern(issuer, comm_pattern.get(), backtracking);
 320     initial_communications_pattern[issuer].index_comm++;
 321   } else {
 322     /* Store comm pattern */
 323     initial_communications_pattern[issuer].list.push_back(std::move(comm_pattern));
 324   }
 325 }
 326
 327 CommunicationDeterminismChecker::CommunicationDeterminismChecker(Session* session) : Checker(session)
 328 {
 329   CommDetExtension::EXTENSION_ID = simgrid::mc::Checker::extension_create<CommDetExtension>();
 330   StateCommDet::EXTENSION_ID = simgrid::mc::State::extension_create<StateCommDet>();
 331 }
 332
 333 CommunicationDeterminismChecker::~CommunicationDeterminismChecker() = default;
 334
 335 RecordTrace CommunicationDeterminismChecker::get_record_trace() // override
 336 {
 337   RecordTrace res;
 338   for (auto const& state : stack_)
 339     res.push_back(state->get_transition());
 340   return res;
 341 }
 342
 343 std::vector<std::string> CommunicationDeterminismChecker::get_textual_trace() // override
 344 {
 345   std::vector<std::string> trace;
 346   for (auto const& state : stack_)
 347     trace.push_back(state->get_transition()->to_string());
 348   return trace;
 349 }
 350
 351 void CommunicationDeterminismChecker::log_state() // override
 352 {
 353   if (_sg_mc_comms_determinism) {
 354     if (extension<CommDetExtension>()->send_deterministic && not extension<CommDetExtension>()->recv_deterministic) {
 355       XBT_INFO("*******************************************************");
 356       XBT_INFO("**** Only-send-deterministic communication pattern ****");
 357       XBT_INFO("*******************************************************");
 358       XBT_INFO("%s", extension<CommDetExtension>()->recv_diff.c_str());
 359     }
 360     if (not extension<CommDetExtension>()->send_deterministic && extension<CommDetExtension>()->recv_deterministic) {
 361       XBT_INFO("*******************************************************");
 362       XBT_INFO("**** Only-recv-deterministic communication pattern ****");
 363       XBT_INFO("*******************************************************");
 364       XBT_INFO("%s", extension<CommDetExtension>()->send_diff.c_str());
 365     }
 366   }
 367   XBT_INFO("Expanded states = %ld", State::get_expanded_states());
 368   XBT_INFO("Visited states = %lu", api::get().mc_get_visited_states());
 369   XBT_INFO("Executed transitions = %lu", Transition::get_executed_transitions());
 370   XBT_INFO("Send-deterministic : %s", extension<CommDetExtension>()->send_deterministic ? "Yes" : "No");
 371   if (_sg_mc_comms_determinism)
 372     XBT_INFO("Recv-deterministic : %s", extension<CommDetExtension>()->recv_deterministic ? "Yes" : "No");
 373 }
 374
 375 void CommunicationDeterminismChecker::prepare()
 376 {
 377   auto initial_state = std::make_unique<State>();
 378   extension_set(new CommDetExtension());
 379   initial_state->extension_set(new StateCommDet(extension<CommDetExtension>()));
 380
 381   XBT_DEBUG("********* Start communication determinism verification *********");
 382
 383   /* Add all enabled actors to the interleave set of the initial state */
 384   for (auto& act : api::get().get_actors()) {
 385     auto actor = act.copy.get_buffer();
 386     if (get_session().actor_is_enabled(actor->get_pid()))
 387       initial_state->mark_todo(actor->get_pid());
 388   }
 389
 390   stack_.push_back(std::move(initial_state));
 391 }
 392
 393 void CommunicationDeterminismChecker::restoreState()
 394 {
 395   auto extension = this->extension<CommDetExtension>();
 396
 397   /* Intermediate backtracking */
 398   State* last_state = stack_.back().get();
 399   if (last_state->system_state_) {
 400     api::get().restore_state(last_state->system_state_);
 401     extension->restore_communications_pattern(last_state);
 402     return;
 403   }
 404
 405   get_session().restore_initial_state();
 406
 407   const unsigned long maxpid = api::get().get_maxpid();
 408   assert(maxpid == extension->incomplete_communications_pattern.size());
 409   assert(maxpid == extension->initial_communications_pattern.size());
 410   for (unsigned long j = 0; j < maxpid; j++) {
 411     extension->incomplete_communications_pattern[j].clear();
 412     extension->initial_communications_pattern[j].index_comm = 0;
 413   }
 414
 415   /* Traverse the stack from the state at position start and re-execute the transitions */
 416   for (std::unique_ptr<simgrid::mc::State> const& state : stack_) {
 417     if (state == stack_.back())
 418       break;
 419
 420     int req_num                    = state->get_transition()->times_considered_;
 421     const s_smx_simcall* saved_req = &state->executed_req_;
 422     xbt_assert(saved_req);
 423
 424     /* because we got a copy of the executed request, we have to fetch the
 425        real one, pointed by the request field of the issuer process */
 426
 427     const smx_actor_t issuer = api::get().simcall_get_issuer(saved_req);
 428     smx_simcall_t req        = &issuer->simcall_;
 429
 430     /* TODO : handle test and testany simcalls */
 431     CallType call = MC_get_call_type(req);
 432     state->get_transition()->replay();
 433     extension->handle_comm_pattern(call, req, req_num, true);
 434
 435     /* Update statistics */
 436     api::get().mc_inc_visited_states();
 437   }
 438 }
 439
 440 void CommDetExtension::handle_comm_pattern(simgrid::mc::CallType call_type, smx_simcall_t req, int value,
 441                                            bool backtracking)
 442 {
 443   using simgrid::mc::CallType;
 444   switch(call_type) {
 445     case CallType::NONE:
 446       break;
 447     case CallType::SEND:
 448     case CallType::RECV:
 449       get_comm_pattern(req, call_type, backtracking);
 450       break;
 451     case CallType::WAIT:
 452     case CallType::WAITANY: {
 453       RemotePtr<simgrid::kernel::activity::CommImpl> comm_addr;
 454       if (call_type == CallType::WAIT)
 455         comm_addr = remote(simcall_comm_wait__getraw__comm(req));
 456       else
 457         comm_addr = api::get().get_comm_waitany_raw_addr(req, value);
 458       auto simcall_issuer = api::get().simcall_get_issuer(req);
 459       complete_comm_pattern(comm_addr, simcall_issuer->get_pid(), backtracking);
 460     } break;
 461   default:
 462     xbt_die("Unexpected call type %i", (int)call_type);
 463   }
 464 }
 465
 466 void CommunicationDeterminismChecker::real_run()
 467 {
 468   auto extension = this->extension<CommDetExtension>();
 469
 470   std::unique_ptr<VisitedState> visited_state = nullptr;
 471   const unsigned long maxpid                  = api::get().get_maxpid();
 472
 473   while (not stack_.empty()) {
 474     /* Get current state */
 475     State* cur_state = stack_.back().get();
 476
 477     XBT_DEBUG("**************************************************");
 478     XBT_DEBUG("Exploration depth = %zu (state = %ld, interleaved processes = %zu)", stack_.size(), cur_state->num_,
 479               cur_state->count_todo());
 480
 481     /* Update statistics */
 482     api::get().mc_inc_visited_states();
 483
 484     int next_transition = -1;
 485     if (stack_.size() <= (std::size_t)_sg_mc_max_depth)
 486       next_transition = cur_state->next_transition();
 487
 488     if (next_transition >= 0 && visited_state == nullptr) {
 489       cur_state->execute_next(next_transition);
 490
 491       int req_num       = cur_state->get_transition()->times_considered_;
 492       smx_simcall_t req = &cur_state->executed_req_;
 493
 494       XBT_DEBUG("Execute: %s", cur_state->get_transition()->to_string().c_str());
 495
 496       std::string req_str;
 497       if (dot_output != nullptr)
 498         req_str = api::get().request_get_dot_output(cur_state->get_transition());
 499
 500       /* TODO : handle test and testany simcalls */
 501       CallType call = CallType::NONE;
 502       if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
 503         call = MC_get_call_type(req);
 504
 505       extension->handle_comm_pattern(call, req, req_num, false);
 506
 507       /* Create the new expanded state */
 508       auto next_state = std::make_unique<State>();
 509       next_state->extension_set(new StateCommDet(extension));
 510
 511       bool all_communications_are_finished = true;
 512       for (size_t current_actor = 1; all_communications_are_finished && current_actor < maxpid; current_actor++) {
 513         if (not extension->incomplete_communications_pattern[current_actor].empty()) {
 514           XBT_DEBUG("Some communications are not finished, cannot stop the exploration! State not visited.");
 515           all_communications_are_finished = false;
 516         }
 517       }
 518
 519       /* If comm determinism verification, we cannot stop the exploration if some communications are not finished (at
 520        * least, data are transferred). These communications  are incomplete and they cannot be analyzed and compared
 521        * with the initial pattern. */
 522       bool compare_snapshots = extension->initial_communications_pattern_done && all_communications_are_finished;
 523
 524       if (_sg_mc_max_visited_states != 0)
 525         visited_state = visited_states_.addVisitedState(next_state->num_, next_state.get(), compare_snapshots);
 526       else
 527         visited_state = nullptr;
 528
 529       if (visited_state == nullptr) {
 530         /* Add all enabled actors to the interleave set of the next state */
 531         for (auto& act : api::get().get_actors()) {
 532           auto actor = act.copy.get_buffer();
 533           if (get_session().actor_is_enabled(actor->get_pid()))
 534             next_state->mark_todo(actor->get_pid());
 535         }
 536
 537         if (dot_output != nullptr)
 538           fprintf(dot_output, "\"%ld\" -> \"%ld\" [%s];\n", cur_state->num_, next_state->num_, req_str.c_str());
 539
 540       } else if (dot_output != nullptr)
 541         fprintf(dot_output, "\"%ld\" -> \"%ld\" [%s];\n", cur_state->num_,
 542                 visited_state->original_num == -1 ? visited_state->num : visited_state->original_num, req_str.c_str());
 543
 544       stack_.push_back(std::move(next_state));
 545     } else {
 546       if (stack_.size() > (std::size_t)_sg_mc_max_depth)
 547         XBT_WARN("/!\\ Max depth reached! /!\\ ");
 548       else if (visited_state != nullptr)
 549         XBT_DEBUG("State already visited (equal to state %ld), exploration stopped on this path.",
 550                   visited_state->original_num == -1 ? visited_state->num : visited_state->original_num);
 551       else
 552         XBT_DEBUG("There are no more processes to interleave. (depth %zu)", stack_.size());
 553
 554       extension->initial_communications_pattern_done = true;
 555
 556       /* Trash the current state, no longer needed */
 557       XBT_DEBUG("Delete state %ld at depth %zu", cur_state->num_, stack_.size());
 558       stack_.pop_back();
 559
 560       visited_state = nullptr;
 561
 562       api::get().mc_check_deadlock();
 563
 564       while (not stack_.empty()) {
 565         std::unique_ptr<State> state(std::move(stack_.back()));
 566         stack_.pop_back();
 567         if (state->count_todo() && stack_.size() < (std::size_t)_sg_mc_max_depth) {
 568           /* We found a back-tracking point, let's loop */
 569           XBT_DEBUG("Back-tracking to state %ld at depth %zu", state->num_, stack_.size() + 1);
 570           stack_.push_back(std::move(state));
 571
 572           this->restoreState();
 573
 574           XBT_DEBUG("Back-tracking to state %ld at depth %zu done", stack_.back()->num_, stack_.size());
 575
 576           break;
 577         } else {
 578           XBT_DEBUG("Delete state %ld at depth %zu", state->num_, stack_.size() + 1);
 579         }
 580       }
 581     }
 582   }
 583
 584   api::get().log_state();
 585 }
 586
 587 void CommunicationDeterminismChecker::run()
 588 {
 589   XBT_INFO("Check communication determinism");
 590   get_session().take_initial_snapshot();
 591
 592   this->prepare();
 593   this->real_run();
 594 }
 595
 596 Checker* create_communication_determinism_checker(Session* session)
 597 {
 598   return new CommunicationDeterminismChecker(session);
 599 }
 600
 601 } // namespace mc
 602 } // namespace simgrid