MC_SET_RAW_MEM;
/* Get an enabled process and insert it in the interleave set of the initial state */
xbt_swag_foreach(process, simix_global->process_list){
- if(SIMIX_process_is_enabled(process)){
- MC_state_add_to_interleave(initial_state, process);
+ if(MC_process_is_enabled(process)){
+ MC_state_interleave_process(initial_state, process);
break;
}
}
void MC_dpor(void)
{
char *req_str;
- char value;
- smx_req_t req = NULL;
+ int value;
+ smx_req_t req = NULL, prev_req = NULL;
mc_state_t state = NULL, prev_state = NULL, next_state = NULL;
smx_process_t process = NULL;
xbt_fifo_item_t item = NULL;
/* Debug information */
if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
- req_str = MC_request_to_string(req);
- DEBUG1("Execute: %s", req_str);
+ req_str = MC_request_to_string(req, value);
+ if(req->call == REQ_COMM_WAITANY)
+ DEBUG3("Execute: %s (%u of %lu)", req_str, value, xbt_dynar_length(req->comm_waitany.comms));
+ else if(req->call == REQ_COMM_TESTANY)
+ DEBUG3("Execute: %s (%u of %lu)", req_str, value, xbt_dynar_length(req->comm_testany.comms));
+ else
+ DEBUG1("Execute: %s", req_str);
xbt_free(req_str);
}
- MC_state_set_executed_request(state, req);
+ MC_state_set_executed_request(state, req, value);
mc_stats->executed_transitions++;
/* Answer the request */
- SIMIX_request_pre(req); /* After this call req is no longer usefull */
+ SIMIX_request_pre(req, value); /* After this call req is no longer usefull */
/* Wait for requests (schedules processes) */
MC_wait_for_requests();
next_state = MC_state_new();
xbt_fifo_unshift(mc_stack, next_state);
-
/* Get an enabled process and insert it in the interleave set of the next state */
xbt_swag_foreach(process, simix_global->process_list){
- if(SIMIX_process_is_enabled(process)){
- MC_state_add_to_interleave(next_state, process);
+ if(MC_process_is_enabled(process)){
+ MC_state_interleave_process(next_state, process);
break;
}
}
} else {
DEBUG0("There are no more processes to interleave.");
+ /* Trash the current state, no longer needed */
+ MC_SET_RAW_MEM;
+ xbt_fifo_shift(mc_stack);
+ MC_state_delete(state);
+ MC_UNSET_RAW_MEM;
+
/* Check for deadlocks */
if(MC_deadlock_check()){
- MC_show_deadlock(&process->request);
+ MC_show_deadlock(NULL);
return;
}
- /* Trash the current state, no longer needed */
MC_SET_RAW_MEM;
- xbt_fifo_shift(mc_stack);
- MC_state_delete(state);
-
/* 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
executed before it. If it does then add it to the interleave set of the
state that executed that previous request. */
while ((state = xbt_fifo_shift(mc_stack)) != NULL) {
- req = MC_state_get_executed_request(state);
+ req = MC_state_get_internal_request(state);
xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
- if(MC_request_depend(req, MC_state_get_executed_request(prev_state))){
+ if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
DEBUG0("Dependent Transitions:");
- req_str = MC_request_to_string(MC_state_get_executed_request(prev_state));
+ prev_req = MC_state_get_executed_request(prev_state, &value);
+ req_str = MC_request_to_string(prev_req, value);
DEBUG2("%s (state=%p)", req_str, prev_state);
xbt_free(req_str);
- req_str = MC_request_to_string(req);
+ prev_req = MC_state_get_executed_request(state, &value);
+ req_str = MC_request_to_string(prev_req, value);
DEBUG2("%s (state=%p)", req_str, state);
xbt_free(req_str);
}
if(!MC_state_process_is_done(prev_state, req->issuer))
- MC_state_add_to_interleave(prev_state, req->issuer);
+ MC_state_interleave_process(prev_state, req->issuer);
else
DEBUG1("Process %p is in done set", req->issuer);