From: Marion Guthmuller Date: Fri, 21 Oct 2011 12:27:46 +0000 (+0200) Subject: model-checker : test data in libsimgrid memory region between each state X-Git-Tag: exp_20120216~133^2~61 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/daf9d10c7877d35670e36e52be8a5207706d3bb1 model-checker : test data in libsimgrid memory region between each state --- diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c index c3773745d8..60adc472da 100644 --- a/src/mc/mc_liveness.c +++ b/src/mc/mc_liveness.c @@ -24,7 +24,8 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){ if(s1->num_reg != s2->num_reg) return 1; - int i; + int i, errors=0; + for(i=0 ; i< s1->num_reg ; i++){ if(s1->regions[i]->size != s2->regions[i]->size) @@ -33,19 +34,27 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){ if(s1->regions[i]->start_addr != s2->regions[i]->start_addr) return 1; - XBT_DEBUG("(%d) Snapshot ok before memcmp on data", i); - if(s1->regions[i]->type != s2->regions[i]->type) return 1; - if(s1->regions[i]->type == 0){ - if(memcmp(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0) - return 1; + if(s1->regions[i]->type == 0){ + if(mmalloc_compare_heap(s1->regions[i]->start_addr, s2->regions[i]->start_addr)){ + XBT_DEBUG("Different heap (mmalloc_compare)"); + //sleep(1); + errors++; + } + }else{ + if(memcmp(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){ + XBT_DEBUG("Different memcmp for data in libsimgrid (%d)", i); + //sleep(2); + errors++; + } } + } - return 0; + return (errors>0); } @@ -173,26 +182,42 @@ int MC_automaton_evaluate_label(xbt_automaton_t a, xbt_exp_label_t l){ } -/********************* Double-DFS stateful without visited state *******************/ -void MC_ddfs_stateful_init(xbt_automaton_t a){ + +/********************* Double-DFS stateless *******************/ + +void MC_pair_stateless_delete(mc_pair_stateless_t pair){ + xbt_free(pair->graph_state->proc_status); + xbt_free(pair->graph_state); + //xbt_free(pair->automaton_state); -> FIXME : à implémenter + xbt_free(pair); +} + +mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st){ + mc_pair_stateless_t p = NULL; + p = xbt_new0(s_mc_pair_stateless_t, 1); + p->automaton_state = st; + p->graph_state = sg; + mc_stats_pair->expanded_pairs++; + return p; +} + + + +void MC_ddfs_stateless_init(xbt_automaton_t a){ XBT_DEBUG("**************************************************"); - XBT_DEBUG("Double-DFS stateful without visited state init"); + XBT_DEBUG("Double-DFS stateless init"); XBT_DEBUG("**************************************************"); - mc_pair_t mc_initial_pair; - mc_state_t initial_graph_state; + mc_pair_stateless_t mc_initial_pair = NULL; + mc_state_t initial_graph_state = NULL; smx_process_t process; - mc_snapshot_t init_snapshot; MC_wait_for_requests(); MC_SET_RAW_MEM; - - init_snapshot = xbt_new0(s_mc_snapshot_t, 1); - initial_graph_state = MC_state_pair_new(); xbt_swag_foreach(process, simix_global->process_list){ if(MC_process_is_enabled(process)){ @@ -202,77 +227,79 @@ void MC_ddfs_stateful_init(xbt_automaton_t a){ reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL); - MC_take_snapshot(init_snapshot); + initial_snapshot = xbt_new0(s_mc_snapshot_t, 1); + MC_take_snapshot(initial_snapshot); MC_UNSET_RAW_MEM; unsigned int cursor = 0; - xbt_state_t state = NULL; + xbt_state_t state; xbt_dynar_foreach(a->states, cursor, state){ if(state->type == -1){ - + MC_SET_RAW_MEM; - mc_initial_pair = new_pair(init_snapshot, initial_graph_state, state); - xbt_fifo_unshift(mc_stack_liveness_stateful, mc_initial_pair); + mc_initial_pair = new_pair_stateless(initial_graph_state, state); + xbt_fifo_unshift(mc_stack_liveness_stateless, mc_initial_pair); MC_UNSET_RAW_MEM; - + if(cursor == 0){ - MC_ddfs_stateful(a, 0, 0); + MC_ddfs_stateless(a, 0, 0); }else{ - MC_restore_snapshot(init_snapshot); + MC_restore_snapshot(initial_snapshot); MC_UNSET_RAW_MEM; - MC_ddfs_stateful(a, 0, 0); + MC_ddfs_stateless(a, 0, 0); } }else{ - if(state->type == 2){ - - MC_SET_RAW_MEM; - mc_initial_pair = new_pair(init_snapshot, initial_graph_state, state); - xbt_fifo_unshift(mc_stack_liveness_stateful, mc_initial_pair); - MC_UNSET_RAW_MEM; - - if(cursor == 0){ - MC_ddfs_stateful(a, 1, 0); - }else{ - MC_restore_snapshot(init_snapshot); - MC_UNSET_RAW_MEM; - MC_ddfs_stateful(a, 1, 0); - } - } + if(state->type == 2){ + + MC_SET_RAW_MEM; + mc_initial_pair = new_pair_stateless(initial_graph_state, state); + xbt_fifo_unshift(mc_stack_liveness_stateless, mc_initial_pair); + MC_UNSET_RAW_MEM; + + if(cursor == 0){ + MC_ddfs_stateless(a, 1, 0); + }else{ + MC_restore_snapshot(initial_snapshot); + MC_UNSET_RAW_MEM; + MC_ddfs_stateless(a, 1, 0); + } + } } } + } -void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){ +void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){ - smx_process_t process = NULL; - mc_pair_t current_pair = NULL; + smx_process_t process; + mc_pair_stateless_t current_pair = NULL; - if(xbt_fifo_size(mc_stack_liveness_stateful) == 0) + if(xbt_fifo_size(mc_stack_liveness_stateless) == 0) return; - if(restore == 1){ - current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful)); - MC_restore_snapshot(current_pair->system_state); + if(replay == 1){ + MC_replay_liveness(mc_stack_liveness_stateless); + current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateless)); xbt_swag_foreach(process, simix_global->process_list){ if(MC_process_is_enabled(process)){ MC_state_interleave_process(current_pair->graph_state, process); } } - MC_UNSET_RAW_MEM; } - /* Get current state */ - current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful)); - - - XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateful), search_cycle); - 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)); + /* Get current pair */ + current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateless)); + /* Update current state in buchi automaton */ a->current_state = current_pair->automaton_state; + + XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateless), search_cycle); + 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)); + mc_stats_pair->visited_pairs++; int value; @@ -280,30 +307,28 @@ void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){ smx_req_t req = NULL; char *req_str; - mc_pair_t pair_succ; xbt_transition_t transition_succ; - unsigned int cursor; + unsigned int cursor = 0; int res; - xbt_dynar_t successors = NULL; - - mc_pair_t next_pair = NULL; + mc_pair_stateless_t next_pair = NULL; + mc_pair_stateless_t pair_succ; mc_snapshot_t next_snapshot = NULL; mc_snapshot_t current_snapshot = NULL; - - //sleep(1); + + xbt_dynar_t successors = NULL; + MC_SET_RAW_MEM; - successors = xbt_dynar_new(sizeof(mc_pair_t), NULL); + successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL); MC_UNSET_RAW_MEM; - - while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){ + while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){ + MC_SET_RAW_MEM; current_snapshot = xbt_new0(s_mc_snapshot_t, 1); MC_take_snapshot(current_snapshot); MC_UNSET_RAW_MEM; - - + /* Debug information */ if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){ req_str = MC_request_to_string(req, value); @@ -311,8 +336,10 @@ void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){ xbt_free(req_str); } - MC_state_set_executed_request(current_pair->graph_state, req, value); + //sleep(1); + MC_state_set_executed_request(current_pair->graph_state, req, value); + /* Answer the request */ SIMIX_request_pre(req, value); @@ -320,11 +347,11 @@ void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){ MC_wait_for_requests(); - /* Create the new expanded graph_state */ MC_SET_RAW_MEM; + /* Create the new expanded graph_state */ next_graph_state = MC_state_pair_new(); - + /* Get enabled process and insert it in the interleave set of the next graph_state */ xbt_swag_foreach(process, simix_global->process_list){ if(MC_process_is_enabled(process)){ @@ -334,20 +361,26 @@ void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){ next_snapshot = xbt_new0(s_mc_snapshot_t, 1); MC_take_snapshot(next_snapshot); - + xbt_dynar_reset(successors); - MC_UNSET_RAW_MEM; + if(snapshot_compare(current_snapshot,next_snapshot)){ + XBT_DEBUG("Different snapshot"); + //sleep(2); + + } + MC_UNSET_RAW_MEM; - cursor = 0; + + cursor= 0; xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){ res = MC_automaton_evaluate_label(a, transition_succ->label); - + if(res == 1){ // enabled transition in automaton MC_SET_RAW_MEM; - next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst); + next_pair = new_pair_stateless(next_graph_state, transition_succ->dst); xbt_dynar_push(successors, &next_pair); MC_UNSET_RAW_MEM; } @@ -355,128 +388,103 @@ void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){ } cursor = 0; + xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){ - + res = MC_automaton_evaluate_label(a, transition_succ->label); - if(res == 2){ // transition always enabled in automaton + if(res == 2){ // true transition in automaton MC_SET_RAW_MEM; - next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst); + next_pair = new_pair_stateless(next_graph_state, transition_succ->dst); xbt_dynar_push(successors, &next_pair); MC_UNSET_RAW_MEM; } - } if(xbt_dynar_length(successors) == 0){ - MC_SET_RAW_MEM; - next_pair = new_pair(next_snapshot, next_graph_state, current_pair->automaton_state); + next_pair = new_pair_stateless(next_graph_state, current_pair->automaton_state); xbt_dynar_push(successors, &next_pair); MC_UNSET_RAW_MEM; - } - //XBT_DEBUG("Successors in automaton %lu", xbt_dynar_length(successors)); + cursor = 0; - cursor = 0; xbt_dynar_foreach(successors, cursor, pair_succ){ - - //XBT_DEBUG("Search visited pair : graph=%p, automaton=%p", pair_succ->graph_state, pair_succ->automaton_state); - + if((search_cycle == 1) && (reached(a, next_snapshot) == 1)){ XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); XBT_INFO("| ACCEPTANCE CYCLE |"); XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); XBT_INFO("Counter-example that violates formula :"); - MC_show_stack_liveness_stateful(mc_stack_liveness_stateful); - MC_dump_stack_liveness_stateful(mc_stack_liveness_stateful); + MC_show_stack_liveness_stateless(mc_stack_liveness_stateless); + MC_dump_stack_liveness_stateless(mc_stack_liveness_stateless); MC_print_statistics_pairs(mc_stats_pair); exit(0); } - //mc_stats_pair->executed_transitions++; - MC_SET_RAW_MEM; - xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ); + xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ); MC_UNSET_RAW_MEM; - MC_ddfs_stateful(a, search_cycle, 0); - - + MC_ddfs_stateless(a, search_cycle, 0); + + if((search_cycle == 0) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){ + XBT_DEBUG("Acceptance pair %p : graph=%p, automaton=%p(%s)", pair_succ, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id); int res = set_pair_reached(a, next_snapshot); - XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id); - + MC_SET_RAW_MEM; - xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ); + xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ); MC_UNSET_RAW_MEM; + + MC_ddfs_stateless(a, 1, 1); - MC_ddfs_stateful(a, 1, 1); - if(res){ MC_SET_RAW_MEM; xbt_dynar_pop(reached_pairs, NULL); MC_UNSET_RAW_MEM; } } - } if(MC_state_interleave_size(current_pair->graph_state) > 0){ - XBT_DEBUG("Backtracking to depth %u", xbt_fifo_size(mc_stack_liveness_stateful)); - MC_restore_snapshot(current_snapshot); - MC_UNSET_RAW_MEM; - } - + XBT_DEBUG("Backtracking to depth %u", xbt_fifo_size(mc_stack_liveness_stateless)); + MC_replay_liveness(mc_stack_liveness_stateless); + } + } - MC_SET_RAW_MEM; - xbt_fifo_shift(mc_stack_liveness_stateful); - XBT_DEBUG("Pair (graph=%p, automaton =%p) shifted in stack", current_pair->graph_state, current_pair->automaton_state); + xbt_fifo_shift(mc_stack_liveness_stateless); + XBT_DEBUG("Pair (graph=%p, automaton =%p, search_cycle = %u) shifted in stack", current_pair->graph_state, current_pair->automaton_state, search_cycle); MC_UNSET_RAW_MEM; } +/********************* Double-DFS stateful without visited state *******************/ -/********************* Double-DFS stateless *******************/ - -void MC_pair_stateless_delete(mc_pair_stateless_t pair){ - xbt_free(pair->graph_state->proc_status); - xbt_free(pair->graph_state); - //xbt_free(pair->automaton_state); -> FIXME : à implémenter - xbt_free(pair); -} - -mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st){ - mc_pair_stateless_t p = NULL; - p = xbt_new0(s_mc_pair_stateless_t, 1); - p->automaton_state = st; - p->graph_state = sg; - mc_stats_pair->expanded_pairs++; - return p; -} - - - -void MC_ddfs_stateless_init(xbt_automaton_t a){ +void MC_ddfs_stateful_init(xbt_automaton_t a){ XBT_DEBUG("**************************************************"); - XBT_DEBUG("Double-DFS stateless init"); + XBT_DEBUG("Double-DFS stateful without visited state init"); XBT_DEBUG("**************************************************"); - mc_pair_stateless_t mc_initial_pair = NULL; - mc_state_t initial_graph_state = NULL; + mc_pair_t mc_initial_pair; + mc_state_t initial_graph_state; smx_process_t process; + mc_snapshot_t init_snapshot; MC_wait_for_requests(); MC_SET_RAW_MEM; + + init_snapshot = xbt_new0(s_mc_snapshot_t, 1); + initial_graph_state = MC_state_pair_new(); xbt_swag_foreach(process, simix_global->process_list){ if(MC_process_is_enabled(process)){ @@ -486,79 +494,77 @@ void MC_ddfs_stateless_init(xbt_automaton_t a){ reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL); - initial_snapshot = xbt_new0(s_mc_snapshot_t, 1); - MC_take_snapshot(initial_snapshot); + MC_take_snapshot(init_snapshot); MC_UNSET_RAW_MEM; unsigned int cursor = 0; - xbt_state_t state; + xbt_state_t state = NULL; xbt_dynar_foreach(a->states, cursor, state){ if(state->type == -1){ - + MC_SET_RAW_MEM; - mc_initial_pair = new_pair_stateless(initial_graph_state, state); - xbt_fifo_unshift(mc_stack_liveness_stateless, mc_initial_pair); + mc_initial_pair = new_pair(init_snapshot, initial_graph_state, state); + xbt_fifo_unshift(mc_stack_liveness_stateful, mc_initial_pair); MC_UNSET_RAW_MEM; - + if(cursor == 0){ - MC_ddfs_stateless(a, 0, 0); + MC_ddfs_stateful(a, 0, 0); }else{ - MC_restore_snapshot(initial_snapshot); + MC_restore_snapshot(init_snapshot); MC_UNSET_RAW_MEM; - MC_ddfs_stateless(a, 0, 0); + MC_ddfs_stateful(a, 0, 0); } }else{ - if(state->type == 2){ - - MC_SET_RAW_MEM; - mc_initial_pair = new_pair_stateless(initial_graph_state, state); - xbt_fifo_unshift(mc_stack_liveness_stateless, mc_initial_pair); - MC_UNSET_RAW_MEM; - - if(cursor == 0){ - MC_ddfs_stateless(a, 1, 0); - }else{ - MC_restore_snapshot(initial_snapshot); - MC_UNSET_RAW_MEM; - MC_ddfs_stateless(a, 1, 0); - } - } + if(state->type == 2){ + + MC_SET_RAW_MEM; + mc_initial_pair = new_pair(init_snapshot, initial_graph_state, state); + xbt_fifo_unshift(mc_stack_liveness_stateful, mc_initial_pair); + MC_UNSET_RAW_MEM; + + if(cursor == 0){ + MC_ddfs_stateful(a, 1, 0); + }else{ + MC_restore_snapshot(init_snapshot); + MC_UNSET_RAW_MEM; + MC_ddfs_stateful(a, 1, 0); + } + } } } - } -void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){ +void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){ - smx_process_t process; - mc_pair_stateless_t current_pair = NULL; + smx_process_t process = NULL; + mc_pair_t current_pair = NULL; - if(xbt_fifo_size(mc_stack_liveness_stateless) == 0) + if(xbt_fifo_size(mc_stack_liveness_stateful) == 0) return; - if(replay == 1){ - MC_replay_liveness(mc_stack_liveness_stateless); - current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateless)); + if(restore == 1){ + current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful)); + MC_restore_snapshot(current_pair->system_state); xbt_swag_foreach(process, simix_global->process_list){ if(MC_process_is_enabled(process)){ MC_state_interleave_process(current_pair->graph_state, process); } } + MC_UNSET_RAW_MEM; } - /* Get current pair */ - current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateless)); + /* Get current state */ + current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful)); - /* Update current state in buchi automaton */ - a->current_state = current_pair->automaton_state; - - XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateless), search_cycle); + + XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateful), search_cycle); 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)); - + a->current_state = current_pair->automaton_state; + mc_stats_pair->visited_pairs++; int value; @@ -566,23 +572,30 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){ smx_req_t req = NULL; char *req_str; + mc_pair_t pair_succ; xbt_transition_t transition_succ; - unsigned int cursor = 0; + unsigned int cursor; int res; - mc_pair_stateless_t next_pair = NULL; - mc_pair_stateless_t pair_succ; - mc_snapshot_t next_snapshot = NULL; - xbt_dynar_t successors = NULL; - + + mc_pair_t next_pair = NULL; + mc_snapshot_t next_snapshot = NULL; + mc_snapshot_t current_snapshot = NULL; + + //sleep(1); MC_SET_RAW_MEM; - successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL); + successors = xbt_dynar_new(sizeof(mc_pair_t), NULL); MC_UNSET_RAW_MEM; - + while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){ - + MC_SET_RAW_MEM; + current_snapshot = xbt_new0(s_mc_snapshot_t, 1); + MC_take_snapshot(current_snapshot); + MC_UNSET_RAW_MEM; + + /* Debug information */ if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){ req_str = MC_request_to_string(req, value); @@ -590,10 +603,8 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){ xbt_free(req_str); } - //sleep(1); + MC_state_set_executed_request(current_pair->graph_state, req, value); - MC_state_set_executed_request(current_pair->graph_state, req, value); - /* Answer the request */ SIMIX_request_pre(req, value); @@ -601,11 +612,11 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){ MC_wait_for_requests(); + /* Create the new expanded graph_state */ MC_SET_RAW_MEM; - /* Create the new expanded graph_state */ next_graph_state = MC_state_pair_new(); - + /* Get enabled process and insert it in the interleave set of the next graph_state */ xbt_swag_foreach(process, simix_global->process_list){ if(MC_process_is_enabled(process)){ @@ -615,20 +626,20 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){ next_snapshot = xbt_new0(s_mc_snapshot_t, 1); MC_take_snapshot(next_snapshot); - + xbt_dynar_reset(successors); MC_UNSET_RAW_MEM; - - cursor= 0; + + cursor = 0; xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){ res = MC_automaton_evaluate_label(a, transition_succ->label); - + if(res == 1){ // enabled transition in automaton MC_SET_RAW_MEM; - next_pair = new_pair_stateless(next_graph_state, transition_succ->dst); + next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst); xbt_dynar_push(successors, &next_pair); MC_UNSET_RAW_MEM; } @@ -636,80 +647,89 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){ } cursor = 0; - xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){ - + res = MC_automaton_evaluate_label(a, transition_succ->label); - if(res == 2){ // enabled transition in automaton + if(res == 2){ // transition always enabled in automaton MC_SET_RAW_MEM; - next_pair = new_pair_stateless(next_graph_state, transition_succ->dst); + next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst); xbt_dynar_push(successors, &next_pair); MC_UNSET_RAW_MEM; } + } if(xbt_dynar_length(successors) == 0){ + MC_SET_RAW_MEM; - next_pair = new_pair_stateless(next_graph_state, current_pair->automaton_state); + next_pair = new_pair(next_snapshot, next_graph_state, current_pair->automaton_state); xbt_dynar_push(successors, &next_pair); MC_UNSET_RAW_MEM; + } - cursor = 0; + //XBT_DEBUG("Successors in automaton %lu", xbt_dynar_length(successors)); + cursor = 0; xbt_dynar_foreach(successors, cursor, pair_succ){ - + + //XBT_DEBUG("Search visited pair : graph=%p, automaton=%p", pair_succ->graph_state, pair_succ->automaton_state); + if((search_cycle == 1) && (reached(a, next_snapshot) == 1)){ XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); XBT_INFO("| ACCEPTANCE CYCLE |"); XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); XBT_INFO("Counter-example that violates formula :"); - MC_show_stack_liveness_stateless(mc_stack_liveness_stateless); - MC_dump_stack_liveness_stateless(mc_stack_liveness_stateless); + MC_show_stack_liveness_stateful(mc_stack_liveness_stateful); + MC_dump_stack_liveness_stateful(mc_stack_liveness_stateful); MC_print_statistics_pairs(mc_stats_pair); exit(0); } + //mc_stats_pair->executed_transitions++; + MC_SET_RAW_MEM; - xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ); + xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ); MC_UNSET_RAW_MEM; - MC_ddfs_stateless(a, search_cycle, 0); - - + MC_ddfs_stateful(a, search_cycle, 0); + + if((search_cycle == 0) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){ - XBT_DEBUG("Acceptance pair %p : graph=%p, automaton=%p(%s)", pair_succ, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id); int res = set_pair_reached(a, next_snapshot); - + XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id); + MC_SET_RAW_MEM; - xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ); + xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ); MC_UNSET_RAW_MEM; - - MC_ddfs_stateless(a, 1, 1); + MC_ddfs_stateful(a, 1, 1); + if(res){ MC_SET_RAW_MEM; xbt_dynar_pop(reached_pairs, NULL); MC_UNSET_RAW_MEM; } } + } if(MC_state_interleave_size(current_pair->graph_state) > 0){ - XBT_DEBUG("Backtracking to depth %u", xbt_fifo_size(mc_stack_liveness_stateless)); - MC_replay_liveness(mc_stack_liveness_stateless); - } - + XBT_DEBUG("Backtracking to depth %u", xbt_fifo_size(mc_stack_liveness_stateful)); + MC_restore_snapshot(current_snapshot); + MC_UNSET_RAW_MEM; + } + } + MC_SET_RAW_MEM; - xbt_fifo_shift(mc_stack_liveness_stateless); - XBT_DEBUG("Pair (graph=%p, automaton =%p, search_cycle = %u) shifted in stack", current_pair->graph_state, current_pair->automaton_state, search_cycle); + xbt_fifo_shift(mc_stack_liveness_stateful); + XBT_DEBUG("Pair (graph=%p, automaton =%p) shifted in stack", current_pair->graph_state, current_pair->automaton_state); MC_UNSET_RAW_MEM; } - diff --git a/src/mc/memory_map.c b/src/mc/memory_map.c index fa496896d2..9e987f0f07 100644 --- a/src/mc/memory_map.c +++ b/src/mc/memory_map.c @@ -144,14 +144,15 @@ memory_map_t get_memory_map(void) ret->mapsize++; if(XBT_LOG_ISENABLED(mc_memory_map, xbt_log_priority_debug)){ - - if (memreg.pathname == NULL){ - if (memreg.start_addr == std_heap){ - XBT_DEBUG("New region in snapshot : %s", backup_line); - } - } else { - if (!memcmp(basename(memreg.pathname), "libsimgrid", 10)){ - XBT_DEBUG("New region in snapshot : %s", backup_line); + if ((memreg.prot & PROT_WRITE)){ + if (memreg.pathname == NULL){ + if (memreg.start_addr == std_heap){ + XBT_DEBUG("New region in snapshot : %s", backup_line); + } + } else { + if (!memcmp(basename(memreg.pathname), "libsimgrid", 10)){ + XBT_DEBUG("New region in snapshot : %s", backup_line); + } } } } diff --git a/src/xbt/mmalloc/mm_legacy.c b/src/xbt/mmalloc/mm_legacy.c index 3b581c7611..b2814b3fd4 100644 --- a/src/xbt/mmalloc/mm_legacy.c +++ b/src/xbt/mmalloc/mm_legacy.c @@ -256,7 +256,7 @@ int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){ return 1; } - XBT_DEBUG("Heap index : %d", mdp1->heapindex); + //XBT_DEBUG("Heap index : %d", mdp1->heapindex); if(mdp1->base != mdp2->base){ XBT_DEBUG("Different base address of the memory region"); @@ -299,13 +299,15 @@ int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){ size_t block_free1, start1, block_free2 , start2, block_busy1, block_busy2 ; unsigned int i; + void *addr_block1, *addr_block2; + struct mdesc* mdp; start1 = block_free1 = mdp1->heapindex; start2 = block_free2 = mdp2->heapindex; block_busy1 = start1 + mdp1->heapinfo[start1].free.size; block_busy2 = start2 + mdp2->heapinfo[start2].free.size; - //XBT_DEBUG("Block busy : %d - %d", block_busy1, block_busy2); + XBT_DEBUG("Block busy : %d - %d", block_busy1, block_busy2); if(mdp1->heapinfo[start1].free.size != mdp2->heapinfo[start2].free.size){ // <=> check block_busy @@ -322,17 +324,36 @@ int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){ }else{ - for(i=block_busy1 ; iheapinfo[start1].free.next ; i++){ + i=block_busy1 ; + + XBT_DEBUG("Next free : %d", mdp1->heapinfo[start1].free.next); + + + while(iheapinfo[start1].free.next){ + + XBT_DEBUG("i (block busy) : %d", i); + if(mdp1->heapinfo[i].busy.type != mdp2->heapinfo[i].busy.type){ XBT_DEBUG("Different type of busy block"); return 1; }else{ + mdp = mdp1; + addr_block1 = ADDRESS(i); + mdp = mdp2; + addr_block2 = ADDRESS(i); switch(mdp1->heapinfo[i].busy.type){ case 0 : if(mdp1->heapinfo[i].busy.info.size != mdp2->heapinfo[i].busy.info.size){ XBT_DEBUG("Different size of a large cluster"); return 1; + }else{ + XBT_DEBUG("Blocks %d : %p - %p / Data size : %d (%d blocks)", i, addr_block1, addr_block2, (mdp->heapinfo[i].busy.info.size * BLOCKSIZE),mdp->heapinfo[i].busy.info.size ); + if(memcmp(addr_block1, addr_block2, mdp1->heapinfo[i].busy.info.size * BLOCKSIZE) != 0){ + XBT_DEBUG("Different data in block %d", i); + return 1; + } } + i = i + mdp1->heapinfo[i].busy.info.size; break; default : if(mdp1->heapinfo[i].busy.info.frag.nfree != mdp2->heapinfo[i].busy.info.frag.nfree){ @@ -342,68 +363,97 @@ int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){ if(mdp1->heapinfo[i].busy.info.frag.first != mdp2->heapinfo[i].busy.info.frag.first){ XBT_DEBUG("Different first free fragments of the block"); return 1; + }else{ + if(memcmp(addr_block1, addr_block2, BLOCKSIZE) != 0){ + XBT_DEBUG("Different data in block %d", i); + return 1; + } } } + i++; break; } } } - } - block_free1 = mdp1->heapinfo[start1].free.next; - block_free2 = mdp2->heapinfo[start2].free.next; - //XBT_DEBUG("Index of next free cluster : %d", block_free1); + block_free1 = mdp1->heapinfo[start1].free.next; + block_free2 = mdp2->heapinfo[start2].free.next; + + //XBT_DEBUG("Index of next free cluster : %d", block_free1); - while((block_free1 != start1) && (block_free2 != start2)){ + while((block_free1 != start1) && (block_free2 != start2)){ - block_busy1 = block_free1 + mdp1->heapinfo[block_free1].free.size; - block_busy2 = block_free2 + mdp2->heapinfo[block_free2].free.size; + block_busy1 = block_free1 + mdp1->heapinfo[block_free1].free.size; + block_busy2 = block_free2 + mdp2->heapinfo[block_free2].free.size; - if(block_busy1 != block_busy2){ - XBT_DEBUG("Different index of busy block"); - return 1; - }else{ + if(block_busy1 != block_busy2){ + XBT_DEBUG("Different index of busy block"); + return 1; + }else{ - //XBT_DEBUG("Index of next busy block : %d - %d", block_busy1, block_busy2); - //XBT_DEBUG("Index of next free cluster : %d", mdp1->heapinfo[block_free1].free.next); + XBT_DEBUG("Index of next busy block : %d - %d", block_busy1, block_busy2); + XBT_DEBUG("Index of next free cluster : %d", mdp1->heapinfo[block_free1].free.next); - for(i=block_busy1 ; iheapinfo[block_free1].free.next ; i++){ - if(mdp1->heapinfo[i].busy.type != mdp2->heapinfo[i].busy.type){ - XBT_DEBUG("Different type of busy block"); - return 1; - }else{ - switch(mdp1->heapinfo[i].busy.type){ - case 0 : - if(mdp1->heapinfo[i].busy.info.size != mdp2->heapinfo[i].busy.info.size){ - XBT_DEBUG("Different size of a large cluster"); - return 1; - } - break; - default : - if(mdp1->heapinfo[i].busy.info.frag.nfree != mdp2->heapinfo[i].busy.info.frag.nfree){ - XBT_DEBUG("Different free fragments in a fragmented block"); - return 1; - }else{ - if(mdp1->heapinfo[i].busy.info.frag.first != mdp2->heapinfo[i].busy.info.frag.first){ - XBT_DEBUG("Different first free fragments of the block"); - return 1; + i = block_busy1; + + while(iheapinfo[block_free1].free.next){ + + XBT_DEBUG("i (block busy) : %d", i); + + if(mdp1->heapinfo[i].busy.type != mdp2->heapinfo[i].busy.type){ + XBT_DEBUG("Different type of busy block"); + return 1; + }else{ + mdp = mdp1; + addr_block1 = ADDRESS(i); + mdp = mdp2; + addr_block2 = ADDRESS(i); + switch(mdp1->heapinfo[i].busy.type){ + case 0 : + if(mdp1->heapinfo[i].busy.info.size != mdp2->heapinfo[i].busy.info.size){ + XBT_DEBUG("Different size of a large cluster"); + return 1; + }else{ + XBT_DEBUG("Blocks %d : %p - %p / Data size : %d", i, addr_block1, addr_block2, (mdp->heapinfo[i].busy.info.size * BLOCKSIZE)); + //XBT_DEBUG("Size of large cluster %d", mdp->heapinfo[i].busy.info.size); + if(memcmp(addr_block1, addr_block2, (mdp1->heapinfo[i].busy.info.size * BLOCKSIZE)) != 0){ + XBT_DEBUG("Different data in block %d", i); + return 1; + } + } + i = i+mdp1->heapinfo[i].busy.info.size; + break; + default : + if(mdp1->heapinfo[i].busy.info.frag.nfree != mdp2->heapinfo[i].busy.info.frag.nfree){ + XBT_DEBUG("Different free fragments in a fragmented block"); + return 1; + }else{ + if(mdp1->heapinfo[i].busy.info.frag.first != mdp2->heapinfo[i].busy.info.frag.first){ + XBT_DEBUG("Different first free fragments of the block"); + return 1; + }else{ + if(memcmp(addr_block1, addr_block2, BLOCKSIZE) != 0){ + XBT_DEBUG("Different data in fragmented block %d", i); + return 1; + } + } } + i++; + break; } - break; - } - } + } + } } - } - block_free1 = mdp1->heapinfo[block_free1].free.next; - block_free2 = mdp2->heapinfo[block_free2].free.next; + block_free1 = mdp1->heapinfo[block_free1].free.next; + block_free2 = mdp2->heapinfo[block_free2].free.next; - } + } - } - + } + } return 0;