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.data());
 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.data());
 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 =
 251       static_cast<simgrid::simix::Comm*>(temp_comm.data());
 252
 253     char* remote_name;
 254     mc_model_checker->process().read(&remote_name,
 255       remote(comm->mbox ? &comm->mbox->name : &comm->mbox_cpy->name));
 256     pattern->rdv = mc_model_checker->process().read_string(remote_name);
 257     pattern->dst_proc = mc_model_checker->process().resolveProcess(
 258       simgrid::mc::remote(comm->dst_proc))->pid;
 259     pattern->dst_host = MC_smx_process_get_host_name(issuer);
 260   } else
 261     xbt_die("Unexpected call_type %i", (int) call_type);
 262
 263   XBT_DEBUG("Insert incomplete comm pattern %p for process %lu",
 264     pattern.get(), issuer->pid);
 265   xbt_dynar_t dynar =
 266     xbt_dynar_get_as(incomplete_communications_pattern, issuer->pid, xbt_dynar_t);
 267   simgrid::mc::PatternCommunication* pattern2 = pattern.release();
 268   xbt_dynar_push(dynar, &pattern2);
 269 }
 270
 271
 272 void CommunicationDeterminismChecker::complete_comm_pattern(
 273   xbt_dynar_t list, simgrid::mc::RemotePtr<simgrid::simix::Comm> comm_addr,
 274   unsigned int issuer, int backtracking)
 275 {
 276   simgrid::mc::PatternCommunication* current_comm_pattern;
 277   unsigned int cursor = 0;
 278   std::unique_ptr<simgrid::mc::PatternCommunication> comm_pattern;
 279   int completed = 0;
 280
 281   /* Complete comm pattern */
 282   xbt_dynar_foreach(xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t), cursor, current_comm_pattern)
 283     if (remote(current_comm_pattern->comm_addr) == comm_addr) {
 284       update_comm_pattern(current_comm_pattern, comm_addr);
 285       completed = 1;
 286       simgrid::mc::PatternCommunication* temp;
 287       xbt_dynar_remove_at(
 288         xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t),
 289         cursor, &temp);
 290       comm_pattern = std::unique_ptr<simgrid::mc::PatternCommunication>(temp);
 291       XBT_DEBUG("Remove incomplete comm pattern for process %u at cursor %u", issuer, cursor);
 292       break;
 293     }
 294
 295   if(!completed)
 296     xbt_die("Corresponding communication not found!");
 297
 298   simgrid::mc::PatternCommunicationList* pattern = xbt_dynar_get_as(
 299     initial_communications_pattern, issuer, simgrid::mc::PatternCommunicationList*);
 300
 301   if (!this->initial_communications_pattern_done)
 302     /* Store comm pattern */
 303     pattern->list.push_back(std::move(comm_pattern));
 304   else {
 305     /* Evaluate comm determinism */
 306     this->deterministic_comm_pattern(issuer, comm_pattern.get(), backtracking);
 307     pattern->index_comm++;
 308   }
 309 }
 310
 311 CommunicationDeterminismChecker::CommunicationDeterminismChecker(Session& session)
 312   : Checker(session)
 313 {
 314
 315 }
 316
 317 CommunicationDeterminismChecker::~CommunicationDeterminismChecker()
 318 {
 319
 320 }
 321
 322 RecordTrace CommunicationDeterminismChecker::getRecordTrace() // override
 323 {
 324   RecordTrace res;
 325   for (auto const& state : stack_)
 326     res.push_back(state->getTransition());
 327   return res;
 328 }
 329
 330 std::vector<std::string> CommunicationDeterminismChecker::getTextualTrace() // override
 331 {
 332   std::vector<std::string> trace;
 333   for (auto const& state : stack_) {
 334     smx_simcall_t req = &state->executed_req;
 335     if (req)
 336       trace.push_back(simgrid::mc::request_to_string(
 337         req, state->transition.argument, simgrid::mc::RequestType::executed));
 338   }
 339   return trace;
 340 }
 341
 342 void CommunicationDeterminismChecker::logState() // override
 343 {
 344   Checker::logState();
 345   if (_sg_mc_comms_determinism &&
 346       !this->recv_deterministic &&
 347       this->send_deterministic) {
 348     XBT_INFO("******************************************************");
 349     XBT_INFO("**** Only-send-deterministic communication pattern ****");
 350     XBT_INFO("******************************************************");
 351     XBT_INFO("%s", this->recv_diff);
 352   } else if(_sg_mc_comms_determinism &&
 353       !this->send_deterministic &&
 354       this->recv_deterministic) {
 355     XBT_INFO("******************************************************");
 356     XBT_INFO("**** Only-recv-deterministic communication pattern ****");
 357     XBT_INFO("******************************************************");
 358     XBT_INFO("%s", this->send_diff);
 359   }
 360   XBT_INFO("Expanded states = %lu", expandedStatesCount_);
 361   XBT_INFO("Visited states = %lu", mc_model_checker->visited_states);
 362   XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions);
 363   XBT_INFO("Send-deterministic : %s", !this->send_deterministic ? "No" : "Yes");
 364   if (_sg_mc_comms_determinism)
 365     XBT_INFO("Recv-deterministic : %s",
 366       !this->recv_deterministic ? "No" : "Yes");
 367 }
 368
 369 void CommunicationDeterminismChecker::prepare()
 370 {
 371
 372   int i;
 373   const int maxpid = MC_smx_get_maxpid();
 374
 375   // Create initial_communications_pattern elements:
 376   initial_communications_pattern = simgrid::xbt::newDeleteDynar<simgrid::mc::PatternCommunicationList*>();
 377   for (i=0; i < maxpid; i++){
 378     simgrid::mc::PatternCommunicationList* process_list_pattern = new simgrid::mc::PatternCommunicationList();
 379     xbt_dynar_insert_at(initial_communications_pattern, i, &process_list_pattern);
 380   }
 381
 382   // Create incomplete_communications_pattern elements:
 383   incomplete_communications_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp);
 384   for (i=0; i < maxpid; i++){
 385     xbt_dynar_t process_pattern = xbt_dynar_new(sizeof(simgrid::mc::PatternCommunication*), nullptr);
 386     xbt_dynar_insert_at(incomplete_communications_pattern, i, &process_pattern);
 387   }
 388
 389   std::unique_ptr<simgrid::mc::State> initial_state =
 390     std::unique_ptr<simgrid::mc::State>(MC_state_new(++expandedStatesCount_));
 391
 392   XBT_DEBUG("********* Start communication determinism verification *********");
 393
 394   /* Get an enabled process and insert it in the interleave set of the initial state */
 395   for (auto& p : mc_model_checker->process().simix_processes())
 396     if (simgrid::mc::process_is_enabled(&p.copy))
 397       initial_state->interleave(&p.copy);
 398
 399   stack_.push_back(std::move(initial_state));
 400 }
 401
 402 static inline
 403 bool all_communications_are_finished()
 404 {
 405   for (size_t current_process = 1; current_process < MC_smx_get_maxpid(); current_process++) {
 406     xbt_dynar_t pattern = xbt_dynar_get_as(
 407       incomplete_communications_pattern, current_process, xbt_dynar_t);
 408     if (!xbt_dynar_is_empty(pattern)) {
 409       XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
 410       return false;
 411     }
 412   }
 413   return true;
 414 }
 415
 416 void CommunicationDeterminismChecker::restoreState()
 417 {
 418   /* Intermediate backtracking */
 419   {
 420     simgrid::mc::State* state = stack_.back().get();
 421     if (state->system_state) {
 422       simgrid::mc::restore_snapshot(state->system_state);
 423       MC_restore_communications_pattern(state);
 424       return;
 425     }
 426   }
 427
 428   /* Restore the initial state */
 429   simgrid::mc::session->restoreInitialState();
 430
 431   // int n = xbt_dynar_length(incomplete_communications_pattern);
 432   unsigned n = MC_smx_get_maxpid();
 433   assert(n == xbt_dynar_length(incomplete_communications_pattern));
 434   assert(n == xbt_dynar_length(initial_communications_pattern));
 435   for (unsigned j=0; j < n ; j++) {
 436     xbt_dynar_reset((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, j, xbt_dynar_t));
 437     xbt_dynar_get_as(initial_communications_pattern, j, simgrid::mc::PatternCommunicationList*)->index_comm = 0;
 438   }
 439
 440   /* Traverse the stack from the state at position start and re-execute the transitions */
 441   for (std::unique_ptr<simgrid::mc::State> const& state : stack_) {
 442     if (state == stack_.back())
 443       break;
 444
 445     int req_num = state->transition.argument;
 446     smx_simcall_t saved_req = &state->executed_req;
 447     xbt_assert(saved_req);
 448
 449     /* because we got a copy of the executed request, we have to fetch the
 450        real one, pointed by the request field of the issuer process */
 451
 452     const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
 453     smx_simcall_t req = &issuer->simcall;
 454
 455     /* TODO : handle test and testany simcalls */
 456     e_mc_call_type_t call = MC_get_call_type(req);
 457     mc_model_checker->handle_simcall(state->transition);
 458     MC_handle_comm_pattern(call, req, req_num, nullptr, 1);
 459     mc_model_checker->wait_for_requests();
 460
 461     /* Update statistics */
 462     mc_model_checker->visited_states++;
 463     mc_model_checker->executed_transitions++;
 464   }
 465 }
 466
 467 int CommunicationDeterminismChecker::main(void)
 468 {
 469   std::unique_ptr<simgrid::mc::VisitedState> visited_state = nullptr;
 470   smx_simcall_t req = nullptr;
 471
 472   while (!stack_.empty()) {
 473
 474     /* Get current state */
 475     simgrid::mc::State* state = stack_.back().get();
 476
 477     XBT_DEBUG("**************************************************");
 478     XBT_DEBUG("Exploration depth = %zi (state = %d, interleaved processes = %zd)",
 479               stack_.size(), state->num,
 480               state->interleaveSize());
 481
 482     /* Update statistics */
 483     mc_model_checker->visited_states++;
 484
 485     if (stack_.size() <= (std::size_t) _sg_mc_max_depth
 486         && (req = MC_state_get_request(state)) != nullptr
 487         && (visited_state == nullptr)) {
 488
 489       int req_num = state->transition.argument;
 490
 491       XBT_DEBUG("Execute: %s",
 492         simgrid::mc::request_to_string(
 493           req, req_num, simgrid::mc::RequestType::simix).c_str());
 494
 495       std::string req_str;
 496       if (dot_output != nullptr)
 497         req_str = simgrid::mc::request_get_dot_output(req, req_num);
 498
 499       mc_model_checker->executed_transitions++;
 500
 501       /* TODO : handle test and testany simcalls */
 502       e_mc_call_type_t call = MC_CALL_TYPE_NONE;
 503       if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
 504         call = MC_get_call_type(req);
 505
 506       /* Answer the request */
 507       mc_model_checker->handle_simcall(state->transition);
 508       /* After this call req is no longer useful */
 509
 510       if (!this->initial_communications_pattern_done)
 511         MC_handle_comm_pattern(call, req, req_num, initial_communications_pattern, 0);
 512       else
 513         MC_handle_comm_pattern(call, req, req_num, nullptr, 0);
 514
 515       /* Wait for requests (schedules processes) */
 516       mc_model_checker->wait_for_requests();
 517
 518       /* Create the new expanded state */
 519       std::unique_ptr<simgrid::mc::State> next_state =
 520         std::unique_ptr<simgrid::mc::State>(MC_state_new(++expandedStatesCount_));
 521
 522       /* If comm determinism verification, we cannot stop the exploration if
 523          some communications are not finished (at least, data are transfered).
 524          These communications  are incomplete and they cannot be analyzed and
 525          compared with the initial pattern. */
 526       bool compare_snapshots = all_communications_are_finished()
 527         && this->initial_communications_pattern_done;
 528
 529       if (_sg_mc_visited == 0
 530           || (visited_state = visitedStates_.addVisitedState(
 531             expandedStatesCount_, next_state.get(), compare_snapshots)) == nullptr) {
 532
 533         /* Get enabled processes and insert them in the interleave set of the next state */
 534         for (auto& p : mc_model_checker->process().simix_processes())
 535           if (simgrid::mc::process_is_enabled(&p.copy))
 536             next_state->interleave(&p.copy);
 537
 538         if (dot_output != nullptr)
 539           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
 540             state->num,  next_state->num, req_str.c_str());
 541
 542       } else if (dot_output != nullptr)
 543         fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
 544           state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str.c_str());
 545
 546       stack_.push_back(std::move(next_state));
 547
 548     } else {
 549
 550       if (stack_.size() > (std::size_t) _sg_mc_max_depth)
 551         XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 552       else if (visited_state != nullptr)
 553         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);
 554       else
 555         XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
 556           stack_.size());
 557
 558       if (!this->initial_communications_pattern_done)
 559         this->initial_communications_pattern_done = 1;
 560
 561       /* Trash the current state, no longer needed */
 562       XBT_DEBUG("Delete state %d at depth %zi",
 563         state->num, stack_.size());
 564       stack_.pop_back();
 565
 566       visited_state = nullptr;
 567
 568       /* Check for deadlocks */
 569       if (mc_model_checker->checkDeadlock()) {
 570         MC_show_deadlock();
 571         return SIMGRID_MC_EXIT_DEADLOCK;
 572       }
 573
 574       while (!stack_.empty()) {
 575         std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
 576         stack_.pop_back();
 577         if (state->interleaveSize()
 578             && stack_.size() < (std::size_t) _sg_mc_max_depth) {
 579           /* We found a back-tracking point, let's loop */
 580           XBT_DEBUG("Back-tracking to state %d at depth %zi",
 581             state->num, stack_.size() + 1);
 582           stack_.push_back(std::move(state));
 583
 584           this->restoreState();
 585
 586           XBT_DEBUG("Back-tracking to state %d at depth %zi done",
 587             stack_.back()->num, stack_.size());
 588
 589           break;
 590         } else {
 591           XBT_DEBUG("Delete state %d at depth %zi",
 592             state->num, stack_.size() + 1);
 593         }
 594       }
 595     }
 596   }
 597
 598   simgrid::mc::session->logState();
 599   return SIMGRID_MC_EXIT_SUCCESS;
 600 }
 601
 602 int CommunicationDeterminismChecker::run()
 603 {
 604   XBT_INFO("Check communication determinism");
 605   simgrid::mc::session->initialize();
 606
 607   this->prepare();
 608
 609   this->initial_communications_pattern_done = 0;
 610   this->recv_deterministic = 1;
 611   this->send_deterministic = 1;
 612   this->recv_diff = nullptr;
 613   this->send_diff = nullptr;
 614
 615   int res = this->main();
 616   return res;
 617 }
 618
 619 Checker* createCommunicationDeterminismChecker(Session& session)
 620 {
 621   return new CommunicationDeterminismChecker(session);
 622 }
 623
 624 }
 625 }