Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
[mc] mc_comm_pattern.c containing all communication pattern functions
[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_state.h"
8 #include "mc_comm_pattern.h"
9 #include "mc_request.h"
10 #include "mc_safety.h"
11 #include "mc_private.h"
12 #include "mc_record.h"
13 #include "mc_smx.h"
14
15 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_comm_determinism, mc,
16                                 "Logging specific to MC communication determinism detection");
17
18 /********** Global variables **********/
19
20 xbt_dynar_t initial_communications_pattern;
21 xbt_dynar_t incomplete_communications_pattern;
22
23 /********** Static functions ***********/
24
25 static void comm_pattern_free(mc_comm_pattern_t p)
26 {
27   xbt_free(p->rdv);
28   xbt_free(p->data);
29   xbt_free(p);
30   p = NULL;
31 }
32
33 static void list_comm_pattern_free(mc_list_comm_pattern_t l)
34 {
35   xbt_dynar_free(&(l->list));
36   xbt_free(l);
37   l = NULL;
38 }
39
40 static e_mc_comm_pattern_difference_t compare_comm_pattern(mc_comm_pattern_t comm1, mc_comm_pattern_t comm2) {
41   if(comm1->type != comm2->type)
42     return TYPE_DIFF;
43   if (strcmp(comm1->rdv, comm2->rdv) != 0)
44     return RDV_DIFF;
45   if (comm1->src_proc != comm2->src_proc)
46     return SRC_PROC_DIFF;
47   if (comm1->dst_proc != comm2->dst_proc)
48     return DST_PROC_DIFF;
49   if (comm1->tag != comm2->tag)
50     return TAG_DIFF;
51   if (comm1->data_size != comm2->data_size)
52     return DATA_SIZE_DIFF;
53   if(comm1->data == NULL && comm2->data == NULL)
54     return 0;
55   if(comm1->data != NULL && comm2->data !=NULL) {
56     if (!memcmp(comm1->data, comm2->data, comm1->data_size))
57       return 0;
58     return DATA_DIFF;
59   }else{
60     return DATA_DIFF;
61   }
62   return 0;
63 }
64
65 static char* print_determinism_result(e_mc_comm_pattern_difference_t diff, int process, mc_comm_pattern_t comm, unsigned int cursor) {
66   char *type, *res;
67
68   if(comm->type == SIMIX_COMM_SEND)
69     type = bprintf("The send communications pattern of the process %d is different!", process - 1);
70   else
71     type = bprintf("The recv communications pattern of the process %d is different!", process - 1);
72
73   switch(diff) {
74   case TYPE_DIFF:
75     res = bprintf("%s Different type for communication #%d", type, cursor);
76     break;
77   case RDV_DIFF:
78     res = bprintf("%s Different rdv for communication #%d", type, cursor);
79     break;
80   case TAG_DIFF:
81     res = bprintf("%s Different tag for communication #%d", type, cursor);
82     break;
83   case SRC_PROC_DIFF:
84       res = bprintf("%s Different source for communication #%d", type, cursor);
85     break;
86   case DST_PROC_DIFF:
87       res = bprintf("%s Different destination for communication #%d", type, cursor);
88     break;
89   case DATA_SIZE_DIFF:
90     res = bprintf("%s\n Different data size for communication #%d", type, cursor);
91     break;
92   case DATA_DIFF:
93     res = bprintf("%s\n Different data for communication #%d", type, cursor);
94     break;
95   default:
96     res = NULL;
97     break;
98   }
99
100   return res;
101 }
102
103 // FIXME, remote comm
104 static void update_comm_pattern(mc_comm_pattern_t comm_pattern, smx_synchro_t comm)
105 {
106   mc_process_t process = &mc_model_checker->process;
107   void *addr_pointed;
108   smx_process_t src_proc = MC_smx_resolve_process(comm->comm.src_proc);
109   smx_process_t dst_proc = MC_smx_resolve_process(comm->comm.dst_proc);
110   comm_pattern->src_proc = src_proc->pid;
111   comm_pattern->dst_proc = dst_proc->pid;
112   // TODO, resolve host name
113   comm_pattern->src_host = MC_smx_process_get_host_name(src_proc);
114   comm_pattern->dst_host = MC_smx_process_get_host_name(dst_proc);
115   if (comm_pattern->data_size == -1 && comm->comm.src_buff != NULL) {
116     comm_pattern->data_size = *(comm->comm.dst_buff_size);
117     comm_pattern->data = xbt_malloc0(comm_pattern->data_size);
118     addr_pointed = *(void **) comm->comm.src_buff;
119     if (addr_pointed > (void*) process->heap_address
120         && addr_pointed < MC_process_get_heap(process)->breakval)
121       memcpy(comm_pattern->data, addr_pointed, comm_pattern->data_size);
122     else
123       memcpy(comm_pattern->data, comm->comm.src_buff, comm_pattern->data_size);
124   }
125 }
126
127 static void deterministic_comm_pattern(int process, mc_comm_pattern_t comm, int backtracking) {
128
129   mc_list_comm_pattern_t list_comm_pattern = (mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, process, mc_list_comm_pattern_t);
130
131   if(!backtracking){
132     mc_comm_pattern_t initial_comm = xbt_dynar_get_as(list_comm_pattern->list, list_comm_pattern->index_comm, mc_comm_pattern_t);
133     e_mc_comm_pattern_difference_t diff;
134     
135     if((diff = compare_comm_pattern(initial_comm, comm)) != NONE_DIFF){
136       if (comm->type == SIMIX_COMM_SEND){
137         initial_global_state->send_deterministic = 0;
138         if(initial_global_state->send_diff != NULL)
139           xbt_free(initial_global_state->send_diff);
140         initial_global_state->send_diff = print_determinism_result(diff, process, comm, list_comm_pattern->index_comm + 1);
141       }else{
142         initial_global_state->recv_deterministic = 0;
143         if(initial_global_state->recv_diff != NULL)
144           xbt_free(initial_global_state->recv_diff);
145         initial_global_state->recv_diff = print_determinism_result(diff, process, comm, list_comm_pattern->index_comm + 1);
146       }
147       if(_sg_mc_send_determinism && !initial_global_state->send_deterministic){
148         XBT_INFO("*********************************************************");
149         XBT_INFO("***** Non-send-deterministic communications pattern *****");
150         XBT_INFO("*********************************************************");
151         XBT_INFO("%s", initial_global_state->send_diff);
152         xbt_free(initial_global_state->send_diff);
153         initial_global_state->send_diff = NULL;
154         MC_print_statistics(mc_stats);
155         xbt_abort(); 
156       }else if(_sg_mc_comms_determinism && (!initial_global_state->send_deterministic && !initial_global_state->recv_deterministic)) {
157         XBT_INFO("****************************************************");
158         XBT_INFO("***** Non-deterministic communications pattern *****");
159         XBT_INFO("****************************************************");
160         XBT_INFO("%s", initial_global_state->send_diff);
161         XBT_INFO("%s", initial_global_state->recv_diff);
162         xbt_free(initial_global_state->send_diff);
163         initial_global_state->send_diff = NULL;
164         xbt_free(initial_global_state->recv_diff);
165         initial_global_state->recv_diff = NULL;
166         MC_print_statistics(mc_stats);
167         xbt_abort();
168       } 
169     }
170   }
171     
172   comm_pattern_free(comm);
173
174 }
175
176 /********** Non Static functions ***********/
177
178 void comm_pattern_free_voidp(void *p) {
179   comm_pattern_free((mc_comm_pattern_t) * (void **) p);
180 }
181
182 void list_comm_pattern_free_voidp(void *p) {
183   list_comm_pattern_free((mc_list_comm_pattern_t) * (void **) p);
184 }
185
186 void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking)
187 {
188   mc_process_t process = &mc_model_checker->process;
189
190   mc_comm_pattern_t pattern = xbt_new0(s_mc_comm_pattern_t, 1);
191   pattern->data_size = -1;
192   pattern->data = NULL;
193
194   // Fill initial_pattern->index_comm:
195   const smx_process_t issuer = MC_smx_simcall_get_issuer(request);
196   mc_list_comm_pattern_t initial_pattern =
197     (mc_list_comm_pattern_t) xbt_dynar_get_as(initial_communications_pattern, issuer->pid, mc_list_comm_pattern_t);
198   xbt_dynar_t incomplete_pattern =
199     (xbt_dynar_t) xbt_dynar_get_as(incomplete_communications_pattern, issuer->pid, xbt_dynar_t);
200   pattern->index =
201     initial_pattern->index_comm + xbt_dynar_length(incomplete_pattern);
202   
203   void *addr_pointed;
204   
205   if (call_type == MC_CALL_TYPE_SEND) {
206     /* Create comm pattern */
207     pattern->type = SIMIX_COMM_SEND;
208     pattern->comm = simcall_comm_isend__get__result(request);
209     // FIXME, remote access to rdv->name
210     pattern->rdv = (pattern->comm->comm.rdv != NULL) ? strdup(pattern->comm->comm.rdv->name) : strdup(pattern->comm->comm.rdv_cpy->name);
211     pattern->src_proc = MC_smx_resolve_process(pattern->comm->comm.src_proc)->pid;
212     pattern->src_host = MC_smx_process_get_host_name(issuer);
213     pattern->tag = ((MPI_Request)simcall_comm_isend__get__data(request))->tag;
214     if(pattern->comm->comm.src_buff != NULL){
215       pattern->data_size = pattern->comm->comm.src_buff_size;
216       pattern->data = xbt_malloc0(pattern->data_size);
217       addr_pointed = *(void **) pattern->comm->comm.src_buff;
218       if (addr_pointed > (void*) process->heap_address
219           && addr_pointed < MC_process_get_heap(process)->breakval)
220         memcpy(pattern->data, addr_pointed, pattern->data_size);
221       else
222         memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size);
223     }
224     if(((MPI_Request)simcall_comm_isend__get__data(request))->detached){
225       if (!initial_global_state->initial_communications_pattern_done) {
226         /* Store comm pattern */
227         xbt_dynar_push(((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, pattern->src_proc, mc_list_comm_pattern_t))->list, &pattern);
228       } else {
229         /* Evaluate comm determinism */
230         deterministic_comm_pattern(pattern->src_proc, pattern, backtracking);
231         ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, pattern->src_proc, mc_list_comm_pattern_t))->index_comm++;
232       }
233       return;
234     }
235   } else if (call_type == MC_CALL_TYPE_RECV) {                      
236     pattern->type = SIMIX_COMM_RECEIVE;
237     pattern->comm = simcall_comm_irecv__get__result(request);
238     // TODO, remote access
239     pattern->tag = ((MPI_Request)simcall_comm_irecv__get__data(request))->tag;
240     pattern->rdv = (pattern->comm->comm.rdv != NULL) ? strdup(pattern->comm->comm.rdv->name) : strdup(pattern->comm->comm.rdv_cpy->name);
241     pattern->dst_proc = MC_smx_resolve_process(pattern->comm->comm.dst_proc)->pid;
242     // FIXME, remote process access
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
248   xbt_dynar_push((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, issuer->pid, xbt_dynar_t), &pattern);
249
250   XBT_DEBUG("Insert incomplete comm pattern %p for process %lu", pattern, issuer->pid);
251 }
252
253 void complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm, unsigned int issuer, int backtracking) {
254   mc_comm_pattern_t current_comm_pattern;
255   unsigned int cursor = 0;
256   mc_comm_pattern_t comm_pattern;
257   int completed = 0;
258
259   /* Complete comm pattern */
260   xbt_dynar_foreach((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t), cursor, current_comm_pattern) {
261     if (current_comm_pattern-> comm == comm) {
262       update_comm_pattern(current_comm_pattern, comm);
263       completed = 1;
264       xbt_dynar_remove_at((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t), cursor, &comm_pattern);
265       XBT_DEBUG("Remove incomplete comm pattern for process %u at cursor %u", issuer, cursor);
266       break;
267     }
268   }
269   if(!completed)
270     xbt_die("Corresponding communication not found!");
271
272   if (!initial_global_state->initial_communications_pattern_done) {
273     /* Store comm pattern */
274     xbt_dynar_push(((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, issuer, mc_list_comm_pattern_t))->list, &comm_pattern);
275   } else {
276     /* Evaluate comm determinism */
277     deterministic_comm_pattern(issuer, comm_pattern, backtracking);
278     ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, issuer, mc_list_comm_pattern_t))->index_comm++;
279   }
280 }
281
282
283 /************************ Main algorithm ************************/
284
285 void MC_pre_modelcheck_comm_determinism(void)
286 {
287   MC_SET_MC_HEAP;
288
289   mc_state_t initial_state = NULL;
290   smx_process_t process;
291   int i;
292
293   if (_sg_mc_visited > 0)
294     visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
295  
296   initial_communications_pattern = xbt_dynar_new(sizeof(mc_list_comm_pattern_t), list_comm_pattern_free_voidp);
297   for (i=0; i < MC_smx_get_maxpid(); i++){
298     mc_list_comm_pattern_t process_list_pattern = xbt_new0(s_mc_list_comm_pattern_t, 1);
299     process_list_pattern->list = xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp);
300     process_list_pattern->index_comm = 0;
301     xbt_dynar_insert_at(initial_communications_pattern, i, &process_list_pattern);
302   }
303   incomplete_communications_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp);
304   for (i=0; i < MC_smx_get_maxpid(); i++){
305     xbt_dynar_t process_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), NULL);
306     xbt_dynar_insert_at(incomplete_communications_pattern, i, &process_pattern);
307   }
308
309   initial_state = MC_state_new();
310   MC_SET_STD_HEAP;
311   
312   XBT_DEBUG("********* Start communication determinism verification *********");
313
314   /* Wait for requests (schedules processes) */
315   MC_wait_for_requests();
316
317   MC_SET_MC_HEAP;
318
319   /* Get an enabled process and insert it in the interleave set of the initial state */
320   MC_EACH_SIMIX_PROCESS(process,
321     if (MC_process_is_enabled(process)) {
322       MC_state_interleave_process(initial_state, process);
323     }
324   );
325
326   xbt_fifo_unshift(mc_stack, initial_state);
327
328   MC_SET_STD_HEAP;
329
330 }
331
332 void MC_modelcheck_comm_determinism(void)
333 {
334
335   char *req_str = NULL;
336   int value;
337   mc_visited_state_t visited_state = NULL;
338   smx_simcall_t req = NULL;
339   smx_process_t process = NULL;
340   mc_state_t state = NULL, next_state = NULL;
341
342   while (xbt_fifo_size(mc_stack) > 0) {
343
344     /* Get current state */
345     state = (mc_state_t) xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
346
347     XBT_DEBUG("**************************************************");
348     XBT_DEBUG("Exploration depth = %d (state = %d, interleaved processes = %d)",
349               xbt_fifo_size(mc_stack), state->num,
350               MC_state_interleave_size(state));
351
352     /* Update statistics */
353     mc_stats->visited_states++;
354
355     if ((xbt_fifo_size(mc_stack) <= _sg_mc_max_depth)
356         && (req = MC_state_get_request(state, &value))
357         && (visited_state == NULL)) {
358
359       req_str = MC_request_to_string(req, value);  
360       XBT_DEBUG("Execute: %s", req_str);                 
361       xbt_free(req_str);
362       
363       if (dot_output != NULL) {
364         MC_SET_MC_HEAP;
365         req_str = MC_request_get_dot_output(req, value);
366         MC_SET_STD_HEAP;
367       }
368
369       MC_state_set_executed_request(state, req, value);
370       mc_stats->executed_transitions++;
371
372       /* TODO : handle test and testany simcalls */
373       e_mc_call_type_t call = MC_CALL_TYPE_NONE;
374       if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
375         call = mc_get_call_type(req);
376       }
377
378       /* Answer the request */
379       MC_simcall_handle(req, value);    /* After this call req is no longer useful */
380
381       MC_SET_MC_HEAP;
382       if(!initial_global_state->initial_communications_pattern_done)
383         handle_comm_pattern(call, req, value, initial_communications_pattern, 0);
384       else
385         handle_comm_pattern(call, req, value, NULL, 0);
386       MC_SET_STD_HEAP;
387
388       /* Wait for requests (schedules processes) */
389       MC_wait_for_requests();
390
391       /* Create the new expanded state */
392       MC_SET_MC_HEAP;
393
394       next_state = MC_state_new();
395
396       if ((visited_state = is_visited_state(next_state)) == NULL) {
397
398         /* Get enabled processes and insert them in the interleave set of the next state */
399         MC_EACH_SIMIX_PROCESS(process,
400           if (MC_process_is_enabled(process)) {
401             MC_state_interleave_process(next_state, process);
402           }
403         );
404
405         if (dot_output != NULL)
406           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,  next_state->num, req_str);
407
408       } else {
409
410         if (dot_output != NULL)
411           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
412
413       }
414
415       xbt_fifo_unshift(mc_stack, next_state);
416
417       if (dot_output != NULL)
418         xbt_free(req_str);
419
420       MC_SET_STD_HEAP;
421
422     } else {
423
424       if (xbt_fifo_size(mc_stack) > _sg_mc_max_depth) {
425         XBT_WARN("/!\\ Max depth reached ! /!\\ ");
426       } else if (visited_state != NULL) {
427         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);
428       } else {
429         XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack));
430       }
431
432       MC_SET_MC_HEAP;
433
434       if (!initial_global_state->initial_communications_pattern_done) 
435         initial_global_state->initial_communications_pattern_done = 1;
436
437       /* Trash the current state, no longer needed */
438       xbt_fifo_shift(mc_stack);
439       MC_state_delete(state, !state->in_visited_states ? 1 : 0);
440       XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
441
442       MC_SET_STD_HEAP;
443
444       visited_state = NULL;
445
446       /* Check for deadlocks */
447       if (MC_deadlock_check()) {
448         MC_show_deadlock(NULL);
449         return;
450       }
451
452       MC_SET_MC_HEAP;
453
454       while ((state = xbt_fifo_shift(mc_stack)) != NULL) {
455         if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
456           /* We found a back-tracking point, let's loop */
457           XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
458           xbt_fifo_unshift(mc_stack, state);
459           MC_SET_STD_HEAP;
460
461           MC_replay(mc_stack);
462
463           XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack));
464
465           break;
466         } else {
467           XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
468           MC_state_delete(state, !state->in_visited_states ? 1 : 0);
469         }
470       }
471
472       MC_SET_STD_HEAP;
473     }
474   }
475
476   MC_print_statistics(mc_stats);
477   MC_SET_STD_HEAP;
478
479   return;
480 }