Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
d5b086ce2fb9d66b69f6d6bddaf1490ca013e4d0
[simgrid.git] / src / mc / mc_comm_determinism.c
1 /* Copyright (c) 2008-2014. 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 "mc_private.h"
8
9 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_comm_determinism, mc,
10                                 "Logging specific to MC communication determinism detection");
11
12 /********** Global variables **********/
13
14 xbt_dynar_t initial_communications_pattern;
15 xbt_dynar_t incomplete_communications_pattern;
16 xbt_dynar_t communications_pattern;
17 int nb_comm_pattern;
18
19 /********** Static functions ***********/
20
21 static void comm_pattern_free(mc_comm_pattern_t p)
22 {
23   xbt_free(p->rdv);
24   xbt_free(p->data);
25   xbt_free(p);
26   p = NULL;
27 }
28
29 static void comm_pattern_free_voidp(void *p)
30 {
31   comm_pattern_free((mc_comm_pattern_t) * (void **) p);
32 }
33
34 static mc_comm_pattern_t get_comm_pattern_from_idx(xbt_dynar_t pattern,
35                                                    unsigned int *idx,
36                                                    e_smx_comm_type_t type,
37                                                    unsigned long proc)
38 {
39   mc_comm_pattern_t current_comm;
40   while (*idx < xbt_dynar_length(pattern)) {
41     current_comm =
42         (mc_comm_pattern_t) xbt_dynar_get_as(pattern, *idx, mc_comm_pattern_t);
43     if (current_comm->type == type && type == SIMIX_COMM_SEND) {
44       if (current_comm->src_proc == proc)
45         return current_comm;
46     } else if (current_comm->type == type && type == SIMIX_COMM_RECEIVE) {
47       if (current_comm->dst_proc == proc)
48         return current_comm;
49     }
50     (*idx)++;
51   }
52   return NULL;
53 }
54
55 static int compare_comm_pattern(mc_comm_pattern_t comm1,
56                                 mc_comm_pattern_t comm2)
57 {
58   if (strcmp(comm1->rdv, comm2->rdv) != 0)
59     return 1;
60   if (comm1->src_proc != comm2->src_proc)
61     return 1;
62   if (comm1->dst_proc != comm2->dst_proc)
63     return 1;
64   if (comm1->data_size != comm2->data_size)
65     return 1;
66   if (memcmp(comm1->data, comm2->data, comm1->data_size) != 0)
67     return 1;
68   return 0;
69 }
70
71 static void deterministic_pattern(xbt_dynar_t initial_pattern,
72                                   xbt_dynar_t pattern)
73 {
74
75   if (!xbt_dynar_is_empty(incomplete_communications_pattern))
76     xbt_die
77         ("Damn ! Some communications are incomplete that means one or several simcalls are not handle ... ");
78
79   unsigned int cursor = 0, send_index = 0, recv_index = 0;
80   mc_comm_pattern_t comm1, comm2;
81   int comm_comparison = 0;
82   int current_process = 0;
83   while (current_process < simix_process_maxpid) {
84     while (cursor < xbt_dynar_length(initial_pattern)) {
85       comm1 =
86           (mc_comm_pattern_t) xbt_dynar_get_as(initial_pattern, cursor,
87                                                mc_comm_pattern_t);
88       if (comm1->type == SIMIX_COMM_SEND && comm1->src_proc == current_process) {
89         comm2 =
90             get_comm_pattern_from_idx(pattern, &send_index, comm1->type,
91                                       current_process);
92         comm_comparison = compare_comm_pattern(comm1, comm2);
93         if (comm_comparison == 1) {
94           initial_global_state->send_deterministic = 0;
95           initial_global_state->comm_deterministic = 0;
96           return;
97         }
98         send_index++;
99       } else if (comm1->type == SIMIX_COMM_RECEIVE
100                  && comm1->dst_proc == current_process) {
101         comm2 =
102             get_comm_pattern_from_idx(pattern, &recv_index, comm1->type,
103                                       current_process);
104         comm_comparison = compare_comm_pattern(comm1, comm2);
105         if (comm_comparison == 1) {
106           initial_global_state->comm_deterministic = 0;
107           if (!_sg_mc_send_determinism)
108             return;
109         }
110         recv_index++;
111       }
112       cursor++;
113     }
114     cursor = 0;
115     send_index = 0;
116     recv_index = 0;
117     current_process++;
118   }
119 }
120
121 static void print_communications_pattern(xbt_dynar_t comms_pattern)
122 {
123   unsigned int cursor = 0;
124   mc_comm_pattern_t current_comm;
125   xbt_dynar_foreach(comms_pattern, cursor, current_comm) {
126     if (current_comm->type == SIMIX_COMM_SEND)
127       XBT_INFO("[(%lu) %s -> (%lu) %s] %s ", current_comm->src_proc,
128                current_comm->src_host, current_comm->dst_proc,
129                current_comm->dst_host, "iSend");
130     else
131       XBT_INFO("[(%lu) %s <- (%lu) %s] %s ", current_comm->dst_proc,
132                current_comm->dst_host, current_comm->src_proc,
133                current_comm->src_host, "iRecv");
134   }
135 }
136
137
138 /********** Non Static functions ***********/
139
140 void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, int call)
141 {
142   mc_comm_pattern_t pattern = NULL;
143   pattern = xbt_new0(s_mc_comm_pattern_t, 1);
144   pattern->num = ++nb_comm_pattern;
145   pattern->data_size = -1;
146   void *addr_pointed;
147   if (call == 1) {              // ISEND
148     pattern->comm = simcall_comm_isend__get__result(request);
149     pattern->type = SIMIX_COMM_SEND;
150     pattern->src_proc = pattern->comm->comm.src_proc->pid;
151     pattern->src_host = simcall_host_get_name(request->issuer->smx_host);
152     pattern->data_size = pattern->comm->comm.src_buff_size;
153     pattern->data = xbt_malloc0(pattern->data_size);
154     addr_pointed = *(void **) pattern->comm->comm.src_buff;
155     if (addr_pointed > std_heap
156         && addr_pointed < ((xbt_mheap_t) std_heap)->breakval)
157       memcpy(pattern->data, addr_pointed, pattern->data_size);
158     else
159       memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size);
160   } else {                      // IRECV
161     pattern->comm = simcall_comm_irecv__get__result(request);
162     pattern->type = SIMIX_COMM_RECEIVE;
163     pattern->dst_proc = pattern->comm->comm.dst_proc->pid;
164     pattern->dst_host =
165         simcall_host_get_name(pattern->comm->comm.dst_proc->smx_host);
166   }
167
168   if (pattern->comm->comm.rdv != NULL)
169     pattern->rdv = strdup(pattern->comm->comm.rdv->name);
170   else
171     pattern->rdv = strdup(pattern->comm->comm.rdv_cpy->name);
172
173   xbt_dynar_push(list, &pattern);
174
175   xbt_dynar_push_as(incomplete_communications_pattern, int,
176                     xbt_dynar_length(list) - 1);
177
178 }
179
180 void complete_comm_pattern(xbt_dynar_t list, smx_action_t comm)
181 {
182   mc_comm_pattern_t current_pattern;
183   unsigned int cursor = 0;
184   int index;
185   int completed = 0;
186   void *addr_pointed;
187   xbt_dynar_foreach(incomplete_communications_pattern, cursor, index) {
188     current_pattern =
189         (mc_comm_pattern_t) xbt_dynar_get_as(list, index, mc_comm_pattern_t);
190     if (current_pattern->comm == comm) {
191       current_pattern->src_proc = comm->comm.src_proc->pid;
192       current_pattern->dst_proc = comm->comm.dst_proc->pid;
193       current_pattern->src_host =
194           simcall_host_get_name(comm->comm.src_proc->smx_host);
195       current_pattern->dst_host =
196           simcall_host_get_name(comm->comm.dst_proc->smx_host);
197       if (current_pattern->data_size == -1) {
198         current_pattern->data_size = *(comm->comm.dst_buff_size);
199         current_pattern->data = xbt_malloc0(current_pattern->data_size);
200         addr_pointed = *(void **) comm->comm.src_buff;
201         if (addr_pointed > std_heap
202             && addr_pointed < ((xbt_mheap_t) std_heap)->breakval)
203           memcpy(current_pattern->data, addr_pointed,
204                  current_pattern->data_size);
205         else
206           memcpy(current_pattern->data, comm->comm.src_buff,
207                  current_pattern->data_size);
208       }
209       xbt_dynar_remove_at(incomplete_communications_pattern, cursor, NULL);
210       completed++;
211       if (completed == 2)
212         return;
213       cursor--;
214     }
215   }
216 }
217
218 /************************ Main algorithm ************************/
219
220 static void MC_modelcheck_comm_determinism(void)
221 {
222
223   char *req_str = NULL;
224   int value;
225   smx_simcall_t req = NULL;
226   smx_process_t process = NULL;
227   mc_state_t state = NULL, next_state = NULL;
228   int comm_pattern = 0, visited_state = -1;
229   smx_action_t current_comm;
230
231   while (xbt_fifo_size(mc_stack) > 0) {
232
233     /* Get current state */
234     state =
235         (mc_state_t)
236         xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
237
238     XBT_DEBUG("**************************************************");
239     XBT_DEBUG("Exploration depth = %d (state = %d, interleaved processes = %d)",
240               xbt_fifo_size(mc_stack), state->num,
241               MC_state_interleave_size(state));
242
243     /* Update statistics */
244     mc_stats->visited_states++;
245
246     if ((xbt_fifo_size(mc_stack) <= _sg_mc_max_depth)
247         && (req = MC_state_get_request(state, &value))
248         && (visited_state == -1)) {
249
250       /* Debug information */
251       if (XBT_LOG_ISENABLED(mc_comm_determinism, xbt_log_priority_debug)) {
252         req_str = MC_request_to_string(req, value);
253         XBT_DEBUG("Execute: %s", req_str);
254         xbt_free(req_str);
255       }
256
257       MC_SET_MC_HEAP;
258       if (dot_output != NULL)
259         req_str = MC_request_get_dot_output(req, value);
260       MC_SET_STD_HEAP;
261
262       MC_state_set_executed_request(state, req, value);
263       mc_stats->executed_transitions++;
264
265       /* TODO : handle test and testany simcalls */
266       if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
267         if (req->call == SIMCALL_COMM_ISEND)
268           comm_pattern = 1;
269         else if (req->call == SIMCALL_COMM_IRECV)
270           comm_pattern = 2;
271         else if (req->call == SIMCALL_COMM_WAIT)
272           comm_pattern = 3;
273         else if (req->call == SIMCALL_COMM_WAITANY)
274           comm_pattern = 4;
275       }
276
277       /* Answer the request */
278       SIMIX_simcall_pre(req, value);    /* After this call req is no longer usefull */
279
280       MC_SET_MC_HEAP;
281       if (comm_pattern == 1 || comm_pattern == 2) {
282         if (!initial_global_state->initial_communications_pattern_done)
283           get_comm_pattern(initial_communications_pattern, req, comm_pattern);
284         else
285           get_comm_pattern(communications_pattern, req, comm_pattern);
286       } else if (comm_pattern == 3) {
287         current_comm = simcall_comm_wait__get__comm(req);
288         if (current_comm->comm.refcount == 1) { /* First wait only must be considered */
289           if (!initial_global_state->initial_communications_pattern_done)
290             complete_comm_pattern(initial_communications_pattern, current_comm);
291           else
292             complete_comm_pattern(communications_pattern, current_comm);
293         }
294       } else if (comm_pattern == 4) {
295         current_comm =
296             xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value,
297                              smx_action_t);
298         if (current_comm->comm.refcount == 1) { /* First wait only must be considered */
299           if (!initial_global_state->initial_communications_pattern_done)
300             complete_comm_pattern(initial_communications_pattern, current_comm);
301           else
302             complete_comm_pattern(communications_pattern, current_comm);
303         }
304       }
305       MC_SET_STD_HEAP;
306
307       comm_pattern = 0;
308
309       /* Wait for requests (schedules processes) */
310       MC_wait_for_requests();
311
312       /* Create the new expanded state */
313       MC_SET_MC_HEAP;
314
315       next_state = MC_state_new();
316
317       if ((visited_state = is_visited_state()) == -1) {
318
319         /* Get an enabled process and insert it in the interleave set of the next state */
320         xbt_swag_foreach(process, simix_global->process_list) {
321           if (MC_process_is_enabled(process)) {
322             MC_state_interleave_process(next_state, process);
323           }
324         }
325
326         if (dot_output != NULL)
327           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,
328                   next_state->num, req_str);
329
330       } else {
331
332         if (dot_output != NULL)
333           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,
334                   visited_state, req_str);
335
336       }
337
338       xbt_fifo_unshift(mc_stack, next_state);
339
340       if (dot_output != NULL)
341         xbt_free(req_str);
342
343       MC_SET_STD_HEAP;
344
345     } else {
346
347       if (xbt_fifo_size(mc_stack) > _sg_mc_max_depth) {
348         XBT_WARN("/!\\ Max depth reached ! /!\\ ");
349       } else if (visited_state != -1) {
350         XBT_DEBUG("State already visited, stop the exploration");
351       } else {
352         XBT_DEBUG("There are no more processes to interleave. (depth %d)",
353                   xbt_fifo_size(mc_stack) + 1);
354       }
355
356       MC_SET_MC_HEAP;
357
358       if (initial_global_state->initial_communications_pattern_done) {
359         if (visited_state == -1) {
360           deterministic_pattern(initial_communications_pattern,
361                                 communications_pattern);
362           if (initial_global_state->comm_deterministic == 0
363               && _sg_mc_comms_determinism) {
364             XBT_INFO("****************************************************");
365             XBT_INFO("***** Non-deterministic communications pattern *****");
366             XBT_INFO("****************************************************");
367             XBT_INFO("Initial communications pattern:");
368             print_communications_pattern(initial_communications_pattern);
369             XBT_INFO("Communications pattern counter-example:");
370             print_communications_pattern(communications_pattern);
371             MC_print_statistics(mc_stats);
372             return;
373           } else if (initial_global_state->send_deterministic == 0
374                      && _sg_mc_send_determinism) {
375             XBT_INFO
376                 ("*********************************************************");
377             XBT_INFO
378                 ("***** Non-send-deterministic communications pattern *****");
379             XBT_INFO
380                 ("*********************************************************");
381             XBT_INFO("Initial communications pattern:");
382             print_communications_pattern(initial_communications_pattern);
383             XBT_INFO("Communications pattern counter-example:");
384             print_communications_pattern(communications_pattern);
385             MC_print_statistics(mc_stats);
386             return;
387           }
388         } else {
389
390         }
391       } else {
392         initial_global_state->initial_communications_pattern_done = 1;
393       }
394
395       /* Trash the current state, no longer needed */
396       xbt_fifo_shift(mc_stack);
397       MC_state_delete(state);
398       XBT_DEBUG("Delete state %d at depth %d", state->num,
399                 xbt_fifo_size(mc_stack) + 1);
400
401       MC_SET_STD_HEAP;
402
403       visited_state = -1;
404
405       /* Check for deadlocks */
406       if (MC_deadlock_check()) {
407         MC_show_deadlock(NULL);
408         return;
409       }
410
411       while ((state = xbt_fifo_shift(mc_stack)) != NULL) {
412         if (MC_state_interleave_size(state)
413             && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
414           /* We found a back-tracking point, let's loop */
415           XBT_DEBUG("Back-tracking to state %d at depth %d", state->num,
416                     xbt_fifo_size(mc_stack) + 1);
417           xbt_fifo_unshift(mc_stack, state);
418           MC_SET_STD_HEAP;
419
420           MC_replay(mc_stack, -1);
421
422           XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num,
423                     xbt_fifo_size(mc_stack));
424           break;
425         } else {
426           XBT_DEBUG("Delete state %d at depth %d", state->num,
427                     xbt_fifo_size(mc_stack) + 1);
428           MC_state_delete(state);
429         }
430       }
431
432       MC_SET_STD_HEAP;
433     }
434   }
435
436   MC_print_statistics(mc_stats);
437   MC_SET_STD_HEAP;
438
439   return;
440 }
441
442 void MC_pre_modelcheck_comm_determinism(void)
443 {
444
445   int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
446
447   mc_state_t initial_state = NULL;
448   smx_process_t process;
449
450   if (!mc_mem_set)
451     MC_SET_MC_HEAP;
452
453   if (_sg_mc_visited > 0)
454     visited_states =
455         xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
456
457   initial_communications_pattern =
458       xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp);
459   communications_pattern =
460       xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp);
461   incomplete_communications_pattern = xbt_dynar_new(sizeof(int), NULL);
462   nb_comm_pattern = 0;
463
464   initial_state = MC_state_new();
465
466   MC_SET_STD_HEAP;
467
468   XBT_DEBUG("********* Start communication determinism verification *********");
469
470   /* Wait for requests (schedules processes) */
471   MC_wait_for_requests();
472
473   if (_sg_mc_visited > 0) {
474     MC_ignore_heap(simix_global->process_to_run->data, 0);
475     MC_ignore_heap(simix_global->process_that_ran->data, 0);
476   }
477
478   MC_SET_MC_HEAP;
479
480   /* Get an enabled process and insert it in the interleave set of the initial state */
481   xbt_swag_foreach(process, simix_global->process_list) {
482     if (MC_process_is_enabled(process)) {
483       MC_state_interleave_process(initial_state, process);
484     }
485   }
486
487   xbt_fifo_unshift(mc_stack, initial_state);
488
489   MC_SET_STD_HEAP;
490
491   MC_modelcheck_comm_determinism();
492
493 }