Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
fc8cb90d996819849dd3500ee1a0dd81d0f5d8f6
[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 void MC_pre_modelcheck_comm_determinism(void)
221 {
222
223   int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
224
225   mc_state_t initial_state = NULL;
226   smx_process_t process;
227
228   if (!mc_mem_set)
229     MC_SET_MC_HEAP;
230
231   if (_sg_mc_visited > 0)
232     visited_states =
233         xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
234
235   initial_communications_pattern =
236       xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp);
237   communications_pattern =
238       xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp);
239   incomplete_communications_pattern = xbt_dynar_new(sizeof(int), NULL);
240   nb_comm_pattern = 0;
241
242   initial_state = MC_state_new();
243
244   MC_SET_STD_HEAP;
245
246   XBT_DEBUG("********* Start communication determinism verification *********");
247
248   /* Wait for requests (schedules processes) */
249   MC_wait_for_requests();
250
251   MC_SET_MC_HEAP;
252
253   /* Get an enabled process and insert it in the interleave set of the initial state */
254   xbt_swag_foreach(process, simix_global->process_list) {
255     if (MC_process_is_enabled(process)) {
256       MC_state_interleave_process(initial_state, process);
257     }
258   }
259
260   xbt_fifo_unshift(mc_stack, initial_state);
261
262   MC_SET_STD_HEAP;
263
264 }
265
266 void MC_modelcheck_comm_determinism(void)
267 {
268
269   char *req_str = NULL;
270   int value;
271   smx_simcall_t req = NULL;
272   smx_process_t process = NULL;
273   mc_state_t state = NULL, next_state = NULL;
274   int comm_pattern = 0, visited_state = -1;
275   smx_action_t current_comm;
276
277   while (xbt_fifo_size(mc_stack) > 0) {
278
279     /* Get current state */
280     state =
281         (mc_state_t)
282         xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
283
284     XBT_DEBUG("**************************************************");
285     XBT_DEBUG("Exploration depth = %d (state = %d, interleaved processes = %d)",
286               xbt_fifo_size(mc_stack), state->num,
287               MC_state_interleave_size(state));
288
289     /* Update statistics */
290     mc_stats->visited_states++;
291
292     if ((xbt_fifo_size(mc_stack) <= _sg_mc_max_depth)
293         && (req = MC_state_get_request(state, &value))
294         && (visited_state == -1)) {
295
296       /* Debug information */
297       if (XBT_LOG_ISENABLED(mc_comm_determinism, xbt_log_priority_debug)) {
298         req_str = MC_request_to_string(req, value);
299         XBT_DEBUG("Execute: %s", req_str);
300         xbt_free(req_str);
301       }
302
303       MC_SET_MC_HEAP;
304       if (dot_output != NULL)
305         req_str = MC_request_get_dot_output(req, value);
306       MC_SET_STD_HEAP;
307
308       MC_state_set_executed_request(state, req, value);
309       mc_stats->executed_transitions++;
310
311       /* TODO : handle test and testany simcalls */
312       if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
313         if (req->call == SIMCALL_COMM_ISEND)
314           comm_pattern = 1;
315         else if (req->call == SIMCALL_COMM_IRECV)
316           comm_pattern = 2;
317         else if (req->call == SIMCALL_COMM_WAIT)
318           comm_pattern = 3;
319         else if (req->call == SIMCALL_COMM_WAITANY)
320           comm_pattern = 4;
321       }
322
323       /* Answer the request */
324       SIMIX_simcall_pre(req, value);    /* After this call req is no longer usefull */
325
326       MC_SET_MC_HEAP;
327       if (comm_pattern == 1 || comm_pattern == 2) {
328         if (!initial_global_state->initial_communications_pattern_done)
329           get_comm_pattern(initial_communications_pattern, req, comm_pattern);
330         else
331           get_comm_pattern(communications_pattern, req, comm_pattern);
332       } else if (comm_pattern == 3) {
333         current_comm = simcall_comm_wait__get__comm(req);
334         if (current_comm->comm.refcount == 1) { /* First wait only must be considered */
335           if (!initial_global_state->initial_communications_pattern_done)
336             complete_comm_pattern(initial_communications_pattern, current_comm);
337           else
338             complete_comm_pattern(communications_pattern, current_comm);
339         }
340       } else if (comm_pattern == 4) {
341         current_comm =
342             xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value,
343                              smx_action_t);
344         if (current_comm->comm.refcount == 1) { /* First wait only must be considered */
345           if (!initial_global_state->initial_communications_pattern_done)
346             complete_comm_pattern(initial_communications_pattern, current_comm);
347           else
348             complete_comm_pattern(communications_pattern, current_comm);
349         }
350       }
351       MC_SET_STD_HEAP;
352
353       comm_pattern = 0;
354
355       /* Wait for requests (schedules processes) */
356       MC_wait_for_requests();
357
358       /* Create the new expanded state */
359       MC_SET_MC_HEAP;
360
361       next_state = MC_state_new();
362
363       if ((visited_state = is_visited_state()) == -1) {
364
365         /* Get an enabled process and insert it in the interleave set of the next state */
366         xbt_swag_foreach(process, simix_global->process_list) {
367           if (MC_process_is_enabled(process)) {
368             MC_state_interleave_process(next_state, process);
369           }
370         }
371
372         if (dot_output != NULL)
373           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,
374                   next_state->num, req_str);
375
376       } else {
377
378         if (dot_output != NULL)
379           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,
380                   visited_state, req_str);
381
382       }
383
384       xbt_fifo_unshift(mc_stack, next_state);
385
386       if (dot_output != NULL)
387         xbt_free(req_str);
388
389       MC_SET_STD_HEAP;
390
391     } else {
392
393       if (xbt_fifo_size(mc_stack) > _sg_mc_max_depth) {
394         XBT_WARN("/!\\ Max depth reached ! /!\\ ");
395       } else if (visited_state != -1) {
396         XBT_DEBUG("State already visited, stop the exploration");
397       } else {
398         XBT_DEBUG("There are no more processes to interleave. (depth %d)",
399                   xbt_fifo_size(mc_stack) + 1);
400       }
401
402       MC_SET_MC_HEAP;
403
404       if (initial_global_state->initial_communications_pattern_done) {
405         if (visited_state == -1) {
406           deterministic_pattern(initial_communications_pattern,
407                                 communications_pattern);
408           if (initial_global_state->comm_deterministic == 0
409               && _sg_mc_comms_determinism) {
410             XBT_INFO("****************************************************");
411             XBT_INFO("***** Non-deterministic communications pattern *****");
412             XBT_INFO("****************************************************");
413             XBT_INFO("Initial communications pattern:");
414             print_communications_pattern(initial_communications_pattern);
415             XBT_INFO("Communications pattern counter-example:");
416             print_communications_pattern(communications_pattern);
417             MC_print_statistics(mc_stats);
418             return;
419           } else if (initial_global_state->send_deterministic == 0
420                      && _sg_mc_send_determinism) {
421             XBT_INFO
422                 ("*********************************************************");
423             XBT_INFO
424                 ("***** Non-send-deterministic communications pattern *****");
425             XBT_INFO
426                 ("*********************************************************");
427             XBT_INFO("Initial communications pattern:");
428             print_communications_pattern(initial_communications_pattern);
429             XBT_INFO("Communications pattern counter-example:");
430             print_communications_pattern(communications_pattern);
431             MC_print_statistics(mc_stats);
432             return;
433           }
434         } else {
435
436         }
437       } else {
438         initial_global_state->initial_communications_pattern_done = 1;
439       }
440
441       /* Trash the current state, no longer needed */
442       xbt_fifo_shift(mc_stack);
443       MC_state_delete(state);
444       XBT_DEBUG("Delete state %d at depth %d", state->num,
445                 xbt_fifo_size(mc_stack) + 1);
446
447       MC_SET_STD_HEAP;
448
449       visited_state = -1;
450
451       /* Check for deadlocks */
452       if (MC_deadlock_check()) {
453         MC_show_deadlock(NULL);
454         return;
455       }
456
457       MC_SET_MC_HEAP;
458
459       while ((state = xbt_fifo_shift(mc_stack)) != NULL) {
460         if (MC_state_interleave_size(state)
461             && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
462           /* We found a back-tracking point, let's loop */
463           XBT_DEBUG("Back-tracking to state %d at depth %d", state->num,
464                     xbt_fifo_size(mc_stack) + 1);
465           xbt_fifo_unshift(mc_stack, state);
466           MC_SET_STD_HEAP;
467
468           MC_replay(mc_stack, -1);
469
470           XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num,
471                     xbt_fifo_size(mc_stack));
472           break;
473         } else {
474           XBT_DEBUG("Delete state %d at depth %d", state->num,
475                     xbt_fifo_size(mc_stack) + 1);
476           MC_state_delete(state);
477         }
478       }
479
480       MC_SET_STD_HEAP;
481     }
482   }
483
484   MC_print_statistics(mc_stats);
485   MC_SET_STD_HEAP;
486
487   return;
488 }