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)){
+ if(MC_process_is_enabled(process)){
MC_state_interleave_process(initial_state, process);
break;
}
void MC_dpor(void)
{
char *req_str;
- unsigned int 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);
- DEBUG2("Execute: %s (%u)", req_str, value);
+ 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);
}
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)){
+ 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, &value);
+ 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, &value))){
+ 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, &value));
+ 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);
}