Logo AND Algorithmique Numérique Distribuée

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