From d344049c320eee19a74e2fe4e1be14986207d83b Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Tue, 4 Oct 2011 09:52:30 +0200 Subject: [PATCH] model-checker : add type in s_mc_mem_region (0=std_heap, 1=libsimgrid) --- src/mc/mc_checkpoint.c | 21 ++++++++++++------- src/mc/mc_liveness.c | 39 +++++++++++++++++++++-------------- src/mc/memory_map.c | 21 ++++++++++++++++++- src/mc/private.h | 46 +++++++++++++++++++++++------------------- 4 files changed, 83 insertions(+), 44 deletions(-) diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c index dc85a3b5d3..a2bb87b08f 100644 --- a/src/mc/mc_checkpoint.c +++ b/src/mc/mc_checkpoint.c @@ -1,15 +1,20 @@ #include #include "private.h" -static mc_mem_region_t MC_region_new(void *start_addr, size_t size); + +XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_checkpoint, mc, + "Logging specific to mc_checkpoint"); + +static mc_mem_region_t MC_region_new(int type, void *start_addr, size_t size); static void MC_region_restore(mc_mem_region_t reg); static void MC_region_destroy(mc_mem_region_t reg); -static void MC_snapshot_add_region(mc_snapshot_t snapshot, void *start_addr, size_t size); +static void MC_snapshot_add_region(mc_snapshot_t snapshot, int type, void *start_addr, size_t size); -static mc_mem_region_t MC_region_new(void *start_addr, size_t size) +static mc_mem_region_t MC_region_new(int type, void *start_addr, size_t size) { mc_mem_region_t new_reg = xbt_new0(s_mc_mem_region_t, 1); + new_reg->type = type; new_reg->start_addr = start_addr; new_reg->size = size; new_reg->data = xbt_malloc0(size); @@ -30,9 +35,9 @@ static void MC_region_destroy(mc_mem_region_t reg) xbt_free(reg); } -static void MC_snapshot_add_region(mc_snapshot_t snapshot, void *start_addr, size_t size) +static void MC_snapshot_add_region(mc_snapshot_t snapshot, int type, void *start_addr, size_t size) { - mc_mem_region_t new_reg = MC_region_new(start_addr, size); + 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; snapshot->num_reg++; @@ -45,17 +50,19 @@ void MC_take_snapshot(mc_snapshot_t snapshot) s_map_region reg; memory_map_t maps = get_memory_map(); + XBT_DEBUG("Take snapshot"); + /* Save the std heap and the writable mapped pages of libsimgrid */ while (i < maps->mapsize) { reg = maps->regions[i]; if ((reg.prot & PROT_WRITE)){ if (maps->regions[i].pathname == NULL){ if (reg.start_addr == std_heap){ // only save the std heap (and not the raw one) - MC_snapshot_add_region(snapshot, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr); + MC_snapshot_add_region(snapshot, 0, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr); } } else { if (!memcmp(basename(maps->regions[i].pathname), "libsimgrid", 10)){ - MC_snapshot_add_region(snapshot, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr); + MC_snapshot_add_region(snapshot, 1, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr); } } } diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c index 74086a1842..c3773745d8 100644 --- a/src/mc/mc_liveness.c +++ b/src/mc/mc_liveness.c @@ -26,15 +26,22 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){ int i; for(i=0 ; i< s1->num_reg ; i++){ - + if(s1->regions[i]->size != s2->regions[i]->size) return 1; - + if(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("(%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; + } } @@ -42,7 +49,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){ } -int reached(xbt_automaton_t a){ +int reached(xbt_automaton_t a, mc_snapshot_t s){ if(xbt_dynar_is_empty(reached_pairs)){ return 0; @@ -53,8 +60,7 @@ int reached(xbt_automaton_t a){ pair = xbt_new0(s_mc_pair_reached_t, 1); pair->automaton_state = a->current_state; pair->prop_ato = xbt_dynar_new(sizeof(int), NULL); - pair->system_state = xbt_new0(s_mc_snapshot_t, 1); - MC_take_snapshot(pair->system_state); + pair->system_state = s; /* Get values of propositional symbols */ unsigned int cursor = 0; @@ -85,9 +91,9 @@ int reached(xbt_automaton_t a){ } } -int set_pair_reached(xbt_automaton_t a){ +int set_pair_reached(xbt_automaton_t a, mc_snapshot_t s){ - if(reached(a) == 0){ + if(reached(a, s) == 0){ MC_SET_RAW_MEM; @@ -95,8 +101,7 @@ int set_pair_reached(xbt_automaton_t a){ pair = xbt_new0(s_mc_pair_reached_t, 1); pair->automaton_state = a->current_state; pair->prop_ato = xbt_dynar_new(sizeof(int), NULL); - pair->system_state = xbt_new0(s_mc_snapshot_t, 1); - MC_take_snapshot(pair->system_state); + pair->system_state = s; /* Get values of propositional symbols */ unsigned int cursor = 0; @@ -381,7 +386,7 @@ void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){ //XBT_DEBUG("Search visited pair : graph=%p, automaton=%p", pair_succ->graph_state, pair_succ->automaton_state); - if((search_cycle == 1) && (reached(a) == 1)){ + if((search_cycle == 1) && (reached(a, next_snapshot) == 1)){ XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); XBT_INFO("| ACCEPTANCE CYCLE |"); XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); @@ -403,7 +408,7 @@ void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){ if((search_cycle == 0) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){ - int res = set_pair_reached(a); + 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; @@ -567,6 +572,7 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){ mc_pair_stateless_t next_pair = NULL; mc_pair_stateless_t pair_succ; + mc_snapshot_t next_snapshot = NULL; xbt_dynar_t successors = NULL; @@ -606,6 +612,9 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){ MC_state_interleave_process(next_graph_state, process); } } + + next_snapshot = xbt_new0(s_mc_snapshot_t, 1); + MC_take_snapshot(next_snapshot); xbt_dynar_reset(successors); @@ -653,7 +662,7 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){ xbt_dynar_foreach(successors, cursor, pair_succ){ - if((search_cycle == 1) && (reached(a) == 1)){ + if((search_cycle == 1) && (reached(a, next_snapshot) == 1)){ XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); XBT_INFO("| ACCEPTANCE CYCLE |"); XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); @@ -674,7 +683,7 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){ 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); + int res = set_pair_reached(a, next_snapshot); MC_SET_RAW_MEM; xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ); diff --git a/src/mc/memory_map.c b/src/mc/memory_map.c index d1f279e1dd..fa496896d2 100644 --- a/src/mc/memory_map.c +++ b/src/mc/memory_map.c @@ -18,6 +18,8 @@ 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"); @@ -32,7 +34,9 @@ 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_DEBUG("%s", line); + //XBT_INFO("%s", line); + if(XBT_LOG_ISENABLED(mc_memory_map, xbt_log_priority_debug)) + backup_line = strdup(line); /* Wipeout the new line character */ line[read - 1] = '\0'; @@ -138,6 +142,21 @@ memory_map_t get_memory_map(void) xbt_realloc(ret->regions, sizeof(memreg) * (ret->mapsize + 1)); memcpy(ret->regions + ret->mapsize, &memreg, sizeof(memreg)); 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 (line) diff --git a/src/mc/private.h b/src/mc/private.h index 3ea8ad98f9..839f1ae69e 100644 --- a/src/mc/private.h +++ b/src/mc/private.h @@ -24,6 +24,7 @@ /****************************** Snapshots ***********************************/ typedef struct s_mc_mem_region{ + int type; void *start_addr; void *data; size_t size; @@ -180,6 +181,28 @@ typedef struct s_memory_map { memory_map_t get_memory_map(void); +/********************************** DPOR for safety (stateless) **************************************/ +void MC_dpor_init(void); +void MC_dpor(void); +void MC_dpor_exit(void); + +/***** DPOR for safety (stateful) **** */ + +typedef struct s_mc_state_with_snapshot{ + mc_snapshot_t system_state; + mc_state_t graph_state; +}s_mc_state_ws_t, *mc_state_ws_t; + +extern xbt_fifo_t mc_stack_safety_stateful; + +void MC_init_stateful(void); +void MC_modelcheck_stateful(void); +mc_state_ws_t new_state_ws(mc_snapshot_t s, mc_state_t gs); +void MC_dpor_stateful_init(void); +void MC_dpor_stateful(void); +void MC_exit_stateful(void); + + /********************************** Double-DFS for liveness property**************************************/ typedef struct s_mc_pair{ @@ -199,8 +222,8 @@ extern xbt_fifo_t mc_stack_liveness_stateful; 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); -int set_pair_reached(xbt_automaton_t a); +int reached(xbt_automaton_t a, mc_snapshot_t s); +int set_pair_reached(xbt_automaton_t a, mc_snapshot_t s); 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); @@ -229,25 +252,6 @@ void MC_show_stack_liveness_stateless(xbt_fifo_t stack); void MC_dump_stack_liveness_stateless(xbt_fifo_t stack); void MC_pair_stateless_delete(mc_pair_stateless_t pair); -/********************************** DPOR for safety (stateless) **************************************/ -void MC_dpor_init(void); -void MC_dpor(void); -void MC_dpor_exit(void); - -/***** DPOR for safety (stateful) **** */ - -typedef struct s_mc_state_with_snapshot{ - mc_snapshot_t system_state; - mc_state_t graph_state; -}s_mc_state_ws_t, *mc_state_ws_t; - -extern xbt_fifo_t mc_stack_safety_stateful; -void MC_init_stateful(void); -void MC_modelcheck_stateful(void); -mc_state_ws_t new_state_ws(mc_snapshot_t s, mc_state_t gs); -void MC_dpor_stateful_init(void); -void MC_dpor_stateful(void); -void MC_exit_stateful(void); #endif -- 2.20.1