X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/525f475f139a3cb313bf7eff204db8a4e38e6ed5..edde8f7fbc1b74a81551bf9eb7bac1935b999296:/src/mc/mc_global.c diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index 556fa707fb..128e06d118 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; /** @@ -116,13 +117,12 @@ void MC_init_liveness_stateful(xbt_automaton_t a){ MC_UNSET_RAW_MEM; - MC_vddfs_stateful_init(a); //MC_ddfs_stateful_init(a); //MC_dpor2_init(a); //MC_dpor3_init(a); } -void MC_init_liveness_stateless(xbt_automaton_t a){ +void MC_init_liveness_stateless(xbt_automaton_t a, char *prgm){ XBT_DEBUG("Start init mc"); @@ -143,7 +143,7 @@ void MC_init_liveness_stateless(xbt_automaton_t a){ MC_UNSET_RAW_MEM; - MC_ddfs_stateless_init(a); + MC_ddfs_stateless_init(a, prgm); } @@ -168,16 +168,17 @@ void MC_modelcheck_liveness_stateful(xbt_automaton_t a){ MC_exit_liveness(); } -void MC_modelcheck_liveness_stateless(xbt_automaton_t a){ - MC_init_liveness_stateless(a); +void MC_modelcheck_liveness_stateless(xbt_automaton_t a, char *prgm){ + MC_init_liveness_stateless(a, prgm); MC_exit_liveness(); } void MC_exit_liveness(void) { MC_print_statistics_pairs(mc_stats_pair); - xbt_free(mc_time); - MC_memory_exit(); + //xbt_free(mc_time); + //MC_memory_exit(); + exit(0); } @@ -204,7 +205,7 @@ void MC_wait_for_requests(void) smx_req_t req; unsigned int iter; - while (xbt_dynar_length(simix_global->process_to_run)) { + while (!xbt_dynar_is_empty(simix_global->process_to_run)) { SIMIX_process_runall(); xbt_dynar_foreach(simix_global->process_that_ran, iter, process) { req = &process->request; @@ -283,7 +284,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; @@ -291,45 +292,98 @@ void MC_replay_liveness(xbt_fifo_t stack) xbt_fifo_item_t item; mc_state_t state; mc_pair_stateless_t pair; + int depth = 1; 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; - /* 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; - saved_req = MC_state_get_executed_request(state, &value); - //XBT_DEBUG("SavedReq->call %u", saved_req->call); + item = xbt_fifo_get_last_item(stack); + + 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){ - 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); + 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(); + } - /* Debug information */ - if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){ - req_str = MC_request_to_string(req, value); - XBT_DEBUG("Replay: %s (%p)", req_str, state); - xbt_free(req_str); + depth++; + + /* Update statistics */ + mc_stats_pair->visited_pairs++; + + item = xbt_fifo_get_prev_item(item); + } + + }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++; } - - SIMIX_request_pre(req, value); - MC_wait_for_requests(); - - /* Update statistics */ - mc_stats_pair->visited_pairs++; - } + } + XBT_DEBUG("**** End Replay ****"); } @@ -473,9 +527,13 @@ void MC_show_stack_liveness_stateless(xbt_fifo_t stack){ : (NULL)); item = xbt_fifo_get_prev_item(item)) { req = MC_state_get_executed_request(pair->graph_state, &value); if(req){ - req_str = MC_request_to_string(req, value); - XBT_INFO("%s", req_str); - xbt_free(req_str); + if(pair->requests>0){ + req_str = MC_request_to_string(req, value); + XBT_INFO("%s", req_str); + xbt_free(req_str); + }else{ + XBT_INFO("End of system requests but evolution in Büchi automaton"); + } } } }