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