Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : move creation of initial_state_liveness in MC_init_liveness
[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->initial_snapshot = MC_take_snapshot_liveness();
280
281   MC_UNSET_RAW_MEM; 
282   
283   unsigned int cursor = 0;
284   xbt_state_t state;
285
286   xbt_dynar_foreach(_mc_property_automaton->states, cursor, state){
287     if(state->type == -1){
288       
289       MC_SET_RAW_MEM;
290       mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
291       xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
292       MC_UNSET_RAW_MEM;
293       
294       if(cursor != 0){
295         MC_restore_snapshot(initial_state_liveness->initial_snapshot);
296         MC_UNSET_RAW_MEM;
297       }
298
299       MC_ddfs(0);
300
301     }else{
302       if(state->type == 2){
303       
304         MC_SET_RAW_MEM;
305         mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
306         xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
307         MC_UNSET_RAW_MEM;
308
309         set_pair_reached(state);
310
311         if(cursor != 0){
312           MC_restore_snapshot(initial_state_liveness->initial_snapshot);
313           MC_UNSET_RAW_MEM;
314         }
315   
316         MC_ddfs(1);
317   
318       }
319     }
320   }
321
322   if(raw_mem_set)
323     MC_SET_RAW_MEM;
324   else
325     MC_UNSET_RAW_MEM;
326   
327
328 }
329
330
331 void MC_ddfs(int search_cycle){
332
333   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
334
335   smx_process_t process;
336   mc_pair_stateless_t current_pair = NULL;
337
338   if(xbt_fifo_size(mc_stack_liveness) == 0)
339     return;
340
341
342   /* Get current pair */
343   current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness));
344
345   /* Update current state in buchi automaton */
346   _mc_property_automaton->current_state = current_pair->automaton_state;
347
348  
349   XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle);
350  
351   mc_stats_pair->visited_pairs++;
352
353   //sleep(1);
354
355   int value;
356   mc_state_t next_graph_state = NULL;
357   smx_simcall_t req = NULL;
358   char *req_str;
359
360   xbt_transition_t transition_succ;
361   unsigned int cursor = 0;
362   int res;
363
364   mc_pair_stateless_t next_pair = NULL;
365   mc_pair_stateless_t pair_succ;
366
367   mc_pair_stateless_t remove_pair;
368   mc_pair_reached_t remove_pair_reached;
369   
370   if(xbt_fifo_size(mc_stack_liveness) < MAX_DEPTH_LIVENESS){
371
372     if(current_pair->requests > 0){
373
374       while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
375    
376         /* Debug information */
377        
378         req_str = MC_request_to_string(req, value);
379         XBT_DEBUG("Execute: %s", req_str);
380         xbt_free(req_str);
381
382         MC_state_set_executed_request(current_pair->graph_state, req, value);   
383
384         /* Answer the request */
385         SIMIX_simcall_pre(req, value);
386
387         /* Wait for requests (schedules processes) */
388         MC_wait_for_requests();
389
390         MC_SET_RAW_MEM;
391
392         /* Create the new expanded graph_state */
393         next_graph_state = MC_state_pair_new();
394
395         /* Get enabled process and insert it in the interleave set of the next graph_state */
396
397         xbt_swag_foreach(process, simix_global->process_list){
398           if(MC_process_is_enabled(process)){
399             XBT_DEBUG("Process %lu enabled with simcall : %d", process->pid, (&process->simcall)->call); 
400           }
401         }
402
403         xbt_swag_foreach(process, simix_global->process_list){
404           if(MC_process_is_enabled(process)){
405             MC_state_interleave_process(next_graph_state, process);
406           }
407         }
408
409         xbt_dynar_reset(successors);
410
411         MC_UNSET_RAW_MEM;
412
413
414         cursor= 0;
415         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
416
417           res = MC_automaton_evaluate_label(transition_succ->label);
418
419           if(res == 1){ // enabled transition in automaton
420             MC_SET_RAW_MEM;
421             next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
422             xbt_dynar_push(successors, &next_pair);
423             MC_UNSET_RAW_MEM;
424           }
425
426         }
427
428         cursor = 0;
429    
430         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
431       
432           res = MC_automaton_evaluate_label(transition_succ->label);
433   
434           if(res == 2){ // true transition in automaton
435             MC_SET_RAW_MEM;
436             next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
437             xbt_dynar_push(successors, &next_pair);
438             MC_UNSET_RAW_MEM;
439           }
440
441         }
442
443         cursor = 0; 
444   
445         xbt_dynar_foreach(successors, cursor, pair_succ){
446
447           if(search_cycle == 1){
448
449             if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ 
450           
451               if(reached(pair_succ->automaton_state)){
452         
453                 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));
454
455                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
456                 XBT_INFO("|             ACCEPTANCE CYCLE            |");
457                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
458                 XBT_INFO("Counter-example that violates formula :");
459                 MC_show_stack_liveness(mc_stack_liveness);
460                 MC_dump_stack_liveness(mc_stack_liveness);
461                 MC_print_statistics_pairs(mc_stats_pair);
462                 xbt_abort();
463
464               }else{
465
466                 XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
467
468                 XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
469
470                 MC_SET_RAW_MEM;
471                 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
472                 MC_UNSET_RAW_MEM;
473     
474                 MC_ddfs(search_cycle);
475
476               }
477
478             }else{
479
480               MC_SET_RAW_MEM;
481               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
482               MC_UNSET_RAW_MEM;
483               
484               MC_ddfs(search_cycle);
485                
486             }
487
488           }else{
489     
490             if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
491
492               XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
493       
494               set_pair_reached(pair_succ->automaton_state); 
495
496               search_cycle = 1;
497
498               XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
499
500             }
501
502             MC_SET_RAW_MEM;
503             xbt_fifo_unshift(mc_stack_liveness, pair_succ);
504             MC_UNSET_RAW_MEM;
505             
506             MC_ddfs(search_cycle);
507            
508           }
509
510    
511           /* Restore system before checking others successors */
512           if(cursor != (xbt_dynar_length(successors) - 1))
513             MC_replay_liveness(mc_stack_liveness, 1);
514   
515     
516         }
517
518         if(MC_state_interleave_size(current_pair->graph_state) > 0){
519           XBT_DEBUG("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
520           MC_replay_liveness(mc_stack_liveness, 0);
521         }
522       }
523
524  
525     }else{
526       
527       XBT_DEBUG("No more request to execute in this state, search evolution in B├╝chi Automaton.");
528
529       MC_SET_RAW_MEM;
530
531       /* Create the new expanded graph_state */
532       next_graph_state = MC_state_pair_new();
533
534       xbt_dynar_reset(successors);
535
536       MC_UNSET_RAW_MEM;
537
538
539       cursor= 0;
540       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
541
542         res = MC_automaton_evaluate_label(transition_succ->label);
543
544         if(res == 1){ // enabled transition in automaton
545           MC_SET_RAW_MEM;
546           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
547           xbt_dynar_push(successors, &next_pair);
548           MC_UNSET_RAW_MEM;
549         }
550
551       }
552
553       cursor = 0;
554    
555       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
556       
557         res = MC_automaton_evaluate_label(transition_succ->label);
558   
559         if(res == 2){ // true transition in automaton
560           MC_SET_RAW_MEM;
561           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
562           xbt_dynar_push(successors, &next_pair);
563           MC_UNSET_RAW_MEM;
564         }
565
566       }
567
568       cursor = 0; 
569      
570       xbt_dynar_foreach(successors, cursor, pair_succ){
571
572         if(search_cycle == 1){
573
574           if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ 
575
576             if(reached(pair_succ->automaton_state)){
577            
578               XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1);
579         
580               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
581               XBT_INFO("|             ACCEPTANCE CYCLE            |");
582               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
583               XBT_INFO("Counter-example that violates formula :");
584               MC_show_stack_liveness(mc_stack_liveness);
585               MC_dump_stack_liveness(mc_stack_liveness);
586               MC_print_statistics_pairs(mc_stats_pair);
587               exit(0);
588
589             }else{
590
591               XBT_INFO("Next pair (depth = %d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
592         
593               XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
594
595               MC_SET_RAW_MEM;
596               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
597               MC_UNSET_RAW_MEM;
598         
599               MC_ddfs(search_cycle);
600
601             }
602
603           }else{
604
605             MC_SET_RAW_MEM;
606             xbt_fifo_unshift(mc_stack_liveness, pair_succ);
607             MC_UNSET_RAW_MEM;
608             
609             MC_ddfs(search_cycle);
610             
611           }
612       
613
614         }else{
615       
616           if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
617
618             set_pair_reached(pair_succ->automaton_state);
619          
620             search_cycle = 1;
621
622             XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
623
624           }
625
626           MC_SET_RAW_MEM;
627           xbt_fifo_unshift(mc_stack_liveness, pair_succ);
628           MC_UNSET_RAW_MEM;
629           
630           MC_ddfs(search_cycle);
631           
632         }
633
634         /* Restore system before checking others successors */
635         if(cursor != xbt_dynar_length(successors) - 1)
636           MC_replay_liveness(mc_stack_liveness, 1);
637
638       }           
639
640     }
641     
642   }else{
643     
644     XBT_DEBUG("Max depth reached");
645
646   }
647
648   if(xbt_fifo_size(mc_stack_liveness) == MAX_DEPTH_LIVENESS ){
649     XBT_DEBUG("Pair (depth = %d) shifted in stack, maximum depth reached", xbt_fifo_size(mc_stack_liveness) );
650   }else{
651     XBT_DEBUG("Pair (depth = %d) shifted in stack", xbt_fifo_size(mc_stack_liveness) );
652   }
653
654   
655   MC_SET_RAW_MEM;
656   remove_pair = xbt_fifo_shift(mc_stack_liveness);
657   xbt_fifo_remove(mc_stack_liveness, remove_pair);
658   remove_pair = NULL;
659   if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
660     remove_pair_reached = xbt_dynar_pop_as(reached_pairs, mc_pair_reached_t);
661     pair_reached_free(remove_pair_reached);
662     remove_pair_reached = NULL;
663   }
664   MC_UNSET_RAW_MEM;
665
666   if(raw_mem_set)
667     MC_SET_RAW_MEM;
668
669 }