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