1 /* Copyright (c) 2011-2013 Da SimGrid Team. All rights reserved. */
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. */
6 #include "mc_private.h"
10 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
11 "Logging specific to algorithms for liveness properties verification");
13 /********* Global variables *********/
15 xbt_dynar_t acceptance_pairs;
16 xbt_dynar_t visited_pairs;
17 xbt_dynar_t successors;
20 /********* Static functions *********/
22 static int is_reached_acceptance_pair(xbt_automaton_state_t st){
24 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
28 mc_acceptance_pair_t new_pair = NULL;
29 new_pair = xbt_new0(s_mc_acceptance_pair_t, 1);
30 new_pair->num = xbt_dynar_length(acceptance_pairs) + 1;
31 new_pair->automaton_state = st;
32 new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
33 new_pair->system_state = MC_take_snapshot();
35 /* Get values of propositional symbols */
38 unsigned int cursor = 0;
39 xbt_automaton_propositional_symbol_t ps = NULL;
40 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
41 f = (int_f_void_t)ps->function;
43 xbt_dynar_push_as(new_pair->prop_ato, int, res);
48 if(xbt_dynar_is_empty(acceptance_pairs)){
51 /* New acceptance pair */
52 xbt_dynar_push(acceptance_pairs, &new_pair);
65 mc_acceptance_pair_t pair_test = NULL;
67 xbt_dynar_foreach(acceptance_pairs, cursor, pair_test){
68 if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug))
69 XBT_DEBUG("****** Pair reached #%d ******", pair_test->num);
70 if(xbt_automaton_state_compare(pair_test->automaton_state, st) == 0){
71 if(xbt_automaton_propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
72 if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
82 XBT_DEBUG("Different values of propositional symbols");
85 XBT_DEBUG("Different automaton state");
89 /* New acceptance pair */
90 xbt_dynar_push(acceptance_pairs, &new_pair);
105 static void set_acceptance_pair_reached(xbt_automaton_state_t st){
107 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
111 mc_acceptance_pair_t pair = NULL;
112 pair = xbt_new0(s_mc_acceptance_pair_t, 1);
113 pair->num = xbt_dynar_length(acceptance_pairs) + 1;
114 pair->automaton_state = st;
115 pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
116 pair->system_state = MC_take_snapshot();
118 /* Get values of propositional symbols */
119 unsigned int cursor = 0;
120 xbt_automaton_propositional_symbol_t ps = NULL;
124 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
125 f = (int_f_void_t)ps->function;
127 xbt_dynar_push_as(pair->prop_ato, int, res);
130 xbt_dynar_push(acceptance_pairs, &pair);
139 static mc_visited_pair_t visited_pair_new(xbt_automaton_state_t as){
141 mc_visited_pair_t new_pair = NULL;
142 new_pair = xbt_new0(s_mc_visited_pair_t, 1);
143 new_pair->automaton_state = as;
144 new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
145 new_pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
146 new_pair->nb_processes = xbt_swag_size(simix_global->process_list);
147 new_pair->system_state = MC_take_snapshot();
149 /* Get values of propositional symbols */
152 unsigned int cursor = 0;
153 xbt_automaton_propositional_symbol_t ps = NULL;
154 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
155 f = (int_f_void_t)ps->function;
157 xbt_dynar_push_as(new_pair->prop_ato, int, res);
164 static int is_visited_pair(xbt_automaton_state_t as){
166 if(_sg_mc_visited == 0)
169 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
172 mc_visited_pair_t new_pair = visited_pair_new(as);
175 if(xbt_dynar_is_empty(visited_pairs)){
178 xbt_dynar_push(visited_pairs, &new_pair);
190 size_t current_bytes_used = new_pair->heap_bytes_used;
191 int current_nb_processes = new_pair->nb_processes;
193 unsigned int cursor = 0;
194 int previous_cursor = 0, next_cursor = 0;
196 int end = xbt_dynar_length(visited_pairs) - 1;
198 mc_visited_pair_t pair_test = NULL;
199 size_t bytes_used_test;
200 int nb_processes_test;
201 int same_processes_and_bytes_not_found = 1;
203 while(start <= end && same_processes_and_bytes_not_found){
204 cursor = (start + end) / 2;
205 pair_test = (mc_visited_pair_t)xbt_dynar_get_as(visited_pairs, cursor, mc_visited_pair_t);
206 bytes_used_test = pair_test->heap_bytes_used;
207 nb_processes_test = pair_test->nb_processes;
208 if(nb_processes_test < current_nb_processes)
210 if(nb_processes_test > current_nb_processes)
212 if(nb_processes_test == current_nb_processes){
213 if(bytes_used_test < current_bytes_used)
215 if(bytes_used_test > current_bytes_used)
217 if(bytes_used_test == current_bytes_used){
218 same_processes_and_bytes_not_found = 0;
219 if(xbt_automaton_state_compare(pair_test->automaton_state, as) == 0){
220 if(xbt_automaton_propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
221 if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
222 xbt_dynar_remove_at(visited_pairs, cursor, NULL);
223 xbt_dynar_insert_at(visited_pairs, cursor, &new_pair);
224 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_pair->num, pair_test->num);
229 return pair_test->num;
233 /* Search another pair with same number of bytes used in std_heap */
234 previous_cursor = cursor - 1;
235 while(previous_cursor >= 0){
236 pair_test = (mc_visited_pair_t)xbt_dynar_get_as(visited_pairs, previous_cursor, mc_visited_pair_t);
237 bytes_used_test = pair_test->system_state->heap_bytes_used;
238 if(bytes_used_test != current_bytes_used)
240 if(xbt_automaton_state_compare(pair_test->automaton_state, as) == 0){
241 if(xbt_automaton_propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
242 if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
243 xbt_dynar_remove_at(visited_pairs, previous_cursor, NULL);
244 xbt_dynar_insert_at(visited_pairs, previous_cursor, &new_pair);
245 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_pair->num, pair_test->num);
250 return pair_test->num;
256 next_cursor = cursor + 1;
257 while(next_cursor < xbt_dynar_length(visited_pairs)){
258 pair_test = (mc_visited_pair_t)xbt_dynar_get_as(visited_pairs, next_cursor, mc_visited_pair_t);
259 bytes_used_test = pair_test->system_state->heap_bytes_used;
260 if(bytes_used_test != current_bytes_used)
262 if(xbt_automaton_state_compare(pair_test->automaton_state, as) == 0){
263 if(xbt_automaton_propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
264 if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
265 xbt_dynar_remove_at(visited_pairs, next_cursor, NULL);
266 xbt_dynar_insert_at(visited_pairs, next_cursor, &new_pair);
267 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_pair->num, pair_test->num);
272 return pair_test->num;
282 pair_test = (mc_visited_pair_t)xbt_dynar_get_as(visited_pairs, cursor, mc_visited_pair_t);
283 bytes_used_test = pair_test->heap_bytes_used;
285 if(bytes_used_test < current_bytes_used)
286 xbt_dynar_insert_at(visited_pairs, cursor + 1, &new_pair);
288 xbt_dynar_insert_at(visited_pairs, cursor, &new_pair);
290 if(xbt_dynar_length(visited_pairs) > _sg_mc_visited){
291 int min = mc_stats->expanded_states;
292 unsigned int cursor2 = 0;
293 unsigned int index = 0;
294 xbt_dynar_foreach(visited_pairs, cursor2, pair_test){
295 if(pair_test->num < min){
297 min = pair_test->num;
300 xbt_dynar_remove_at(visited_pairs, index, NULL);
304 xbt_dynar_foreach(visited_pairs, cursor, pair_test){
305 fprintf(stderr, "Visited pair %d, nb_processes %d and heap_bytes_used %zu\n", pair_test->num, pair_test->nb_processes, pair_test->heap_bytes_used);
319 static int MC_automaton_evaluate_label(xbt_automaton_exp_label_t l){
323 int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
324 int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
325 return (left_res || right_res);
328 int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
329 int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
330 return (left_res && right_res);
333 int res = MC_automaton_evaluate_label(l->u.exp_not);
337 unsigned int cursor = 0;
338 xbt_automaton_propositional_symbol_t p = NULL;
340 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, p){
341 if(strcmp(p->pred, l->u.predicat) == 0){
342 f = (int_f_void_t)p->function;
357 /********* Free functions *********/
359 static void visited_pair_free(mc_visited_pair_t pair){
361 xbt_dynar_free(&(pair->prop_ato));
362 MC_free_snapshot(pair->system_state);
367 static void visited_pair_free_voidp(void *p){
368 visited_pair_free((mc_visited_pair_t) * (void **) p);
371 static void acceptance_pair_free(mc_acceptance_pair_t pair){
373 xbt_dynar_free(&(pair->prop_ato));
374 MC_free_snapshot(pair->system_state);
379 static void acceptance_pair_free_voidp(void *p){
380 acceptance_pair_free((mc_acceptance_pair_t) * (void **) p);
384 /********* DDFS Algorithm *********/
387 void MC_ddfs_init(void){
389 initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
391 XBT_DEBUG("**************************************************");
392 XBT_DEBUG("Double-DFS init");
393 XBT_DEBUG("**************************************************");
395 mc_pair_t mc_initial_pair = NULL;
396 mc_state_t initial_graph_state = NULL;
397 smx_process_t process;
400 MC_wait_for_requests();
404 initial_graph_state = MC_state_new();
405 xbt_swag_foreach(process, simix_global->process_list){
406 if(MC_process_is_enabled(process)){
407 MC_state_interleave_process(initial_graph_state, process);
411 acceptance_pairs = xbt_dynar_new(sizeof(mc_acceptance_pair_t), acceptance_pair_free_voidp);
412 visited_pairs = xbt_dynar_new(sizeof(mc_visited_pair_t), visited_pair_free_voidp);
413 successors = xbt_dynar_new(sizeof(mc_pair_t), NULL);
415 /* Save the initial state */
416 initial_state_liveness->snapshot = MC_take_snapshot();
420 unsigned int cursor = 0;
421 xbt_automaton_state_t automaton_state;
423 xbt_dynar_foreach(_mc_property_automaton->states, cursor, automaton_state){
424 if(automaton_state->type == -1){
427 mc_initial_pair = MC_pair_new(initial_graph_state, automaton_state, MC_state_interleave_size(initial_graph_state));
428 xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
432 MC_restore_snapshot(initial_state_liveness->snapshot);
439 if(automaton_state->type == 2){
442 mc_initial_pair = MC_pair_new(initial_graph_state, automaton_state, MC_state_interleave_size(initial_graph_state));
443 xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
446 set_acceptance_pair_reached(automaton_state);
449 MC_restore_snapshot(initial_state_liveness->snapshot);
459 if(initial_state_liveness->raw_mem_set)
468 void MC_ddfs(int search_cycle){
470 smx_process_t process;
471 mc_pair_t current_pair = NULL;
473 if(xbt_fifo_size(mc_stack_liveness) == 0)
477 /* Get current pair */
478 current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness));
480 /* Update current state in buchi automaton */
481 _mc_property_automaton->current_state = current_pair->automaton_state;
484 XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle);
486 mc_stats->visited_states++;
489 mc_state_t next_graph_state = NULL;
490 smx_simcall_t req = NULL;
493 xbt_automaton_transition_t transition_succ;
494 unsigned int cursor = 0;
497 mc_pair_t next_pair = NULL;
500 mc_pair_t pair_to_remove;
501 mc_acceptance_pair_t acceptance_pair_to_remove;
503 if(xbt_fifo_size(mc_stack_liveness) < _sg_mc_max_depth){
505 if(current_pair->requests > 0){
507 while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
509 /* Debug information */
511 if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
512 req_str = MC_request_to_string(req, value);
513 XBT_DEBUG("Execute: %s", req_str);
517 MC_state_set_executed_request(current_pair->graph_state, req, value);
518 mc_stats->executed_transitions++;
520 /* Answer the request */
521 SIMIX_simcall_pre(req, value);
523 /* Wait for requests (schedules processes) */
524 MC_wait_for_requests();
528 /* Create the new expanded graph_state */
529 next_graph_state = MC_state_new();
531 /* Get enabled process and insert it in the interleave set of the next graph_state */
532 xbt_swag_foreach(process, simix_global->process_list){
533 if(MC_process_is_enabled(process)){
534 XBT_DEBUG("Process %lu enabled with simcall : %d", process->pid, (&process->simcall)->call);
538 xbt_swag_foreach(process, simix_global->process_list){
539 if(MC_process_is_enabled(process)){
540 MC_state_interleave_process(next_graph_state, process);
544 xbt_dynar_reset(successors);
550 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
552 res = MC_automaton_evaluate_label(transition_succ->label);
554 if(res == 1){ // enabled transition in automaton
556 next_pair = MC_pair_new(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
557 xbt_dynar_push(successors, &next_pair);
565 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
567 res = MC_automaton_evaluate_label(transition_succ->label);
569 if(res == 2){ // true transition in automaton
571 next_pair = MC_pair_new(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
572 xbt_dynar_push(successors, &next_pair);
580 xbt_dynar_foreach(successors, cursor, pair_succ){
582 if(search_cycle == 1){
584 if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
586 if(is_reached_acceptance_pair(pair_succ->automaton_state)){
588 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));
590 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
591 XBT_INFO("| ACCEPTANCE CYCLE |");
592 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
593 XBT_INFO("Counter-example that violates formula :");
594 MC_show_stack_liveness(mc_stack_liveness);
595 MC_dump_stack_liveness(mc_stack_liveness);
596 MC_print_statistics(mc_stats);
601 if(is_visited_pair(pair_succ->automaton_state) != -1){
603 XBT_DEBUG("Next pair already visited !");
608 XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
610 XBT_DEBUG("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));
613 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
616 MC_ddfs(search_cycle);
624 if(is_visited_pair(pair_succ->automaton_state) != -1){
626 XBT_DEBUG("Next pair already visited !");
632 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
635 MC_ddfs(search_cycle);
642 if(is_visited_pair(pair_succ->automaton_state) != -1){
644 XBT_DEBUG("Next pair already visited !");
649 if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
651 XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
653 set_acceptance_pair_reached(pair_succ->automaton_state);
657 XBT_DEBUG("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));
662 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
665 MC_ddfs(search_cycle);
671 /* Restore system before checking others successors */
672 if(cursor != (xbt_dynar_length(successors) - 1))
673 MC_replay_liveness(mc_stack_liveness, 1);
677 if(MC_state_interleave_size(current_pair->graph_state) > 0){
678 XBT_DEBUG("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
679 MC_replay_liveness(mc_stack_liveness, 0);
686 mc_stats->executed_transitions++;
688 XBT_DEBUG("No more request to execute in this state, search evolution in Büchi Automaton.");
692 /* Create the new expanded graph_state */
693 next_graph_state = MC_state_new();
695 xbt_dynar_reset(successors);
701 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
703 res = MC_automaton_evaluate_label(transition_succ->label);
705 if(res == 1){ // enabled transition in automaton
707 next_pair = MC_pair_new(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
708 xbt_dynar_push(successors, &next_pair);
716 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
718 res = MC_automaton_evaluate_label(transition_succ->label);
720 if(res == 2){ // true transition in automaton
722 next_pair = MC_pair_new(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
723 xbt_dynar_push(successors, &next_pair);
731 xbt_dynar_foreach(successors, cursor, pair_succ){
733 if(search_cycle == 1){
735 if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
737 if(is_reached_acceptance_pair(pair_succ->automaton_state)){
739 XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1);
741 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
742 XBT_INFO("| ACCEPTANCE CYCLE |");
743 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
744 XBT_INFO("Counter-example that violates formula :");
745 MC_show_stack_liveness(mc_stack_liveness);
746 MC_dump_stack_liveness(mc_stack_liveness);
747 MC_print_statistics(mc_stats);
752 if(is_visited_pair(pair_succ->automaton_state) != -1){
754 XBT_DEBUG("Next pair already visited !");
759 XBT_INFO("Next pair (depth = %d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
761 XBT_INFO("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));
764 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
767 MC_ddfs(search_cycle);
775 if(is_visited_pair(pair_succ->automaton_state) != -1){
777 XBT_DEBUG("Next pair already visited !");
783 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
786 MC_ddfs(search_cycle);
795 if(is_visited_pair(pair_succ->automaton_state) != -1){
797 XBT_DEBUG("Next pair already visited !");
802 if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
804 set_acceptance_pair_reached(pair_succ->automaton_state);
808 XBT_INFO("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));
813 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
816 MC_ddfs(search_cycle);
822 /* Restore system before checking others successors */
823 if(cursor != xbt_dynar_length(successors) - 1)
824 MC_replay_liveness(mc_stack_liveness, 1);
832 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
833 if(MC_state_interleave_size(current_pair->graph_state) > 0){
834 XBT_WARN("/!\\ But, there are still processes to interleave. Model-checker will not be able to ensure the soundness of the verification from now. /!\\ ");
835 XBT_WARN("Notice : the default value of max depth is 1000 but you can change it with cfg=model-check/max_depth:value.");
840 if(xbt_fifo_size(mc_stack_liveness) == _sg_mc_max_depth ){
841 XBT_DEBUG("Pair (depth = %d) shifted in stack, maximum depth reached", xbt_fifo_size(mc_stack_liveness) );
843 XBT_DEBUG("Pair (depth = %d) shifted in stack", xbt_fifo_size(mc_stack_liveness) );
848 pair_to_remove = xbt_fifo_shift(mc_stack_liveness);
849 xbt_fifo_remove(mc_stack_liveness, pair_to_remove);
850 pair_to_remove = NULL;
851 if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
852 acceptance_pair_to_remove = xbt_dynar_pop_as(acceptance_pairs, mc_acceptance_pair_t);
853 acceptance_pair_free(acceptance_pair_to_remove);
854 acceptance_pair_to_remove = NULL;