From 7641e1b61b13d593d2eb86fc7cbcb6c8bcb89d8d Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Thu, 22 Sep 2011 18:05:17 +0200 Subject: [PATCH 1/1] model-checker : nettoyage du code --- src/mc/mc_checkpoint.c | 2 +- src/mc/mc_dpor.c | 818 ----------------------------------------- src/mc/mc_global.c | 1 - src/mc/mc_liveness.c | 335 +---------------- src/mc/private.h | 86 +---- 5 files changed, 9 insertions(+), 1233 deletions(-) diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c index f2d404ba14..dc85a3b5d3 100644 --- a/src/mc/mc_checkpoint.c +++ b/src/mc/mc_checkpoint.c @@ -50,7 +50,7 @@ void MC_take_snapshot(mc_snapshot_t snapshot) reg = maps->regions[i]; if ((reg.prot & PROT_WRITE)){ if (maps->regions[i].pathname == NULL){ - if (reg.start_addr == std_heap){ + 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); } } else { diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c index 330eb877be..3d5b514593 100644 --- a/src/mc/mc_dpor.c +++ b/src/mc/mc_dpor.c @@ -355,821 +355,3 @@ void MC_dpor_stateful(){ -/************ DPOR 2 (invisible and independant transitions) ************/ - -xbt_dynar_t reached_pairs_prop; -xbt_dynar_t visible_transitions; -xbt_dynar_t enabled_processes; - -mc_prop_ato_t new_proposition(char* id, int value){ - mc_prop_ato_t prop = NULL; - prop = xbt_new0(s_mc_prop_ato_t, 1); - prop->id = strdup(id); - prop->value = value; - return prop; -} - -mc_pair_prop_t new_pair_prop(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st){ - mc_pair_prop_t pair = NULL; - pair = xbt_new0(s_mc_pair_prop_t, 1); - pair->system_state = sn; - pair->automaton_state = st; - pair->graph_state = sg; - pair->propositions = xbt_dynar_new(sizeof(mc_prop_ato_t), NULL); - pair->fully_expanded = 0; - pair->interleave = 0; - mc_stats_pair->expanded_pairs++; - return pair; -} - -int reached_prop(mc_pair_prop_t pair){ - - char* hash_reached = malloc(sizeof(char)*160); - unsigned int c= 0; - - MC_SET_RAW_MEM; - char *hash = malloc(sizeof(char)*160); - xbt_sha((char *)&pair, hash); - xbt_dynar_foreach(reached_pairs_prop, c, hash_reached){ - if(strcmp(hash, hash_reached) == 0){ - MC_UNSET_RAW_MEM; - return 1; - } - } - - MC_UNSET_RAW_MEM; - return 0; -} - -void set_pair_prop_reached(mc_pair_prop_t pair){ - - if(reached_prop(pair) == 0){ - MC_SET_RAW_MEM; - char *hash = malloc(sizeof(char)*160) ; - xbt_sha((char *)&pair, hash); - xbt_dynar_push(reached_pairs_prop, &hash); - MC_UNSET_RAW_MEM; - } - -} - -int invisible(mc_pair_prop_t p, mc_pair_prop_t np){ - mc_prop_ato_t prop1; - mc_prop_ato_t prop2; - int i; - for(i=0;ipropositions); i++){ - prop1 = xbt_dynar_get_as(p->propositions, i, mc_prop_ato_t); - prop2 = xbt_dynar_get_as(np->propositions, i, mc_prop_ato_t); - //XBT_DEBUG("test invisible : prop 1 = %s : %d / prop 2 = %s : %d", prop1->id, prop1->value, prop2->id, prop2->value); - if(prop1->value != prop2->value) - return 0; - } - return 1; - -} - -void set_fully_expanded(mc_pair_prop_t pair){ - pair->fully_expanded = 1; -} - -void MC_dpor2_init(xbt_automaton_t a) -{ - mc_pair_prop_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; - - - MC_SET_RAW_MEM; - initial_graph_state = MC_state_new(); - MC_UNSET_RAW_MEM; - - /* Wait for requests (schedules processes) */ - MC_wait_for_requests(); - - 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(initial_automaton_state != NULL) - break; - } - - if(initial_automaton_state == NULL){ - cursor = 0; - xbt_dynar_foreach(a->states, cursor, automaton_state){ - if(automaton_state->type == -1){ - initial_automaton_state = automaton_state; - break; - } - } - } - - reached_pairs_prop = xbt_dynar_new(sizeof(char *), NULL); - visible_transitions = xbt_dynar_new(sizeof(s_smx_req_t), NULL); - enabled_processes = xbt_dynar_new(sizeof(smx_process_t), NULL); - - MC_SET_RAW_MEM; - initial_system_state = xbt_new0(s_mc_snapshot_t, 1); - MC_take_snapshot(initial_system_state); - initial_pair = new_pair_prop(initial_system_state, initial_graph_state, initial_automaton_state); - cursor = 0; - xbt_propositional_symbol_t ps; - xbt_dynar_foreach(a->propositional_symbols, cursor, ps){ - int (*f)() = ps->function; - int val = (*f)(); - mc_prop_ato_t pa = new_proposition(ps->pred, val); - xbt_dynar_push(initial_pair->propositions, &pa); - } - xbt_fifo_unshift(mc_stack_liveness_stateful, 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_prop_t pair = NULL, next_pair = NULL, prev_pair = NULL; - smx_process_t process = NULL; - xbt_fifo_item_t item = NULL; - int d; - - - while (xbt_fifo_size(mc_stack_liveness_stateful) > 0) { - - /* Get current pair */ - pair = (mc_pair_prop_t) - xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful)); - - XBT_DEBUG("**************************************************"); - XBT_DEBUG("Exploration depth=%d (pair=%p) (%d interleave)", - xbt_fifo_size(mc_stack_liveness_stateful), pair, MC_state_interleave_size(pair->graph_state)); - - if(MC_state_interleave_size(pair->graph_state) == 0){ - - xbt_dynar_reset(enabled_processes); - - MC_SET_RAW_MEM; - - xbt_swag_foreach(process, simix_global->process_list){ - if(MC_process_is_enabled(process)){ - xbt_dynar_push(enabled_processes, &process); - //XBT_DEBUG("Process : pid=%lu",process->pid); - } - } - - //XBT_DEBUG("Enabled processes before pop : %lu", xbt_dynar_length(enabled_processes)); - - //XBT_DEBUG("Processes already interleaved : %d", pair->interleave); - - if(xbt_dynar_length(enabled_processes) > 0){ - for(d=0;dinterleave;d++){ - xbt_dynar_shift(enabled_processes, NULL); - } - } - - //XBT_DEBUG("Enabled processes after pop : %lu", xbt_dynar_length(enabled_processes)); - - if(pair->fully_expanded == 0){ - if(xbt_dynar_length(enabled_processes) > 0){ - MC_state_interleave_process(pair->graph_state, xbt_dynar_get_as(enabled_processes, 0, smx_process_t)); - //XBT_DEBUG("Interleave process"); - } - } - - MC_UNSET_RAW_MEM; - - } - - - /* Update statistics */ - mc_stats_pair->visited_pairs++; - //sleep(1); - - /*cursor = 0; - mc_prop_ato_t pato; - xbt_dynar_foreach(pair->propositions, cursor, pato){ - XBT_DEBUG("%s : %d", pato->id, pato->value); - }*/ - - /* Test acceptance pair and acceptance cycle*/ - - if(pair->automaton_state->type == 1){ - if(search_cycle == 0){ - set_pair_prop_reached(pair); - XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair->graph_state, pair->automaton_state, pair->automaton_state->id); - }else{ - if(reached_prop(pair) == 1){ - XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); - XBT_INFO("| ACCEPTANCE CYCLE |"); - XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); - XBT_INFO("Counter-example that violates formula :"); - MC_show_stack_liveness_stateful(mc_stack_liveness_stateful); - MC_dump_stack_liveness_stateful(mc_stack_liveness_stateful); - 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_stack_liveness_stateful) < 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; - - pair->interleave++; - //XBT_DEBUG("Process interleaved in pair %p : %u", pair, MC_state_interleave_size(pair->graph_state)); - //xbt_dynar_pop(enabled_processes, NULL); - - next_graph_state = MC_state_new(); - - 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_prop(next_system_state, next_graph_state, next_automaton_state); - cursor = 0; - xbt_propositional_symbol_t ps; - xbt_dynar_foreach(a->propositional_symbols, cursor, ps){ - int (*f)() = ps->function; - int val = (*f)(); - mc_prop_ato_t pa = new_proposition(ps->pred, val); - xbt_dynar_push(next_pair->propositions, &pa); - //XBT_DEBUG("%s : %d", pa->id, pa->value); - } - xbt_fifo_unshift(mc_stack_liveness_stateful, next_pair); - - cursor = 0; - if((invisible(pair, next_pair) == 0) && (pair->fully_expanded == 0)){ - set_fully_expanded(pair); - if(xbt_dynar_length(enabled_processes) > 1){ // Si 1 seul process activé, déjà exécuté juste avant donc état complètement étudié - xbt_dynar_foreach(enabled_processes, cursor, process){ - MC_state_interleave_process(pair->graph_state, process); - } - } - XBT_DEBUG("Pair %p fully expanded (%u interleave)", pair, MC_state_interleave_size(pair->graph_state)); - } - - 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_stack_liveness_stateful); - //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_stack_liveness_stateful)) != NULL) { - req = MC_state_get_internal_request(pair->graph_state); - xbt_fifo_foreach(mc_stack_liveness_stateful, item, prev_pair, mc_pair_prop_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(prev_pair->fully_expanded == 0){ - if(!MC_state_process_is_done(prev_pair->graph_state, req->issuer)){ - MC_state_interleave_process(prev_pair->graph_state, req->issuer); - XBT_DEBUG("Process %p (%lu) interleaved in pair %p", req->issuer, req->issuer->pid, prev_pair); - }else{ - XBT_DEBUG("Process %p (%lu) is in done set", req->issuer, req->issuer->pid); - } - } - - break; - } - } - - - if (MC_state_interleave_size(pair->graph_state) > 0) { - /* We found a back-tracking point, let's loop */ - MC_restore_snapshot(pair->system_state); - xbt_fifo_unshift(mc_stack_liveness_stateful, pair); - XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_liveness_stateful)); - MC_UNSET_RAW_MEM; - break; - } else { - //MC_state_delete(state); - } - } - MC_UNSET_RAW_MEM; - } - } - MC_UNSET_RAW_MEM; - return; -} - -/************ DPOR 3 (invisible and independant transitions with coloration of pairs) ************/ - -int expanded; -xbt_dynar_t reached_pairs_prop_col; -xbt_dynar_t visited_pairs_prop_col; - - - -mc_pair_prop_col_t new_pair_prop_col(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st){ - - mc_pair_prop_col_t pair = NULL; - pair = xbt_new0(s_mc_pair_prop_col_t, 1); - pair->system_state = sn; - pair->automaton_state = st; - pair->graph_state = sg; - pair->propositions = xbt_dynar_new(sizeof(mc_prop_ato_t), NULL); - pair->fully_expanded = 0; - pair->interleave = 0; - pair->color=ORANGE; - mc_stats_pair->expanded_pairs++; - //XBT_DEBUG("New pair %p : automaton=%p", pair, st); - return pair; -} - -void set_expanded(mc_pair_prop_col_t pair){ - pair->expanded = expanded; -} - -int reached_prop_col(mc_pair_prop_col_t pair){ - - char* hash_reached = malloc(sizeof(char)*160); - unsigned int c= 0; - - MC_SET_RAW_MEM; - char *hash = malloc(sizeof(char)*160); - xbt_sha((char *)&pair, hash); - xbt_dynar_foreach(reached_pairs_prop_col, c, hash_reached){ - if(strcmp(hash, hash_reached) == 0){ - MC_UNSET_RAW_MEM; - return 1; - } - } - - MC_UNSET_RAW_MEM; - return 0; -} - -void set_pair_prop_col_reached(mc_pair_prop_col_t pair){ - - if(reached_prop_col(pair) == 0){ - MC_SET_RAW_MEM; - char *hash = malloc(sizeof(char)*160) ; - xbt_sha((char *)&pair, hash); - xbt_dynar_push(reached_pairs_prop_col, &hash); - MC_UNSET_RAW_MEM; - } - -} - -int invisible_col(mc_pair_prop_col_t p, mc_pair_prop_col_t np){ - mc_prop_ato_t prop1; - mc_prop_ato_t prop2; - int i; - for(i=0;ipropositions); i++){ - prop1 = xbt_dynar_get_as(p->propositions, i, mc_prop_ato_t); - prop2 = xbt_dynar_get_as(np->propositions, i, mc_prop_ato_t); - //XBT_DEBUG("test invisible : prop 1 = %s : %d / prop 2 = %s : %d", prop1->id, prop1->value, prop2->id, prop2->value); - if(prop1->value != prop2->value) - return 0; - } - return 1; - -} - -void set_fully_expanded_col(mc_pair_prop_col_t pair){ - pair->fully_expanded = 1; - pair->color = GREEN; -} - -void set_pair_prop_col_visited(mc_pair_prop_col_t pair, int sc){ - - MC_SET_RAW_MEM; - mc_visited_pair_prop_col_t p = NULL; - p = xbt_new0(s_mc_visited_pair_prop_col_t, 1); - p->pair = pair; - p->search_cycle = sc; - char *hash = malloc(sizeof(char)*160); - xbt_sha((char *)&p, hash); - xbt_dynar_push(visited_pairs_prop_col, &hash); - MC_UNSET_RAW_MEM; - -} - -int visited_pair_prop_col(mc_pair_prop_col_t pair, int sc){ - - char* hash_visited = malloc(sizeof(char)*160); - unsigned int c= 0; - - MC_SET_RAW_MEM; - mc_visited_pair_prop_col_t p = NULL; - p = xbt_new0(s_mc_visited_pair_prop_col_t, 1); - p->pair = pair; - p->search_cycle = sc; - char *hash = malloc(sizeof(char)*160); - xbt_sha((char *)&p, hash); - xbt_dynar_foreach(visited_pairs_prop_col, c, hash_visited){ - if(strcmp(hash, hash_visited) == 0){ - MC_UNSET_RAW_MEM; - return 1; - } - } - - MC_UNSET_RAW_MEM; - return 0; - -} - -void MC_dpor3_init(xbt_automaton_t a) -{ - mc_pair_prop_col_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; - - - MC_SET_RAW_MEM; - initial_graph_state = MC_state_new(); - MC_UNSET_RAW_MEM; - - /* Wait for requests (schedules processes) */ - MC_wait_for_requests(); - - 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(initial_automaton_state != NULL) - break; - } - - if(initial_automaton_state == NULL){ - cursor = 0; - xbt_dynar_foreach(a->states, cursor, automaton_state){ - if(automaton_state->type == -1){ - initial_automaton_state = automaton_state; - break; - } - } - } - - reached_pairs_prop_col = xbt_dynar_new(sizeof(char *), NULL); - visited_pairs_prop_col = xbt_dynar_new(sizeof(char *), NULL); - visible_transitions = xbt_dynar_new(sizeof(s_smx_req_t), NULL); - enabled_processes = xbt_dynar_new(sizeof(smx_process_t), NULL); - expanded = 0; - - MC_SET_RAW_MEM; - initial_system_state = xbt_new0(s_mc_snapshot_t, 1); - MC_take_snapshot(initial_system_state); - initial_pair = new_pair_prop_col(initial_system_state, initial_graph_state, initial_automaton_state); - cursor = 0; - xbt_propositional_symbol_t ps; - xbt_dynar_foreach(a->propositional_symbols, cursor, ps){ - int (*f)() = ps->function; - int val = (*f)(); - mc_prop_ato_t pa = new_proposition(ps->pred, val); - xbt_dynar_push(initial_pair->propositions, &pa); - } - xbt_fifo_unshift(mc_stack_liveness_stateful, initial_pair); - MC_UNSET_RAW_MEM; - - - XBT_DEBUG("**************************************************"); - XBT_DEBUG("Initial pair"); - - MC_dpor3(a, 0); - -} - - -void MC_dpor3(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_prop_col_t pair = NULL, next_pair = NULL, prev_pair = NULL; - smx_process_t process = NULL; - xbt_fifo_item_t item = NULL; - int d; - - - while (xbt_fifo_size(mc_stack_liveness_stateful) > 0) { - - /* Get current pair */ - pair = (mc_pair_prop_col_t) - xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful)); - - XBT_DEBUG("**************************************************"); - XBT_DEBUG("Exploration depth=%d (pair=%p) (%d interleave)", - xbt_fifo_size(mc_stack_liveness_stateful), pair, MC_state_interleave_size(pair->graph_state)); - - if(MC_state_interleave_size(pair->graph_state) == 0){ - - xbt_dynar_reset(enabled_processes); - - MC_SET_RAW_MEM; - - xbt_swag_foreach(process, simix_global->process_list){ - if(MC_process_is_enabled(process)){ - xbt_dynar_push(enabled_processes, &process); - //XBT_DEBUG("Process : pid=%lu",process->pid); - } - } - - //XBT_DEBUG("Enabled processes before pop : %lu", xbt_dynar_length(enabled_processes)); - - //XBT_DEBUG("Processes already interleaved : %d", pair->interleave); - - if(xbt_dynar_length(enabled_processes) > 0){ - for(d=0;dinterleave;d++){ - xbt_dynar_shift(enabled_processes, NULL); - } - } - - //XBT_DEBUG("Enabled processes after pop : %lu", xbt_dynar_length(enabled_processes)); - - if(pair->fully_expanded == 0){ - if(xbt_dynar_length(enabled_processes) > 0){ - MC_state_interleave_process(pair->graph_state, xbt_dynar_get_as(enabled_processes, 0, smx_process_t)); - //XBT_DEBUG("Interleave process"); - } - } - - MC_UNSET_RAW_MEM; - - } - - - /* Update statistics */ - mc_stats_pair->visited_pairs++; - //sleep(1); - - /* Test acceptance pair and acceptance cycle*/ - - if(pair->automaton_state->type == 1){ - if(search_cycle == 0){ - set_pair_prop_col_reached(pair); - XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair->graph_state, pair->automaton_state, pair->automaton_state->id); - }else{ - if(reached_prop_col(pair) == 1){ - XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); - XBT_INFO("| ACCEPTANCE CYCLE |"); - XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); - XBT_INFO("Counter-example that violates formula :"); - MC_show_stack_liveness_stateful(mc_stack_liveness_stateful); - MC_dump_stack_liveness_stateful(mc_stack_liveness_stateful); - 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_stack_liveness_stateful) < MAX_DEPTH && - (req = MC_state_get_request(pair->graph_state, &value))) { - - set_pair_prop_col_visited(pair, search_cycle); - - /* 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); - - /* 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; - - pair->interleave++; - - next_graph_state = MC_state_new(); - - 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_prop_col(next_system_state, next_graph_state, next_automaton_state); - cursor = 0; - xbt_propositional_symbol_t ps; - xbt_dynar_foreach(a->propositional_symbols, cursor, ps){ - int (*f)() = ps->function; - int val = (*f)(); - mc_prop_ato_t pa = new_proposition(ps->pred, val); - xbt_dynar_push(next_pair->propositions, &pa); - } - xbt_fifo_unshift(mc_stack_liveness_stateful, next_pair); - - cursor = 0; - if((invisible_col(pair, next_pair) == 0) && (pair->fully_expanded == 0)){ - set_fully_expanded_col(pair); - if(xbt_dynar_length(enabled_processes) > 1){ // Si 1 seul process activé, déjà exécuté juste avant donc état complètement étudié - xbt_dynar_foreach(enabled_processes, cursor, process){ - MC_state_interleave_process(pair->graph_state, process); - } - } - XBT_DEBUG("Pair %p fully expanded (%u interleave)", pair, MC_state_interleave_size(pair->graph_state)); - } - - 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_stack_liveness_stateful); - //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_stack_liveness_stateful)) != NULL) { - req = MC_state_get_internal_request(pair->graph_state); - xbt_fifo_foreach(mc_stack_liveness_stateful, item, prev_pair, mc_pair_prop_col_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(prev_pair->fully_expanded == 0){ - if(!MC_state_process_is_done(prev_pair->graph_state, req->issuer)){ - MC_state_interleave_process(prev_pair->graph_state, req->issuer); - XBT_DEBUG("Process %p (%lu) interleaved in pair %p", req->issuer, req->issuer->pid, prev_pair); - }else{ - XBT_DEBUG("Process %p (%lu) is in done set", req->issuer, req->issuer->pid); - } - } - - break; - } - } - - - if (MC_state_interleave_size(pair->graph_state) > 0) { - /* We found a back-tracking point, let's loop */ - MC_restore_snapshot(pair->system_state); - xbt_fifo_unshift(mc_stack_liveness_stateful, pair); - XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_liveness_stateful)); - 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 addfdbbcc4..7da8e4b9be 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -116,7 +116,6 @@ 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); diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c index 32e8b3b308..74086a1842 100644 --- a/src/mc/mc_liveness.c +++ b/src/mc/mc_liveness.c @@ -70,11 +70,8 @@ int reached(xbt_automaton_t a){ xbt_dynar_foreach(reached_pairs, cursor, pair_test){ if(automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){ - //XBT_DEBUG("Same automaton state"); if(xbt_dynar_compare(pair_test->prop_ato, pair->prop_ato, propositional_symbols_compare_value) == 0){ - //XBT_DEBUG("Same values of propositional symbols"); if(snapshot_compare(pair_test->system_state, pair->system_state) == 0){ - //XBT_DEBUG("Same system state"); MC_UNSET_RAW_MEM; return 1; } @@ -171,334 +168,6 @@ int MC_automaton_evaluate_label(xbt_automaton_t a, xbt_exp_label_t l){ } - -/******************************* DFS with visited state *******************************/ - -xbt_dynar_t visited_pairs; - -void set_pair_visited(mc_pair_t pair, int sc){ - - MC_SET_RAW_MEM; - mc_visited_pair_t p = NULL; - p = xbt_new0(s_mc_visited_pair_t, 1); - p->pair = pair; - p->search_cycle = sc; - char hash[41]; - xbt_sha((const char *)&p, hash); - xbt_dynar_push(visited_pairs, &hash); - MC_UNSET_RAW_MEM; - -} - -int visited(mc_pair_t pair, int sc){ - - MC_SET_RAW_MEM; - - mc_visited_pair_t p = NULL; - p = xbt_new0(s_mc_visited_pair_t, 1); - p->pair = pair; - p->search_cycle = sc; - char hash[41]; - xbt_sha((const char *)&p, hash); - if(xbt_dynar_member(visited_pairs, hash)){ - MC_UNSET_RAW_MEM; - return 1; - }else{ - MC_UNSET_RAW_MEM; - return 0; - } -} - - -void MC_vddfs_stateful_init(xbt_automaton_t a){ - - XBT_DEBUG("**************************************************"); - XBT_DEBUG("Double-DFS stateful with visited state init"); - XBT_DEBUG("**************************************************"); - - mc_pair_t mc_initial_pair; - mc_state_t initial_graph_state; - smx_process_t process; - mc_snapshot_t init_snapshot; - - MC_wait_for_requests(); - - MC_SET_RAW_MEM; - - init_snapshot = xbt_new0(s_mc_snapshot_t, 1); - - initial_graph_state = MC_state_pair_new(); - xbt_swag_foreach(process, simix_global->process_list){ - if(MC_process_is_enabled(process)){ - MC_state_interleave_process(initial_graph_state, process); - } - } - - visited_pairs = xbt_dynar_new(sizeof(char *), NULL); - reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL); - - MC_take_snapshot(init_snapshot); - - MC_UNSET_RAW_MEM; - - unsigned int cursor = 0; - xbt_state_t state = NULL; - - xbt_dynar_foreach(a->states, cursor, state){ - if(state->type == -1){ - - MC_SET_RAW_MEM; - mc_initial_pair = new_pair(init_snapshot, initial_graph_state, state); - xbt_fifo_unshift(mc_stack_liveness_stateful, mc_initial_pair); - MC_UNSET_RAW_MEM; - - if(cursor == 0){ - MC_vddfs_stateful(a, 0, 0); - }else{ - MC_restore_snapshot(init_snapshot); - MC_UNSET_RAW_MEM; - MC_vddfs_stateful(a, 0, 0); - } - }else{ - if(state->type == 2){ - - MC_SET_RAW_MEM; - mc_initial_pair = new_pair(init_snapshot, initial_graph_state, state); - xbt_fifo_unshift(mc_stack_liveness_stateful, mc_initial_pair); - MC_UNSET_RAW_MEM; - - if(cursor == 0){ - MC_vddfs_stateful(a, 1, 0); - }else{ - MC_restore_snapshot(init_snapshot); - MC_UNSET_RAW_MEM; - MC_vddfs_stateful(a, 1, 0); - } - } - } - } -} - - -void MC_vddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){ - - smx_process_t process = NULL; - - - if(xbt_fifo_size(mc_stack_liveness_stateful) == 0) - return; - - if(restore == 1){ - MC_restore_snapshot(((mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful)))->system_state); - MC_UNSET_RAW_MEM; - } - - - /* Get current state */ - mc_pair_t current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful)); - - if(restore == 1){ - xbt_swag_foreach(process, simix_global->process_list){ - if(MC_process_is_enabled(process)){ - MC_state_interleave_process(current_pair->graph_state, process); - } - } - } - - XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateful), search_cycle); - XBT_DEBUG("Pair : graph=%p, automaton=%p(%s), %u interleave", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id,MC_state_interleave_size(current_pair->graph_state)); - - a->current_state = current_pair->automaton_state; - - mc_stats_pair->visited_pairs++; - - int value; - mc_state_t next_graph_state = NULL; - smx_req_t req = NULL; - char *req_str; - - - xbt_transition_t transition_succ; - unsigned int cursor; - int res; - - xbt_dynar_t successors = NULL; - - mc_pair_t next_pair = NULL; - mc_snapshot_t next_snapshot = NULL; - mc_snapshot_t current_snapshot = NULL; - mc_pair_t pair_succ = NULL; - - MC_SET_RAW_MEM; - successors = xbt_dynar_new(sizeof(mc_pair_t), NULL); - MC_UNSET_RAW_MEM; - - - while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){ - - MC_SET_RAW_MEM; - current_snapshot = xbt_new0(s_mc_snapshot_t, 1); - MC_take_snapshot(current_snapshot); - MC_UNSET_RAW_MEM; - - - /* Debug information */ - if(XBT_LOG_ISENABLED(mc_liveness, 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(current_pair->graph_state, req, value); - - /* Answer the request */ - SIMIX_request_pre(req, value); - - /* Wait for requests (schedules processes) */ - MC_wait_for_requests(); - - - /* Create the new expanded graph_state */ - MC_SET_RAW_MEM; - - next_graph_state = MC_state_pair_new(); - - /* Get enabled process and insert it in the interleave set of the next graph_state */ - xbt_swag_foreach(process, simix_global->process_list){ - if(MC_process_is_enabled(process)){ - 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); - - MC_UNSET_RAW_MEM; - - cursor = 0; - xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){ - - res = MC_automaton_evaluate_label(a, transition_succ->label); - - if(res == 1){ - MC_SET_RAW_MEM; - next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst); - xbt_dynar_push(successors, &next_pair); - MC_UNSET_RAW_MEM; - } - } - - cursor = 0; - xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){ - - res = MC_automaton_evaluate_label(a, transition_succ->label); - - if(res == 2){ - MC_SET_RAW_MEM; - next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst); - xbt_dynar_push(successors, &next_pair); - MC_UNSET_RAW_MEM; - } - } - - - - if(xbt_dynar_length(successors) == 0){ - - MC_SET_RAW_MEM; - next_pair = new_pair(next_snapshot, next_graph_state, current_pair->automaton_state); - xbt_dynar_push(successors, &next_pair); - MC_UNSET_RAW_MEM; - - } - - - //XBT_DEBUG("Successors length %lu", xbt_dynar_length(successors)); - - cursor = 0; - - xbt_dynar_foreach(successors, cursor, pair_succ){ - - /*XBT_DEBUG("Search reached pair %p : graph=%p, automaton=%p", pair_succ, pair_succ->graph_state, pair_succ->automaton_state); - char hash[41]; - XBT_DEBUG("Const char pair %s", (const char *)&pair_succ); - xbt_sha((const char *)&pair_succ, hash); - XBT_DEBUG("Hash pair_succ %s", hash);*/ - - if((search_cycle == 1) && (reached(a) == 1)){ - XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); - XBT_INFO("| ACCEPTANCE CYCLE |"); - XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); - XBT_INFO("Counter-example that violates formula :"); - MC_show_stack_liveness_stateful(mc_stack_liveness_stateful); - MC_dump_stack_liveness_stateful(mc_stack_liveness_stateful); - MC_print_statistics_pairs(mc_stats_pair); - exit(0); - } - - XBT_DEBUG("Search visited pair %p : graph %p, automaton %p", pair_succ, pair_succ->graph_state, pair_succ->automaton_state); - - if(visited(pair_succ, search_cycle) == 0){ - - //mc_stats_pair->executed_transitions++; - set_pair_visited(pair_succ, search_cycle); - - MC_SET_RAW_MEM; - xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ); - MC_UNSET_RAW_MEM; - - MC_vddfs_stateful(a, search_cycle, 0); - - //XBT_DEBUG("Pair (graph=%p, automaton=%p) expanded", pair_succ->graph_state, pair_succ->automaton_state); - - if((search_cycle == 0) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){ - - XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id); - int res = set_pair_reached(a); - - MC_SET_RAW_MEM; - xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ); - MC_UNSET_RAW_MEM; - - MC_vddfs_stateful(a, 1, 1); - - if(res){ - MC_SET_RAW_MEM; - xbt_dynar_pop(reached_pairs, NULL); - MC_UNSET_RAW_MEM; - } - - } - - }else{ - - XBT_DEBUG("Pair already visited !"); - } - - } - - - if(MC_state_interleave_size(current_pair->graph_state) > 0){ - MC_restore_snapshot(current_snapshot); - MC_UNSET_RAW_MEM; - - } - } - - - MC_SET_RAW_MEM; - xbt_fifo_shift(mc_stack_liveness_stateful); - XBT_DEBUG("Pair (graph=%p, automaton =%p) shifted in stack", current_pair->graph_state, current_pair->automaton_state); - MC_UNSET_RAW_MEM; - - - -} - - - /********************* Double-DFS stateful without visited state *******************/ @@ -875,10 +544,10 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){ } } - /* Get current state */ + /* Get current pair */ current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateless)); - /* Update current state in automaton */ + /* Update current state in buchi automaton */ a->current_state = current_pair->automaton_state; XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateless), search_cycle); diff --git a/src/mc/private.h b/src/mc/private.h index 31fa84a6ed..3ea8ad98f9 100644 --- a/src/mc/private.h +++ b/src/mc/private.h @@ -66,10 +66,6 @@ int MC_request_is_enabled(smx_req_t req); int MC_request_is_enabled_by_idx(smx_req_t req, unsigned int idx); int MC_process_is_enabled(smx_process_t process); -/********************************** DPOR **************************************/ -void MC_dpor_init(void); -void MC_dpor(void); -void MC_dpor_exit(void); /******************************** States **************************************/ /* Possible exploration status of a process in a state */ @@ -196,7 +192,6 @@ typedef struct s_mc_pair_reached{ xbt_state_t automaton_state; xbt_dynar_t prop_ato; mc_snapshot_t system_state; - }s_mc_pair_reached_t, *mc_pair_reached_t; extern xbt_fifo_t mc_stack_liveness_stateful; @@ -218,18 +213,6 @@ mc_state_t MC_state_pair_new(void); void MC_ddfs_stateful_init(xbt_automaton_t a); void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore); -/* **** Double-DFS stateful with visited state **** */ - -typedef struct s_mc_visited_pair{ - mc_pair_t pair; - int search_cycle; -}s_mc_visited_pair_t, *mc_visited_pair_t; - -void MC_vddfs_stateful_init(xbt_automaton_t a); -void MC_vddfs_stateful(xbt_automaton_t automaton, int search_cycle, int restore); -void set_pair_visited(mc_pair_t p, int search_cycle); -int visited(mc_pair_t p, int search_cycle); - /* **** Double-DFS stateless **** */ typedef struct s_mc_pair_stateless{ @@ -246,7 +229,12 @@ 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 Cristian stateful **** */ +/********************************** 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; @@ -262,66 +250,4 @@ void MC_dpor_stateful_init(void); void MC_dpor_stateful(void); void MC_exit_stateful(void); -/* **** DPOR 2 (invisible and independant transitions) **** */ - -typedef struct s_mc_prop_ato{ - char *id; - int value; -}s_mc_prop_ato_t, *mc_prop_ato_t; - -typedef struct s_mc_pair_prop{ - mc_snapshot_t system_state; - mc_state_t graph_state; - xbt_state_t automaton_state; - int num; - xbt_dynar_t propositions; - int fully_expanded; - int interleave; -}s_mc_pair_prop_t, *mc_pair_prop_t; - -mc_prop_ato_t new_proposition(char* id, int value); -mc_pair_prop_t new_pair_prop(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st); -int reached_prop(mc_pair_prop_t pair); -void set_pair_prop_reached(mc_pair_prop_t pair); -void MC_dpor2_init(xbt_automaton_t a); -void MC_dpor2(xbt_automaton_t a, int search_cycle); -int invisible(mc_pair_prop_t p, mc_pair_prop_t np); -void set_fully_expanded(mc_pair_prop_t pair); - -/* **** DPOR 3 (invisible and independant transitions with coloration of pairs) **** */ - -typedef enum { - GREEN=0, - ORANGE, - RED -} e_mc_color_pair_t; - -typedef struct s_mc_pair_prop_col{ - mc_snapshot_t system_state; - mc_state_t graph_state; - xbt_state_t automaton_state; - int num; - xbt_dynar_t propositions; - int fully_expanded; - int interleave; - e_mc_color_pair_t color; - int expanded; -}s_mc_pair_prop_col_t, *mc_pair_prop_col_t; - -typedef struct s_mc_visited_pair_prop_col{ - mc_pair_prop_col_t pair; - int search_cycle; -}s_mc_visited_pair_prop_col_t, *mc_visited_pair_prop_col_t; - -void MC_dpor3_init(xbt_automaton_t a); -void MC_dpor3(xbt_automaton_t a, int search_cycle); -mc_pair_prop_col_t new_pair_prop_col(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st); -void set_expanded(mc_pair_prop_col_t pair); -int reached_prop_col(mc_pair_prop_col_t pair); -void set_pair_prop_col_reached(mc_pair_prop_col_t pair); -int invisible_col(mc_pair_prop_col_t p, mc_pair_prop_col_t np); -void set_fully_expanded_col(mc_pair_prop_col_t pair); -void set_pair_prop_col_visited(mc_pair_prop_col_t pair, int sc); -int visited_pair_prop_col(mc_pair_prop_col_t pair, int sc); - #endif -- 2.20.1