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