Logo AND Algorithmique Numérique Distribuée

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