X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/efbda81c4d794ef571a347d2f9e1fc22529929f8..626ed5e4e88f6a33ba9482881820080b0caa8afa:/src/mc/mc_global.c diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index 9fa095a3e3..da3f134a0c 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -14,22 +14,21 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc, /* MC global data structures */ mc_snapshot_t initial_snapshot = NULL; xbt_fifo_t mc_stack = NULL; -xbt_setset_t mc_setset = NULL; mc_stats_t mc_stats = NULL; mc_state_t mc_current_state = NULL; char mc_replay_mode = FALSE; - +double *mc_time = NULL; /** * \brief Initialize the model-checker data structures */ void MC_init(void) { - smx_process_t process; - /* 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; @@ -41,14 +40,6 @@ void MC_init(void) /* Create exploration stack */ mc_stack = xbt_fifo_new(); - /* Create the container for the sets */ - mc_setset = xbt_setset_new(20); - - /* Add the existing processes to mc's setset so they have an ID designated */ - /* FIXME: check what happen if there are processes created during the exploration */ - xbt_swag_foreach(process, simix_global->process_list){ - xbt_setset_elm_add(mc_setset, process); - } MC_UNSET_RAW_MEM; MC_dpor_init(); @@ -69,6 +60,8 @@ void MC_modelcheck(void) void MC_exit(void) { + MC_print_statistics(mc_stats); + xbt_free(mc_time); MC_memory_exit(); } @@ -78,6 +71,39 @@ int MC_random(int min, int max) return 0; } +/** + * \brief Schedules all the process that are ready to run + */ +void MC_wait_for_requests(void) +{ + smx_req_t req = NULL; + + do { + SIMIX_context_runall(simix_global->process_to_run); + while((req = SIMIX_request_pop())){ + if(!MC_request_is_visible(req)) + SIMIX_request_pre(req, 0); + } + } while (xbt_dynar_length(simix_global->process_to_run)); +} + +int MC_deadlock_check() +{ + int deadlock = FALSE; + smx_process_t process; + if(xbt_swag_size(simix_global->process_list)){ + deadlock = TRUE; + xbt_swag_foreach(process, simix_global->process_list){ + if(process->request.call != REQ_NO_REQ + && MC_request_is_enabled(&process->request)){ + deadlock = FALSE; + break; + } + } + } + return deadlock; +} + /** * \brief Re-executes from the initial state all the transitions indicated by * a given model-checker stack. @@ -85,6 +111,7 @@ int MC_random(int min, int max) */ void MC_replay(xbt_fifo_t stack) { + int value; char *req_str; smx_req_t req = NULL, saved_req = NULL; xbt_fifo_item_t item; @@ -104,7 +131,7 @@ void MC_replay(xbt_fifo_t stack) item = xbt_fifo_get_prev_item(item)) { state = (mc_state_t) xbt_fifo_get_item_content(item); - saved_req = MC_state_get_executed_request(state); + saved_req = MC_state_get_executed_request(state, &value); if(saved_req){ /* because we got a copy of the executed request, we have to fetch the @@ -113,13 +140,13 @@ void MC_replay(xbt_fifo_t stack) /* Debug information */ if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){ - req_str = MC_request_to_string(req); + req_str = MC_request_to_string(req, value); DEBUG2("Replay: %s (%p)", req_str, state); xbt_free(req_str); } } - SIMIX_request_pre(req); + SIMIX_request_pre(req, value); MC_wait_for_requests(); /* Update statistics */ @@ -148,6 +175,7 @@ void MC_dump_stack(xbt_fifo_t stack) void MC_show_stack(xbt_fifo_t stack) { + int value; mc_state_t state; xbt_fifo_item_t item; smx_req_t req; @@ -156,40 +184,29 @@ void MC_show_stack(xbt_fifo_t stack) for (item = xbt_fifo_get_last_item(stack); (item ? (state = (mc_state_t) (xbt_fifo_get_item_content(item))) : (NULL)); item = xbt_fifo_get_prev_item(item)) { - req = MC_state_get_executed_request(state); + req = MC_state_get_executed_request(state, &value); if(req){ - req_str = MC_request_to_string(req); + req_str = MC_request_to_string(req, value); INFO1("%s", req_str); xbt_free(req_str); } } } -/** - * \brief Schedules all the process that are ready to run - */ -void MC_wait_for_requests(void) +void MC_show_deadlock(smx_req_t req) { - char *req_str = NULL; - smx_req_t req = NULL; - - do { - SIMIX_context_runall(simix_global->process_to_run); - while((req = SIMIX_request_pop())){ - if(!SIMIX_request_is_visible(req)) - SIMIX_request_pre(req); - else if(req->call == REQ_COMM_WAITANY) - THROW_UNIMPLEMENTED; - else if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){ - req_str = MC_request_to_string(req); - DEBUG1("Got: %s", req_str); - xbt_free(req_str); - } - } - } while (xbt_dynar_length(simix_global->process_to_run)); + /*char *req_str = NULL;*/ + INFO0("**************************"); + INFO0("*** DEAD-LOCK DETECTED ***"); + INFO0("**************************"); + INFO0("Locked request:"); + /*req_str = MC_request_to_string(req); + INFO1("%s", req_str); + xbt_free(req_str);*/ + INFO0("Counter-example execution trace:"); + MC_dump_stack(mc_stack); } -/****************************** Statistics ************************************/ void MC_print_statistics(mc_stats_t stats) { INFO1("State space size ~= %lu", stats->state_size); @@ -202,7 +219,6 @@ void MC_print_statistics(mc_stats_t stats) (double)stats->expanded_states / stats->state_size); */ } -/************************* Assertion Checking *********************************/ void MC_assert(int prop) { if (MC_IS_ENABLED && !prop) { @@ -216,16 +232,15 @@ void MC_assert(int prop) } } -void MC_show_deadlock(smx_req_t req) +void MC_process_clock_add(smx_process_t process, double amount) { - char *req_str = NULL; - INFO0("**************************"); - INFO0("*** DEAD-LOCK DETECTED ***"); - INFO0("**************************"); - INFO0("Locked request:"); - req_str = MC_request_to_string(req); - INFO1("%s", req_str); - xbt_free(req_str); - INFO0("Counter-example execution trace:"); - MC_dump_stack(mc_stack); + mc_time[process->pid] += amount; +} + +double MC_process_clock_get(smx_process_t process) +{ + if(mc_time) + return mc_time[process->pid]; + else + return 0; }