src/mc/checker/CommunicationDeterminismChecker.cpp

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