Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : move functions about snapshot comparison in a separate file mc_compare.c
[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 successors;
15
16 int create_dump(int pair)
17 {
18    // Try to enable core dumps
19   struct rlimit core_limit;
20   core_limit.rlim_cur = RLIM_INFINITY;
21   core_limit.rlim_max = RLIM_INFINITY;
22   
23   if(setrlimit(RLIMIT_CORE, &core_limit) < 0)
24     fprintf(stderr, "setrlimit: %s\nWarning: core dumps may be truncated or non-existant\n", strerror(errno));
25   
26   int status;
27   switch(fork()){
28   case 0:
29     // We are the child process -- run the actual program
30     xbt_abort();
31     break;
32     
33   case -1:
34     // An error occurred, shouldn't happen
35     perror("fork");
36     return -1;
37     
38   default:
39     // We are the parent process -- wait for the child process to exit
40     if(wait(&status) < 0)
41       perror("wait");
42     if(WIFSIGNALED(status) && WCOREDUMP(status)){
43       char *core_name = malloc(20);
44       sprintf(core_name,"core_%d", pair); 
45       rename("core", core_name);
46       free(core_name);
47     }
48   }
49
50   return 0;
51 }
52
53 int reached(xbt_state_t st){
54
55   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
56
57   MC_SET_RAW_MEM;
58
59   mc_pair_reached_t new_pair = NULL;
60   new_pair = xbt_new0(s_mc_pair_reached_t, 1);
61   new_pair->nb = xbt_dynar_length(reached_pairs) + 1;
62   new_pair->automaton_state = st;
63   new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
64   new_pair->system_state = xbt_new0(s_mc_snapshot_t, 1); 
65   MC_take_snapshot_liveness(new_pair->system_state);  
66   
67   /* Get values of propositional symbols */
68   int res;
69   int_f_void_t f;
70   unsigned int cursor = 0;
71   xbt_propositional_symbol_t ps = NULL;
72   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
73     f = (int_f_void_t)ps->function;
74     res = (*f)();
75     xbt_dynar_push_as(new_pair->prop_ato, int, res);
76   }
77   
78   MC_UNSET_RAW_MEM;
79   
80   if(xbt_dynar_is_empty(reached_pairs) || !compare){
81
82     MC_SET_RAW_MEM;
83     /* New pair reached */
84     xbt_dynar_push(reached_pairs, &new_pair); 
85     MC_UNSET_RAW_MEM;
86  
87     return 0;
88
89   }else{
90
91     MC_SET_RAW_MEM;
92     
93     cursor = 0;
94     mc_pair_reached_t pair_test = NULL;
95      
96     xbt_dynar_foreach(reached_pairs, cursor, pair_test){
97       XBT_INFO("Pair reached #%d", pair_test->nb);
98       if(automaton_state_compare(pair_test->automaton_state, st) == 0){
99         if(propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
100           if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
101             
102             if(raw_mem_set)
103               MC_SET_RAW_MEM;
104             else
105               MC_UNSET_RAW_MEM;
106             
107             return 1;
108           }       
109         }else{
110           XBT_INFO("Different values of propositional symbols");
111         }
112       }else{
113         XBT_INFO("Different automaton state");
114       }
115     }
116
117     /* New pair reached */
118     xbt_dynar_push(reached_pairs, &new_pair); 
119     
120     MC_UNSET_RAW_MEM;
121
122     if(raw_mem_set)
123       MC_SET_RAW_MEM;
124     else
125       MC_UNSET_RAW_MEM;
126
127     compare = 0;
128     
129     return 0;
130     
131   }
132 }
133
134
135 void set_pair_reached(xbt_state_t st){
136
137   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
138  
139   MC_SET_RAW_MEM;
140
141   mc_pair_reached_t pair = NULL;
142   pair = xbt_new0(s_mc_pair_reached_t, 1);
143   pair->nb = xbt_dynar_length(reached_pairs) + 1;
144   pair->automaton_state = st;
145   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
146   pair->system_state = xbt_new0(s_mc_snapshot_t, 1); 
147   MC_take_snapshot_liveness(pair->system_state);
148
149   /* Get values of propositional symbols */
150   unsigned int cursor = 0;
151   xbt_propositional_symbol_t ps = NULL;
152   int res;
153   int_f_void_t f;
154
155   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
156     f = (int_f_void_t)ps->function;
157     res = (*f)();
158     xbt_dynar_push_as(pair->prop_ato, int, res);
159   }
160
161   xbt_dynar_push(reached_pairs, &pair); 
162   
163   MC_UNSET_RAW_MEM;
164
165   if(raw_mem_set)
166     MC_SET_RAW_MEM;
167   else
168     MC_UNSET_RAW_MEM;
169     
170 }
171
172 void MC_pair_delete(mc_pair_t pair){
173   xbt_free(pair->graph_state->proc_status);
174   xbt_free(pair->graph_state);
175   xbt_free(pair);
176 }
177
178
179
180 int MC_automaton_evaluate_label(xbt_exp_label_t l){
181   
182   switch(l->type){
183   case 0 : {
184     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
185     int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
186     return (left_res || right_res);
187   }
188   case 1 : {
189     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
190     int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
191     return (left_res && right_res);
192   }
193   case 2 : {
194     int res = MC_automaton_evaluate_label(l->u.exp_not);
195     return (!res);
196   }
197   case 3 : { 
198     unsigned int cursor = 0;
199     xbt_propositional_symbol_t p = NULL;
200     int_f_void_t f;
201     xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, p){
202       if(strcmp(p->pred, l->u.predicat) == 0){
203         f = (int_f_void_t)p->function;
204         return (*f)();
205       }
206     }
207     return -1;
208   }
209   case 4 : {
210     return 2;
211   }
212   default : 
213     return -1;
214   }
215 }
216
217
218 /********************* Double-DFS stateless *******************/
219
220 void MC_pair_stateless_delete(mc_pair_stateless_t pair){
221   xbt_free(pair->graph_state->proc_status);
222   xbt_free(pair->graph_state);
223   xbt_free(pair);
224 }
225
226 mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r){
227   mc_pair_stateless_t p = NULL;
228   p = xbt_new0(s_mc_pair_stateless_t, 1);
229   p->automaton_state = st;
230   p->graph_state = sg;
231   p->requests = r;
232   mc_stats_pair->expanded_pairs++;
233   return p;
234 }
235
236 void MC_ddfs_init(void){
237
238   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
239
240   XBT_INFO("**************************************************");
241   XBT_INFO("Double-DFS init");
242   XBT_INFO("**************************************************");
243
244   mc_pair_stateless_t mc_initial_pair = NULL;
245   mc_state_t initial_graph_state = NULL;
246   smx_process_t process; 
247
248  
249   MC_wait_for_requests();
250
251   MC_SET_RAW_MEM;
252
253   initial_graph_state = MC_state_pair_new();
254   xbt_swag_foreach(process, simix_global->process_list){
255     if(MC_process_is_enabled(process)){
256       MC_state_interleave_process(initial_graph_state, process);
257     }
258   }
259
260   reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL);
261   successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
262
263   /* Save the initial state */
264   initial_snapshot_liveness = xbt_new0(s_mc_snapshot_t, 1);
265   MC_take_snapshot_liveness(initial_snapshot_liveness);
266
267   MC_UNSET_RAW_MEM; 
268
269   /* Get .plt section (start and end addresses) for data libsimgrid comparison */
270   get_plt_section();
271
272   unsigned int cursor = 0;
273   xbt_state_t state;
274
275   xbt_dynar_foreach(_mc_property_automaton->states, cursor, state){
276     if(state->type == -1){
277       
278       MC_SET_RAW_MEM;
279       mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
280       xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
281       MC_UNSET_RAW_MEM;
282       
283       if(cursor != 0){
284         MC_restore_snapshot(initial_snapshot_liveness);
285         MC_UNSET_RAW_MEM;
286       }
287
288       MC_ddfs(0);
289
290     }else{
291       if(state->type == 2){
292       
293         MC_SET_RAW_MEM;
294         mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
295         xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
296         MC_UNSET_RAW_MEM;
297
298         set_pair_reached(state);
299
300         if(cursor != 0){
301           MC_restore_snapshot(initial_snapshot_liveness);
302           MC_UNSET_RAW_MEM;
303         }
304   
305         MC_ddfs(1);
306   
307       }
308     }
309   }
310
311   if(raw_mem_set)
312     MC_SET_RAW_MEM;
313   else
314     MC_UNSET_RAW_MEM;
315   
316
317 }
318
319
320 void MC_ddfs(int search_cycle){
321
322   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
323
324   smx_process_t process;
325   mc_pair_stateless_t current_pair = NULL;
326
327   if(xbt_fifo_size(mc_stack_liveness) == 0)
328     return;
329
330
331   /* Get current pair */
332   current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness));
333
334   /* Update current state in buchi automaton */
335   _mc_property_automaton->current_state = current_pair->automaton_state;
336
337  
338   XBT_INFO("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle);
339  
340   mc_stats_pair->visited_pairs++;
341
342   //sleep(1);
343
344   int value;
345   mc_state_t next_graph_state = NULL;
346   smx_simcall_t req = NULL;
347   char *req_str;
348
349   xbt_transition_t transition_succ;
350   unsigned int cursor = 0;
351   int res;
352
353   mc_pair_stateless_t next_pair = NULL;
354   mc_pair_stateless_t pair_succ;
355   
356   if(xbt_fifo_size(mc_stack_liveness) < MAX_DEPTH_LIVENESS){
357
358     if(current_pair->requests > 0){
359
360       while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
361    
362         /* Debug information */
363        
364         req_str = MC_request_to_string(req, value);
365         XBT_INFO("Execute: %s", req_str);
366         xbt_free(req_str);
367
368         MC_state_set_executed_request(current_pair->graph_state, req, value);   
369
370         /* Answer the request */
371         SIMIX_simcall_pre(req, value);
372
373         /* Wait for requests (schedules processes) */
374         MC_wait_for_requests();
375
376         MC_SET_RAW_MEM;
377
378         /* Create the new expanded graph_state */
379         next_graph_state = MC_state_pair_new();
380
381         /* Get enabled process and insert it in the interleave set of the next graph_state */
382         xbt_swag_foreach(process, simix_global->process_list){
383           if(MC_process_is_enabled(process)){
384             MC_state_interleave_process(next_graph_state, process);
385           }
386         }
387
388         xbt_dynar_reset(successors);
389
390         MC_UNSET_RAW_MEM;
391
392
393         cursor= 0;
394         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
395
396           res = MC_automaton_evaluate_label(transition_succ->label);
397
398           if(res == 1){ // enabled transition in automaton
399             MC_SET_RAW_MEM;
400             next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
401             xbt_dynar_push(successors, &next_pair);
402             MC_UNSET_RAW_MEM;
403           }
404
405         }
406
407         cursor = 0;
408    
409         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
410       
411           res = MC_automaton_evaluate_label(transition_succ->label);
412   
413           if(res == 2){ // true transition in automaton
414             MC_SET_RAW_MEM;
415             next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
416             xbt_dynar_push(successors, &next_pair);
417             MC_UNSET_RAW_MEM;
418           }
419
420         }
421
422         cursor = 0; 
423   
424         xbt_dynar_foreach(successors, cursor, pair_succ){
425
426           if(search_cycle == 1){
427
428             if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ 
429           
430               if(reached(pair_succ->automaton_state)){
431         
432                 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));
433
434                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
435                 XBT_INFO("|             ACCEPTANCE CYCLE            |");
436                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
437                 XBT_INFO("Counter-example that violates formula :");
438                 MC_show_stack_liveness(mc_stack_liveness);
439                 MC_dump_stack_liveness(mc_stack_liveness);
440                 MC_print_statistics_pairs(mc_stats_pair);
441                 exit(0);
442
443               }else{
444
445                 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);
446
447                 XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
448
449                 MC_SET_RAW_MEM;
450                 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
451                 MC_UNSET_RAW_MEM;
452     
453                 MC_ddfs(search_cycle);
454
455               }
456
457             }else{
458
459               MC_SET_RAW_MEM;
460               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
461               MC_UNSET_RAW_MEM;
462               
463               MC_ddfs(search_cycle);
464                
465             }
466
467           }else{
468     
469             if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
470
471               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);
472       
473               set_pair_reached(pair_succ->automaton_state); 
474
475               search_cycle = 1;
476
477               XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
478
479             }
480
481             MC_SET_RAW_MEM;
482             xbt_fifo_unshift(mc_stack_liveness, pair_succ);
483             MC_UNSET_RAW_MEM;
484             
485             MC_ddfs(search_cycle);
486            
487           }
488
489    
490           /* Restore system before checking others successors */
491           if(cursor != (xbt_dynar_length(successors) - 1))
492             MC_replay_liveness(mc_stack_liveness, 1);
493   
494     
495         }
496
497         if(MC_state_interleave_size(current_pair->graph_state) > 0){
498           XBT_INFO("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
499           MC_replay_liveness(mc_stack_liveness, 0);
500         }
501       }
502
503  
504     }else{  /*No request to execute, search evolution in B├╝chi automaton */
505
506       MC_SET_RAW_MEM;
507
508       /* Create the new expanded graph_state */
509       next_graph_state = MC_state_pair_new();
510
511       xbt_dynar_reset(successors);
512
513       MC_UNSET_RAW_MEM;
514
515
516       cursor= 0;
517       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
518
519         res = MC_automaton_evaluate_label(transition_succ->label);
520
521         if(res == 1){ // enabled transition in automaton
522           MC_SET_RAW_MEM;
523           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
524           xbt_dynar_push(successors, &next_pair);
525           MC_UNSET_RAW_MEM;
526         }
527
528       }
529
530       cursor = 0;
531    
532       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
533       
534         res = MC_automaton_evaluate_label(transition_succ->label);
535   
536         if(res == 2){ // true transition in automaton
537           MC_SET_RAW_MEM;
538           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
539           xbt_dynar_push(successors, &next_pair);
540           MC_UNSET_RAW_MEM;
541         }
542
543       }
544
545       cursor = 0; 
546      
547       xbt_dynar_foreach(successors, cursor, pair_succ){
548
549         if(search_cycle == 1){
550
551           if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ 
552
553             if(reached(pair_succ->automaton_state)){
554            
555               XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1);
556         
557               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
558               XBT_INFO("|             ACCEPTANCE CYCLE            |");
559               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
560               XBT_INFO("Counter-example that violates formula :");
561               MC_show_stack_liveness(mc_stack_liveness);
562               MC_dump_stack_liveness(mc_stack_liveness);
563               MC_print_statistics_pairs(mc_stats_pair);
564               exit(0);
565
566             }else{
567
568               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);
569         
570               XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
571
572               MC_SET_RAW_MEM;
573               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
574               MC_UNSET_RAW_MEM;
575         
576               MC_ddfs(search_cycle);
577
578             }
579
580           }else{
581
582             MC_SET_RAW_MEM;
583             xbt_fifo_unshift(mc_stack_liveness, pair_succ);
584             MC_UNSET_RAW_MEM;
585             
586             MC_ddfs(search_cycle);
587             
588           }
589       
590
591         }else{
592       
593           if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
594
595             set_pair_reached(pair_succ->automaton_state);
596          
597             search_cycle = 1;
598
599             XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
600
601           }
602
603           MC_SET_RAW_MEM;
604           xbt_fifo_unshift(mc_stack_liveness, pair_succ);
605           MC_UNSET_RAW_MEM;
606           
607           MC_ddfs(search_cycle);
608           
609         }
610
611         /* Restore system before checking others successors */
612         if(cursor != xbt_dynar_length(successors) - 1)
613           MC_replay_liveness(mc_stack_liveness, 1);
614
615    
616       }
617            
618     }
619     
620   }else{
621     
622     XBT_INFO("Max depth reached");
623
624   }
625
626   if(xbt_fifo_size(mc_stack_liveness) == MAX_DEPTH_LIVENESS ){
627     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) );
628   }else{
629     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) );
630   }
631
632   
633   MC_SET_RAW_MEM;
634   xbt_fifo_shift(mc_stack_liveness);
635   if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
636     xbt_dynar_pop(reached_pairs, NULL);
637   }
638   MC_UNSET_RAW_MEM;
639
640   if(raw_mem_set)
641     MC_SET_RAW_MEM;
642   else
643     MC_UNSET_RAW_MEM;
644
645 }