From 4b6daec896cfa8220c801d9c7dcf2af7eedcbff0 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Tue, 5 Jul 2011 11:16:08 +0200 Subject: [PATCH] model-checker : DPOR (independant transitions) algorithm for liveness properties --- examples/msg/mc/example_automaton.c | 5 +- src/mc/mc_dpor.c | 246 ++++++++++++++++++++++++++++ src/mc/mc_global.c | 4 +- src/mc/mc_liveness.c | 2 + src/mc/private.h | 8 +- 5 files changed, 260 insertions(+), 5 deletions(-) diff --git a/examples/msg/mc/example_automaton.c b/examples/msg/mc/example_automaton.c index a5094ada88..62fc3cfa55 100644 --- a/examples/msg/mc/example_automaton.c +++ b/examples/msg/mc/example_automaton.c @@ -16,7 +16,7 @@ extern xbt_automaton_t automaton; int p=1; int r=0; int q=1; -int e=0; +int e=1; int d=1; @@ -55,8 +55,7 @@ int server(int argc, char *argv[]) } MSG_task_receive(&task, "mymailbox"); count++; - //e=(e+1)%2; - //d=(d+1)%2; + //r=(r+1)%2; //XBT_INFO("r (server) = %d", r); } diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c index 9378ddd1a6..267e61098a 100644 --- a/src/mc/mc_dpor.c +++ b/src/mc/mc_dpor.c @@ -342,3 +342,249 @@ void MC_dpor_with_restore_snapshot(){ return; } + + +/************ DPOR 2 (invisible and independant transitions) ************/ + + +void MC_dpor2_init(xbt_automaton_t a) +{ + mc_pair_t initial_pair = NULL; + mc_state_t initial_graph_state = NULL; + mc_snapshot_t initial_system_state = NULL; + xbt_state_t initial_automaton_state = NULL; + smx_process_t process; + + + MC_SET_RAW_MEM; + initial_graph_state = MC_state_new(); + MC_UNSET_RAW_MEM; + + /* Wait for requests (schedules processes) */ + MC_wait_for_requests(); + + MC_SET_RAW_MEM; + xbt_swag_foreach(process, simix_global->process_list){ + if(MC_process_is_enabled(process)){ + MC_state_interleave_process(initial_graph_state, process); + break; + } + } + MC_UNSET_RAW_MEM; + + unsigned int cursor = 0; + unsigned int cursor2 = 0; + xbt_state_t automaton_state = NULL; + int res; + xbt_transition_t transition_succ; + + xbt_dynar_foreach(a->states, cursor, automaton_state){ + if(automaton_state->type == -1){ + xbt_dynar_foreach(automaton_state->out, cursor2, transition_succ){ + res = MC_automaton_evaluate_label(a, transition_succ->label); + if((res == 1) || (res == 2)){ + initial_automaton_state = transition_succ->dst; + break; + } + } + } + + if(xbt_fifo_size(mc_snapshot_stack) > 0) + break; + } + + if(xbt_fifo_size(mc_snapshot_stack) == 0){ + cursor = 0; + xbt_dynar_foreach(a->states, cursor, automaton_state){ + if(automaton_state->type == -1){ + initial_automaton_state = automaton_state; + break; + } + } + } + + MC_SET_RAW_MEM; + initial_system_state = xbt_new0(s_mc_snapshot_t, 1); + MC_take_snapshot(initial_system_state); + initial_pair = new_pair(initial_system_state, initial_graph_state, initial_automaton_state); + xbt_fifo_unshift(mc_snapshot_stack, initial_pair); + MC_UNSET_RAW_MEM; + + XBT_DEBUG("**************************************************"); + XBT_DEBUG("Initial pair"); + + MC_dpor2(a, 0); + +} + + +void MC_dpor2(xbt_automaton_t a, int search_cycle) +{ + char *req_str; + int value; + smx_req_t req = NULL, prev_req = NULL; + mc_state_t next_graph_state = NULL; + mc_snapshot_t next_system_state = NULL; + xbt_state_t next_automaton_state = NULL; + xbt_transition_t transition_succ; + unsigned int cursor; + int res; + mc_pair_t pair = NULL, next_pair = NULL, prev_pair = NULL; + smx_process_t process = NULL; + xbt_fifo_item_t item = NULL; + + while (xbt_fifo_size(mc_snapshot_stack) > 0) { + + /* Get current pair */ + pair = (mc_pair_t) + xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack)); + + XBT_DEBUG("**************************************************"); + XBT_DEBUG("Exploration depth=%d (pair=%p)(%u interleave)", + xbt_fifo_size(mc_snapshot_stack), pair, + MC_state_interleave_size(pair->graph_state)); + + /* Update statistics */ + mc_stats_pair->visited_pairs++; + + /* Test acceptance pair and acceptance cycle*/ + + if(pair->automaton_state->type == 1){ + if(search_cycle == 0){ + set_pair_reached(pair); + XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair->graph_state, pair->automaton_state, pair->automaton_state->id); + }else{ + if(reached(pair) == 1){ + XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); + XBT_INFO("| ACCEPTANCE CYCLE |"); + XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); + XBT_INFO("Counter-example that violates formula :"); + MC_show_snapshot_stack(mc_snapshot_stack); + MC_dump_snapshot_stack(mc_snapshot_stack); + MC_print_statistics_pairs(mc_stats_pair); + exit(0); + } + } + } + + /* If there are processes to interleave and the maximum depth has not been reached + then perform one step of the exploration algorithm */ + if (xbt_fifo_size(mc_snapshot_stack) < MAX_DEPTH && + (req = MC_state_get_request(pair->graph_state, &value))) { + + /* Debug information */ + if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){ + req_str = MC_request_to_string(req, value); + XBT_DEBUG("Execute: %s", req_str); + xbt_free(req_str); + } + + MC_state_set_executed_request(pair->graph_state, req, value); + //mc_stats_pairs->executed_transitions++; + + /* Answer the request */ + SIMIX_request_pre(req, value); /* After this call req is no longer usefull */ + + /* Wait for requests (schedules processes) */ + MC_wait_for_requests(); + + /* Create the new expanded state */ + MC_SET_RAW_MEM; + next_graph_state = MC_state_new(); + + /* Get an enabled process and insert it in the interleave set of the next state */ + xbt_swag_foreach(process, simix_global->process_list){ + if(MC_process_is_enabled(process)){ + MC_state_interleave_process(next_graph_state, process); + break; + } + } + + next_system_state = xbt_new0(s_mc_snapshot_t, 1); + MC_take_snapshot(next_system_state); + MC_UNSET_RAW_MEM; + + cursor = 0; + xbt_dynar_foreach(pair->automaton_state->out, cursor, transition_succ){ + res = MC_automaton_evaluate_label(a, transition_succ->label); + if((res == 1) || (res == 2)){ // enabled transition in automaton + next_automaton_state = transition_succ->dst; + break; + } + } + + if(next_automaton_state == NULL){ + next_automaton_state = pair->automaton_state; + } + + MC_SET_RAW_MEM; + next_pair = new_pair(next_system_state, next_graph_state, next_automaton_state); + xbt_fifo_unshift(mc_snapshot_stack, next_pair); + MC_UNSET_RAW_MEM; + + /* Let's loop again */ + + /* The interleave set is empty or the maximum depth is reached, let's back-track */ + } else { + XBT_DEBUG("There are no more processes to interleave."); + + /* Trash the current state, no longer needed */ + MC_SET_RAW_MEM; + xbt_fifo_shift(mc_snapshot_stack); + //MC_state_delete(state); + MC_UNSET_RAW_MEM; + + /* Check for deadlocks */ + if(MC_deadlock_check()){ + MC_show_deadlock(NULL); + return; + } + + MC_SET_RAW_MEM; + /* Traverse the stack backwards until a state with a non empty interleave + set is found, deleting all the states that have it empty in the way. + For each deleted state, check if the request that has generated it + (from it's predecesor state), depends on any other previous request + executed before it. If it does then add it to the interleave set of the + state that executed that previous request. */ + while ((pair = xbt_fifo_shift(mc_snapshot_stack)) != NULL) { + req = MC_state_get_internal_request(pair->graph_state); + xbt_fifo_foreach(mc_snapshot_stack, item, prev_pair, mc_pair_t) { + if(MC_request_depend(req, MC_state_get_internal_request(prev_pair->graph_state))){ + if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){ + XBT_DEBUG("Dependent Transitions:"); + prev_req = MC_state_get_executed_request(prev_pair->graph_state, &value); + req_str = MC_request_to_string(prev_req, value); + XBT_DEBUG("%s (pair=%p)", req_str, prev_pair); + xbt_free(req_str); + prev_req = MC_state_get_executed_request(pair->graph_state, &value); + req_str = MC_request_to_string(prev_req, value); + XBT_DEBUG("%s (pair=%p)", req_str, pair); + xbt_free(req_str); + } + + if(!MC_state_process_is_done(prev_pair->graph_state, req->issuer)) + MC_state_interleave_process(prev_pair->graph_state, req->issuer); + else + XBT_DEBUG("Process %p is in done set", req->issuer); + + break; + } + } + if (MC_state_interleave_size(pair->graph_state)) { + /* We found a back-tracking point, let's loop */ + MC_restore_snapshot(pair->system_state); + xbt_fifo_unshift(mc_snapshot_stack, pair); + XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_snapshot_stack)); + MC_UNSET_RAW_MEM; + break; + } else { + //MC_state_delete(state); + } + } + MC_UNSET_RAW_MEM; + } + } + MC_UNSET_RAW_MEM; + return; +} diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index 492d9e488d..839c96b135 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -67,6 +67,7 @@ void MC_init_with_automaton(xbt_automaton_t a){ /* Initialize statistics */ mc_stats_pair = xbt_new0(s_mc_stats_pair_t, 1); + mc_stats = xbt_new0(s_mc_stats_t, 1); //mc_stats_pair->pair_size = 1; XBT_DEBUG("Creating snapshot_stack"); @@ -77,7 +78,8 @@ void MC_init_with_automaton(xbt_automaton_t a){ MC_UNSET_RAW_MEM; //MC_vddfs_with_restore_snapshot_init(a); - MC_ddfs_with_restore_snapshot_init(a); + //MC_ddfs_with_restore_snapshot_init(a); + MC_dpor2_init(a); } diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c index f28b56fd1d..9b92e214cb 100644 --- a/src/mc/mc_liveness.c +++ b/src/mc/mc_liveness.c @@ -455,6 +455,7 @@ void MC_vddfs_with_restore_snapshot(xbt_automaton_t a, int search_cycle, int res /********************* Double-DFS without visited state *******************/ + void MC_ddfs_with_restore_snapshot_init(xbt_automaton_t a){ XBT_DEBUG("**************************************************"); @@ -720,3 +721,4 @@ void MC_ddfs_with_restore_snapshot(xbt_automaton_t a, int search_cycle, int rest MC_UNSET_RAW_MEM; } + diff --git a/src/mc/private.h b/src/mc/private.h index 02c10df817..fc931b6335 100644 --- a/src/mc/private.h +++ b/src/mc/private.h @@ -220,7 +220,7 @@ void set_pair_visited(mc_pair_t p, int search_cycle); int visited(mc_pair_t p, int search_cycle); -/* **** DPOR with restore snapshot **** */ +/* **** DPOR Cristian with restore snapshot **** */ typedef struct s_mc_state_with_snapshot{ mc_snapshot_t system_state; @@ -231,4 +231,10 @@ mc_state_ws_t new_state_ws(mc_snapshot_t s, mc_state_t gs); void MC_dpor_with_restore_snapshot_init(void); void MC_dpor_with_restore_snapshot(void); +/* **** DPOR 2 (invisible and independant transitions) **** */ + + +void MC_dpor2_init(xbt_automaton_t a); +void MC_dpor2(xbt_automaton_t a, int search_cycle); + #endif -- 2.20.1