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",
44 trans->process->name);
45 xbt_setset_foreach(initial_state->enabled_transitions, cursor,
47 if (trans_tmp->process == trans->process)
48 xbt_setset_set_insert(initial_state->interleave, trans_tmp);
53 /* Update Statistics */
54 mc_stats->state_size +=
55 xbt_setset_set_size(initial_state->enabled_transitions);
60 * \brief Perform the model-checking operation using a depth-first search exploration
61 * with Dynamic Partial Order Reductions
65 mc_transition_t trans, trans_tmp = NULL;
66 mc_state_t next_state = NULL;
67 xbt_setset_cursor_t cursor = NULL;
69 while (xbt_fifo_size(mc_stack) > 0) {
71 DEBUG0("**************************************************");
73 /* FIXME: Think about what happen if there are no transitions but there are
74 some actions on the models. (ex. all the processes do a sleep(0) in a round). */
76 /* Get current state */
77 mc_current_state = (mc_state_t)
78 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
80 /* If there are transitions to execute and the maximun depth has not been reached
81 then perform one step of the exploration algorithm */
82 if (xbt_setset_set_size(mc_current_state->interleave) > 0
83 && xbt_fifo_size(mc_stack) < MAX_DEPTH) {
85 DEBUG4("Exploration detph=%d (state=%p)(%d interleave) (%d enabled)",
86 xbt_fifo_size(mc_stack), mc_current_state,
87 xbt_setset_set_size(mc_current_state->interleave),
88 xbt_setset_set_size(mc_current_state->enabled_transitions));
90 /* Update statistics */
91 mc_stats->visited_states++;
92 mc_stats->executed_transitions++;
94 /* Choose a transition to execute from the interleave set of the current
95 state, and create the data structures for the new expanded state in the
98 trans = xbt_setset_set_extract(mc_current_state->interleave);
100 /* Add the transition in the done set of the current state */
101 xbt_setset_set_insert(mc_current_state->done, trans);
103 next_state = MC_state_new();
104 xbt_fifo_unshift(mc_stack, next_state);
106 /* Set it as the executed transition of the current state */
107 mc_current_state->executed_transition = trans;
110 /* Execute the selected transition by scheduling it's associated process.
111 Then schedule every process that got ready to run due to the execution
113 DEBUG1("Executing transition %s", trans->name);
114 SIMIX_process_schedule(trans->process);
115 MC_execute_surf_actions();
117 while (xbt_swag_size(simix_global->process_to_run)) {
118 MC_schedule_enabled_processes();
119 MC_execute_surf_actions();
122 /* Calculate the enabled transitions set of the next state */
125 xbt_setset_foreach(mc_current_state->transitions, cursor, trans_tmp) {
126 if (trans_tmp->process != trans->process) {
127 xbt_setset_set_insert(next_state->transitions, trans_tmp);
131 MC_trans_compute_enabled(next_state->enabled_transitions,
132 next_state->transitions);
134 /* Choose one transition to interleave from the enabled transition set */
135 trans = xbt_setset_set_choose(next_state->enabled_transitions);
137 DEBUG1("Choosing process %s for next interleave",
138 trans->process->name);
139 xbt_setset_foreach(next_state->enabled_transitions, cursor,
141 if (trans_tmp->process == trans->process)
142 xbt_setset_set_insert(next_state->interleave, trans_tmp);
147 /* Update Statistics */
148 mc_stats->state_size +=
149 xbt_setset_set_size(next_state->enabled_transitions);
151 /* Let's loop again */
153 /* The interleave set is empty or the maximum depth is reached, let's back-track */
155 DEBUG0("There are no more transitions to interleave.");
158 /* Check for deadlocks */
159 xbt_setset_substract(mc_current_state->transitions,
160 mc_current_state->done);
161 if (xbt_setset_set_size(mc_current_state->transitions) > 0) {
162 INFO0("**************************");
163 INFO0("*** DEAD-LOCK DETECTED ***");
164 INFO0("**************************");
165 INFO0("Locked transitions:");
166 xbt_setset_foreach(mc_current_state->transitions, cursor, trans) {
167 INFO3("%s [src=%p, dst=%p]", trans->name,
168 trans->wait.comm->src_proc, trans->wait.comm->dst_proc);
171 INFO0("Counter-example execution trace:");
172 MC_dump_stack(mc_stack);
174 MC_print_statistics(mc_stats);
178 mc_transition_t q = NULL;
179 xbt_fifo_item_t item = NULL;
180 mc_state_t state = NULL;
183 INFO0("*********************************");
184 MC_show_stack(mc_stack); */
186 /* Trash the current state, no longer needed */
188 xbt_fifo_shift(mc_stack);
189 MC_state_delete(mc_current_state);
191 /* Traverse the stack backwards until a state with a non empty interleave
192 set is found, deleting all the states that have it empty in the way.
193 For each deleted state, check if the transition that has generated it
194 (from it's predecesor state), depends on any other previous transition
195 executed before it. If it does then add it to the interleave set of the
196 state that executed that previous transition. */
197 while ((mc_current_state = xbt_fifo_shift(mc_stack)) != NULL) {
198 q = mc_current_state->executed_transition;
199 xbt_fifo_foreach(mc_stack, item, state, mc_state_t) {
200 if (MC_transition_depend(q, state->executed_transition)) {
201 xbt_setset_foreach(state->enabled_transitions, cursor, trans) {
202 if ((trans->process == q->process)
203 && !xbt_setset_set_belongs(state->done, trans)) {
204 DEBUG3("%s depend with %s at %p", q->name,
205 state->executed_transition->name, state);
207 xbt_setset_foreach(state->enabled_transitions, cursor,
209 if (trans->process == q->process)
210 xbt_setset_set_insert(state->interleave, trans);
212 /* FIXME: hack to make it work */
221 if (xbt_setset_set_size(mc_current_state->interleave) > 0) {
222 /* We found a back-tracking point, let's loop */
223 xbt_fifo_unshift(mc_stack, mc_current_state);
224 DEBUG1("Back-tracking to depth %d", xbt_fifo_size(mc_stack));
229 MC_state_delete(mc_current_state);
234 DEBUG0("We are done");
235 /* We are done, show the statistics and return */
236 MC_print_statistics(mc_stats);