Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
503cbec3923aa53ed01ecf36e07821629829f5a8
[simgrid.git] / 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 }