From 674e42f3c2fb237a6e690a939a909a32e6cebc98 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Thu, 10 Nov 2011 11:12:52 +0100 Subject: [PATCH] model-checker : MC_replay_liveness function extended to replay all pairs in stack or just a part --- src/mc/mc_global.c | 98 +++++++++++++++++++++++++---------- src/mc/mc_liveness.c | 118 +++++++++++++++++++++++-------------------- src/mc/private.h | 2 +- 3 files changed, 136 insertions(+), 82 deletions(-) diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index abc9a87da7..a1d46ebbfb 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -282,7 +282,7 @@ void MC_replay(xbt_fifo_t stack) XBT_DEBUG("**** End Replay ****"); } -void MC_replay_liveness(xbt_fifo_t stack) +void MC_replay_liveness(xbt_fifo_t stack, int all_stack) { int value; char *req_str; @@ -300,42 +300,86 @@ void MC_replay_liveness(xbt_fifo_t stack) * it will set it back again, we have to unset it to continue */ MC_UNSET_RAW_MEM; - /* Traverse the stack from the initial state and re-execute the transitions */ - for (item = xbt_fifo_get_last_item(stack); - item != xbt_fifo_get_first_item(stack); - item = xbt_fifo_get_prev_item(item)) { + if(all_stack){ - pair = (mc_pair_stateless_t) xbt_fifo_get_item_content(item); - state = (mc_state_t) pair->graph_state; + item = xbt_fifo_get_last_item(stack); - if(pair->requests > 0){ + while(depth <= xbt_fifo_size(stack)){ + + pair = (mc_pair_stateless_t) xbt_fifo_get_item_content(item); + state = (mc_state_t) pair->graph_state; + + if(pair->requests > 0){ - saved_req = MC_state_get_executed_request(state, &value); - //XBT_DEBUG("SavedReq->call %u", saved_req->call); + saved_req = MC_state_get_executed_request(state, &value); + //XBT_DEBUG("SavedReq->call %u", saved_req->call); - if(saved_req != NULL){ - /* because we got a copy of the executed request, we have to fetch the - real one, pointed by the request field of the issuer process */ - req = &saved_req->issuer->request; - //XBT_DEBUG("Req->call %u", req->call); + if(saved_req != NULL){ + /* because we got a copy of the executed request, we have to fetch the + real one, pointed by the request field of the issuer process */ + req = &saved_req->issuer->request; + //XBT_DEBUG("Req->call %u", req->call); - /* Debug information */ - if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){ - req_str = MC_request_to_string(req, value); - XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state); - xbt_free(req_str); - } + /* Debug information */ + if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){ + req_str = MC_request_to_string(req, value); + XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state); + xbt_free(req_str); + } - } + } - SIMIX_request_pre(req, value); - MC_wait_for_requests(); + SIMIX_request_pre(req, value); + MC_wait_for_requests(); + } + + depth++; + + /* Update statistics */ + mc_stats_pair->visited_pairs++; + + item = xbt_fifo_get_prev_item(item); } - depth++; + }else{ + + /* Traverse the stack from the initial state and re-execute the transitions */ + for (item = xbt_fifo_get_last_item(stack); + item != xbt_fifo_get_first_item(stack); + item = xbt_fifo_get_prev_item(item)) { + + pair = (mc_pair_stateless_t) xbt_fifo_get_item_content(item); + state = (mc_state_t) pair->graph_state; + + if(pair->requests > 0){ + + saved_req = MC_state_get_executed_request(state, &value); + //XBT_DEBUG("SavedReq->call %u", saved_req->call); + + if(saved_req != NULL){ + /* because we got a copy of the executed request, we have to fetch the + real one, pointed by the request field of the issuer process */ + req = &saved_req->issuer->request; + //XBT_DEBUG("Req->call %u", req->call); + + /* Debug information */ + if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){ + req_str = MC_request_to_string(req, value); + XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state); + xbt_free(req_str); + } + + } + + SIMIX_request_pre(req, value); + MC_wait_for_requests(); + } + + depth++; - /* Update statistics */ - mc_stats_pair->visited_pairs++; + /* Update statistics */ + mc_stats_pair->visited_pairs++; + } } XBT_DEBUG("**** End Replay ****"); diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c index 6e207a39b6..aa1c15e67e 100644 --- a/src/mc/mc_liveness.c +++ b/src/mc/mc_liveness.c @@ -17,17 +17,6 @@ mc_snapshot_t next_snapshot = NULL; mc_snapshot_t current_snapshot = NULL; -mc_pair_t new_pair(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st){ - mc_pair_t p = NULL; - p = xbt_new0(s_mc_pair_t, 1); - p->system_state = sn; - p->automaton_state = st; - p->graph_state = sg; - mc_stats_pair->expanded_pairs++; - return p; - -} - int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){ if(s1->num_reg != s2->num_reg) @@ -287,7 +276,7 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){ return; if(replay == 1){ - MC_replay_liveness(mc_stack_liveness_stateless); + MC_replay_liveness(mc_stack_liveness_stateless, 0); 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)){ @@ -322,10 +311,11 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){ mc_pair_stateless_t pair_succ; - if(MC_state_interleave_size(current_pair->graph_state) > 0){ + if(current_pair->requests > 0){ while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL && (xbt_fifo_size(mc_stack_liveness_stateless) < MAX_DEPTH_LIVENESS)){ + /* Debug information */ if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){ req_str = MC_request_to_string(req, value); @@ -398,18 +388,20 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){ MC_UNSET_RAW_MEM; } - cursor = 0; + /*MC_SET_RAW_MEM; + MC_take_snapshot(snapshot); + MC_UNSET_RAW_MEM;*/ + cursor = 0; + xbt_dynar_foreach(successors, cursor, pair_succ){ - - if((search_cycle == 1) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)) ){ - + MC_SET_RAW_MEM; MC_take_snapshot(snapshot); MC_UNSET_RAW_MEM; - + if(reached(a, pair_succ->automaton_state, snapshot) == 1){ XBT_DEBUG("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness_stateless) + 1); @@ -426,32 +418,36 @@ 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("Take snapshot of acceptance pair (depth = %d)", xbt_fifo_size(mc_stack_liveness_stateless) + 1 ); - MC_SET_RAW_MEM; - MC_take_snapshot(snapshot); - MC_UNSET_RAW_MEM; - } - MC_SET_RAW_MEM; xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ); MC_UNSET_RAW_MEM; + + if(xbt_fifo_size(mc_stack_liveness_stateless) == MAX_DEPTH_LIVENESS){ + XBT_DEBUG("Maximum depth reached"); + } MC_ddfs_stateless(a, search_cycle, 0); - if((search_cycle == 0) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){ + if((search_cycle == 0) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)) && (xbt_fifo_size(mc_stack_liveness_stateless) < (MAX_DEPTH_LIVENESS - 1))){ XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id); - - set_pair_reached(a, pair_succ->automaton_state, snapshot); - - /* Pair shifted from stack when first MC_ddfs finished and returned at this point */ MC_SET_RAW_MEM; xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ); MC_UNSET_RAW_MEM; + + /* Restore system before starting detection of acceptance cycle */ + MC_replay_liveness(mc_stack_liveness_stateless, 0); + + MC_SET_RAW_MEM; + MC_take_snapshot(snapshot); + MC_UNSET_RAW_MEM; + + set_pair_reached(a, pair_succ->automaton_state, snapshot); + + XBT_DEBUG("Detection of acceptance cycle enabled"); MC_ddfs_stateless(a, 1, 1); @@ -461,11 +457,16 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){ MC_UNSET_RAW_MEM; } + + /* Restore system before checking others successors */ + MC_replay_liveness(mc_stack_liveness_stateless, 1); + } - - XBT_DEBUG("Backtracking to depth %u", xbt_fifo_size(mc_stack_liveness_stateless)); - MC_replay_liveness(mc_stack_liveness_stateless); + if(xbt_dynar_is_empty(successors)){ + XBT_DEBUG("Backtracking to depth %u", xbt_fifo_size(mc_stack_liveness_stateless)); + MC_replay_liveness(mc_stack_liveness_stateless, 0); + } } @@ -474,14 +475,6 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){ if((xbt_fifo_size(mc_stack_liveness_stateless) < MAX_DEPTH_LIVENESS)){ - // MC_state_set_executed_request(current_pair->graph_state, NULL, value); - - /* Answer the request */ - //SIMIX_request_pre(req, value); - - /* Wait for requests (schedules processes) */ - //MC_wait_for_requests(); - MC_SET_RAW_MEM; /* Create the new expanded graph_state */ @@ -553,14 +546,6 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){ exit(0); } } - - - if((search_cycle == 0) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){ - XBT_DEBUG("Take snapshot of acceptance pair (depth = %d)", xbt_fifo_size(mc_stack_liveness_stateless) + 1 ); - MC_SET_RAW_MEM; - MC_take_snapshot(snapshot); - MC_UNSET_RAW_MEM; - } MC_SET_RAW_MEM; xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ); @@ -569,18 +554,25 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){ MC_ddfs_stateless(a, search_cycle, 0); - if((search_cycle == 0) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){ + if((search_cycle == 0) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)) && (xbt_fifo_size(mc_stack_liveness_stateless) < (MAX_DEPTH_LIVENESS - 1))){ XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id); + /* Restore system before taking snapshot of system */ + MC_replay_liveness(mc_stack_liveness_stateless, 0); + + MC_SET_RAW_MEM; + MC_take_snapshot(snapshot); + MC_UNSET_RAW_MEM; set_pair_reached(a, pair_succ->automaton_state, snapshot); - - + /* Pair shifted from stack when first MC_ddfs finished and returned at this point */ MC_SET_RAW_MEM; xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ); - MC_UNSET_RAW_MEM; + MC_UNSET_RAW_MEM; + + XBT_DEBUG("Backtracking to depth %d, detection of acceptance cycle enabled", xbt_fifo_size(mc_stack_liveness_stateless)); MC_ddfs_stateless(a, 1, 1); @@ -590,20 +582,38 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){ MC_UNSET_RAW_MEM; } + + /* Restore system before checking others successors */ + MC_replay_liveness(mc_stack_liveness_stateless, 1); + } } } MC_SET_RAW_MEM; + if(xbt_fifo_size(mc_stack_liveness_stateless) == MAX_DEPTH_LIVENESS - 1){ + 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); + }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_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 *******************/ +mc_pair_t new_pair(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st){ + mc_pair_t p = NULL; + p = xbt_new0(s_mc_pair_t, 1); + p->system_state = sn; + p->automaton_state = st; + p->graph_state = sg; + mc_stats_pair->expanded_pairs++; + return p; + +} void MC_ddfs_stateful_init(xbt_automaton_t a){ diff --git a/src/mc/private.h b/src/mc/private.h index 17400d2d63..89e78929c6 100644 --- a/src/mc/private.h +++ b/src/mc/private.h @@ -48,7 +48,7 @@ extern double *mc_time; int MC_deadlock_check(void); void MC_replay(xbt_fifo_t stack); -void MC_replay_liveness(xbt_fifo_t stack); +void MC_replay_liveness(xbt_fifo_t stack, int all_stack); void MC_wait_for_requests(void); void MC_get_enabled_processes(); void MC_show_deadlock(smx_req_t req); -- 2.20.1