X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/c8c284176e4f5ae35bf26ad48515f4b029866ef2..79a5552c4e41de77e291df5a0a30726a83bbee48:/src/mc/mc_global.c diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index 0d4543dd6d..4614ac9c77 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -11,16 +11,19 @@ #include #include +#define UNW_LOCAL_ONLY +#include + #include "simgrid/sg_config.h" #include "../surf/surf_private.h" #include "../simix/smx_private.h" #include "../xbt/mmalloc/mmprivate.h" #include "xbt/fifo.h" #include "mc_private.h" +#include "mc_record.h" #include "xbt/automaton.h" #include "xbt/dict.h" -XBT_LOG_NEW_CATEGORY(mc, "All MC categories"); XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc, "Logging specific to MC (global)"); @@ -108,6 +111,21 @@ static void MC_init_debug_info(void) mc_model_checker_t mc_model_checker = NULL; +mc_model_checker_t MC_model_checker_new() +{ + mc_model_checker_t mc = xbt_new0(s_mc_model_checker_t, 1); + mc->pages = mc_pages_store_new(); + mc->fd_clear_refs = -1; + mc->fd_pagemap = -1; + return mc; +} + +void MC_model_checker_delete(mc_model_checker_t mc) { + mc_pages_store_delete(mc->pages); + if(mc->record) + xbt_dynar_free(&mc->record); +} + void MC_init() { int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); @@ -119,10 +137,7 @@ void MC_init() MC_SET_MC_HEAP; - mc_model_checker = xbt_new0(s_mc_model_checker_t, 1); - mc_model_checker->pages = mc_pages_store_new(); - mc_model_checker->fd_clear_refs = -1; - mc_model_checker->fd_pagemap = -1; + mc_model_checker = MC_model_checker_new(); mc_comp_times = xbt_new0(s_mc_comparison_times_t, 1); @@ -175,10 +190,7 @@ void MC_init() MC_ignore_global_variable("communications_pattern"); MC_ignore_global_variable("initial_communications_pattern"); MC_ignore_global_variable("incomplete_communications_pattern"); - - if (MC_is_active()) { - MC_ignore_global_variable("mc_diff_info"); - } + MC_ignore_global_variable("mc_diff_info"); MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double)); @@ -322,38 +334,6 @@ void MC_exit(void) //xbt_abort(); } -int SIMIX_pre_mc_random(smx_simcall_t simcall, int min, int max) -{ - - return simcall->mc_value; -} - - -int MC_random(int min, int max) -{ - /*FIXME: return mc_current_state->executed_transition->random.value; */ - return simcall_mc_random(min, max); -} - -/** - * \brief Schedules all the process that are ready to run - */ -void MC_wait_for_requests(void) -{ - smx_process_t process; - smx_simcall_t req; - unsigned int iter; - - 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->simcall; - if (req->call != SIMCALL_NONE && !MC_request_is_visible(req)) - SIMIX_simcall_enter(req, 0); - } - } -} - int MC_deadlock_check() { int deadlock = FALSE; @@ -380,11 +360,11 @@ void mc_update_comm_pattern(mc_call_type call_type, smx_simcall_t req, int value break; case MC_CALL_TYPE_WAIT: { - smx_action_t current_comm = NULL; + smx_synchro_t current_comm = NULL; if (call_type == MC_CALL_TYPE_WAIT) current_comm = simcall_comm_wait__get__comm(req); else - current_comm = xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value, smx_action_t); + current_comm = xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value, smx_synchro_t); // First wait only must be considered: if (current_comm->comm.refcount == 1) complete_comm_pattern(pattern, current_comm); @@ -400,6 +380,13 @@ void mc_update_comm_pattern(mc_call_type call_type, smx_simcall_t req, int value * a given model-checker stack. * \param stack The stack with the transitions to execute. * \param start Start index to begin the re-execution. + * + * If start==-1, restore the initial state and replay the actions the + * the transitions in the stack. + * + * Otherwise, we only replay a part of the transitions of the stacks + * without restoring the state: it is assumed that the current state + * match with the transitions to execute. */ void MC_replay(xbt_fifo_t stack, int start) { @@ -455,7 +442,6 @@ void MC_replay(xbt_fifo_t stack, int start) MC_SET_STD_HEAP; - /* Traverse the stack from the state at position start and re-execute the transitions */ for (item = start_item; item != xbt_fifo_get_first_item(stack); @@ -491,7 +477,7 @@ void MC_replay(xbt_fifo_t stack, int start) call = mc_get_call_type(req); } - SIMIX_simcall_enter(req, value); + SIMIX_simcall_handle(req, value); if (_sg_mc_comms_determinism || _sg_mc_send_determinism) { MC_SET_MC_HEAP; @@ -586,7 +572,7 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack) } - SIMIX_simcall_enter(req, value); + SIMIX_simcall_handle(req, value); MC_wait_for_requests(); } @@ -759,6 +745,7 @@ void MC_assert(int prop) XBT_INFO("*** PROPERTY NOT VALID ***"); XBT_INFO("**************************"); XBT_INFO("Counter-example execution trace:"); + MC_record_dump_path(mc_stack); MC_dump_stack_safety(mc_stack); MC_print_statistics(mc_stats); xbt_abort(); @@ -824,3 +811,33 @@ void MC_automaton_new_propositional_symbol(const char *id, void *fct) MC_SET_MC_HEAP; } + +void MC_dump_stacks(FILE* file) +{ + int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); + MC_SET_MC_HEAP; + + int nstack = 0; + stack_region_t current_stack; + unsigned cursor; + xbt_dynar_foreach(stacks_areas, cursor, current_stack) { + unw_context_t * context = (unw_context_t *)current_stack->context; + fprintf(file, "Stack %i:\n", nstack); + + int nframe = 0; + char buffer[100]; + unw_cursor_t c; + unw_init_local (&c, context); + unw_word_t off; + do { + const char * name = !unw_get_proc_name(&c, buffer, 100, &off) ? buffer : "?"; + fprintf(file, " %i: %s\n", nframe, name); + ++nframe; + } while(unw_step(&c)); + + ++nstack; + } + + if (raw_mem_set) + MC_SET_MC_HEAP; +}