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