X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/7e9b6e88f6c2daa87a9f5370596e5acc7f73fc6a..c0dc66a3644be860680e6df4092484c522e59d40:/src/mc/mc_liveness.c diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c index a49dbfbedc..1b05a14c13 100644 --- a/src/mc/mc_liveness.c +++ b/src/mc/mc_liveness.c @@ -137,6 +137,8 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){ int reached(xbt_state_t st){ + raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + if(xbt_dynar_is_empty(reached_pairs)){ @@ -156,7 +158,7 @@ int reached(xbt_state_t st){ /* Get values of propositional symbols */ unsigned int cursor = 0; xbt_propositional_symbol_t ps = NULL; - xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){ + xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){ f = (int_f_void_t)ps->function; res = (*f)(); xbt_dynar_push_as(prop_ato, int, res); @@ -180,6 +182,12 @@ int reached(xbt_state_t st){ xbt_dynar_reset(prop_ato); xbt_free(prop_ato); MC_UNSET_RAW_MEM; + + if(raw_mem_set) + MC_SET_RAW_MEM; + else + MC_UNSET_RAW_MEM; + return 1; } /* } @@ -198,6 +206,12 @@ int reached(xbt_state_t st){ xbt_dynar_reset(prop_ato); xbt_free(prop_ato); MC_UNSET_RAW_MEM; + + if(raw_mem_set) + MC_SET_RAW_MEM; + else + MC_UNSET_RAW_MEM; + return 0; } @@ -366,6 +380,7 @@ int rdv_points_compare(xbt_dict_t d1, xbt_dict_t d2){ /* d1 = pair_test, d2 = cu void set_pair_reached(xbt_state_t st){ + raw_mem_set = (mmalloc_get_current_heap() == raw_heap); MC_SET_RAW_MEM; @@ -384,7 +399,7 @@ void set_pair_reached(xbt_state_t st){ int res; int_f_void_t f; - xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){ + xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){ f = (int_f_void_t)ps->function; res = (*f)(); xbt_dynar_push_as(pair->prop_ato, int, res); @@ -417,12 +432,18 @@ void set_pair_reached(xbt_state_t st){ xbt_dynar_push(reached_pairs, &pair); MC_UNSET_RAW_MEM; - + + if(raw_mem_set) + MC_SET_RAW_MEM; + else + MC_UNSET_RAW_MEM; + } int reached_hash(xbt_state_t st){ + raw_mem_set = (mmalloc_get_current_heap() == raw_heap); if(xbt_dynar_is_empty(reached_pairs_hash)){ @@ -449,7 +470,7 @@ int reached_hash(xbt_state_t st){ int res; int_f_void_t f; - xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){ + xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){ f = (int_f_void_t)ps->function; res = (*f)(); xbt_dynar_push_as(prop_ato, int, res); @@ -475,6 +496,12 @@ int reached_hash(xbt_state_t st){ xbt_dynar_reset(prop_ato); xbt_free(prop_ato); MC_UNSET_RAW_MEM; + + if(raw_mem_set) + MC_SET_RAW_MEM; + else + MC_UNSET_RAW_MEM; + return 1; }else{ XBT_INFO("Different snapshot"); @@ -493,12 +520,20 @@ int reached_hash(xbt_state_t st){ xbt_dynar_reset(prop_ato); xbt_free(prop_ato); MC_UNSET_RAW_MEM; + + if(raw_mem_set) + MC_SET_RAW_MEM; + else + MC_UNSET_RAW_MEM; + return 0; } } void set_pair_reached_hash(xbt_state_t st){ + + raw_mem_set = (mmalloc_get_current_heap() == raw_heap); MC_SET_RAW_MEM; @@ -523,7 +558,7 @@ void set_pair_reached_hash(xbt_state_t st){ int res; int_f_void_t f; - xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){ + xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){ f = (int_f_void_t)ps->function; res = (*f)(); xbt_dynar_push_as(pair->prop_ato, int, res); @@ -534,12 +569,18 @@ void set_pair_reached_hash(xbt_state_t st){ MC_free_snapshot(sn); MC_UNSET_RAW_MEM; - + + if(raw_mem_set) + MC_SET_RAW_MEM; + else + MC_UNSET_RAW_MEM; + } int visited(xbt_state_t st, int sc){ + raw_mem_set = (mmalloc_get_current_heap() == raw_heap); if(xbt_dynar_is_empty(visited_pairs)){ @@ -560,7 +601,7 @@ int visited(xbt_state_t st, int sc){ int res; int_f_void_t f; - xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){ + xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){ f = (int_f_void_t)ps->function; res = (*f)(); xbt_dynar_push_as(prop_ato, int, res); @@ -580,6 +621,11 @@ int visited(xbt_state_t st, int sc){ xbt_free(prop_ato); MC_UNSET_RAW_MEM; + if(raw_mem_set) + MC_SET_RAW_MEM; + else + MC_UNSET_RAW_MEM; + return 1; }else{ @@ -601,6 +647,12 @@ int visited(xbt_state_t st, int sc){ xbt_dynar_reset(prop_ato); xbt_free(prop_ato); MC_UNSET_RAW_MEM; + + if(raw_mem_set) + MC_SET_RAW_MEM; + else + MC_UNSET_RAW_MEM; + return 0; } @@ -609,6 +661,7 @@ int visited(xbt_state_t st, int sc){ int visited_hash(xbt_state_t st, int sc){ + raw_mem_set = (mmalloc_get_current_heap() == raw_heap); if(xbt_dynar_is_empty(visited_pairs_hash)){ @@ -635,7 +688,7 @@ int visited_hash(xbt_state_t st, int sc){ int res; int_f_void_t f; - xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){ + xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){ f = (int_f_void_t)ps->function; res = (*f)(); xbt_dynar_push_as(prop_ato, int, res); @@ -661,6 +714,12 @@ int visited_hash(xbt_state_t st, int sc){ xbt_dynar_reset(prop_ato); xbt_free(prop_ato); MC_UNSET_RAW_MEM; + + if(raw_mem_set) + MC_SET_RAW_MEM; + else + MC_UNSET_RAW_MEM; + return 1; }else{ //XBT_INFO("Different snapshot"); @@ -682,12 +741,20 @@ int visited_hash(xbt_state_t st, int sc){ xbt_dynar_reset(prop_ato); xbt_free(prop_ato); MC_UNSET_RAW_MEM; + + if(raw_mem_set) + MC_SET_RAW_MEM; + else + MC_UNSET_RAW_MEM; + return 0; } } void set_pair_visited_hash(xbt_state_t st, int sc){ + + raw_mem_set = (mmalloc_get_current_heap() == raw_heap); MC_SET_RAW_MEM; @@ -713,7 +780,7 @@ void set_pair_visited_hash(xbt_state_t st, int sc){ int res; int_f_void_t f; - xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){ + xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){ f = (int_f_void_t)ps->function; res = (*f)(); xbt_dynar_push_as(pair->prop_ato, int, res); @@ -725,10 +792,16 @@ void set_pair_visited_hash(xbt_state_t st, int sc){ MC_UNSET_RAW_MEM; + if(raw_mem_set) + MC_SET_RAW_MEM; + else + MC_UNSET_RAW_MEM; + } void set_pair_visited(xbt_state_t st, int sc){ + raw_mem_set = (mmalloc_get_current_heap() == raw_heap); MC_SET_RAW_MEM; @@ -747,7 +820,7 @@ void set_pair_visited(xbt_state_t st, int sc){ int res; int_f_void_t f; - xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){ + xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){ f = (int_f_void_t)ps->function; res = (*f)(); xbt_dynar_push_as(pair->prop_ato, int, res); @@ -757,6 +830,10 @@ void set_pair_visited(xbt_state_t st, int sc){ MC_UNSET_RAW_MEM; + if(raw_mem_set) + MC_SET_RAW_MEM; + else + MC_UNSET_RAW_MEM; } @@ -789,7 +866,7 @@ int MC_automaton_evaluate_label(xbt_exp_label_t l){ unsigned int cursor = 0; xbt_propositional_symbol_t p = NULL; int_f_void_t f; - xbt_dynar_foreach(automaton->propositional_symbols, cursor, p){ + xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, p){ if(strcmp(p->pred, l->u.predicat) == 0){ f = (int_f_void_t)p->function; return (*f)(); @@ -826,6 +903,8 @@ mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r){ void MC_ddfs_init(void){ + raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + XBT_INFO("**************************************************"); XBT_INFO("Double-DFS init"); XBT_INFO("**************************************************"); @@ -849,7 +928,7 @@ void MC_ddfs_init(void){ reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL); //reached_pairs_hash = xbt_dynar_new(sizeof(mc_pair_reached_hash_t), NULL); //visited_pairs = xbt_dynar_new(sizeof(mc_pair_visited_t), NULL); - visited_pairs_hash = xbt_dynar_new(sizeof(mc_pair_visited_hash_t), NULL); + //visited_pairs_hash = xbt_dynar_new(sizeof(mc_pair_visited_hash_t), NULL); successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL); /* Save the initial state */ @@ -861,7 +940,7 @@ void MC_ddfs_init(void){ unsigned int cursor = 0; xbt_state_t state; - xbt_dynar_foreach(automaton->states, cursor, state){ + xbt_dynar_foreach(_mc_property_automaton->states, cursor, state){ if(state->type == -1){ MC_SET_RAW_MEM; @@ -896,13 +975,21 @@ void MC_ddfs_init(void){ } } - } + } + + if(raw_mem_set) + MC_SET_RAW_MEM; + else + MC_UNSET_RAW_MEM; + } void MC_ddfs(int search_cycle){ + raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + smx_process_t process; mc_pair_stateless_t current_pair = NULL; @@ -914,7 +1001,7 @@ void MC_ddfs(int search_cycle){ current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness)); /* Update current state in buchi automaton */ - automaton->current_state = current_pair->automaton_state; + _mc_property_automaton->current_state = current_pair->automaton_state; XBT_INFO("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle); @@ -939,10 +1026,10 @@ void MC_ddfs(int search_cycle){ if(xbt_fifo_size(mc_stack_liveness) < MAX_DEPTH_LIVENESS){ //set_pair_visited(current_pair->automaton_state, search_cycle); - set_pair_visited_hash(current_pair->automaton_state, search_cycle); + //set_pair_visited_hash(current_pair->automaton_state, search_cycle); //XBT_INFO("Visited pairs : %lu", xbt_dynar_length(visited_pairs)); - XBT_INFO("Visited pairs : %lu", xbt_dynar_length(visited_pairs_hash)); + //XBT_INFO("Visited pairs : %lu", xbt_dynar_length(visited_pairs_hash)); if(current_pair->requests > 0){ @@ -1051,7 +1138,7 @@ void MC_ddfs(int search_cycle){ }else{ - if(!visited_hash(pair_succ->automaton_state, search_cycle)){ + //if(!visited_hash(pair_succ->automaton_state, search_cycle)){ //if(!visited(pair_succ->automaton_state, search_cycle)){ MC_SET_RAW_MEM; @@ -1060,11 +1147,11 @@ void MC_ddfs(int search_cycle){ MC_ddfs(search_cycle); - }else{ + /*}else{ XBT_INFO("Next pair already visited ! "); - } + }*/ } @@ -1084,7 +1171,7 @@ void MC_ddfs(int search_cycle){ } - if(!visited_hash(pair_succ->automaton_state, search_cycle)){ + //if(!visited_hash(pair_succ->automaton_state, search_cycle)){ //if(!visited(pair_succ->automaton_state, search_cycle)){ MC_SET_RAW_MEM; @@ -1093,11 +1180,11 @@ void MC_ddfs(int search_cycle){ MC_ddfs(search_cycle); - }else{ + /*}else{ XBT_INFO("Next pair already visited ! "); - } + }*/ } @@ -1199,7 +1286,7 @@ void MC_ddfs(int search_cycle){ }else{ - if(!visited_hash(pair_succ->automaton_state, search_cycle)){ + //if(!visited_hash(pair_succ->automaton_state, search_cycle)){ //if(!visited(pair_succ->automaton_state, search_cycle)){ MC_SET_RAW_MEM; @@ -1208,11 +1295,11 @@ void MC_ddfs(int search_cycle){ MC_ddfs(search_cycle); - }else{ + /*}else{ XBT_INFO("Next pair already visited ! "); - } + }*/ } @@ -1230,7 +1317,7 @@ void MC_ddfs(int search_cycle){ } - if(!visited_hash(pair_succ->automaton_state, search_cycle)){ + //if(!visited_hash(pair_succ->automaton_state, search_cycle)){ //if(!visited(pair_succ->automaton_state, search_cycle)){ MC_SET_RAW_MEM; @@ -1239,11 +1326,11 @@ void MC_ddfs(int search_cycle){ MC_ddfs(search_cycle); - }else{ + /*}else{ XBT_INFO("Next pair already visited ! "); - } + }*/ } @@ -1276,8 +1363,11 @@ void MC_ddfs(int search_cycle){ //xbt_dynar_pop(reached_pairs_hash, NULL); } MC_UNSET_RAW_MEM; - - + + if(raw_mem_set) + MC_SET_RAW_MEM; + else + MC_UNSET_RAW_MEM; }