Logo AND Algorithmique Numérique Distribuée

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