1 /* Copyright (c) 2008 Martin Quinson, Cristian Rosa.
2 All rights reserved. */
4 /* This program is free software; you can redistribute it and/or modify it
5 * under the terms of the license (GNU LGPL) which comes with this package. */
9 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dpor, mc,
10 "Logging specific to MC DPOR exploration");
13 * \brief Initialize the DPOR exploration algorithm
17 mc_state_t initial_state = NULL;
18 mc_transition_t trans, trans_tmp = NULL;
19 xbt_setset_cursor_t cursor = NULL;
21 /* Create the initial state and push it into the exploration stack */
23 initial_state = MC_state_new();
24 xbt_fifo_unshift(mc_stack, initial_state);
27 /* Schedule all the processes to detect the transitions of the initial state */
28 DEBUG0("**************************************************");
29 DEBUG0("Initial state");
31 while(xbt_swag_size(simix_global->process_to_run)){
32 MC_schedule_enabled_processes();
33 MC_execute_surf_actions();
37 MC_trans_compute_enabled(initial_state->enabled_transitions,
38 initial_state->transitions);
40 /* Fill the interleave set of the initial state with an enabled process */
41 trans = xbt_setset_set_choose(initial_state->enabled_transitions);
43 DEBUG1("Choosing process %s for next interleave", trans->process->name);
44 xbt_setset_foreach(initial_state->enabled_transitions, cursor, trans_tmp){
45 if(trans_tmp->process == trans->process)
46 xbt_setset_set_insert(initial_state->interleave, trans_tmp);
51 /* Update Statistics */
52 mc_stats->state_size += xbt_setset_set_size(initial_state->enabled_transitions);
57 * \brief Perform the model-checking operation using a depth-first search exploration
58 * with Dynamic Partial Order Reductions
62 mc_transition_t trans, trans_tmp = NULL;
63 mc_state_t next_state = NULL;
64 xbt_setset_cursor_t cursor = NULL;
66 while(xbt_fifo_size(mc_stack) > 0){
68 DEBUG0("**************************************************");
70 /* FIXME: Think about what happen if there are no transitions but there are
71 some actions on the models. (ex. all the processes do a sleep(0) in a round). */
73 /* Get current state */
74 mc_current_state = (mc_state_t) xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
76 /* If there are transitions to execute and the maximun depth has not been reached
77 then perform one step of the exploration algorithm */
78 if(xbt_setset_set_size(mc_current_state->interleave) > 0 && xbt_fifo_size(mc_stack) < MAX_DEPTH){
80 DEBUG4("Exploration detph=%d (state=%p)(%d interleave) (%d enabled)", xbt_fifo_size(mc_stack),
81 mc_current_state, xbt_setset_set_size(mc_current_state->interleave),
82 xbt_setset_set_size(mc_current_state->enabled_transitions));
84 /* Update statistics */
85 mc_stats->visited_states++;
86 mc_stats->executed_transitions++;
88 /* Choose a transition to execute from the interleave set of the current
89 state, and create the data structures for the new expanded state in the
92 trans = xbt_setset_set_extract(mc_current_state->interleave);
94 /* Add the transition in the done set of the current state */
95 xbt_setset_set_insert(mc_current_state->done, trans);
97 next_state = MC_state_new();
98 xbt_fifo_unshift(mc_stack, next_state);
100 /* Set it as the executed transition of the current state */
101 mc_current_state->executed_transition = trans;
104 /* Execute the selected transition by scheduling it's associated process.
105 Then schedule every process that got ready to run due to the execution
107 DEBUG1("Executing transition %s", trans->name);
108 SIMIX_process_schedule(trans->process);
109 MC_execute_surf_actions();
111 while(xbt_swag_size(simix_global->process_to_run)){
112 MC_schedule_enabled_processes();
113 MC_execute_surf_actions();
116 /* Calculate the enabled transitions set of the next state */
119 xbt_setset_foreach(mc_current_state->transitions, cursor, trans_tmp){
120 if(trans_tmp->process != trans->process){
121 xbt_setset_set_insert(next_state->transitions, trans_tmp);
125 MC_trans_compute_enabled(next_state->enabled_transitions, next_state->transitions);
127 /* Choose one transition to interleave from the enabled transition set */
128 trans = xbt_setset_set_choose(next_state->enabled_transitions);
130 DEBUG1("Choosing process %s for next interleave", trans->process->name);
131 xbt_setset_foreach(next_state->enabled_transitions, cursor, trans_tmp){
132 if(trans_tmp->process == trans->process)
133 xbt_setset_set_insert(next_state->interleave, trans_tmp);
138 /* Update Statistics */
139 mc_stats->state_size += xbt_setset_set_size(next_state->enabled_transitions);
141 /* Let's loop again */
143 /* The interleave set is empty or the maximum depth is reached, let's back-track */
145 DEBUG0("There are no more transitions to interleave.");
148 /* Check for deadlocks */
149 xbt_setset_substract(mc_current_state->transitions, mc_current_state->done);
150 if(xbt_setset_set_size(mc_current_state->transitions) > 0){
151 INFO0("**************************");
152 INFO0("*** DEAD-LOCK DETECTED ***");
153 INFO0("**************************");
154 INFO0("Locked transitions:");
155 xbt_setset_foreach(mc_current_state->transitions, cursor, trans){
156 INFO3("%s [src=%p, dst=%p]", trans->name, trans->wait.comm->src_proc,
157 trans->wait.comm->dst_proc);
160 INFO0("Counter-example execution trace:");
161 MC_dump_stack(mc_stack);
163 MC_print_statistics(mc_stats);
167 mc_transition_t q = NULL;
168 xbt_fifo_item_t item = NULL;
169 mc_state_t state = NULL;
172 INFO0("*********************************");
173 MC_show_stack(mc_stack);*/
175 /* Trash the current state, no longer needed */
177 xbt_fifo_shift(mc_stack);
178 MC_state_delete(mc_current_state);
180 /* Traverse the stack backwards until a state with a non empty interleave
181 set is found, deleting all the states that have it empty in the way.
182 For each deleted state, check if the transition that has generated it
183 (from it's predecesor state), depends on any other previous transition
184 executed before it. If it does then add it to the interleave set of the
185 state that executed that previous transition. */
186 while((mc_current_state = xbt_fifo_shift(mc_stack)) != NULL){
187 q = mc_current_state->executed_transition;
188 xbt_fifo_foreach(mc_stack, item, state, mc_state_t){
189 if(MC_transition_depend(q, state->executed_transition)){
190 xbt_setset_foreach(state->enabled_transitions, cursor, trans){
191 if((trans->process == q->process) && !xbt_setset_set_belongs(state->done, trans)){
192 DEBUG3("%s depend with %s at %p", q->name,
193 state->executed_transition->name, state);
195 xbt_setset_foreach(state->enabled_transitions, cursor, trans){
196 if(trans->process == q->process)
197 xbt_setset_set_insert(state->interleave, trans);
199 /* FIXME: hack to make it work*/
208 if(xbt_setset_set_size(mc_current_state->interleave) > 0){
209 /* We found a back-tracking point, let's loop */
210 xbt_fifo_unshift(mc_stack, mc_current_state);
211 DEBUG1("Back-tracking to depth %d", xbt_fifo_size(mc_stack));
216 MC_state_delete(mc_current_state);
221 DEBUG0("We are done");
222 /* We are done, show the statistics and return */
223 MC_print_statistics(mc_stats);