Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : add debug information on processes enabled for each state
[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 = MC_take_snapshot_liveness();  
65   
66   /* Get values of propositional symbols */
67   int res;
68   int_f_void_t f;
69   unsigned int cursor = 0;
70   xbt_propositional_symbol_t ps = NULL;
71   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
72     f = (int_f_void_t)ps->function;
73     res = (*f)();
74     xbt_dynar_push_as(new_pair->prop_ato, int, res);
75   }
76   
77   MC_UNSET_RAW_MEM;
78   
79   if(xbt_dynar_is_empty(reached_pairs)/* || !compare*/){
80
81     MC_SET_RAW_MEM;
82     /* New pair reached */
83     xbt_dynar_push(reached_pairs, &new_pair); 
84     MC_UNSET_RAW_MEM;
85
86     if(raw_mem_set)
87       MC_SET_RAW_MEM;
88  
89     return 0;
90
91   }else{
92
93     MC_SET_RAW_MEM;
94     
95     cursor = 0;
96     mc_pair_reached_t pair_test = NULL;
97      
98     xbt_dynar_foreach(reached_pairs, cursor, pair_test){
99       XBT_INFO("Pair reached #%d", pair_test->nb);
100       if(automaton_state_compare(pair_test->automaton_state, st) == 0){
101         if(propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
102           if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
103             
104             if(raw_mem_set)
105               MC_SET_RAW_MEM;
106             else
107               MC_UNSET_RAW_MEM;
108             
109             return 1;
110           }       
111         }else{
112           XBT_INFO("Different values of propositional symbols");
113         }
114       }else{
115         XBT_INFO("Different automaton state");
116       }
117     }
118
119     /* New pair reached */
120     xbt_dynar_push(reached_pairs, &new_pair); 
121     
122     MC_UNSET_RAW_MEM;
123
124     if(raw_mem_set)
125       MC_SET_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 = MC_take_snapshot_liveness();
147
148   /* Get values of propositional symbols */
149   unsigned int cursor = 0;
150   xbt_propositional_symbol_t ps = NULL;
151   int res;
152   int_f_void_t f;
153
154   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
155     f = (int_f_void_t)ps->function;
156     res = (*f)();
157     xbt_dynar_push_as(pair->prop_ato, int, res);
158   }
159
160   xbt_dynar_push(reached_pairs, &pair); 
161   
162   MC_UNSET_RAW_MEM;
163
164   if(raw_mem_set)
165     MC_SET_RAW_MEM;
166     
167 }
168
169 void MC_pair_delete(mc_pair_t pair){
170   xbt_free(pair->graph_state->proc_status);
171   xbt_free(pair->graph_state);
172   xbt_free(pair);
173 }
174
175
176
177 int MC_automaton_evaluate_label(xbt_exp_label_t l){
178   
179   switch(l->type){
180   case 0 : {
181     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
182     int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
183     return (left_res || right_res);
184   }
185   case 1 : {
186     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
187     int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
188     return (left_res && right_res);
189   }
190   case 2 : {
191     int res = MC_automaton_evaluate_label(l->u.exp_not);
192     return (!res);
193   }
194   case 3 : { 
195     unsigned int cursor = 0;
196     xbt_propositional_symbol_t p = NULL;
197     int_f_void_t f;
198     xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, p){
199       if(strcmp(p->pred, l->u.predicat) == 0){
200         f = (int_f_void_t)p->function;
201         return (*f)();
202       }
203     }
204     return -1;
205   }
206   case 4 : {
207     return 2;
208   }
209   default : 
210     return -1;
211   }
212 }
213
214
215 /********************* Double-DFS stateless *******************/
216
217 void pair_stateless_free(mc_pair_stateless_t pair){
218   xbt_free(pair->graph_state->system_state);
219   xbt_free(pair->graph_state->proc_status);
220   xbt_free(pair->graph_state);
221   xbt_free(pair);
222 }
223
224 void pair_stateless_free_voidp(void *p){
225   pair_stateless_free((mc_pair_stateless_t) * (void **) p);
226 }
227
228 mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r){
229   mc_pair_stateless_t p = NULL;
230   p = xbt_new0(s_mc_pair_stateless_t, 1);
231   p->automaton_state = st;
232   p->graph_state = sg;
233   p->requests = r;
234   mc_stats_pair->expanded_pairs++;
235   return p;
236 }
237
238 void pair_reached_free(mc_pair_reached_t pair){
239   if(pair){
240     pair->automaton_state = NULL;
241     xbt_dynar_free(&(pair->prop_ato));
242     MC_free_snapshot(pair->system_state);
243     xbt_free(pair);
244   }
245 }
246
247 void pair_reached_free_voidp(void *p){
248   pair_reached_free((mc_pair_reached_t) * (void **) p);
249 }
250
251 void MC_ddfs_init(void){
252
253   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
254
255   XBT_INFO("**************************************************");
256   XBT_INFO("Double-DFS init");
257   XBT_INFO("**************************************************");
258
259   mc_pair_stateless_t mc_initial_pair = NULL;
260   mc_state_t initial_graph_state = NULL;
261   smx_process_t process; 
262
263  
264   MC_wait_for_requests();
265
266   MC_SET_RAW_MEM;
267
268   initial_graph_state = MC_state_pair_new();
269   xbt_swag_foreach(process, simix_global->process_list){
270     if(MC_process_is_enabled(process)){
271       MC_state_interleave_process(initial_graph_state, process);
272     }
273   }
274
275   reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), pair_reached_free_voidp);
276   successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
277
278   /* Save the initial state */
279   initial_state_liveness = xbt_new0(s_mc_global_t, 1);
280   initial_state_liveness->initial_snapshot = MC_take_snapshot_liveness();
281
282   MC_UNSET_RAW_MEM; 
283   
284   unsigned int cursor = 0;
285   xbt_state_t state;
286
287   xbt_dynar_foreach(_mc_property_automaton->states, cursor, state){
288     if(state->type == -1){
289       
290       MC_SET_RAW_MEM;
291       mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
292       xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
293       MC_UNSET_RAW_MEM;
294       
295       if(cursor != 0){
296         MC_restore_snapshot(initial_state_liveness->initial_snapshot);
297         MC_UNSET_RAW_MEM;
298       }
299
300       MC_ddfs(0);
301
302     }else{
303       if(state->type == 2){
304       
305         MC_SET_RAW_MEM;
306         mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
307         xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
308         MC_UNSET_RAW_MEM;
309
310         set_pair_reached(state);
311
312         if(cursor != 0){
313           MC_restore_snapshot(initial_state_liveness->initial_snapshot);
314           MC_UNSET_RAW_MEM;
315         }
316   
317         MC_ddfs(1);
318   
319       }
320     }
321   }
322
323   if(raw_mem_set)
324     MC_SET_RAW_MEM;
325   else
326     MC_UNSET_RAW_MEM;
327   
328
329 }
330
331
332 void MC_ddfs(int search_cycle){
333
334   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
335
336   smx_process_t process;
337   mc_pair_stateless_t current_pair = NULL;
338
339   if(xbt_fifo_size(mc_stack_liveness) == 0)
340     return;
341
342
343   /* Get current pair */
344   current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness));
345
346   /* Update current state in buchi automaton */
347   _mc_property_automaton->current_state = current_pair->automaton_state;
348
349  
350   XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle);
351  
352   mc_stats_pair->visited_pairs++;
353
354   //sleep(1);
355
356   int value;
357   mc_state_t next_graph_state = NULL;
358   smx_simcall_t req = NULL;
359   char *req_str;
360
361   xbt_transition_t transition_succ;
362   unsigned int cursor = 0;
363   int res;
364
365   mc_pair_stateless_t next_pair = NULL;
366   mc_pair_stateless_t pair_succ;
367
368   mc_pair_stateless_t remove_pair;
369   mc_pair_reached_t remove_pair_reached;
370   
371   if(xbt_fifo_size(mc_stack_liveness) < MAX_DEPTH_LIVENESS){
372
373     if(current_pair->requests > 0){
374
375       while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
376    
377         /* Debug information */
378        
379         req_str = MC_request_to_string(req, value);
380         XBT_DEBUG("Execute: %s", req_str);
381         xbt_free(req_str);
382
383         MC_state_set_executed_request(current_pair->graph_state, req, value);   
384
385         /* Answer the request */
386         SIMIX_simcall_pre(req, value);
387
388         /* Wait for requests (schedules processes) */
389         MC_wait_for_requests();
390
391         MC_SET_RAW_MEM;
392
393         /* Create the new expanded graph_state */
394         next_graph_state = MC_state_pair_new();
395
396         /* Get enabled process and insert it in the interleave set of the next graph_state */
397
398         xbt_swag_foreach(process, simix_global->process_list){
399           if(MC_process_is_enabled(process)){
400             XBT_DEBUG("Process %lu enabled with simcall : %d", process->pid, (&process->simcall)->call); 
401           }
402         }
403
404         xbt_swag_foreach(process, simix_global->process_list){
405           if(MC_process_is_enabled(process)){
406             MC_state_interleave_process(next_graph_state, process);
407           }
408         }
409
410         xbt_dynar_reset(successors);
411
412         MC_UNSET_RAW_MEM;
413
414
415         cursor= 0;
416         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
417
418           res = MC_automaton_evaluate_label(transition_succ->label);
419
420           if(res == 1){ // enabled transition in automaton
421             MC_SET_RAW_MEM;
422             next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
423             xbt_dynar_push(successors, &next_pair);
424             MC_UNSET_RAW_MEM;
425           }
426
427         }
428
429         cursor = 0;
430    
431         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
432       
433           res = MC_automaton_evaluate_label(transition_succ->label);
434   
435           if(res == 2){ // true transition in automaton
436             MC_SET_RAW_MEM;
437             next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
438             xbt_dynar_push(successors, &next_pair);
439             MC_UNSET_RAW_MEM;
440           }
441
442         }
443
444         cursor = 0; 
445   
446         xbt_dynar_foreach(successors, cursor, pair_succ){
447
448           if(search_cycle == 1){
449
450             if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ 
451           
452               if(reached(pair_succ->automaton_state)){
453         
454                 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));
455
456                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
457                 XBT_INFO("|             ACCEPTANCE CYCLE            |");
458                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
459                 XBT_INFO("Counter-example that violates formula :");
460                 MC_show_stack_liveness(mc_stack_liveness);
461                 MC_dump_stack_liveness(mc_stack_liveness);
462                 MC_print_statistics_pairs(mc_stats_pair);
463                 xbt_abort();
464
465               }else{
466
467                 XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
468
469                 XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
470
471                 MC_SET_RAW_MEM;
472                 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
473                 MC_UNSET_RAW_MEM;
474     
475                 MC_ddfs(search_cycle);
476
477               }
478
479             }else{
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           }else{
490     
491             if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
492
493               XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
494       
495               set_pair_reached(pair_succ->automaton_state); 
496
497               search_cycle = 1;
498
499               XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
500
501             }
502
503             MC_SET_RAW_MEM;
504             xbt_fifo_unshift(mc_stack_liveness, pair_succ);
505             MC_UNSET_RAW_MEM;
506             
507             MC_ddfs(search_cycle);
508            
509           }
510
511    
512           /* Restore system before checking others successors */
513           if(cursor != (xbt_dynar_length(successors) - 1))
514             MC_replay_liveness(mc_stack_liveness, 1);
515   
516     
517         }
518
519         if(MC_state_interleave_size(current_pair->graph_state) > 0){
520           XBT_DEBUG("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
521           MC_replay_liveness(mc_stack_liveness, 0);
522         }
523       }
524
525  
526     }else{
527       
528       XBT_DEBUG("No more request to execute in this state, search evolution in B├╝chi Automaton.");
529
530       MC_SET_RAW_MEM;
531
532       /* Create the new expanded graph_state */
533       next_graph_state = MC_state_pair_new();
534
535       xbt_dynar_reset(successors);
536
537       MC_UNSET_RAW_MEM;
538
539
540       cursor= 0;
541       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
542
543         res = MC_automaton_evaluate_label(transition_succ->label);
544
545         if(res == 1){ // enabled transition in automaton
546           MC_SET_RAW_MEM;
547           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
548           xbt_dynar_push(successors, &next_pair);
549           MC_UNSET_RAW_MEM;
550         }
551
552       }
553
554       cursor = 0;
555    
556       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
557       
558         res = MC_automaton_evaluate_label(transition_succ->label);
559   
560         if(res == 2){ // true transition in automaton
561           MC_SET_RAW_MEM;
562           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
563           xbt_dynar_push(successors, &next_pair);
564           MC_UNSET_RAW_MEM;
565         }
566
567       }
568
569       cursor = 0; 
570      
571       xbt_dynar_foreach(successors, cursor, pair_succ){
572
573         if(search_cycle == 1){
574
575           if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ 
576
577             if(reached(pair_succ->automaton_state)){
578            
579               XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1);
580         
581               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
582               XBT_INFO("|             ACCEPTANCE CYCLE            |");
583               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
584               XBT_INFO("Counter-example that violates formula :");
585               MC_show_stack_liveness(mc_stack_liveness);
586               MC_dump_stack_liveness(mc_stack_liveness);
587               MC_print_statistics_pairs(mc_stats_pair);
588               exit(0);
589
590             }else{
591
592               XBT_INFO("Next pair (depth = %d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
593         
594               XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
595
596               MC_SET_RAW_MEM;
597               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
598               MC_UNSET_RAW_MEM;
599         
600               MC_ddfs(search_cycle);
601
602             }
603
604           }else{
605
606             MC_SET_RAW_MEM;
607             xbt_fifo_unshift(mc_stack_liveness, pair_succ);
608             MC_UNSET_RAW_MEM;
609             
610             MC_ddfs(search_cycle);
611             
612           }
613       
614
615         }else{
616       
617           if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
618
619             set_pair_reached(pair_succ->automaton_state);
620          
621             search_cycle = 1;
622
623             XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
624
625           }
626
627           MC_SET_RAW_MEM;
628           xbt_fifo_unshift(mc_stack_liveness, pair_succ);
629           MC_UNSET_RAW_MEM;
630           
631           MC_ddfs(search_cycle);
632           
633         }
634
635         /* Restore system before checking others successors */
636         if(cursor != xbt_dynar_length(successors) - 1)
637           MC_replay_liveness(mc_stack_liveness, 1);
638
639       }           
640
641     }
642     
643   }else{
644     
645     XBT_DEBUG("Max depth reached");
646
647   }
648
649   if(xbt_fifo_size(mc_stack_liveness) == MAX_DEPTH_LIVENESS ){
650     XBT_DEBUG("Pair (depth = %d) shifted in stack, maximum depth reached", xbt_fifo_size(mc_stack_liveness) );
651   }else{
652     XBT_DEBUG("Pair (depth = %d) shifted in stack", xbt_fifo_size(mc_stack_liveness) );
653   }
654
655   
656   MC_SET_RAW_MEM;
657   remove_pair = xbt_fifo_shift(mc_stack_liveness);
658   xbt_fifo_remove(mc_stack_liveness, remove_pair);
659   remove_pair = NULL;
660   if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
661     remove_pair_reached = xbt_dynar_pop_as(reached_pairs, mc_pair_reached_t);
662     pair_reached_free(remove_pair_reached);
663     remove_pair_reached = NULL;
664   }
665   MC_UNSET_RAW_MEM;
666
667   if(raw_mem_set)
668     MC_SET_RAW_MEM;
669
670 }