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