4 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
5 "Logging specific to algorithms for liveness properties verification");
7 xbt_dynar_t initial_pairs = NULL;
8 xbt_dynar_t reached_pairs;
9 mc_snapshot_t snapshot = NULL;
10 extern mc_snapshot_t initial_snapshot;
12 mc_pair_t new_pair(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st){
14 p = xbt_new0(s_mc_pair_t, 1);
16 p->automaton_state = st;
18 mc_stats_pair->expanded_pairs++;
23 int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
25 if(s1->num_reg != s2->num_reg)
30 for(i=0 ; i< s1->num_reg ; i++){
32 if(s1->regions[i]->size != s2->regions[i]->size)
35 if(s1->regions[i]->start_addr != s2->regions[i]->start_addr)
38 if(s1->regions[i]->type != s2->regions[i]->type)
41 if(s1->regions[i]->type == 0){
42 if(mmalloc_compare_heap(s1->regions[i]->start_addr, s2->regions[i]->start_addr)){
43 XBT_DEBUG("Different heap (mmalloc_compare)");
48 if(memcmp(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
49 XBT_DEBUG("Different memcmp for data in libsimgrid");
62 int reached(xbt_automaton_t a, xbt_state_t st, mc_snapshot_t s){
65 if(xbt_dynar_is_empty(reached_pairs)){
70 xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
72 /* Get values of propositional symbols */
73 unsigned int cursor = 0;
74 xbt_propositional_symbol_t ps = NULL;
75 xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
76 int (*f)() = ps->function;
78 xbt_dynar_push_as(prop_ato, int, res);
82 mc_pair_reached_t pair_test;
84 xbt_dynar_foreach(reached_pairs, cursor, pair_test){
85 if(automaton_state_compare(pair_test->automaton_state, st) == 0){
86 if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
87 if(snapshot_compare(pair_test->system_state, s) == 0){
101 int set_pair_reached(xbt_automaton_t a, xbt_state_t st, mc_snapshot_t sn){
103 if(reached(a, st, sn) == 0){
107 mc_pair_reached_t pair = NULL;
108 pair = xbt_new0(s_mc_pair_reached_t, 1);
109 pair->automaton_state = st;
110 pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
111 pair->system_state = sn;
113 /* Get values of propositional symbols */
114 unsigned int cursor = 0;
115 xbt_propositional_symbol_t ps = NULL;
116 xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
117 int (*f)() = ps->function;
119 xbt_dynar_push_as(pair->prop_ato, int, res);
122 xbt_dynar_push(reached_pairs, &pair);
133 void MC_pair_delete(mc_pair_t pair){
134 xbt_free(pair->graph_state->proc_status);
135 xbt_free(pair->graph_state);
136 //xbt_free(pair->automaton_state); -> FIXME : à implémenter
142 int MC_automaton_evaluate_label(xbt_automaton_t a, xbt_exp_label_t l){
146 int left_res = MC_automaton_evaluate_label(a, l->u.or_and.left_exp);
147 int right_res = MC_automaton_evaluate_label(a, l->u.or_and.right_exp);
148 return (left_res || right_res);
152 int left_res = MC_automaton_evaluate_label(a, l->u.or_and.left_exp);
153 int right_res = MC_automaton_evaluate_label(a, l->u.or_and.right_exp);
154 return (left_res && right_res);
158 int res = MC_automaton_evaluate_label(a, l->u.exp_not);
163 unsigned int cursor = 0;
164 xbt_propositional_symbol_t p = NULL;
165 xbt_dynar_foreach(a->propositional_symbols, cursor, p){
166 if(strcmp(p->pred, l->u.predicat) == 0){
167 int (*f)() = p->function;
187 /********************* Double-DFS stateless *******************/
189 void MC_pair_stateless_delete(mc_pair_stateless_t pair){
190 xbt_free(pair->graph_state->proc_status);
191 xbt_free(pair->graph_state);
192 //xbt_free(pair->automaton_state); -> FIXME : à implémenter
196 mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st){
197 mc_pair_stateless_t p = NULL;
198 p = xbt_new0(s_mc_pair_stateless_t, 1);
199 p->automaton_state = st;
201 mc_stats_pair->expanded_pairs++;
207 void MC_ddfs_stateless_init(xbt_automaton_t a){
209 XBT_DEBUG("**************************************************");
210 XBT_DEBUG("Double-DFS stateless init");
211 XBT_DEBUG("**************************************************");
213 mc_pair_stateless_t mc_initial_pair = NULL;
214 mc_state_t initial_graph_state = NULL;
215 smx_process_t process;
217 MC_wait_for_requests();
221 initial_graph_state = MC_state_pair_new();
222 xbt_swag_foreach(process, simix_global->process_list){
223 if(MC_process_is_enabled(process)){
224 MC_state_interleave_process(initial_graph_state, process);
228 reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL);
230 initial_snapshot = xbt_new0(s_mc_snapshot_t, 1);
231 snapshot = xbt_new0(s_mc_snapshot_t, 1);
232 MC_take_snapshot(initial_snapshot);
236 unsigned int cursor = 0;
239 xbt_dynar_foreach(a->states, cursor, state){
240 if(state->type == -1){
243 mc_initial_pair = new_pair_stateless(initial_graph_state, state);
244 xbt_fifo_unshift(mc_stack_liveness_stateless, mc_initial_pair);
248 MC_ddfs_stateless(a, 0, 0);
250 MC_restore_snapshot(initial_snapshot);
252 MC_ddfs_stateless(a, 0, 0);
255 if(state->type == 2){
258 mc_initial_pair = new_pair_stateless(initial_graph_state, state);
259 xbt_fifo_unshift(mc_stack_liveness_stateless, mc_initial_pair);
263 MC_ddfs_stateless(a, 1, 0);
265 MC_restore_snapshot(initial_snapshot);
267 MC_ddfs_stateless(a, 1, 0);
276 void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){
278 smx_process_t process;
279 mc_pair_stateless_t current_pair = NULL;
281 if(xbt_fifo_size(mc_stack_liveness_stateless) == 0)
285 MC_replay_liveness(mc_stack_liveness_stateless);
286 current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateless));
287 xbt_swag_foreach(process, simix_global->process_list){
288 if(MC_process_is_enabled(process)){
289 MC_state_interleave_process(current_pair->graph_state, process);
294 /* Get current pair */
295 current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateless));
297 /* Update current state in buchi automaton */
298 a->current_state = current_pair->automaton_state;
301 XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateless), search_cycle);
302 XBT_DEBUG("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));
306 mc_stats_pair->visited_pairs++;
309 mc_state_t next_graph_state = NULL;
310 smx_req_t req = NULL;
313 xbt_transition_t transition_succ;
314 unsigned int cursor = 0;
317 mc_pair_stateless_t next_pair = NULL;
318 mc_pair_stateless_t pair_succ;
319 //mc_snapshot_t next_snapshot = NULL;
321 xbt_dynar_t successors = NULL;
324 successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
327 while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
329 /* Debug information */
330 if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
331 req_str = MC_request_to_string(req, value);
332 XBT_DEBUG("Execute: %s", req_str);
338 MC_state_set_executed_request(current_pair->graph_state, req, value);
340 /* Answer the request */
341 SIMIX_request_pre(req, value);
343 /* Wait for requests (schedules processes) */
344 MC_wait_for_requests();
349 /* Create the new expanded graph_state */
350 next_graph_state = MC_state_pair_new();
352 /* Get enabled process and insert it in the interleave set of the next graph_state */
353 xbt_swag_foreach(process, simix_global->process_list){
354 if(MC_process_is_enabled(process)){
355 MC_state_interleave_process(next_graph_state, process);
359 xbt_dynar_reset(successors);
365 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
367 res = MC_automaton_evaluate_label(a, transition_succ->label);
369 if(res == 1){ // enabled transition in automaton
371 next_pair = new_pair_stateless(next_graph_state, transition_succ->dst);
372 xbt_dynar_push(successors, &next_pair);
380 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
382 res = MC_automaton_evaluate_label(a, transition_succ->label);
384 if(res == 2){ // true transition in automaton
386 next_pair = new_pair_stateless(next_graph_state, transition_succ->dst);
387 xbt_dynar_push(successors, &next_pair);
394 if(xbt_dynar_length(successors) == 0){
396 next_pair = new_pair_stateless(next_graph_state, current_pair->automaton_state);
397 xbt_dynar_push(successors, &next_pair);
403 xbt_dynar_foreach(successors, cursor, pair_succ){
404 if((search_cycle == 1) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
406 MC_take_snapshot(snapshot);
409 if(reached(a, pair_succ->automaton_state, snapshot) == 1){
410 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
411 XBT_INFO("| ACCEPTANCE CYCLE |");
412 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
413 XBT_INFO("Counter-example that violates formula :");
414 MC_show_stack_liveness_stateless(mc_stack_liveness_stateless);
415 MC_dump_stack_liveness_stateless(mc_stack_liveness_stateless);
416 MC_print_statistics_pairs(mc_stats_pair);
417 //MC_exit_liveness();
423 xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
426 //XBT_DEBUG("Stack size before : %d", xbt_fifo_size(mc_stack_liveness_stateless));
428 MC_ddfs_stateless(a, search_cycle, 0);
430 //XBT_DEBUG("Stack size after : %d", xbt_fifo_size(mc_stack_liveness_stateless));
433 if((search_cycle == 0) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
435 XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
438 MC_take_snapshot(snapshot);
441 int pr = set_pair_reached(a, pair_succ->automaton_state, snapshot);
444 /* pair shifted from stack when first MC_ddfs finished and returned at this point */
446 xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
449 MC_ddfs_stateless(a, 1, 1);
454 xbt_dynar_pop(reached_pairs, NULL);
460 if(MC_state_interleave_size(current_pair->graph_state) > 0){
461 XBT_DEBUG("Backtracking to depth %u", xbt_fifo_size(mc_stack_liveness_stateless));
462 MC_replay_liveness(mc_stack_liveness_stateless);
468 xbt_fifo_shift(mc_stack_liveness_stateless);
469 XBT_DEBUG("Pair (graph=%p, automaton =%p, search_cycle = %u) shifted in stack", current_pair->graph_state, current_pair->automaton_state, search_cycle);
474 /********************* Double-DFS stateful without visited state *******************/
477 void MC_ddfs_stateful_init(xbt_automaton_t a){
479 XBT_DEBUG("**************************************************");
480 XBT_DEBUG("Double-DFS stateful without visited state init");
481 XBT_DEBUG("**************************************************");
483 mc_pair_t mc_initial_pair;
484 mc_state_t initial_graph_state;
485 smx_process_t process;
486 mc_snapshot_t init_snapshot;
488 MC_wait_for_requests();
492 init_snapshot = xbt_new0(s_mc_snapshot_t, 1);
494 initial_graph_state = MC_state_pair_new();
495 xbt_swag_foreach(process, simix_global->process_list){
496 if(MC_process_is_enabled(process)){
497 MC_state_interleave_process(initial_graph_state, process);
501 reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL);
503 MC_take_snapshot(init_snapshot);
507 unsigned int cursor = 0;
508 xbt_state_t state = NULL;
510 xbt_dynar_foreach(a->states, cursor, state){
511 if(state->type == -1){
514 mc_initial_pair = new_pair(init_snapshot, initial_graph_state, state);
515 xbt_fifo_unshift(mc_stack_liveness_stateful, mc_initial_pair);
519 MC_ddfs_stateful(a, 0, 0);
521 MC_restore_snapshot(init_snapshot);
523 MC_ddfs_stateful(a, 0, 0);
526 if(state->type == 2){
529 mc_initial_pair = new_pair(init_snapshot, initial_graph_state, state);
530 xbt_fifo_unshift(mc_stack_liveness_stateful, mc_initial_pair);
534 MC_ddfs_stateful(a, 1, 0);
536 MC_restore_snapshot(init_snapshot);
538 MC_ddfs_stateful(a, 1, 0);
546 void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){
548 smx_process_t process = NULL;
549 mc_pair_t current_pair = NULL;
551 if(xbt_fifo_size(mc_stack_liveness_stateful) == 0)
555 current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful));
556 MC_restore_snapshot(current_pair->system_state);
557 xbt_swag_foreach(process, simix_global->process_list){
558 if(MC_process_is_enabled(process)){
559 MC_state_interleave_process(current_pair->graph_state, process);
565 /* Get current state */
566 current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful));
569 XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateful), search_cycle);
570 XBT_DEBUG("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));
572 a->current_state = current_pair->automaton_state;
574 mc_stats_pair->visited_pairs++;
577 mc_state_t next_graph_state = NULL;
578 smx_req_t req = NULL;
582 xbt_transition_t transition_succ;
586 xbt_dynar_t successors = NULL;
588 mc_pair_t next_pair = NULL;
589 mc_snapshot_t next_snapshot = NULL;
590 mc_snapshot_t current_snapshot = NULL;
594 successors = xbt_dynar_new(sizeof(mc_pair_t), NULL);
597 while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
600 current_snapshot = xbt_new0(s_mc_snapshot_t, 1);
601 MC_take_snapshot(current_snapshot);
605 /* Debug information */
606 if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
607 req_str = MC_request_to_string(req, value);
608 XBT_DEBUG("Execute: %s", req_str);
612 MC_state_set_executed_request(current_pair->graph_state, req, value);
614 /* Answer the request */
615 SIMIX_request_pre(req, value);
617 /* Wait for requests (schedules processes) */
618 MC_wait_for_requests();
621 /* Create the new expanded graph_state */
624 next_graph_state = MC_state_pair_new();
626 /* Get enabled process and insert it in the interleave set of the next graph_state */
627 xbt_swag_foreach(process, simix_global->process_list){
628 if(MC_process_is_enabled(process)){
629 MC_state_interleave_process(next_graph_state, process);
633 next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
634 MC_take_snapshot(next_snapshot);
636 xbt_dynar_reset(successors);
642 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
644 res = MC_automaton_evaluate_label(a, transition_succ->label);
646 if(res == 1){ // enabled transition in automaton
648 next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst);
649 xbt_dynar_push(successors, &next_pair);
656 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
658 res = MC_automaton_evaluate_label(a, transition_succ->label);
660 if(res == 2){ // transition always enabled in automaton
662 next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst);
663 xbt_dynar_push(successors, &next_pair);
671 if(xbt_dynar_length(successors) == 0){
674 next_pair = new_pair(next_snapshot, next_graph_state, current_pair->automaton_state);
675 xbt_dynar_push(successors, &next_pair);
680 //XBT_DEBUG("Successors in automaton %lu", xbt_dynar_length(successors));
683 xbt_dynar_foreach(successors, cursor, pair_succ){
685 //XBT_DEBUG("Search visited pair : graph=%p, automaton=%p", pair_succ->graph_state, pair_succ->automaton_state);
686 if((search_cycle == 1) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
688 next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
689 MC_take_snapshot(current_snapshot);
692 if(reached(a, pair_succ->automaton_state, next_snapshot) == 1){
693 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
694 XBT_INFO("| ACCEPTANCE CYCLE |");
695 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
696 XBT_INFO("Counter-example that violates formula :");
697 MC_show_stack_liveness_stateful(mc_stack_liveness_stateful);
698 MC_dump_stack_liveness_stateful(mc_stack_liveness_stateful);
699 MC_print_statistics_pairs(mc_stats_pair);
704 //mc_stats_pair->executed_transitions++;
707 xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ);
710 MC_ddfs_stateful(a, search_cycle, 0);
713 if((search_cycle == 0) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
715 int res = set_pair_reached(a, pair_succ->automaton_state, next_snapshot);
716 XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
719 xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ);
722 MC_ddfs_stateful(a, 1, 1);
726 xbt_dynar_pop(reached_pairs, NULL);
733 if(MC_state_interleave_size(current_pair->graph_state) > 0){
734 XBT_DEBUG("Backtracking to depth %u", xbt_fifo_size(mc_stack_liveness_stateful));
735 MC_restore_snapshot(current_snapshot);
743 xbt_fifo_shift(mc_stack_liveness_stateful);
744 XBT_DEBUG("Pair (graph=%p, automaton =%p) shifted in stack", current_pair->graph_state, current_pair->automaton_state);