X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/984b8e1616cfd626c6244a34ccd42ee0b1e89bcd..21fce2eda21e3c3bea7a19630948ccd6ec64145f:/src/mc/mc_liveness.c diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c index 08a6d5429c..b0877f6707 100644 --- a/src/mc/mc_liveness.c +++ b/src/mc/mc_liveness.c @@ -33,110 +33,10 @@ unsigned int hash_region(char *str, int str_len){ } -int data_program_region_compare(void *d1, void *d2, size_t size){ - int distance = 0; - int i; - - for(i=0; inum_reg != s2->num_reg){ - XBT_INFO("Different num_reg (s1 = %u, s2 = %u)", s1->num_reg, s2->num_reg); - return 1; - } - - int i; - int errors = 0; - - for(i=0 ; i< s1->num_reg ; i++){ - - if(s1->regions[i]->type != s2->regions[i]->type){ - XBT_INFO("Different type of region"); - errors++; - } - - switch(s1->regions[i]->type){ - case 0: - if(s1->regions[i]->size != s2->regions[i]->size){ - XBT_INFO("Different size of heap (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size); - errors++; - } - if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){ - XBT_INFO("Different start addr of heap (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr); - errors++; - } - if(mmalloc_compare_heap(s1->regions[i]->data, s2->regions[i]->data)){ - XBT_INFO("Different heap (mmalloc_compare)"); - errors++; - } - break; - case 1 : - if(s1->regions[i]->size != s2->regions[i]->size){ - XBT_INFO("Different size of libsimgrid (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size); - errors++; - } - if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){ - XBT_INFO("Different start addr of libsimgrid (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr); - errors++; - } - if(data_libsimgrid_region_compare(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){ - XBT_INFO("Different memcmp for data in libsimgrid"); - errors++; - } - break; - case 2 : - if(s1->regions[i]->size != s2->regions[i]->size){ - XBT_INFO("Different size of data program (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size); - errors++; - } - if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){ - XBT_INFO("Different start addr of data program (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr); - errors++; - } - if(data_program_region_compare(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){ - XBT_INFO("Different memcmp for data in program"); - errors++; - } - break; - default: - break; - } - } - - return (errors > 0); - -} - int reached(xbt_state_t st){ + raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + if(xbt_dynar_is_empty(reached_pairs)){ @@ -180,6 +80,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 +104,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 +278,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; @@ -417,12 +330,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)){ @@ -475,6 +394,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 +418,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; @@ -534,12 +467,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)){ @@ -580,6 +519,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 +545,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 +559,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)){ @@ -661,6 +612,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 +639,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; @@ -725,10 +690,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; @@ -757,6 +728,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; } @@ -826,6 +801,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 +826,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 */ @@ -896,13 +873,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; @@ -939,10 +924,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 +1036,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 +1045,11 @@ void MC_ddfs(int search_cycle){ MC_ddfs(search_cycle); - }else{ + /*}else{ XBT_INFO("Next pair already visited ! "); - } + }*/ } @@ -1084,7 +1069,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 +1078,11 @@ void MC_ddfs(int search_cycle){ MC_ddfs(search_cycle); - }else{ + /*}else{ XBT_INFO("Next pair already visited ! "); - } + }*/ } @@ -1199,7 +1184,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 +1193,11 @@ void MC_ddfs(int search_cycle){ MC_ddfs(search_cycle); - }else{ + /*}else{ XBT_INFO("Next pair already visited ! "); - } + }*/ } @@ -1230,7 +1215,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 +1224,11 @@ void MC_ddfs(int search_cycle){ MC_ddfs(search_cycle); - }else{ + /*}else{ XBT_INFO("Next pair already visited ! "); - } + }*/ } @@ -1276,8 +1261,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; }