From: Marion Guthmuller Date: Tue, 16 Aug 2011 14:01:23 +0000 (+0200) Subject: model-checker : new example bugged1 for stateful dpor X-Git-Tag: exp_20120216~133^2~77 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/30cbad5558adbe624358be3b839ae57a0b034d9e model-checker : new example bugged1 for stateful dpor --- diff --git a/examples/msg/mc/CMakeLists.txt b/examples/msg/mc/CMakeLists.txt index 4b36391890..f1daa84a49 100644 --- a/examples/msg/mc/CMakeLists.txt +++ b/examples/msg/mc/CMakeLists.txt @@ -4,6 +4,7 @@ set(EXECUTABLE_OUTPUT_PATH "${CMAKE_CURRENT_BINARY_DIR}") add_executable(centralized centralized_mutex.c) add_executable(bugged1 bugged1.c) +add_executable(bugged1_stateful bugged1_stateful.c) add_executable(bugged2 bugged2.c) add_executable(bugged3 bugged3.c) add_executable(random_test random_test.c) @@ -11,6 +12,7 @@ add_executable(example_automaton automaton.c automatonparse_promela.c example_au target_link_libraries(centralized simgrid m ) target_link_libraries(bugged1 simgrid m ) +target_link_libraries(bugged1_stateful simgrid m) target_link_libraries(bugged2 simgrid m ) target_link_libraries(bugged3 simgrid m ) target_link_libraries(random_test simgrid m ) diff --git a/examples/msg/mc/bugged1_stateful.c b/examples/msg/mc/bugged1_stateful.c new file mode 100644 index 0000000000..d76edba9ac --- /dev/null +++ b/examples/msg/mc/bugged1_stateful.c @@ -0,0 +1,65 @@ +/******************** Non-deterministic message ordering *********************/ +/* Server assumes a fixed order in the reception of messages from its clients */ +/* which is incorrect because the message ordering is non-deterministic */ +/******************************************************************************/ + +#include +#include +#define N 3 + +XBT_LOG_NEW_DEFAULT_CATEGORY(example, "this example"); + +int server(int argc, char *argv[]); +int client(int argc, char *argv[]); + +int server(int argc, char *argv[]) +{ + m_task_t task = NULL; + int count = 0; + while (count < N) { + if (task) { + MSG_task_destroy(task); + task = NULL; + } + MSG_task_receive(&task, "mymailbox"); + count++; + } + MC_assert_stateful(atoi(MSG_task_get_name(task)) == 3); + + XBT_INFO("OK"); + return 0; +} + +int client(int argc, char *argv[]) +{ + + m_task_t task = + MSG_task_create(argv[1], 0 /*comp cost */ , 10000 /*comm size */ , + NULL /*arbitrary data */ ); + + MSG_task_send(task, "mymailbox"); + + XBT_INFO("Sent!"); + return 0; +} + +int main(int argc, char *argv[]) +{ + + MSG_global_init(&argc, argv); + + MSG_create_environment("platform.xml"); + + MSG_function_register("server", server); + + MSG_function_register("client", client); + + MSG_launch_application("deploy_bugged1.xml"); + + MSG_main_stateful(); + + MSG_clean(); + + return 0; + +} diff --git a/examples/msg/mc/example_automaton.c b/examples/msg/mc/example_automaton.c index e3849e609e..62fc3cfa55 100644 --- a/examples/msg/mc/example_automaton.c +++ b/examples/msg/mc/example_automaton.c @@ -14,7 +14,7 @@ extern xbt_automaton_t automaton; int p=1; -int r=1; +int r=0; int q=1; int e=1; int d=1; diff --git a/include/mc/modelchecker.h b/include/mc/modelchecker.h index dd65adb2cb..5b1c813b77 100644 --- a/include/mc/modelchecker.h +++ b/include/mc/modelchecker.h @@ -1,5 +1,6 @@ #include "xbt.h" XBT_PUBLIC(void) MC_assert(int); +XBT_PUBLIC(void) MC_assert_stateful(int); XBT_PUBLIC(void) MC_assert_pair(int); XBT_PUBLIC(int) MC_random(int min, int max); diff --git a/include/msg/msg.h b/include/msg/msg.h index 89350f1451..77b97784fd 100644 --- a/include/msg/msg.h +++ b/include/msg/msg.h @@ -22,6 +22,7 @@ XBT_PUBLIC(void) MSG_global_init_args(int *argc, char **argv); XBT_PUBLIC(MSG_error_t) MSG_set_channel_number(int number); XBT_PUBLIC(int) MSG_get_channel_number(void); XBT_PUBLIC(MSG_error_t) MSG_main(void); +XBT_PUBLIC(MSG_error_t) MSG_main_stateful(void); XBT_PUBLIC(MSG_error_t) MSG_main_with_automaton(xbt_automaton_t a); XBT_PUBLIC(MSG_error_t) MSG_clean(void); XBT_PUBLIC(void) MSG_function_register(const char *name, diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h index 06cc3ebede..7820146d00 100644 --- a/src/include/mc/mc.h +++ b/src/include/mc/mc.h @@ -29,11 +29,14 @@ SG_BEGIN_DECL() /********************************* Global *************************************/ XBT_PUBLIC(void) MC_init(void); +XBT_PUBLIC(void) MC_init_stateful(void); XBT_PUBLIC(void) MC_init_with_automaton(xbt_automaton_t a); XBT_PUBLIC(void) MC_exit(void); XBT_PUBLIC(void) MC_assert(int); +XBT_PUBLIC(void) MC_assert_stateful(int); XBT_PUBLIC(void) MC_assert_pair(int); XBT_PUBLIC(void) MC_modelcheck(void); +XBT_PUBLIC(void) MC_modelcheck_stateful(void); XBT_PUBLIC(void) MC_modelcheck_with_automaton(xbt_automaton_t a); XBT_PUBLIC(int) MC_random(int, int); XBT_PUBLIC(void) MC_process_clock_add(smx_process_t, double); diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c index 8cf636135f..e51d986e23 100644 --- a/src/mc/mc_dpor.c +++ b/src/mc/mc_dpor.c @@ -189,10 +189,10 @@ mc_state_ws_t new_state_ws(mc_snapshot_t s, mc_state_t gs){ return sws; } -void MC_dpor_with_restore_snapshot_init(){ +void MC_dpor_stateful_init(){ XBT_DEBUG("**************************************************"); - XBT_DEBUG("DPOR (with restore snapshot) init"); + XBT_DEBUG("DPOR (stateful) init"); XBT_DEBUG("**************************************************"); mc_state_t initial_graph_state; @@ -220,12 +220,10 @@ void MC_dpor_with_restore_snapshot_init(){ xbt_fifo_unshift(mc_snapshot_stack, initial_state); MC_UNSET_RAW_MEM; - - MC_dpor_with_restore_snapshot(); } -void MC_dpor_with_restore_snapshot(){ +void MC_dpor_stateful(){ smx_process_t process = NULL; @@ -250,6 +248,8 @@ void MC_dpor_with_restore_snapshot(){ XBT_DEBUG("**************************************************"); XBT_DEBUG("Depth : %d, State : %p , %u interleave", xbt_fifo_size(mc_snapshot_stack),current_state, MC_state_interleave_size(current_state->graph_state)); + + mc_stats->visited_states++; if((xbt_fifo_size(mc_snapshot_stack) < MAX_DEPTH) && (req = MC_state_get_request(current_state->graph_state, &value))){ @@ -262,7 +262,8 @@ void MC_dpor_with_restore_snapshot(){ } MC_state_set_executed_request(current_state->graph_state, req, value); - + mc_stats->executed_transitions++; + /* Answer the request */ SIMIX_request_pre(req, value); @@ -298,6 +299,13 @@ void MC_dpor_with_restore_snapshot(){ xbt_fifo_shift(mc_snapshot_stack); MC_UNSET_RAW_MEM; + /* Check for deadlocks */ + if(MC_deadlock_check()){ + MC_show_deadlock_stateful(NULL); + return; + } + + MC_SET_RAW_MEM; while((current_state = xbt_fifo_shift(mc_snapshot_stack)) != NULL){ req = MC_state_get_internal_request(current_state->graph_state); xbt_fifo_foreach(mc_snapshot_stack, item, prev_state, mc_state_ws_t) { @@ -535,9 +543,9 @@ void MC_dpor2(xbt_automaton_t a, int search_cycle) } } - XBT_DEBUG("Enabled processes before pop : %lu", xbt_dynar_length(enabled_processes)); + //XBT_DEBUG("Enabled processes before pop : %lu", xbt_dynar_length(enabled_processes)); - XBT_DEBUG("Processes already interleaved : %d", pair->interleave); + //XBT_DEBUG("Processes already interleaved : %d", pair->interleave); if(xbt_dynar_length(enabled_processes) > 0){ for(d=0;dinterleave;d++){ @@ -545,7 +553,7 @@ void MC_dpor2(xbt_automaton_t a, int search_cycle) } } - XBT_DEBUG("Enabled processes after pop : %lu", xbt_dynar_length(enabled_processes)); + //XBT_DEBUG("Enabled processes after pop : %lu", xbt_dynar_length(enabled_processes)); if(pair->fully_expanded == 0){ if(xbt_dynar_length(enabled_processes) > 0){ @@ -719,6 +727,432 @@ void MC_dpor2(xbt_automaton_t a, int search_cycle) } + 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_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; +} + +/************ 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_snapshot_stack, 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_snapshot_stack) > 0) { + + /* Get current pair */ + pair = (mc_pair_prop_col_t) + xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack)); + + XBT_DEBUG("**************************************************"); + XBT_DEBUG("Exploration depth=%d (pair=%p) (%d interleave)", + xbt_fifo_size(mc_snapshot_stack), 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_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))) { + + 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_snapshot_stack, 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_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_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); diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index 839c96b135..aaac6e5b3a 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -54,6 +54,32 @@ void MC_init(void) MC_UNSET_RAW_MEM; } +void MC_init_stateful(void){ + + /* Check if MC is already initialized */ + if (initial_snapshot) + return; + + mc_time = xbt_new0(double, simix_process_maxpid); + + /* Initialize the data structures that must be persistent across every + iteration of the model-checker (in RAW memory) */ + MC_SET_RAW_MEM; + + /* Initialize statistics */ + mc_stats = xbt_new0(s_mc_stats_t, 1); + mc_stats->state_size = 1; + + /* Create exploration stack */ + mc_snapshot_stack = xbt_fifo_new(); + + MC_UNSET_RAW_MEM; + + MC_dpor_stateful_init(); + + +} + void MC_init_with_automaton(xbt_automaton_t a){ XBT_DEBUG("Start init mc"); @@ -75,11 +101,13 @@ void MC_init_with_automaton(xbt_automaton_t a){ /* Create exploration stack */ mc_snapshot_stack = xbt_fifo_new(); + MC_UNSET_RAW_MEM; //MC_vddfs_with_restore_snapshot_init(a); //MC_ddfs_with_restore_snapshot_init(a); MC_dpor2_init(a); + //MC_dpor3_init(a); } @@ -90,6 +118,13 @@ void MC_modelcheck(void) MC_exit(); } +void MC_modelcheck_stateful(void) +{ + MC_init_stateful(); + MC_dpor_stateful(); + MC_exit(); +} + void MC_modelcheck_with_automaton(xbt_automaton_t a){ MC_init_with_automaton(a); MC_exit_with_automaton(); @@ -109,6 +144,7 @@ void MC_exit(void) MC_memory_exit(); } + int MC_random(int min, int max) { /*FIXME: return mc_current_state->executed_transition->random.value;*/ @@ -220,6 +256,7 @@ void MC_dump_stack(xbt_fifo_t stack) MC_UNSET_RAW_MEM; } + void MC_show_stack(xbt_fifo_t stack) { int value; @@ -254,6 +291,53 @@ void MC_show_deadlock(smx_req_t req) MC_dump_stack(mc_stack); } +void MC_show_deadlock_stateful(smx_req_t req) +{ + /*char *req_str = NULL;*/ + XBT_INFO("**************************"); + XBT_INFO("*** DEAD-LOCK DETECTED ***"); + XBT_INFO("**************************"); + XBT_INFO("Locked request:"); + /*req_str = MC_request_to_string(req); + XBT_INFO("%s", req_str); + xbt_free(req_str);*/ + XBT_INFO("Counter-example execution trace:"); + MC_show_stack_stateful(mc_snapshot_stack); +} + +void MC_dump_stack_stateful(xbt_fifo_t stack) +{ + //mc_state_ws_t state; + + MC_show_stack_stateful(stack); + + /*MC_SET_RAW_MEM; + while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL) + MC_state_delete(state); + MC_UNSET_RAW_MEM;*/ +} + + +void MC_show_stack_stateful(xbt_fifo_t stack) +{ + int value; + mc_state_ws_t state; + xbt_fifo_item_t item; + smx_req_t req; + char *req_str = NULL; + + for (item = xbt_fifo_get_last_item(stack); + (item ? (state = (mc_state_ws_t) (xbt_fifo_get_item_content(item))) + : (NULL)); item = xbt_fifo_get_prev_item(item)) { + req = MC_state_get_executed_request(state->graph_state, &value); + if(req){ + req_str = MC_request_to_string(req, value); + XBT_INFO("%s", req_str); + xbt_free(req_str); + } + } +} + void MC_print_statistics(mc_stats_t stats) { XBT_INFO("State space size ~= %lu", stats->state_size); @@ -290,6 +374,19 @@ void MC_assert(int prop) } } +void MC_assert_stateful(int prop) +{ + if (MC_IS_ENABLED && !prop) { + XBT_INFO("**************************"); + XBT_INFO("*** PROPERTY NOT VALID ***"); + XBT_INFO("**************************"); + XBT_INFO("Counter-example execution trace:"); + MC_dump_stack_stateful(mc_snapshot_stack); + MC_print_statistics(mc_stats); + xbt_abort(); + } +} + void MC_assert_pair(int prop){ if (MC_IS_ENABLED && !prop) { XBT_INFO("**************************"); diff --git a/src/mc/private.h b/src/mc/private.h index d2e676cdd0..54563472b1 100644 --- a/src/mc/private.h +++ b/src/mc/private.h @@ -51,6 +51,9 @@ void MC_get_enabled_processes(); void MC_show_deadlock(smx_req_t req); void MC_show_stack(xbt_fifo_t stack); void MC_dump_stack(xbt_fifo_t stack); +void MC_show_deadlock_stateful(smx_req_t req); +void MC_show_stack_stateful(xbt_fifo_t stack); +void MC_dump_stack_stateful(xbt_fifo_t stack); /********************************* Requests ***********************************/ int MC_request_depend(smx_req_t req1, smx_req_t req2); @@ -220,16 +223,19 @@ void set_pair_visited(mc_pair_t p, int search_cycle); int visited(mc_pair_t p, int search_cycle); -/* **** DPOR Cristian with restore snapshot **** */ +/* **** DPOR Cristian 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; +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_with_restore_snapshot_init(void); -void MC_dpor_with_restore_snapshot(void); +void MC_dpor_stateful_init(void); +void MC_dpor_stateful(void); +void MC_exit_stateful(void); /* **** DPOR 2 (invisible and independant transitions) **** */ @@ -248,7 +254,6 @@ typedef struct s_mc_pair_prop{ 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); @@ -258,4 +263,40 @@ 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 diff --git a/src/msg/global.c b/src/msg/global.c index 386057b4ce..f17edf031b 100644 --- a/src/msg/global.c +++ b/src/msg/global.c @@ -153,6 +153,21 @@ MSG_error_t MSG_main(void) return MSG_OK; } +MSG_error_t MSG_main_stateful(void) +{ + /* Clean IO before the run */ + fflush(stdout); + fflush(stderr); + + if (MC_IS_ENABLED) { + MC_modelcheck_stateful(); + } + else { + SIMIX_run(); + } + return MSG_OK; +} + MSG_error_t MSG_main_with_automaton(xbt_automaton_t a) { /* Clean IO before the run */