src/mc/CommunicationDeterminismChecker.cpp

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