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
*/
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;
void MC_exit(void)
{
+ xbt_free(mc_time);
MC_memory_exit();
}
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;
+ 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);
DEBUG1("Got: %s", req_str);
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;
}
*/
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;
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
}
}
- SIMIX_request_pre(req);
+ SIMIX_request_pre(req, value);
MC_wait_for_requests();
/* Update statistics */
void MC_show_stack(xbt_fifo_t stack)
{
+ int value;
mc_state_t state;
xbt_fifo_item_t item;
smx_req_t req;
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);
INFO1("%s", req_str);
void MC_show_deadlock(smx_req_t req)
{
- char *req_str = NULL;
+ /*char *req_str = NULL;*/
INFO0("**************************");
INFO0("*** DEAD-LOCK DETECTED ***");
INFO0("**************************");
INFO0("Locked request:");
- req_str = MC_request_to_string(req);
+ /*req_str = MC_request_to_string(req);
INFO1("%s", req_str);
- xbt_free(req_str);
+ xbt_free(req_str);*/
INFO0("Counter-example execution trace:");
MC_dump_stack(mc_stack);
}
}
}
+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;
+}