Logo AND Algorithmique Numérique Distribuée

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