Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
6c353804681dd4850bcca4d2a4810353b858ddb3
[simgrid.git] / src / mc / mc_liveness.c
1 /* Copyright (c) 2008-2012 Da SimGrid Team. All rights reserved.            */
2
3 /* This program is free software; you can redistribute it and/or modify it
4  * under the terms of the license (GNU LGPL) which comes with this package. */
5
6 #include "mc_private.h"
7 #include <unistd.h>
8 #include <sys/wait.h>
9
10 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
11                                 "Logging specific to algorithms for liveness properties verification");
12
13 xbt_dynar_t reached_pairs;
14 xbt_dynar_t reached_pairs_hash;
15 xbt_dynar_t visited_pairs;
16 xbt_dynar_t visited_pairs_hash;
17 xbt_dynar_t successors;
18
19 xbt_dynar_t hosts_table;
20
21
22 /* fast implementation of djb2 algorithm */
23 unsigned int hash_region(char *str, int str_len){
24
25   int c;
26   register unsigned int hash = 5381;
27
28   while (str_len--) {
29     c = *str++;
30     hash = ((hash << 5) + hash) + c;    /* hash * 33 + c */
31   }
32
33   return hash;
34
35 }
36
37 int create_dump(int pair)
38 {
39    // Try to enable core dumps
40   struct rlimit core_limit;
41   core_limit.rlim_cur = RLIM_INFINITY;
42   core_limit.rlim_max = RLIM_INFINITY;
43   
44   if(setrlimit(RLIMIT_CORE, &core_limit) < 0)
45     fprintf(stderr, "setrlimit: %s\nWarning: core dumps may be truncated or non-existant\n", strerror(errno));
46   
47   int status;
48   switch(fork()){
49   case 0:
50     // We are the child process -- run the actual program
51     abort();
52     break;
53     
54   case -1:
55     // An error occurred, shouldn't happen
56     perror("fork");
57     return -1;
58     
59   default:
60     // We are the parent process -- wait for the child process to exit
61     if(wait(&status) < 0)
62       perror("wait");
63     printf("child exited with status %d\n", status);
64     if(WIFSIGNALED(status) && WCOREDUMP(status)){
65       printf("got a core dump\n");
66       char *core_name = malloc(20);
67       sprintf(core_name,"mv core core_%d", pair); 
68       system((char *)core_name);
69       free(core_name);
70     }
71   }
72
73   return 0;
74 }
75
76 int reached(xbt_state_t st){
77
78   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
79
80
81   if(xbt_dynar_is_empty(reached_pairs)){
82
83     return 0;
84
85   }else{
86
87     MC_SET_RAW_MEM;
88
89     mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
90     MC_take_snapshot_liveness(sn);    
91     
92     xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
93     int res;
94     int_f_void_t f;
95
96     /* Get values of propositional symbols */
97     unsigned int cursor = 0;
98     xbt_propositional_symbol_t ps = NULL;
99     xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
100       f = (int_f_void_t)ps->function;
101       res = (*f)();
102       xbt_dynar_push_as(prop_ato, int, res);
103     }
104
105     cursor = 0;
106     mc_pair_reached_t pair_test = NULL;
107
108     //xbt_dict_t current_rdv_points = SIMIX_get_rdv_points();
109      
110     xbt_dynar_foreach(reached_pairs, cursor, pair_test){
111       XBT_INFO("Pair reached #%d", pair_test->nb);
112       if(automaton_state_compare(pair_test->automaton_state, st) == 0){
113         if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
114           //XBT_INFO("Rdv points size %d - %d", xbt_dict_length(pair_test->rdv_points), xbt_dict_length(current_rdv_points));
115           //if(xbt_dict_length(pair_test->rdv_points) == xbt_dict_length(current_rdv_points)){
116           //if(rdv_points_compare(pair_test->rdv_points, current_rdv_points) == 0){
117           if(snapshot_compare(pair_test->system_state, sn) == 0){
118      
119             MC_free_snapshot(sn);
120             xbt_dynar_reset(prop_ato);
121             xbt_free(prop_ato);
122             MC_UNSET_RAW_MEM;
123
124             if(raw_mem_set)
125               MC_SET_RAW_MEM;
126             else
127               MC_UNSET_RAW_MEM;
128             
129             return 1;
130           }
131           /* }
132              }else{
133              XBT_INFO("Different size of rdv points (%d - %d)",xbt_dict_length(pair_test->rdv_points), xbt_dict_length(current_rdv_points) );
134              }*/
135         }else{
136           XBT_INFO("Different values of propositional symbols");
137         }
138       }else{
139         XBT_INFO("Different automaton state");
140       }
141     }
142
143     MC_free_snapshot(sn);
144     xbt_dynar_reset(prop_ato);
145     xbt_free(prop_ato);
146     MC_UNSET_RAW_MEM;
147
148     if(raw_mem_set)
149       MC_SET_RAW_MEM;
150     else
151       MC_UNSET_RAW_MEM;
152     
153     return 0;
154     
155   }
156 }
157
158 int rdv_points_compare(xbt_dict_t d1, xbt_dict_t d2){ /* d1 = pair_test, d2 = current_pair */ 
159   
160   xbt_dict_cursor_t cursor_dict = NULL;
161   char *key;
162   char *data;
163   smx_rdv_t rdv1, rdv2;
164   xbt_fifo_item_t item1, item2;
165   smx_action_t action1, action2;
166   xbt_fifo_item_t item_req1, item_req2;
167   smx_simcall_t req1, req2;
168   int i=0;
169   int j=0;
170
171   xbt_dict_foreach(d1, cursor_dict, key, data){
172     rdv1 = (smx_rdv_t)data;
173     rdv2 = xbt_dict_get_or_null(d2, rdv1->name);
174     if(rdv2 == NULL){
175       XBT_INFO("Rdv point unknown");
176       return 1;
177     }else{
178       if(xbt_fifo_size(rdv1->comm_fifo) != xbt_fifo_size(rdv2->comm_fifo)){
179         XBT_INFO("Different total of actions in mailbox \"%s\" (%d - %d)", rdv1->name, xbt_fifo_size(rdv1->comm_fifo),xbt_fifo_size(rdv2->comm_fifo) );
180         return 1;
181       }else{
182    
183         XBT_INFO("Total of actions in mailbox \"%s\" : %d", rdv1->name, xbt_fifo_size(rdv1->comm_fifo)); 
184    
185         item1 = xbt_fifo_get_first_item(rdv1->comm_fifo);  
186         item2 = xbt_fifo_get_first_item(rdv2->comm_fifo);
187
188         while(i<xbt_fifo_size(rdv1->comm_fifo)){
189           action1 = (smx_action_t) xbt_fifo_get_item_content(item1);
190           action2 = (smx_action_t) xbt_fifo_get_item_content(item2);
191
192           if(action1->type != action2->type){
193             XBT_INFO("Different type of action");
194             return 1;
195           }
196
197           if(action1->state != action2->state){
198             XBT_INFO("Different state of action");
199             return 1;
200           }
201
202           if(xbt_fifo_size(action1->simcalls) != xbt_fifo_size(action2->simcalls)){
203             XBT_INFO("Different size of simcall list (%d - %d", xbt_fifo_size(action1->simcalls), xbt_fifo_size(action2->simcalls));
204             return 1;
205           }else{
206
207             item_req1 = xbt_fifo_get_first_item(action1->simcalls);  
208             item_req2 = xbt_fifo_get_first_item(action2->simcalls);
209
210             while(j<xbt_fifo_size(action1->simcalls)){
211
212               req1 = (smx_simcall_t) xbt_fifo_get_item_content(item_req1);
213               req2 = (smx_simcall_t) xbt_fifo_get_item_content(item_req2);
214          
215               if(req1->call != req2->call){
216                 XBT_INFO("Different simcall call in simcalls of action (%d - %d)", (int)req1->call, (int)req2->call);
217                 return 1;
218               }
219               if(req1->issuer->pid != req2->issuer->pid){
220                 XBT_INFO("Different simcall issuer in simcalls of action (%lu- %lu)", req1->issuer->pid, req2->issuer->pid);
221                 return 1;
222               }
223
224               item_req1 = xbt_fifo_get_next_item(item_req1);  
225               item_req2 = xbt_fifo_get_next_item(item_req2);
226               j++;
227          
228             }
229           }
230
231           switch(action1->type){
232           case 0: /* execution */
233           case 1: /* parallel execution */
234             if(strcmp(action1->execution.host->name, action2->execution.host->name) != 0)
235               return 1;
236             break;
237           case 2: /* comm */
238             if(action1->comm.type != action2->comm.type)
239               return 1;
240             //XBT_INFO("Type of comm : %d", action1->comm.type);
241        
242             switch(action1->comm.type){
243             case 0: /* SEND */
244               if(action1->comm.src_proc->pid != action2->comm.src_proc->pid)
245                 return 1;
246               if(strcmp(action1->comm.src_proc->smx_host->name, action2->comm.src_proc->smx_host->name) != 0)
247                 return 1;
248               break;
249             case 1: /* RECEIVE */
250               if(action1->comm.dst_proc->pid != action2->comm.dst_proc->pid)
251                 return 1;
252               if(strcmp(action1->comm.dst_proc->smx_host->name, action2->comm.dst_proc->smx_host->name) != 0)
253                 return 1;
254               break;
255             case 2: /* READY */
256               if(action1->comm.src_proc->pid != action2->comm.src_proc->pid)
257                 return 1;
258               if(strcmp(action1->comm.src_proc->smx_host->name, action2->comm.src_proc->smx_host->name) != 0)
259                 return 1;
260               if(action1->comm.dst_proc->pid != action2->comm.dst_proc->pid)
261                 return 1;
262               if(strcmp(action1->comm.dst_proc->smx_host->name, action2->comm.dst_proc->smx_host->name) != 0)
263                 return 1;
264               break;
265             case 3: /* DONE */
266               if(action1->comm.src_proc->pid != action2->comm.src_proc->pid)
267                 return 1;
268               if(strcmp(action1->comm.src_proc->smx_host->name, action2->comm.src_proc->smx_host->name) != 0)
269                 return 1;
270               if(action1->comm.dst_proc->pid != action2->comm.dst_proc->pid)
271                 return 1;
272               if(strcmp(action1->comm.dst_proc->smx_host->name, action2->comm.dst_proc->smx_host->name) != 0)
273                 return 1;
274               break;
275          
276             } /* end of switch on type of comm */
277        
278             if(action1->comm.refcount != action2->comm.refcount)
279               return 1;
280             if(action1->comm.detached != action2->comm.detached)
281               return 1;
282             if(action1->comm.rate != action2->comm.rate)
283               return 1;
284             if(action1->comm.task_size != action2->comm.task_size)
285               return 1;
286             if(action1->comm.src_buff != action2->comm.src_buff)
287               return 1;
288             if(action1->comm.dst_buff != action2->comm.dst_buff)
289               return 1;
290             if(action1->comm.src_data != action2->comm.src_data)
291               return 1;
292             if(action1->comm.dst_data != action2->comm.dst_data)
293               return 1;
294        
295             break;
296           case 3: /* sleep */
297             if(strcmp(action1->sleep.host->name, action2->sleep.host->name) != 0)
298               return 1;
299             break;
300           case 4: /* synchro */
301        
302             break;
303           default:
304             break;
305           }
306
307           item1 = xbt_fifo_get_next_item(item1);  
308           item2 = xbt_fifo_get_next_item(item2);
309           i++;
310         }
311       }
312     }
313   }
314
315   return 0;
316    
317 }
318
319 void set_pair_reached(xbt_state_t st){
320
321   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
322  
323   MC_SET_RAW_MEM;
324   
325   mc_pair_reached_t pair = NULL;
326   pair = xbt_new0(s_mc_pair_reached_t, 1);
327   pair->nb = xbt_dynar_length(reached_pairs) + 1;
328   pair->automaton_state = st;
329   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
330   pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
331   //pair->rdv_points = xbt_dict_new();  
332   MC_take_snapshot_liveness(pair->system_state);
333
334   /* Get values of propositional symbols */
335   unsigned int cursor = 0;
336   xbt_propositional_symbol_t ps = NULL;
337   int res;
338   int_f_void_t f;
339
340   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
341     f = (int_f_void_t)ps->function;
342     res = (*f)();
343     xbt_dynar_push_as(pair->prop_ato, int, res);
344   }
345
346   /*xbt_dict_t rdv_points = SIMIX_get_rdv_points();
347
348     xbt_dict_cursor_t cursor_dict = NULL;
349     char *key;
350     char *data;
351     xbt_fifo_item_t item;
352     smx_action_t action;
353
354     xbt_dict_foreach(rdv_points, cursor_dict, key, data){
355     smx_rdv_t new_rdv = xbt_new0(s_smx_rvpoint_t, 1);
356     new_rdv->name = strdup(((smx_rdv_t)data)->name);
357     new_rdv->comm_fifo = xbt_fifo_new();
358     xbt_fifo_foreach(((smx_rdv_t)data)->comm_fifo, item, action, smx_action_t) {
359     smx_action_t a = xbt_new0(s_smx_action_t, 1);
360     memcpy(a, action, sizeof(s_smx_action_t));
361     xbt_fifo_push(new_rdv->comm_fifo, a);
362     XBT_INFO("New action (type = %d, state = %d) in mailbox \"%s\"", action->type, action->state, key);
363     if(action->type==2)
364     XBT_INFO("Type of communication : %d, Ref count = %d", action->comm.type, action->comm.refcount);
365     }
366     //new_rdv->comm_fifo = xbt_fifo_copy(((smx_rdv_t)data)->comm_fifo);
367     xbt_dict_set(pair->rdv_points, new_rdv->name, new_rdv, NULL);
368     }*/
369  
370   xbt_dynar_push(reached_pairs, &pair); 
371
372   MC_UNSET_RAW_MEM;
373
374   if(raw_mem_set)
375     MC_SET_RAW_MEM;
376   else
377     MC_UNSET_RAW_MEM;
378
379   create_dump(xbt_dynar_length(reached_pairs));
380     
381 }
382
383
384 int reached_hash(xbt_state_t st){
385
386   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
387
388   if(xbt_dynar_is_empty(reached_pairs_hash)){
389
390     return 0;
391
392   }else{
393
394     MC_SET_RAW_MEM;
395
396     mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
397     MC_take_snapshot_liveness(sn);
398
399     int j;
400     unsigned int hash_regions[sn->num_reg];
401     for(j=0; j<sn->num_reg; j++){
402       hash_regions[j] = hash_region(sn->regions[j]->data, sn->regions[j]->size);
403     }
404
405
406     /* Get values of propositional symbols */
407     xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
408     unsigned int cursor = 0;
409     xbt_propositional_symbol_t ps = NULL;
410     int res;
411     int_f_void_t f;
412
413     xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
414       f = (int_f_void_t)ps->function;
415       res = (*f)();
416       xbt_dynar_push_as(prop_ato, int, res);
417     }
418
419     mc_pair_reached_hash_t pair_test = NULL;
420
421     int region_diff = 0;
422
423     cursor = 0;
424
425     xbt_dynar_foreach(reached_pairs_hash, cursor, pair_test){
426
427       if(automaton_state_compare(pair_test->automaton_state, st) == 0){
428         if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
429           for(j=0 ; j< sn->num_reg ; j++){
430             if(hash_regions[j] != pair_test->hash_regions[j]){
431               region_diff++;
432             }
433           }
434           if(region_diff == 0){
435             MC_free_snapshot(sn);
436             xbt_dynar_reset(prop_ato);
437             xbt_free(prop_ato);
438             MC_UNSET_RAW_MEM;
439
440             if(raw_mem_set)
441               MC_SET_RAW_MEM;
442             else
443               MC_UNSET_RAW_MEM;
444             
445             return 1;
446           }else{
447             XBT_INFO("Different snapshot");
448           }
449         }else{
450           XBT_INFO("Different values of propositional symbols");
451         }
452       }else{
453         XBT_INFO("Different automaton state");
454       }
455
456       region_diff = 0;
457     }
458     
459     MC_free_snapshot(sn);
460     xbt_dynar_reset(prop_ato);
461     xbt_free(prop_ato);
462     MC_UNSET_RAW_MEM;
463
464     if(raw_mem_set)
465       MC_SET_RAW_MEM;
466     else
467       MC_UNSET_RAW_MEM;
468     
469     return 0;
470     
471   }
472 }
473
474 void set_pair_reached_hash(xbt_state_t st){
475
476   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
477  
478   MC_SET_RAW_MEM;
479
480   mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
481   MC_take_snapshot_liveness(sn);
482  
483   mc_pair_reached_hash_t pair = NULL;
484   pair = xbt_new0(s_mc_pair_reached_hash_t, 1);
485   pair->automaton_state = st;
486   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
487   pair->hash_regions = malloc(sizeof(unsigned int) * sn->num_reg);
488   
489   int i;
490
491   for(i=0 ; i< sn->num_reg ; i++){
492     pair->hash_regions[i] = hash_region(sn->regions[i]->data, sn->regions[i]->size);
493   }
494   
495   /* Get values of propositional symbols */
496   unsigned int cursor = 0;
497   xbt_propositional_symbol_t ps = NULL;
498   int res;
499   int_f_void_t f;
500
501   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
502     f = (int_f_void_t)ps->function;
503     res = (*f)();
504     xbt_dynar_push_as(pair->prop_ato, int, res);
505   }
506   
507   xbt_dynar_push(reached_pairs_hash, &pair);
508
509   MC_free_snapshot(sn);
510   
511   MC_UNSET_RAW_MEM;
512
513   if(raw_mem_set)
514     MC_SET_RAW_MEM;
515   else
516     MC_UNSET_RAW_MEM;
517       
518 }
519
520
521 int visited(xbt_state_t st, int sc){
522
523   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
524
525   if(xbt_dynar_is_empty(visited_pairs)){
526
527     return 0;
528
529   }else{
530
531     MC_SET_RAW_MEM;
532
533     mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
534     MC_take_snapshot_liveness(sn);
535
536     xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
537
538     /* Get values of propositional symbols */
539     unsigned int cursor = 0;
540     xbt_propositional_symbol_t ps = NULL;
541     int res;
542     int_f_void_t f;
543
544     xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
545       f = (int_f_void_t)ps->function;
546       res = (*f)();
547       xbt_dynar_push_as(prop_ato, int, res);
548     }
549
550     cursor = 0;
551     mc_pair_visited_t pair_test = NULL;
552
553     xbt_dynar_foreach(visited_pairs, cursor, pair_test){
554       if(pair_test->search_cycle == sc) {
555         if(automaton_state_compare(pair_test->automaton_state, st) == 0){
556           if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
557             if(snapshot_compare(pair_test->system_state, sn) == 0){
558       
559               MC_free_snapshot(sn);
560               xbt_dynar_reset(prop_ato);
561               xbt_free(prop_ato);
562               MC_UNSET_RAW_MEM;
563     
564               if(raw_mem_set)
565                 MC_SET_RAW_MEM;
566               else
567                 MC_UNSET_RAW_MEM;
568               
569               return 1;
570   
571             }else{
572               XBT_INFO("Different snapshot");
573             }
574           }else{
575             XBT_INFO("Different values of propositional symbols"); 
576           }
577         }else{
578           XBT_INFO("Different automaton state");
579         }
580       }else{
581         XBT_INFO("Different value of search_cycle");
582       }
583     }
584
585
586     MC_free_snapshot(sn);
587     xbt_dynar_reset(prop_ato);
588     xbt_free(prop_ato);
589     MC_UNSET_RAW_MEM;
590
591     if(raw_mem_set)
592       MC_SET_RAW_MEM;
593     else
594       MC_UNSET_RAW_MEM;
595     
596     return 0;
597     
598   }
599 }
600
601
602 int visited_hash(xbt_state_t st, int sc){
603
604   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
605
606   if(xbt_dynar_is_empty(visited_pairs_hash)){
607
608     return 0;
609
610   }else{
611
612     MC_SET_RAW_MEM;
613
614     mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
615     MC_take_snapshot_liveness(sn);
616
617     int j;
618     unsigned int hash_regions[sn->num_reg];
619     for(j=0; j<sn->num_reg; j++){
620       hash_regions[j] = hash_region(sn->regions[j]->data, sn->regions[j]->size);
621     }
622
623     
624     /* Get values of propositional symbols */
625     xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
626     unsigned int cursor = 0;
627     xbt_propositional_symbol_t ps = NULL;
628     int res;
629     int_f_void_t f;
630
631     xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
632       f = (int_f_void_t)ps->function;
633       res = (*f)();
634       xbt_dynar_push_as(prop_ato, int, res);
635     }
636
637     mc_pair_visited_hash_t pair_test = NULL;
638
639     int region_diff = 0;
640     cursor = 0;
641
642     xbt_dynar_foreach(visited_pairs_hash, cursor, pair_test){
643   
644       if(pair_test->search_cycle == sc) {
645         if(automaton_state_compare(pair_test->automaton_state, st) == 0){
646           if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
647             for(j=0 ; j< sn->num_reg ; j++){
648               if(hash_regions[j] != pair_test->hash_regions[j]){
649                 region_diff++;
650               }
651             }
652             if(region_diff == 0){
653               MC_free_snapshot(sn);
654               xbt_dynar_reset(prop_ato);
655               xbt_free(prop_ato);
656               MC_UNSET_RAW_MEM;
657               
658               if(raw_mem_set)
659                 MC_SET_RAW_MEM;
660               else
661                 MC_UNSET_RAW_MEM;
662   
663               return 1;
664             }else{
665               //XBT_INFO("Different snapshot");
666             }
667           }else{
668             //XBT_INFO("Different values of propositional symbols"); 
669           }
670         }else{
671           //XBT_INFO("Different automaton state");
672         }
673       }else{
674         //XBT_INFO("Different value of search_cycle");
675       }
676       
677       region_diff = 0;
678     }
679     
680     MC_free_snapshot(sn);
681     xbt_dynar_reset(prop_ato);
682     xbt_free(prop_ato);
683     MC_UNSET_RAW_MEM;
684   
685     if(raw_mem_set)
686       MC_SET_RAW_MEM;
687     else
688       MC_UNSET_RAW_MEM;
689   
690     return 0;
691     
692   }
693 }
694
695 void set_pair_visited_hash(xbt_state_t st, int sc){
696
697   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
698  
699   MC_SET_RAW_MEM;
700
701   mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
702   MC_take_snapshot_liveness(sn);
703  
704   mc_pair_visited_hash_t pair = NULL;
705   pair = xbt_new0(s_mc_pair_visited_hash_t, 1);
706   pair->automaton_state = st;
707   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
708   pair->search_cycle = sc;
709   pair->hash_regions = malloc(sizeof(unsigned int) * sn->num_reg);
710   
711   int i;
712
713   for(i=0 ; i< sn->num_reg ; i++){
714     pair->hash_regions[i] = hash_region(sn->regions[i]->data, sn->regions[i]->size);
715   }
716   
717   /* Get values of propositional symbols */
718   unsigned int cursor = 0;
719   xbt_propositional_symbol_t ps = NULL;
720   int res;
721   int_f_void_t f;
722
723   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
724     f = (int_f_void_t)ps->function;
725     res = (*f)();
726     xbt_dynar_push_as(pair->prop_ato, int, res);
727   }
728   
729   xbt_dynar_push(visited_pairs_hash, &pair);
730
731   MC_free_snapshot(sn);
732   
733   MC_UNSET_RAW_MEM;
734     
735   if(raw_mem_set)
736     MC_SET_RAW_MEM;
737   else
738     MC_UNSET_RAW_MEM;
739   
740 }
741
742 void set_pair_visited(xbt_state_t st, int sc){
743
744   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
745  
746   MC_SET_RAW_MEM;
747  
748   mc_pair_visited_t pair = NULL;
749   pair = xbt_new0(s_mc_pair_visited_t, 1);
750   pair->automaton_state = st;
751   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
752   pair->search_cycle = sc;
753   pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
754   MC_take_snapshot_liveness(pair->system_state);
755
756
757   /* Get values of propositional symbols */
758   unsigned int cursor = 0;
759   xbt_propositional_symbol_t ps = NULL;
760   int res;
761   int_f_void_t f;
762
763   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
764     f = (int_f_void_t)ps->function;
765     res = (*f)();
766     xbt_dynar_push_as(pair->prop_ato, int, res);
767   }
768   
769   xbt_dynar_push(visited_pairs, &pair);
770   
771   MC_UNSET_RAW_MEM;
772   
773   if(raw_mem_set)
774     MC_SET_RAW_MEM;
775   else
776     MC_UNSET_RAW_MEM;
777   
778 }
779
780 void MC_pair_delete(mc_pair_t pair){
781   xbt_free(pair->graph_state->proc_status);
782   xbt_free(pair->graph_state);
783   xbt_free(pair);
784 }
785
786
787
788 int MC_automaton_evaluate_label(xbt_exp_label_t l){
789   
790   switch(l->type){
791   case 0 : {
792     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
793     int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
794     return (left_res || right_res);
795   }
796   case 1 : {
797     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
798     int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
799     return (left_res && right_res);
800   }
801   case 2 : {
802     int res = MC_automaton_evaluate_label(l->u.exp_not);
803     return (!res);
804   }
805   case 3 : { 
806     unsigned int cursor = 0;
807     xbt_propositional_symbol_t p = NULL;
808     int_f_void_t f;
809     xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, p){
810       if(strcmp(p->pred, l->u.predicat) == 0){
811         f = (int_f_void_t)p->function;
812         return (*f)();
813       }
814     }
815     return -1;
816   }
817   case 4 : {
818     return 2;
819   }
820   default : 
821     return -1;
822   }
823 }
824
825
826 /********************* Double-DFS stateless *******************/
827
828 void MC_pair_stateless_delete(mc_pair_stateless_t pair){
829   xbt_free(pair->graph_state->proc_status);
830   xbt_free(pair->graph_state);
831   xbt_free(pair);
832 }
833
834 mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r){
835   mc_pair_stateless_t p = NULL;
836   p = xbt_new0(s_mc_pair_stateless_t, 1);
837   p->automaton_state = st;
838   p->graph_state = sg;
839   p->requests = r;
840   mc_stats_pair->expanded_pairs++;
841   return p;
842 }
843
844 void MC_ddfs_init(void){
845
846   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
847
848   XBT_INFO("**************************************************");
849   XBT_INFO("Double-DFS init");
850   XBT_INFO("**************************************************");
851
852   mc_pair_stateless_t mc_initial_pair = NULL;
853   mc_state_t initial_graph_state = NULL;
854   smx_process_t process; 
855
856  
857   MC_wait_for_requests();
858
859   MC_SET_RAW_MEM;
860
861   initial_graph_state = MC_state_pair_new();
862   xbt_swag_foreach(process, simix_global->process_list){
863     if(MC_process_is_enabled(process)){
864       MC_state_interleave_process(initial_graph_state, process);
865     }
866   }
867
868   reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL);
869   //reached_pairs_hash = xbt_dynar_new(sizeof(mc_pair_reached_hash_t), NULL);
870   //visited_pairs = xbt_dynar_new(sizeof(mc_pair_visited_t), NULL);
871   //visited_pairs_hash = xbt_dynar_new(sizeof(mc_pair_visited_hash_t), NULL);
872   successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
873
874   /* Save the initial state */
875   initial_snapshot_liveness = xbt_new0(s_mc_snapshot_t, 1);
876   MC_take_snapshot_liveness(initial_snapshot_liveness);
877
878   MC_UNSET_RAW_MEM; 
879
880   unsigned int cursor = 0;
881   xbt_state_t state;
882
883   xbt_dynar_foreach(_mc_property_automaton->states, cursor, state){
884     if(state->type == -1){
885       
886       MC_SET_RAW_MEM;
887       mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
888       xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
889       MC_UNSET_RAW_MEM;
890       
891       if(cursor != 0){
892         MC_restore_snapshot(initial_snapshot_liveness);
893         MC_UNSET_RAW_MEM;
894       }
895
896       MC_ddfs(0);
897
898     }else{
899       if(state->type == 2){
900       
901         MC_SET_RAW_MEM;
902         mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
903         xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
904         MC_UNSET_RAW_MEM;
905
906         set_pair_reached(state);
907         //set_pair_reached_hash(state);
908
909         if(cursor != 0){
910           MC_restore_snapshot(initial_snapshot_liveness);
911           MC_UNSET_RAW_MEM;
912         }
913   
914         MC_ddfs(1);
915   
916       }
917     }
918   }
919
920   if(raw_mem_set)
921     MC_SET_RAW_MEM;
922   else
923     MC_UNSET_RAW_MEM;
924   
925
926 }
927
928
929 void MC_ddfs(int search_cycle){
930
931   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
932
933   smx_process_t process;
934   mc_pair_stateless_t current_pair = NULL;
935
936   if(xbt_fifo_size(mc_stack_liveness) == 0)
937     return;
938
939
940   /* Get current pair */
941   current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness));
942
943   /* Update current state in buchi automaton */
944   _mc_property_automaton->current_state = current_pair->automaton_state;
945
946  
947   XBT_INFO("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle);
948   XBT_INFO("Pair : graph=%p, automaton=%p(%s), %u interleave", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id, MC_state_interleave_size(current_pair->graph_state));
949  
950   mc_stats_pair->visited_pairs++;
951
952   //sleep(1);
953
954   int value;
955   mc_state_t next_graph_state = NULL;
956   smx_simcall_t req = NULL;
957   char *req_str;
958
959   xbt_transition_t transition_succ;
960   unsigned int cursor = 0;
961   int res;
962
963   mc_pair_stateless_t next_pair = NULL;
964   mc_pair_stateless_t pair_succ;
965   
966   if(xbt_fifo_size(mc_stack_liveness) < MAX_DEPTH_LIVENESS){
967
968     //set_pair_visited(current_pair->automaton_state, search_cycle);
969     //set_pair_visited_hash(current_pair->automaton_state, search_cycle);
970
971     //XBT_INFO("Visited pairs : %lu", xbt_dynar_length(visited_pairs));
972     //XBT_INFO("Visited pairs : %lu", xbt_dynar_length(visited_pairs_hash));
973
974     if(current_pair->requests > 0){
975
976       while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
977    
978         /* Debug information */
979
980         req_str = MC_request_to_string(req, value);
981         XBT_INFO("Execute: %s", req_str);
982         xbt_free(req_str);
983
984         MC_state_set_executed_request(current_pair->graph_state, req, value);   
985
986         /* Answer the request */
987         SIMIX_simcall_pre(req, value);
988
989         /* Wait for requests (schedules processes) */
990         MC_wait_for_requests();
991
992
993         MC_SET_RAW_MEM;
994
995         /* Create the new expanded graph_state */
996         next_graph_state = MC_state_pair_new();
997
998         /* Get enabled process and insert it in the interleave set of the next graph_state */
999         xbt_swag_foreach(process, simix_global->process_list){
1000           if(MC_process_is_enabled(process)){
1001             MC_state_interleave_process(next_graph_state, process);
1002           }
1003         }
1004
1005         xbt_dynar_reset(successors);
1006
1007         MC_UNSET_RAW_MEM;
1008
1009
1010         cursor= 0;
1011         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
1012
1013           res = MC_automaton_evaluate_label(transition_succ->label);
1014
1015           if(res == 1){ // enabled transition in automaton
1016             MC_SET_RAW_MEM;
1017             next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
1018             xbt_dynar_push(successors, &next_pair);
1019             MC_UNSET_RAW_MEM;
1020           }
1021
1022         }
1023
1024         cursor = 0;
1025    
1026         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
1027       
1028           res = MC_automaton_evaluate_label(transition_succ->label);
1029   
1030           if(res == 2){ // true transition in automaton
1031             MC_SET_RAW_MEM;
1032             next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
1033             xbt_dynar_push(successors, &next_pair);
1034             MC_UNSET_RAW_MEM;
1035           }
1036
1037         }
1038
1039         cursor = 0; 
1040   
1041         xbt_dynar_foreach(successors, cursor, pair_succ){
1042
1043           if(search_cycle == 1){
1044
1045             if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ 
1046           
1047               if(reached(pair_succ->automaton_state)){
1048                 //if(reached_hash(pair_succ->automaton_state)){
1049         
1050                 XBT_INFO("Next pair (depth = %d, %u interleave) already reached !", xbt_fifo_size(mc_stack_liveness) + 1, MC_state_interleave_size(pair_succ->graph_state));
1051
1052                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
1053                 XBT_INFO("|             ACCEPTANCE CYCLE            |");
1054                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
1055                 XBT_INFO("Counter-example that violates formula :");
1056                 MC_show_stack_liveness(mc_stack_liveness);
1057                 MC_dump_stack_liveness(mc_stack_liveness);
1058                 MC_print_statistics_pairs(mc_stats_pair);
1059                 exit(0);
1060
1061               }else{
1062
1063                 XBT_INFO("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
1064         
1065                 set_pair_reached(pair_succ->automaton_state);
1066                 //set_pair_reached_hash(pair_succ->automaton_state);
1067
1068                 XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
1069                 //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
1070
1071                 MC_SET_RAW_MEM;
1072                 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1073                 MC_UNSET_RAW_MEM;
1074     
1075                 MC_ddfs(search_cycle);
1076
1077               }
1078
1079             }else{
1080
1081               //if(!visited_hash(pair_succ->automaton_state, search_cycle)){
1082                 //if(!visited(pair_succ->automaton_state, search_cycle)){
1083     
1084                 MC_SET_RAW_MEM;
1085                 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1086                 MC_UNSET_RAW_MEM;
1087     
1088                 MC_ddfs(search_cycle);
1089     
1090                 /*}else{
1091
1092                 XBT_INFO("Next pair already visited ! ");
1093
1094                 }*/
1095         
1096             }
1097
1098           }else{
1099     
1100             if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
1101
1102               XBT_INFO("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
1103       
1104               set_pair_reached(pair_succ->automaton_state); 
1105               //set_pair_reached_hash(pair_succ->automaton_state);
1106
1107               search_cycle = 1;
1108
1109               XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
1110               //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
1111
1112             }
1113
1114             //if(!visited_hash(pair_succ->automaton_state, search_cycle)){
1115               //if(!visited(pair_succ->automaton_state, search_cycle)){
1116         
1117               MC_SET_RAW_MEM;
1118               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1119               MC_UNSET_RAW_MEM;
1120         
1121               MC_ddfs(search_cycle);
1122         
1123               /*}else{
1124
1125               XBT_INFO("Next pair already visited ! ");
1126
1127               }*/
1128
1129           }
1130
1131    
1132           /* Restore system before checking others successors */
1133           if(cursor != (xbt_dynar_length(successors) - 1))
1134             MC_replay_liveness(mc_stack_liveness, 1);
1135   
1136     
1137         }
1138
1139         if(MC_state_interleave_size(current_pair->graph_state) > 0){
1140           XBT_INFO("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
1141           MC_replay_liveness(mc_stack_liveness, 0);
1142         }
1143       }
1144
1145  
1146     }else{  /*No request to execute, search evolution in B├╝chi automaton */
1147
1148       MC_SET_RAW_MEM;
1149
1150       /* Create the new expanded graph_state */
1151       next_graph_state = MC_state_pair_new();
1152
1153       xbt_dynar_reset(successors);
1154
1155       MC_UNSET_RAW_MEM;
1156
1157
1158       cursor= 0;
1159       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
1160
1161         res = MC_automaton_evaluate_label(transition_succ->label);
1162
1163         if(res == 1){ // enabled transition in automaton
1164           MC_SET_RAW_MEM;
1165           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
1166           xbt_dynar_push(successors, &next_pair);
1167           MC_UNSET_RAW_MEM;
1168         }
1169
1170       }
1171
1172       cursor = 0;
1173    
1174       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
1175       
1176         res = MC_automaton_evaluate_label(transition_succ->label);
1177   
1178         if(res == 2){ // true transition in automaton
1179           MC_SET_RAW_MEM;
1180           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
1181           xbt_dynar_push(successors, &next_pair);
1182           MC_UNSET_RAW_MEM;
1183         }
1184
1185       }
1186
1187       cursor = 0; 
1188      
1189       xbt_dynar_foreach(successors, cursor, pair_succ){
1190
1191         if(search_cycle == 1){
1192
1193           if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ 
1194
1195             if(reached(pair_succ->automaton_state)){
1196               //if(reached_hash(pair_succ->automaton_state)){
1197
1198               XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1);
1199         
1200               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
1201               XBT_INFO("|             ACCEPTANCE CYCLE            |");
1202               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
1203               XBT_INFO("Counter-example that violates formula :");
1204               MC_show_stack_liveness(mc_stack_liveness);
1205               MC_dump_stack_liveness(mc_stack_liveness);
1206               MC_print_statistics_pairs(mc_stats_pair);
1207               exit(0);
1208
1209             }else{
1210
1211               XBT_INFO("Next pair (depth = %d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
1212         
1213               set_pair_reached(pair_succ->automaton_state);
1214               //set_pair_reached_hash(pair_succ->automaton_state);
1215     
1216               XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
1217               //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
1218
1219               MC_SET_RAW_MEM;
1220               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1221               MC_UNSET_RAW_MEM;
1222         
1223               MC_ddfs(search_cycle);
1224
1225             }
1226
1227           }else{
1228
1229             //if(!visited_hash(pair_succ->automaton_state, search_cycle)){
1230               //if(!visited(pair_succ->automaton_state, search_cycle)){
1231
1232               MC_SET_RAW_MEM;
1233               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1234               MC_UNSET_RAW_MEM;
1235         
1236               MC_ddfs(search_cycle);
1237         
1238               /*}else{
1239
1240               XBT_INFO("Next pair already visited ! ");
1241
1242               }*/
1243           }
1244       
1245
1246         }else{
1247       
1248           if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
1249
1250             set_pair_reached(pair_succ->automaton_state);
1251             //set_pair_reached_hash(pair_succ->automaton_state);
1252             
1253             search_cycle = 1;
1254
1255             XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
1256             //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
1257
1258           }
1259
1260           //if(!visited_hash(pair_succ->automaton_state, search_cycle)){
1261             //if(!visited(pair_succ->automaton_state, search_cycle)){
1262
1263             MC_SET_RAW_MEM;
1264             xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1265             MC_UNSET_RAW_MEM;
1266       
1267             MC_ddfs(search_cycle);
1268       
1269             /*}else{
1270
1271             XBT_INFO("Next pair already visited ! ");
1272
1273             }*/
1274
1275         }
1276
1277         /* Restore system before checking others successors */
1278         if(cursor != xbt_dynar_length(successors) - 1)
1279           MC_replay_liveness(mc_stack_liveness, 1);
1280
1281    
1282       }
1283            
1284     }
1285     
1286   }else{
1287     
1288     XBT_INFO("Max depth reached");
1289
1290   }
1291
1292   if(xbt_fifo_size(mc_stack_liveness) == MAX_DEPTH_LIVENESS ){
1293     XBT_INFO("Pair (graph=%p, automaton =%p, search_cycle = %d, depth = %d) shifted in stack, maximum depth reached", current_pair->graph_state, current_pair->automaton_state, search_cycle, xbt_fifo_size(mc_stack_liveness) );
1294   }else{
1295     XBT_INFO("Pair (graph=%p, automaton =%p, search_cycle = %d, depth = %d) shifted in stack", current_pair->graph_state, current_pair->automaton_state, search_cycle, xbt_fifo_size(mc_stack_liveness) );
1296   }
1297
1298   
1299   MC_SET_RAW_MEM;
1300   xbt_fifo_shift(mc_stack_liveness);
1301   if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
1302     xbt_dynar_pop(reached_pairs, NULL);
1303     //xbt_dynar_pop(reached_pairs_hash, NULL);
1304   }
1305   MC_UNSET_RAW_MEM;
1306
1307   if(raw_mem_set)
1308     MC_SET_RAW_MEM;
1309   else
1310     MC_UNSET_RAW_MEM;
1311
1312 }