X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/68bbe0a999c4d78d2ac27ed0b4bb325f4e6a3b03..bed0bd887ad1b2584aab20cf8b447df2e3a217aa:/src/mc/mc_global.c diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index 4e24e3c079..6c4c2b23be 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -17,7 +17,7 @@ xbt_fifo_t mc_stack = 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 */ @@ -27,6 +27,8 @@ void MC_init(void) 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; @@ -58,6 +60,7 @@ void MC_modelcheck(void) void MC_exit(void) { + xbt_free(mc_time); MC_memory_exit(); } @@ -78,7 +81,7 @@ void MC_wait_for_requests(void) do { SIMIX_context_runall(simix_global->process_to_run); while((req = SIMIX_request_pop())){ - if(!SIMIX_request_is_visible(req)) + if(!MC_request_is_visible(req)) SIMIX_request_pre(req, 0); else if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){ req_str = MC_request_to_string(req); @@ -97,7 +100,7 @@ int MC_deadlock_check() deadlock = TRUE; xbt_swag_foreach(process, simix_global->process_list){ if(process->request.call != REQ_NO_REQ - && SIMIX_request_is_enabled(&process->request)){ + && MC_request_is_enabled(&process->request)){ deadlock = FALSE; break; } @@ -113,7 +116,7 @@ int MC_deadlock_check() */ void MC_replay(xbt_fifo_t stack) { - unsigned int value; + int value; char *req_str; smx_req_t req = NULL, saved_req = NULL; xbt_fifo_item_t item; @@ -177,7 +180,7 @@ void MC_dump_stack(xbt_fifo_t stack) void MC_show_stack(xbt_fifo_t stack) { - unsigned int value; + int value; mc_state_t state; xbt_fifo_item_t item; smx_req_t req; @@ -234,3 +237,15 @@ void MC_assert(int prop) } } +void MC_process_clock_add(smx_process_t process, double amount) +{ + 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; +}