void MC_dpor_init()
{
mc_state_t initial_state = NULL;
- mc_transition_t trans = NULL;
+ mc_transition_t trans, trans_tmp = NULL;
xbt_setset_cursor_t cursor = NULL;
/* Create the initial state and push it into the exploration stack */
/* Schedule all the processes to detect the transitions of the initial state */
DEBUG0("**************************************************");
DEBUG0("Initial state");
- MC_schedule_enabled_processes();
- MC_SET_RAW_MEM;
- xbt_setset_add(initial_state->enabled_transitions, initial_state->transitions);
- xbt_setset_foreach(initial_state->enabled_transitions, cursor, trans){
- if(trans->type == mc_wait
- && (trans->comm->src_proc == NULL || trans->comm->dst_proc == NULL)){
- xbt_setset_set_remove(initial_state->enabled_transitions, trans);
- }
+ while(xbt_swag_size(simix_global->process_to_run)){
+ MC_schedule_enabled_processes();
+ MC_execute_surf_actions();
}
+ MC_SET_RAW_MEM;
+ MC_trans_compute_enabled(initial_state->enabled_transitions,
+ initial_state->transitions);
+
/* Fill the interleave set of the initial state with an enabled process */
trans = xbt_setset_set_choose(initial_state->enabled_transitions);
- if(trans)
- xbt_setset_set_insert(initial_state->interleave, trans);
+ if(trans){
+ DEBUG1("Choosing process %s for next interleave", trans->process->name);
+ xbt_setset_foreach(initial_state->enabled_transitions, cursor, trans_tmp){
+ if(trans_tmp->process == trans->process)
+ xbt_setset_set_insert(initial_state->interleave, trans_tmp);
+ }
+ }
MC_UNSET_RAW_MEM;
/* Update Statistics */
*/
void MC_dpor(void)
{
- mc_transition_t trans = NULL;
+ mc_transition_t trans, trans_tmp = NULL;
mc_state_t next_state = NULL;
xbt_setset_cursor_t cursor = NULL;
DEBUG4("Exploration detph=%d (state=%p)(%d interleave) (%d enabled)", xbt_fifo_size(mc_stack),
mc_current_state, xbt_setset_set_size(mc_current_state->interleave),
xbt_setset_set_size(mc_current_state->enabled_transitions));
-
- xbt_setset_foreach(mc_current_state->enabled_transitions, cursor, trans){
- DEBUG1("\t %s", trans->name);
- }
/* Update statistics */
mc_stats->visited_states++;
state, and create the data structures for the new expanded state in the
exploration stack. */
MC_SET_RAW_MEM;
- trans = xbt_setset_set_choose(mc_current_state->interleave);
- if(!trans->type == mc_random){
- xbt_setset_set_remove(mc_current_state->interleave, trans);
- /* Add the transition in the done set of the current state */
- xbt_setset_set_insert(mc_current_state->done, trans);
- }
+ trans = xbt_setset_set_extract(mc_current_state->interleave);
+
+ /* Add the transition in the done set of the current state */
+ xbt_setset_set_insert(mc_current_state->done, trans);
next_state = MC_state_new();
xbt_fifo_unshift(mc_stack, next_state);
of the transition */
DEBUG1("Executing transition %s", trans->name);
SIMIX_process_schedule(trans->process);
- MC_execute_surf_actions(); /* Do surf's related black magic */
- MC_schedule_enabled_processes();
-
- if(trans->type == mc_random && trans->current_value < trans->max ){
- trans->current_value++;
- }else{
- trans->current_value = trans->min;
- xbt_setset_set_remove(mc_current_state->interleave, trans);
- xbt_setset_set_insert(mc_current_state->done, trans);
+ MC_execute_surf_actions();
+
+ while(xbt_swag_size(simix_global->process_to_run)){
+ MC_schedule_enabled_processes();
+ MC_execute_surf_actions();
}
- /* Calculate the enabled transitions set of the next state:
- -add the transition sets of the current state and the next state
- -remove the executed transition from that set
- -remove all the transitions that are disabled (mc_wait only)
- -use the resulting set as the enabled transitions of the next state */
+ /* Calculate the enabled transitions set of the next state */
MC_SET_RAW_MEM;
- xbt_setset_add(next_state->transitions, mc_current_state->transitions);
- xbt_setset_set_remove(next_state->transitions, trans);
- xbt_setset_add(next_state->enabled_transitions, next_state->transitions);
- xbt_setset_foreach(next_state->enabled_transitions, cursor, trans){
- if(trans->type == mc_wait
- && (trans->comm->src_proc == NULL || trans->comm->dst_proc == NULL)){
- xbt_setset_set_remove(next_state->enabled_transitions, trans);
+
+ xbt_setset_foreach(mc_current_state->transitions, cursor, trans_tmp){
+ if(trans_tmp->process != trans->process){
+ xbt_setset_set_insert(next_state->transitions, trans_tmp);
}
}
-
+
+ MC_trans_compute_enabled(next_state->enabled_transitions, next_state->transitions);
+
/* Choose one transition to interleave from the enabled transition set */
trans = xbt_setset_set_choose(next_state->enabled_transitions);
- if(trans)
- xbt_setset_set_insert(next_state->interleave, trans);
+ if(trans){
+ DEBUG1("Choosing process %s for next interleave", trans->process->name);
+ xbt_setset_foreach(next_state->enabled_transitions, cursor, trans_tmp){
+ if(trans_tmp->process == trans->process)
+ xbt_setset_set_insert(next_state->interleave, trans_tmp);
+ }
+ }
MC_UNSET_RAW_MEM;
/* Update Statistics */
/* The interleave set is empty or the maximum depth is reached, let's back-track */
}else{
DEBUG0("There are no more transitions to interleave.");
-
+
+
+ /* Check for deadlocks */
+ xbt_setset_substract(mc_current_state->transitions, mc_current_state->done);
+ if(xbt_setset_set_size(mc_current_state->transitions) > 0){
+ INFO0("**************************");
+ INFO0("*** DEAD-LOCK DETECTED ***");
+ INFO0("**************************");
+ INFO0("Locked transitions:");
+ xbt_setset_foreach(mc_current_state->transitions, cursor, trans){
+ INFO3("%s [src=%p, dst=%p]", trans->name, trans->wait.comm->src_proc,
+ trans->wait.comm->dst_proc);
+ }
+
+ INFO0("Counter-example execution trace:");
+ MC_dump_stack(mc_stack);
+
+ MC_print_statistics(mc_stats);
+ xbt_abort();
+ }
+
mc_transition_t q = NULL;
xbt_fifo_item_t item = NULL;
mc_state_t state = NULL;
-
- //MC_show_stack(mc_stack);
+
+ /*
+ INFO0("*********************************");
+ MC_show_stack(mc_stack);*/
/* Trash the current state, no longer needed */
MC_SET_RAW_MEM;
q = mc_current_state->executed_transition;
xbt_fifo_foreach(mc_stack, item, state, mc_state_t){
if(MC_transition_depend(q, state->executed_transition)){
- DEBUG3("Dependence found at state %p (%p,%p)", state, state->executed_transition, q);
xbt_setset_foreach(state->enabled_transitions, cursor, trans){
if((trans->process == q->process) && !xbt_setset_set_belongs(state->done, trans)){
- DEBUG2("Unexplored interleaving found at state %p (%p)", state, trans);
- xbt_setset_set_insert(state->interleave, trans);
+ DEBUG3("%s depend with %s at %p", q->name,
+ state->executed_transition->name, state);
+
+ xbt_setset_foreach(state->enabled_transitions, cursor, trans){
+ if(trans->process == q->process)
+ xbt_setset_set_insert(state->interleave, trans);
+ }
+ /* FIXME: hack to make it work*/
+ trans = q;
break;
}
}
