From 6229ff3a39c8fb195846ea9eb67cf071654de597 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Tue, 22 Nov 2011 17:35:17 +0100 Subject: [PATCH 1/1] model-checker : add snapshot of stack memory region for comparison of pairs reached or simply visited --- src/mc/mc_checkpoint.c | 85 ++++++++++++++++++- src/mc/mc_global.c | 6 +- src/mc/mc_liveness.c | 184 +++++++++++++++++++++++++---------------- src/mc/memory_map.c | 21 +---- src/mc/private.h | 9 +- 5 files changed, 202 insertions(+), 103 deletions(-) diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c index 447a8dbb8b..aec3a719d1 100644 --- a/src/mc/mc_checkpoint.c +++ b/src/mc/mc_checkpoint.c @@ -18,7 +18,9 @@ static mc_mem_region_t MC_region_new(int type, void *start_addr, size_t size) new_reg->start_addr = start_addr; new_reg->size = size; new_reg->data = xbt_malloc0(size); + XBT_DEBUG("New reg data %p, start_addr %p", new_reg->data, start_addr); memcpy(new_reg->data, start_addr, size); + return new_reg; } @@ -26,7 +28,37 @@ static void MC_region_restore(mc_mem_region_t reg) { /*FIXME: check if start_addr is still mapped, if it is not, then map it before copying the data */ - memcpy(reg->start_addr, reg->data, reg->size); + if(reg->type == 3){ + memory_map_t maps = get_memory_map(); + MC_UNSET_RAW_MEM; + unsigned int i=0; + s_map_region r; + while(i < maps->mapsize){ + r = maps->regions[i]; + if (maps->regions[i].pathname != NULL){ + if (!memcmp(maps->regions[i].pathname, "[stack]", 7)){ + size_t diff = (char*)reg->start_addr - (char*)r.start_addr; + void *segment = malloc(reg->size + diff); + XBT_DEBUG("Size of segment : %lu", sizeof(segment)); + memcpy((char *)segment + diff, reg->data, reg->size); + //memset(segment, '\0', diff); + //XBT_DEBUG("Memset ok"); + //memcpy(segment+diff, reg->data, reg->size); + //XBT_DEBUG("Memcpy segment ok"); + memcpy(r.start_addr, segment, sizeof(segment)); + XBT_DEBUG("Memcpy region ok"); + //memcpy(r.start_addr, reg->data, sizeof(reg->data)); + break; + } + } + i++; + } + }else{ + XBT_DEBUG("Memcpy : dest %p, src %p, size %Zu", reg->start_addr, reg->data, reg->size); + memcpy(reg->start_addr, reg->data, reg->size); + } + + //return; } static void MC_region_destroy(mc_mem_region_t reg) @@ -37,6 +69,20 @@ static void MC_region_destroy(mc_mem_region_t reg) static void MC_snapshot_add_region(mc_snapshot_t snapshot, int type, void *start_addr, size_t size) { + switch(type){ + case 0 : + XBT_DEBUG("New region heap"); + break; + case 1 : + XBT_DEBUG("New region libsimgrid"); + break; + case 2 : + XBT_DEBUG("New region program"); + break; + case 3 : + XBT_DEBUG("New region stack"); + break; + } mc_mem_region_t new_reg = MC_region_new(type, start_addr, size); snapshot->regions = xbt_realloc(snapshot->regions, (snapshot->num_reg + 1) * sizeof(mc_mem_region_t)); snapshot->regions[snapshot->num_reg] = new_reg; @@ -77,6 +123,14 @@ void MC_take_snapshot_liveness(mc_snapshot_t snapshot, char *prgm) s_map_region reg; memory_map_t maps = get_memory_map(); + for(i=0; i< snapshot->num_reg; i++){ + MC_region_destroy(snapshot->regions[i]); + } + + snapshot->num_reg = 0; + + i = 0; + /* Save the std heap and the writable mapped pages of libsimgrid */ while (i < maps->mapsize) { reg = maps->regions[i]; @@ -90,8 +144,12 @@ void MC_take_snapshot_liveness(mc_snapshot_t snapshot, char *prgm) MC_snapshot_add_region(snapshot, 1, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr); } else { if (!memcmp(basename(maps->regions[i].pathname), basename(prgm), strlen(basename(prgm)))){ - MC_snapshot_add_region(snapshot, 1, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr); - } + MC_snapshot_add_region(snapshot, 2, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr); + } else { + if (!memcmp(maps->regions[i].pathname, "[stack]", 7)){ + MC_snapshot_add_region(snapshot, 3, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr); + } + } } } } @@ -104,8 +162,25 @@ void MC_take_snapshot_liveness(mc_snapshot_t snapshot, char *prgm) void MC_restore_snapshot(mc_snapshot_t snapshot) { unsigned int i; - for(i=0; i < snapshot->num_reg; i++) + for(i=0; i < snapshot->num_reg; i++){ MC_region_restore(snapshot->regions[i]); + switch(snapshot->regions[i]->type){ + case 0 : + XBT_DEBUG("heap restored"); + break; + case 1: + XBT_DEBUG("libsimgrid (data) restored"); + break; + case 2: + XBT_DEBUG("program (data) restored"); + break; + case 3: + XBT_DEBUG("stack restored"); + break; + } + + } + } void MC_free_snapshot(mc_snapshot_t snapshot) @@ -116,3 +191,5 @@ void MC_free_snapshot(mc_snapshot_t snapshot) xbt_free(snapshot); } + + diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index ec871c133e..41f9316bf6 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -30,6 +30,7 @@ mc_stats_t mc_stats = NULL; xbt_fifo_t mc_stack_liveness_stateful = NULL; mc_stats_pair_t mc_stats_pair = NULL; xbt_fifo_t mc_stack_liveness_stateless = NULL; +mc_snapshot_t initial_snapshot_liveness = NULL; /** @@ -176,7 +177,8 @@ void MC_exit_liveness(void) { MC_print_statistics_pairs(mc_stats_pair); //xbt_free(mc_time); - MC_memory_exit(); + //MC_memory_exit(); + exit(0); } @@ -295,7 +297,7 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack) XBT_DEBUG("**** Begin Replay ****"); /* Restore the initial state */ - MC_restore_snapshot(initial_snapshot); + MC_restore_snapshot(initial_snapshot_liveness); /* At the moment of taking the snapshot the raw heap was set, so restoring * it will set it back again, we have to unset it to continue */ MC_UNSET_RAW_MEM; diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c index bf7c15d6d2..65f81501f4 100644 --- a/src/mc/mc_liveness.c +++ b/src/mc/mc_liveness.c @@ -4,62 +4,102 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc, "Logging specific to algorithms for liveness properties verification"); -xbt_dynar_t initial_pairs = NULL; xbt_fifo_t reached_pairs; xbt_fifo_t visited_pairs; xbt_dynar_t successors = NULL; -extern mc_snapshot_t initial_snapshot; + +//mc_snapshot_t snapshot; int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){ - XBT_DEBUG("Compare snapshot"); + //XBT_DEBUG("Compare snapshot"); if(s1->num_reg != s2->num_reg){ XBT_DEBUG("Different num_reg (s1 = %d, s2 = %d)", s1->num_reg, s2->num_reg); return 1; } + //XBT_DEBUG("Num reg : %d", s1->num_reg); + int i; int errors = 0; for(i=0 ; i< s1->num_reg ; i++){ - - if(s1->regions[i]->size != s2->regions[i]->size){ - XBT_DEBUG("Different size of region"); - return 1; - } - - if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){ - XBT_DEBUG("Different start addr of region"); - return 1; - } - + if(s1->regions[i]->type != s2->regions[i]->type){ - XBT_DEBUG("Different type of region"); + //XBT_DEBUG("Different type of region"); return 1; } - - if(s1->regions[i]->type == 0){ + switch(s1->regions[i]->type){ + case 0: + //XBT_DEBUG("Region : heap"); + if(s1->regions[i]->size != s2->regions[i]->size){ + //XBT_DEBUG("Different size of heap (s1 = %Zu, s2 = %Zu)", s1->regions[i]->size, s2->regions[i]->size); + return 1; + } + if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){ + //XBT_DEBUG("Different start addr of heap (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr); + return 1; + } if(mmalloc_compare_heap(s1->regions[i]->start_addr, s2->regions[i]->start_addr)){ - XBT_DEBUG("Different heap (mmalloc_compare)"); + //XBT_DEBUG("Different heap (mmalloc_compare)"); errors++; } - }else{ + break; + case 1 : + //XBT_DEBUG("Region : libsimgrid"); + if(s1->regions[i]->size != s2->regions[i]->size){ + //XBT_DEBUG("Different size of libsimgrid (s1 = %Zu, s2 = %Zu)", s1->regions[i]->size, s2->regions[i]->size); + return 1; + } + if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){ + //XBT_DEBUG("Different start addr of libsimgrid (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr); + return 1; + } + if(memcmp(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){ + //XBT_DEBUG("Different memcmp for data in libsimgrid"); + errors++; + } + break; + case 2: + //XBT_DEBUG("Region : program"); + if(s1->regions[i]->size != s2->regions[i]->size){ + //XBT_DEBUG("Different size of program (s1 = %Zu, s2 = %Zu)", s1->regions[i]->size, s2->regions[i]->size); + return 1; + } + if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){ + //XBT_DEBUG("Different start addr of program (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr); + return 1; + } if(memcmp(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){ - XBT_DEBUG("Different memcmp for data in libsimgrid or program"); + //XBT_DEBUG("Different memcmp for data in program"); errors++; } + break; + case 3: + //XBT_DEBUG("Region : stack"); + if(s1->regions[i]->size != s2->regions[i]->size){ + //XBT_DEBUG("Different size of stack (s1 = %Zu, s2 = %Zu)", s1->regions[i]->size, s2->regions[i]->size); + return 1; + } + if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){ + //XBT_DEBUG("Different start addr of stack (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr); + return 1; + } + if(memcmp(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){ + //XBT_DEBUG("Different memcmp for data in stack"); + errors++; + } + break; } - - } return (errors>0); - + } -int reached(xbt_automaton_t a, xbt_state_t st, mc_snapshot_t s){ +int reached(xbt_automaton_t a, xbt_state_t st, char *prgm){ if(xbt_fifo_size(reached_pairs) == 0){ @@ -67,8 +107,6 @@ int reached(xbt_automaton_t a, xbt_state_t st, mc_snapshot_t s){ return 0; }else{ - - MC_SET_RAW_MEM; xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL); @@ -81,7 +119,10 @@ int reached(xbt_automaton_t a, xbt_state_t st, mc_snapshot_t s){ xbt_dynar_push_as(prop_ato, int, res); } - + MC_SET_RAW_MEM; + mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1); + MC_take_snapshot_liveness(sn, prgm); + MC_UNSET_RAW_MEM; int i=0; xbt_fifo_item_t item = xbt_fifo_get_first_item(reached_pairs); @@ -93,7 +134,9 @@ int reached(xbt_automaton_t a, xbt_state_t st, mc_snapshot_t s){ if(automaton_state_compare(pair_test->automaton_state, st) == 0){ if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){ - if(snapshot_compare(s, pair_test->system_state) == 0){ + if(snapshot_compare(sn, pair_test->system_state) == 0){ + MC_SET_RAW_MEM; + MC_free_snapshot(sn); MC_UNSET_RAW_MEM; return 1; } @@ -106,13 +149,15 @@ int reached(xbt_automaton_t a, xbt_state_t st, mc_snapshot_t s){ } + MC_SET_RAW_MEM; + MC_free_snapshot(sn); MC_UNSET_RAW_MEM; return 0; } } -void set_pair_reached(xbt_automaton_t a, xbt_state_t st, mc_snapshot_t sn){ +void set_pair_reached(xbt_automaton_t a, xbt_state_t st, char *prgm){ MC_SET_RAW_MEM; @@ -121,7 +166,8 @@ void set_pair_reached(xbt_automaton_t a, xbt_state_t st, mc_snapshot_t sn){ pair = xbt_new0(s_mc_pair_reached_t, 1); pair->automaton_state = st; pair->prop_ato = xbt_dynar_new(sizeof(int), NULL); - pair->system_state = sn; + pair->system_state = xbt_new0(s_mc_snapshot_t, 1); + MC_take_snapshot_liveness(pair->system_state, prgm); /* Get values of propositional symbols */ unsigned int cursor = 0; @@ -139,7 +185,7 @@ void set_pair_reached(xbt_automaton_t a, xbt_state_t st, mc_snapshot_t sn){ } -int visited(xbt_automaton_t a, xbt_state_t st, mc_snapshot_t s, int sc){ +int visited(xbt_automaton_t a, xbt_state_t st, int sc, char *prgm){ if(xbt_fifo_size(visited_pairs) == 0){ @@ -147,8 +193,6 @@ int visited(xbt_automaton_t a, xbt_state_t st, mc_snapshot_t s, int sc){ return 0; }else{ - - MC_SET_RAW_MEM; xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL); @@ -161,6 +205,10 @@ int visited(xbt_automaton_t a, xbt_state_t st, mc_snapshot_t s, int sc){ xbt_dynar_push_as(prop_ato, int, res); } + MC_SET_RAW_MEM; + mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1); + MC_take_snapshot_liveness(sn, prgm); + MC_UNSET_RAW_MEM; int i=0; @@ -174,7 +222,9 @@ int visited(xbt_automaton_t a, xbt_state_t st, mc_snapshot_t s, int sc){ if(pair_test->search_cycle == sc) { if(automaton_state_compare(pair_test->automaton_state, st) == 0){ if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){ - if(snapshot_compare(s, pair_test->system_state) == 0){ + if(snapshot_compare(sn, pair_test->system_state) == 0){ + MC_SET_RAW_MEM; + MC_free_snapshot(sn); MC_UNSET_RAW_MEM; return 1; } @@ -188,22 +238,25 @@ int visited(xbt_automaton_t a, xbt_state_t st, mc_snapshot_t s, int sc){ } + MC_SET_RAW_MEM; + MC_free_snapshot(sn); MC_UNSET_RAW_MEM; return 0; } } -void set_pair_visited(xbt_automaton_t a, xbt_state_t st, mc_snapshot_t sn, int sc){ +void set_pair_visited(xbt_automaton_t a, xbt_state_t st, int sc, char *prgm){ MC_SET_RAW_MEM; - + mc_pair_visited_t pair = NULL; pair = xbt_new0(s_mc_pair_visited_t, 1); pair->automaton_state = st; pair->prop_ato = xbt_dynar_new(sizeof(int), NULL); - pair->system_state = sn; + pair->system_state = xbt_new0(s_mc_snapshot_t, 1); + MC_take_snapshot_liveness(pair->system_state, prgm); pair->search_cycle = sc; /* Get values of propositional symbols */ @@ -320,8 +373,9 @@ void MC_ddfs_stateless_init(xbt_automaton_t a, char *prgm){ visited_pairs = xbt_fifo_new(); successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL); - initial_snapshot = xbt_new0(s_mc_snapshot_t, 1); - MC_take_snapshot_liveness(initial_snapshot, prgm); + /* Save the initial state */ + initial_snapshot_liveness = xbt_new0(s_mc_snapshot_t, 1); + MC_take_snapshot_liveness(initial_snapshot_liveness, prgm); MC_UNSET_RAW_MEM; @@ -337,7 +391,7 @@ void MC_ddfs_stateless_init(xbt_automaton_t a, char *prgm){ MC_UNSET_RAW_MEM; if(cursor != 0){ - MC_restore_snapshot(initial_snapshot); + MC_restore_snapshot(initial_snapshot_liveness); MC_UNSET_RAW_MEM; } @@ -351,10 +405,10 @@ void MC_ddfs_stateless_init(xbt_automaton_t a, char *prgm){ xbt_fifo_unshift(mc_stack_liveness_stateless, mc_initial_pair); MC_UNSET_RAW_MEM; - set_pair_reached(a, state, initial_snapshot); + set_pair_reached(a, state, prgm); if(cursor != 0){ - MC_restore_snapshot(initial_snapshot); + MC_restore_snapshot(initial_snapshot_liveness); MC_UNSET_RAW_MEM; } @@ -371,8 +425,8 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *pr smx_process_t process; mc_pair_stateless_t current_pair = NULL; - mc_snapshot_t snapshot = NULL; - mc_snapshot_t current_snapshot = NULL; + + //mc_snapshot_t current_snapshot = NULL; if(xbt_fifo_size(mc_stack_liveness_stateless) == 0) return; @@ -399,6 +453,8 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *pr mc_stats_pair->visited_pairs++; + //sleep(1); + int value; mc_state_t next_graph_state = NULL; smx_req_t req = NULL; @@ -413,12 +469,7 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *pr if(xbt_fifo_size(mc_stack_liveness_stateless) < MAX_DEPTH_LIVENESS){ - MC_SET_RAW_MEM; - current_snapshot = xbt_new0(s_mc_snapshot_t, 1); - MC_take_snapshot_liveness(current_snapshot, prgm); - MC_UNSET_RAW_MEM; - - set_pair_visited(a, current_pair->automaton_state, current_snapshot, search_cycle); + set_pair_visited(a, current_pair->automaton_state, search_cycle, prgm); if(current_pair->requests > 0){ @@ -487,21 +538,16 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *pr } cursor = 0; - - MC_SET_RAW_MEM; - snapshot = xbt_new0(s_mc_snapshot_t, 1); - MC_take_snapshot_liveness(snapshot, prgm); - MC_UNSET_RAW_MEM; xbt_dynar_foreach(successors, cursor, pair_succ){ - if(!visited(a, pair_succ->automaton_state, snapshot, search_cycle)){ + if(!visited(a, pair_succ->automaton_state, search_cycle, prgm)){ if(search_cycle == 1){ if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ - if(reached(a, pair_succ->automaton_state, snapshot) == 1){ + if(reached(a, pair_succ->automaton_state, prgm) == 1){ XBT_DEBUG("Next pair (depth = %d, %d interleave) already reached !", xbt_fifo_size(mc_stack_liveness_stateless) + 1, MC_state_interleave_size(pair_succ->graph_state)); @@ -518,7 +564,7 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *pr XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness_stateless) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id); - set_pair_reached(a, pair_succ->automaton_state, snapshot); + set_pair_reached(a, pair_succ->automaton_state, prgm); } @@ -530,7 +576,7 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *pr XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness_stateless) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id); - set_pair_reached(a, pair_succ->automaton_state, snapshot); + set_pair_reached(a, pair_succ->automaton_state, prgm); search_cycle = 1; @@ -604,21 +650,16 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *pr } cursor = 0; - - MC_SET_RAW_MEM; - snapshot = xbt_new0(s_mc_snapshot_t, 1); - MC_take_snapshot_liveness(snapshot, prgm); - MC_UNSET_RAW_MEM; xbt_dynar_foreach(successors, cursor, pair_succ){ - if(!visited(a, pair_succ->automaton_state, snapshot, search_cycle)){ + if(!visited(a, pair_succ->automaton_state, search_cycle, prgm)){ if(search_cycle == 1){ if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ - if(reached(a, pair_succ->automaton_state, snapshot) == 1){ + if(reached(a, pair_succ->automaton_state, prgm) == 1){ XBT_DEBUG("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness_stateless) + 1); @@ -635,7 +676,7 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *pr XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness_stateless) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id); - set_pair_reached(a, pair_succ->automaton_state, snapshot); + set_pair_reached(a, pair_succ->automaton_state, prgm); } @@ -645,7 +686,7 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *pr if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)) && (xbt_fifo_size(mc_stack_liveness_stateless) < (MAX_DEPTH_LIVENESS - 1))){ - set_pair_reached(a, pair_succ->automaton_state, snapshot); + set_pair_reached(a, pair_succ->automaton_state, prgm); search_cycle = 1; @@ -680,9 +721,9 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *pr } if(xbt_fifo_size(mc_stack_liveness_stateless) == MAX_DEPTH_LIVENESS ){ - XBT_DEBUG("Pair (graph=%p, automaton =%p, search_cycle = %u) shifted in stack, maximum depth reached", current_pair->graph_state, current_pair->automaton_state, search_cycle); + XBT_DEBUG("Pair (graph=%p, automaton =%p, search_cycle = %u, depth = %d) shifted in stack, maximum depth reached", current_pair->graph_state, current_pair->automaton_state, search_cycle, xbt_fifo_size(mc_stack_liveness_stateless) ); }else{ - XBT_DEBUG("Pair (graph=%p, automaton =%p, search_cycle = %u) shifted in stack", current_pair->graph_state, current_pair->automaton_state, search_cycle); + XBT_DEBUG("Pair (graph=%p, automaton =%p, search_cycle = %u, depth = %d) shifted in stack", current_pair->graph_state, current_pair->automaton_state, search_cycle, xbt_fifo_size(mc_stack_liveness_stateless) ); } @@ -691,9 +732,6 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *pr if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){ xbt_fifo_shift(reached_pairs); } - if(snapshot != NULL) - MC_free_snapshot(snapshot); - MC_pair_stateless_delete(current_pair); MC_UNSET_RAW_MEM; diff --git a/src/mc/memory_map.c b/src/mc/memory_map.c index 9e987f0f07..16e8e02c3a 100644 --- a/src/mc/memory_map.c +++ b/src/mc/memory_map.c @@ -18,8 +18,6 @@ memory_map_t get_memory_map(void) char *lfields[6], *tok, *endptr; int i; - char *backup_line = NULL; - /* Open the actual process's proc maps file and create the memory_map_t */ /* to be returned. */ fp = fopen("/proc/self/maps", "r"); @@ -34,9 +32,7 @@ memory_map_t get_memory_map(void) /* Read one line at the time, parse it and add it to the memory map to be returned */ while ((read = getline(&line, &n, fp)) != -1) { - //XBT_INFO("%s", line); - if(XBT_LOG_ISENABLED(mc_memory_map, xbt_log_priority_debug)) - backup_line = strdup(line); + XBT_DEBUG("%s", line); /* Wipeout the new line character */ line[read - 1] = '\0'; @@ -143,21 +139,6 @@ memory_map_t get_memory_map(void) memcpy(ret->regions + ret->mapsize, &memreg, sizeof(memreg)); ret->mapsize++; - if(XBT_LOG_ISENABLED(mc_memory_map, xbt_log_priority_debug)){ - 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); - } - } - } - } - - } if (line) diff --git a/src/mc/private.h b/src/mc/private.h index aed104f7c3..a35812ea2c 100644 --- a/src/mc/private.h +++ b/src/mc/private.h @@ -229,16 +229,16 @@ typedef struct s_mc_pair_visited{ int MC_automaton_evaluate_label(xbt_automaton_t a, xbt_exp_label_t l); mc_pair_t new_pair(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st); -int reached(xbt_automaton_t a, xbt_state_t st, mc_snapshot_t s); -void set_pair_reached(xbt_automaton_t a, xbt_state_t st, mc_snapshot_t s); +int reached(xbt_automaton_t a, xbt_state_t st, char *prgm); +void set_pair_reached(xbt_automaton_t a, xbt_state_t st, char *prgm); int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2); void MC_show_stack_liveness_stateful(xbt_fifo_t stack); void MC_dump_stack_liveness_stateful(xbt_fifo_t stack); void MC_pair_delete(mc_pair_t pair); void MC_exit_liveness(void); mc_state_t MC_state_pair_new(void); -int visited(xbt_automaton_t a, xbt_state_t st, mc_snapshot_t s, int search_cycle); -void set_pair_visited(xbt_automaton_t a, xbt_state_t st, mc_snapshot_t s, int search_cycle); +int visited(xbt_automaton_t a, xbt_state_t st, int search_cycle, char *prgm); +void set_pair_visited(xbt_automaton_t a, xbt_state_t st, int search_cycle, char *prgm); /* **** Double-DFS stateful without visited state **** */ @@ -256,6 +256,7 @@ typedef struct s_mc_pair_stateless{ }s_mc_pair_stateless_t, *mc_pair_stateless_t; extern xbt_fifo_t mc_stack_liveness_stateless; +extern mc_snapshot_t initial_snapshot_liveness; mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r); void MC_ddfs_stateless_init(xbt_automaton_t a, char *prgm); -- 2.20.1