Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
[mc] Rename the communication pattern types
[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
26 using simgrid::mc::remote;
27
28 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_comm_determinism, mc,
29                                 "Logging specific to MC communication determinism detection");
30
31 /********** Global variables **********/
32
33 xbt_dynar_t initial_communications_pattern;
34 xbt_dynar_t incomplete_communications_pattern;
35
36 /********** Static functions ***********/
37
38 static e_mc_comm_pattern_difference_t compare_comm_pattern(simgrid::mc::PatternCommunication* comm1, simgrid::mc::PatternCommunication* comm2) {
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 == SIMIX_COMM_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(simgrid::mc::PatternCommunication* comm_pattern, smx_synchro_t comm_addr)
95 {
96   s_smx_synchro_t comm;
97   mc_model_checker->process().read(&comm, remote(comm_addr));
98
99   smx_process_t src_proc = MC_smx_resolve_process(comm.comm.src_proc);
100   smx_process_t dst_proc = MC_smx_resolve_process(comm.comm.dst_proc);
101   comm_pattern->src_proc = src_proc->pid;
102   comm_pattern->dst_proc = dst_proc->pid;
103   comm_pattern->src_host = MC_smx_process_get_host_name(src_proc);
104   comm_pattern->dst_host = MC_smx_process_get_host_name(dst_proc);
105   if (comm_pattern->data.size() == 0 && comm.comm.src_buff != nullptr) {
106     size_t buff_size;
107     mc_model_checker->process().read(
108       &buff_size, remote(comm.comm.dst_buff_size));
109     comm_pattern->data.resize(buff_size);
110     mc_model_checker->process().read_bytes(
111       comm_pattern->data.data(), comm_pattern->data.size(),
112       remote(comm.comm.src_buff));
113   }
114 }
115
116 static void deterministic_comm_pattern(int process, simgrid::mc::PatternCommunication* comm, int backtracking) {
117
118   simgrid::mc::PatternCommunicationList* list =
119     xbt_dynar_get_as(initial_communications_pattern, process, simgrid::mc::PatternCommunicationList*);
120
121   if(!backtracking){
122     simgrid::mc::PatternCommunication* initial_comm =
123       xbt_dynar_get_as(list->list, list->index_comm, simgrid::mc::PatternCommunication*);
124     e_mc_comm_pattern_difference_t diff =
125       compare_comm_pattern(initial_comm, comm);
126
127     if (diff != NONE_DIFF) {
128       if (comm->type == SIMIX_COMM_SEND){
129         simgrid::mc::initial_global_state->send_deterministic = 0;
130         if(simgrid::mc::initial_global_state->send_diff != nullptr)
131           xbt_free(simgrid::mc::initial_global_state->send_diff);
132         simgrid::mc::initial_global_state->send_diff = print_determinism_result(diff, process, comm, list->index_comm + 1);
133       }else{
134         simgrid::mc::initial_global_state->recv_deterministic = 0;
135         if(simgrid::mc::initial_global_state->recv_diff != nullptr)
136           xbt_free(simgrid::mc::initial_global_state->recv_diff);
137         simgrid::mc::initial_global_state->recv_diff = print_determinism_result(diff, process, comm, list->index_comm + 1);
138       }
139       if(_sg_mc_send_determinism && !simgrid::mc::initial_global_state->send_deterministic){
140         XBT_INFO("*********************************************************");
141         XBT_INFO("***** Non-send-deterministic communications pattern *****");
142         XBT_INFO("*********************************************************");
143         XBT_INFO("%s", simgrid::mc::initial_global_state->send_diff);
144         xbt_free(simgrid::mc::initial_global_state->send_diff);
145         simgrid::mc::initial_global_state->send_diff = nullptr;
146         MC_print_statistics(mc_stats);
147         mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
148       }else if(_sg_mc_comms_determinism
149           && (!simgrid::mc::initial_global_state->send_deterministic
150             && !simgrid::mc::initial_global_state->recv_deterministic)) {
151         XBT_INFO("****************************************************");
152         XBT_INFO("***** Non-deterministic communications pattern *****");
153         XBT_INFO("****************************************************");
154         XBT_INFO("%s", simgrid::mc::initial_global_state->send_diff);
155         XBT_INFO("%s", simgrid::mc::initial_global_state->recv_diff);
156         xbt_free(simgrid::mc::initial_global_state->send_diff);
157         simgrid::mc::initial_global_state->send_diff = nullptr;
158         xbt_free(simgrid::mc::initial_global_state->recv_diff);
159         simgrid::mc::initial_global_state->recv_diff = nullptr;
160         MC_print_statistics(mc_stats);
161         mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
162       }
163     }
164   }
165
166   delete comm;
167
168 }
169
170 /********** Non Static functions ***********/
171
172 void MC_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   simgrid::mc::PatternCommunication* pattern = new simgrid::mc::PatternCommunication();
181   pattern->index =
182     initial_pattern->index_comm + xbt_dynar_length(incomplete_pattern);
183
184   if (call_type == MC_CALL_TYPE_SEND) {
185     /* Create comm pattern */
186     pattern->type = SIMIX_COMM_SEND;
187     pattern->comm_addr = simcall_comm_isend__get__result(request);
188
189     s_smx_synchro_t synchro = mc_model_checker->process().read<s_smx_synchro_t>(
190       (std::uint64_t) pattern->comm_addr);
191
192     char* remote_name = mc_model_checker->process().read<char*>(
193       (std::uint64_t)(synchro.comm.rdv ? &synchro.comm.rdv->name : &synchro.comm.rdv_cpy->name));
194     pattern->rdv = mc_model_checker->process().read_string(remote_name);
195     pattern->src_proc = MC_smx_resolve_process(synchro.comm.src_proc)->pid;
196     pattern->src_host = MC_smx_process_get_host_name(issuer);
197
198     struct s_smpi_mpi_request mpi_request =
199       mc_model_checker->process().read<s_smpi_mpi_request>(
200         (std::uint64_t) simcall_comm_isend__get__data(request));
201     pattern->tag = mpi_request.tag;
202
203     if(synchro.comm.src_buff != nullptr){
204       pattern->data.resize(synchro.comm.src_buff_size);
205       mc_model_checker->process().read_bytes(
206         pattern->data.data(), pattern->data.size(),
207         remote(synchro.comm.src_buff));
208     }
209     if(mpi_request.detached){
210       if (!simgrid::mc::initial_global_state->initial_communications_pattern_done) {
211         /* Store comm pattern */
212         xbt_dynar_push(
213           xbt_dynar_get_as(
214             initial_communications_pattern, pattern->src_proc, simgrid::mc::PatternCommunicationList*
215           )->list,
216           &pattern);
217       } else {
218         /* Evaluate comm determinism */
219         deterministic_comm_pattern(pattern->src_proc, pattern, backtracking);
220         xbt_dynar_get_as(
221           initial_communications_pattern, pattern->src_proc, simgrid::mc::PatternCommunicationList*
222         )->index_comm++;
223       }
224       return;
225     }
226   } else if (call_type == MC_CALL_TYPE_RECV) {
227     pattern->type = SIMIX_COMM_RECEIVE;
228     pattern->comm_addr = simcall_comm_irecv__get__result(request);
229
230     struct s_smpi_mpi_request mpi_request;
231     mc_model_checker->process().read(
232       &mpi_request, remote((struct s_smpi_mpi_request*)simcall_comm_irecv__get__data(request)));
233     pattern->tag = mpi_request.tag;
234
235     s_smx_synchro_t synchro;
236     mc_model_checker->process().read(&synchro, remote(pattern->comm_addr));
237
238     char* remote_name;
239     mc_model_checker->process().read(&remote_name,
240       remote(synchro.comm.rdv ? &synchro.comm.rdv->name : &synchro.comm.rdv_cpy->name));
241     pattern->rdv = mc_model_checker->process().read_string(remote_name);
242     pattern->dst_proc = MC_smx_resolve_process(synchro.comm.dst_proc)->pid;
243     pattern->dst_host = MC_smx_process_get_host_name(issuer);
244   } else
245     xbt_die("Unexpected call_type %i", (int) call_type);
246
247   xbt_dynar_push(
248     xbt_dynar_get_as(incomplete_communications_pattern, issuer->pid, xbt_dynar_t),
249     &pattern);
250
251   XBT_DEBUG("Insert incomplete comm pattern %p for process %lu", pattern, issuer->pid);
252 }
253
254 void MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigned int issuer, int backtracking) {
255   simgrid::mc::PatternCommunication* current_comm_pattern;
256   unsigned int cursor = 0;
257   simgrid::mc::PatternCommunication* comm_pattern;
258   int completed = 0;
259
260   /* Complete comm pattern */
261   xbt_dynar_foreach(xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t), cursor, current_comm_pattern)
262     if (current_comm_pattern->comm_addr == comm_addr) {
263       update_comm_pattern(current_comm_pattern, comm_addr);
264       completed = 1;
265       xbt_dynar_remove_at(
266         xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t),
267         cursor, &comm_pattern);
268       XBT_DEBUG("Remove incomplete comm pattern for process %u at cursor %u", issuer, cursor);
269       break;
270     }
271
272   if(!completed)
273     xbt_die("Corresponding communication not found!");
274
275   simgrid::mc::PatternCommunicationList* pattern = xbt_dynar_get_as(
276     initial_communications_pattern, issuer, simgrid::mc::PatternCommunicationList*);
277
278   if (!simgrid::mc::initial_global_state->initial_communications_pattern_done)
279     /* Store comm pattern */
280     xbt_dynar_push(pattern->list, &comm_pattern);
281   else {
282     /* Evaluate comm determinism */
283     deterministic_comm_pattern(issuer, comm_pattern, backtracking);
284     pattern->index_comm++;
285   }
286 }
287
288
289 /************************ Main algorithm ************************/
290
291 namespace simgrid {
292 namespace mc {
293
294 CommunicationDeterminismChecker::CommunicationDeterminismChecker(Session& session)
295   : Checker(session)
296 {
297
298 }
299
300 CommunicationDeterminismChecker::~CommunicationDeterminismChecker()
301 {
302
303 }
304
305 // TODO, deduplicate with SafetyChecker
306 RecordTrace CommunicationDeterminismChecker::getRecordTrace() // override
307 {
308   RecordTrace res;
309   for (auto const& state : stack_) {
310     int value = 0;
311     smx_simcall_t saved_req = MC_state_get_executed_request(state.get(), &value);
312     const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
313     const int pid = issuer->pid;
314     res.push_back(RecordTraceElement(pid, value));
315   }
316   return res;
317 }
318
319 // TODO, deduplicate with SafetyChecker
320 std::vector<std::string> CommunicationDeterminismChecker::getTextualTrace() // override
321 {
322   std::vector<std::string> trace;
323   for (auto const& state : stack_) {
324     int value;
325     smx_simcall_t req = MC_state_get_executed_request(state.get(), &value);
326     if (req)
327       trace.push_back(simgrid::mc::request_to_string(
328         req, value, simgrid::mc::RequestType::executed));
329   }
330   return trace;
331 }
332
333 void CommunicationDeterminismChecker::prepare()
334 {
335
336   int i;
337   const int maxpid = MC_smx_get_maxpid();
338
339   // Create initial_communications_pattern elements:
340   initial_communications_pattern = simgrid::xbt::newDeleteDynar<simgrid::mc::PatternCommunicationList*>();
341   for (i=0; i < maxpid; i++){
342     simgrid::mc::PatternCommunicationList* process_list_pattern = new simgrid::mc::PatternCommunicationList();
343     process_list_pattern->list = simgrid::xbt::newDeleteDynar<simgrid::mc::PatternCommunication>();
344     process_list_pattern->index_comm = 0;
345     xbt_dynar_insert_at(initial_communications_pattern, i, &process_list_pattern);
346   }
347
348   // Create incomplete_communications_pattern elements:
349   incomplete_communications_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp);
350   for (i=0; i < maxpid; i++){
351     xbt_dynar_t process_pattern = xbt_dynar_new(sizeof(simgrid::mc::PatternCommunication*), nullptr);
352     xbt_dynar_insert_at(incomplete_communications_pattern, i, &process_pattern);
353   }
354
355   std::unique_ptr<simgrid::mc::State> initial_state =
356     std::unique_ptr<simgrid::mc::State>(MC_state_new());
357
358   XBT_DEBUG("********* Start communication determinism verification *********");
359
360   /* Wait for requests (schedules processes) */
361   mc_model_checker->wait_for_requests();
362
363   /* Get an enabled process and insert it in the interleave set of the initial state */
364   for (auto& p : mc_model_checker->process().simix_processes())
365     if (simgrid::mc::process_is_enabled(&p.copy))
366       MC_state_interleave_process(initial_state.get(), &p.copy);
367
368   stack_.push_back(std::move(initial_state));
369 }
370
371 static inline
372 bool all_communications_are_finished()
373 {
374   for (size_t current_process = 1; current_process < MC_smx_get_maxpid(); current_process++) {
375     xbt_dynar_t pattern = xbt_dynar_get_as(
376       incomplete_communications_pattern, current_process, xbt_dynar_t);
377     if (!xbt_dynar_is_empty(pattern)) {
378       XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
379       return false;
380     }
381   }
382   return true;
383 }
384
385 int CommunicationDeterminismChecker::main(void)
386 {
387   int value;
388   std::unique_ptr<simgrid::mc::VisitedState> visited_state = nullptr;
389   smx_simcall_t req = nullptr;
390
391   while (!stack_.empty()) {
392
393     /* Get current state */
394     simgrid::mc::State* state = stack_.back().get();
395
396     XBT_DEBUG("**************************************************");
397     XBT_DEBUG("Exploration depth = %zi (state = %d, interleaved processes = %zd)",
398               stack_.size(), state->num,
399               state->interleaveSize());
400
401     /* Update statistics */
402     mc_stats->visited_states++;
403
404     if (stack_.size() <= (std::size_t) _sg_mc_max_depth
405         && (req = MC_state_get_request(state, &value))
406         && (visited_state == nullptr)) {
407
408       XBT_DEBUG("Execute: %s",
409         simgrid::mc::request_to_string(
410           req, value, simgrid::mc::RequestType::simix).c_str());
411
412       std::string req_str;
413       if (dot_output != nullptr)
414         req_str = simgrid::mc::request_get_dot_output(req, value);
415
416       MC_state_set_executed_request(state, req, value);
417       mc_stats->executed_transitions++;
418
419       /* TODO : handle test and testany simcalls */
420       e_mc_call_type_t call = MC_CALL_TYPE_NONE;
421       if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
422         call = MC_get_call_type(req);
423
424       /* Answer the request */
425       simgrid::mc::handle_simcall(req, value);    /* After this call req is no longer useful */
426
427       if(!initial_global_state->initial_communications_pattern_done)
428         MC_handle_comm_pattern(call, req, value, initial_communications_pattern, 0);
429       else
430         MC_handle_comm_pattern(call, req, value, nullptr, 0);
431
432       /* Wait for requests (schedules processes) */
433       mc_model_checker->wait_for_requests();
434
435       /* Create the new expanded state */
436       std::unique_ptr<simgrid::mc::State> next_state =
437         std::unique_ptr<simgrid::mc::State>(MC_state_new());
438
439       /* If comm determinism verification, we cannot stop the exploration if
440          some communications are not finished (at least, data are transfered).
441          These communications  are incomplete and they cannot be analyzed and
442          compared with the initial pattern. */
443       bool compare_snapshots = all_communications_are_finished()
444         && initial_global_state->initial_communications_pattern_done;
445
446       if (_sg_mc_visited == 0
447           || (visited_state = visitedStates_.addVisitedState(next_state.get(), compare_snapshots)) == nullptr) {
448
449         /* Get enabled processes and insert them in the interleave set of the next state */
450         for (auto& p : mc_model_checker->process().simix_processes())
451           if (simgrid::mc::process_is_enabled(&p.copy))
452             MC_state_interleave_process(next_state.get(), &p.copy);
453
454         if (dot_output != nullptr)
455           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
456             state->num,  next_state->num, req_str.c_str());
457
458       } else if (dot_output != nullptr)
459         fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
460           state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str.c_str());
461
462       stack_.push_back(std::move(next_state));
463
464     } else {
465
466       if (stack_.size() > (std::size_t) _sg_mc_max_depth)
467         XBT_WARN("/!\\ Max depth reached ! /!\\ ");
468       else if (visited_state != nullptr)
469         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);
470       else
471         XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
472           stack_.size());
473
474       if (!initial_global_state->initial_communications_pattern_done)
475         initial_global_state->initial_communications_pattern_done = 1;
476
477       /* Trash the current state, no longer needed */
478       XBT_DEBUG("Delete state %d at depth %zi",
479         state->num, stack_.size());
480       stack_.pop_back();
481
482       visited_state = nullptr;
483
484       /* Check for deadlocks */
485       if (mc_model_checker->checkDeadlock()) {
486         MC_show_deadlock();
487         return SIMGRID_MC_EXIT_DEADLOCK;
488       }
489
490       while (!stack_.empty()) {
491         std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
492         stack_.pop_back();
493         if (state->interleaveSize()
494             && stack_.size() < (std::size_t) _sg_mc_max_depth) {
495           /* We found a back-tracking point, let's loop */
496           XBT_DEBUG("Back-tracking to state %d at depth %zi",
497             state->num, stack_.size() + 1);
498           stack_.push_back(std::move(state));
499
500           simgrid::mc::replay(stack_);
501
502           XBT_DEBUG("Back-tracking to state %d at depth %zi done",
503             stack_.back()->num, stack_.size());
504
505           break;
506         } else {
507           XBT_DEBUG("Delete state %d at depth %zi",
508             state->num, stack_.size() + 1);
509         }
510       }
511     }
512   }
513
514   MC_print_statistics(mc_stats);
515   return SIMGRID_MC_EXIT_SUCCESS;
516 }
517
518 int CommunicationDeterminismChecker::run()
519 {
520   XBT_INFO("Check communication determinism");
521   mc_model_checker->wait_for_requests();
522
523   this->prepare();
524
525   initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
526   initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
527   initial_global_state->initial_communications_pattern_done = 0;
528   initial_global_state->recv_deterministic = 1;
529   initial_global_state->send_deterministic = 1;
530   initial_global_state->recv_diff = nullptr;
531   initial_global_state->send_diff = nullptr;
532
533   int res = this->main();
534   initial_global_state = nullptr;
535   return res;
536 }
537
538 Checker* createCommunicationDeterminismChecker(Session& session)
539 {
540   return new CommunicationDeterminismChecker(session);
541 }
542
543 }
544 }