Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
05677d22bf9e221b1b3c5163be1112a9dde60223
[simgrid.git] / src / mc / mc_dpor.c
1 /* Copyright (c) 2008 Martin Quinson, Cristian Rosa.
2    All rights reserved.                                          */
3
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. */
6
7 #include "private.h"
8
9 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dpor, mc,
10                                 "Logging specific to MC DPOR exploration");
11
12 /**
13  *  \brief Initialize the DPOR exploration algorithm
14  */
15 void MC_dpor_init()
16 {
17   mc_state_t initial_state = NULL;
18   mc_transition_t trans, trans_tmp = NULL;
19   xbt_setset_cursor_t cursor = NULL;
20   
21   /* Create the initial state and push it into the exploration stack */
22   MC_SET_RAW_MEM;
23   initial_state = MC_state_new();
24   xbt_fifo_unshift(mc_stack, initial_state);
25   MC_UNSET_RAW_MEM;
26
27   /* Schedule all the processes to detect the transitions of the initial state */
28   DEBUG0("**************************************************"); 
29   DEBUG0("Initial state");
30
31   while(xbt_swag_size(simix_global->process_to_run)){
32     MC_schedule_enabled_processes();
33     MC_execute_surf_actions();
34   }
35
36   MC_SET_RAW_MEM;
37   MC_trans_compute_enabled(initial_state->enabled_transitions,
38                            initial_state->transitions);
39
40   /* Fill the interleave set of the initial state with an enabled process */
41   trans = xbt_setset_set_choose(initial_state->enabled_transitions);  
42   if(trans){
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);    
47     }
48   }
49   MC_UNSET_RAW_MEM;
50
51   /* Update Statistics */
52   mc_stats->state_size += xbt_setset_set_size(initial_state->enabled_transitions);
53 }
54
55
56 /**
57  *      \brief Perform the model-checking operation using a depth-first search exploration
58  *         with Dynamic Partial Order Reductions
59  */
60 void MC_dpor(void)
61 {
62   mc_transition_t trans, trans_tmp = NULL;  
63   mc_state_t next_state = NULL;
64   xbt_setset_cursor_t cursor = NULL;
65   
66   while(xbt_fifo_size(mc_stack) > 0){
67   
68     DEBUG0("**************************************************");
69
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). */
72
73     /* Get current state */
74     mc_current_state = (mc_state_t) xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
75    
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){
79
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));
83       
84       /* Update statistics */
85       mc_stats->visited_states++;
86       mc_stats->executed_transitions++;
87       
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
90          exploration stack. */
91       MC_SET_RAW_MEM;
92       trans = xbt_setset_set_extract(mc_current_state->interleave);
93
94       /* Add the transition in the done set of the current state */
95       xbt_setset_set_insert(mc_current_state->done, trans);
96       
97       next_state = MC_state_new();
98       xbt_fifo_unshift(mc_stack, next_state);
99       
100       /* Set it as the executed transition of the current state */
101       mc_current_state->executed_transition = trans;
102       MC_UNSET_RAW_MEM;
103
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
106          of the transition */
107       DEBUG1("Executing transition %s", trans->name);
108       SIMIX_process_schedule(trans->process);
109       MC_execute_surf_actions();
110       
111       while(xbt_swag_size(simix_global->process_to_run)){
112         MC_schedule_enabled_processes();
113         MC_execute_surf_actions();
114       }
115       
116       /* Calculate the enabled transitions set of the next state */
117       MC_SET_RAW_MEM;
118
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);
122         }
123       }
124       
125       MC_trans_compute_enabled(next_state->enabled_transitions, next_state->transitions);
126       
127       /* Choose one transition to interleave from the enabled transition set */      
128       trans = xbt_setset_set_choose(next_state->enabled_transitions);
129       if(trans){
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);    
134         }
135       }
136       MC_UNSET_RAW_MEM;
137
138       /* Update Statistics */
139       mc_stats->state_size += xbt_setset_set_size(next_state->enabled_transitions);
140
141       /* Let's loop again */
142       
143     /* The interleave set is empty or the maximum depth is reached, let's back-track */
144     }else{
145       DEBUG0("There are no more transitions to interleave.");
146
147   
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           INFO1("%s", trans->name);
157         }
158
159         INFO0("Counter-example execution trace:");
160         MC_dump_stack(mc_stack);
161         
162         MC_print_statistics(mc_stats);
163         xbt_abort();
164       }
165               
166       mc_transition_t q = NULL;
167       xbt_fifo_item_t item = NULL;
168       mc_state_t state = NULL;
169
170       /*
171       INFO0("*********************************");
172       MC_show_stack(mc_stack);*/
173       
174       /* Trash the current state, no longer needed */
175       MC_SET_RAW_MEM;
176       xbt_fifo_shift(mc_stack);
177       MC_state_delete(mc_current_state);
178       
179       /* Traverse the stack backwards until a state with a non empty interleave
180          set is found, deleting all the states that have it empty in the way.
181          For each deleted state, check if the transition that has generated it 
182          (from it's predecesor state), depends on any other previous transition 
183          executed before it. If it does then add it to the interleave set of the
184          state that executed that previous transition. */
185       while((mc_current_state = xbt_fifo_shift(mc_stack)) != NULL){
186         q = mc_current_state->executed_transition;
187         xbt_fifo_foreach(mc_stack, item, state, mc_state_t){
188           if(MC_transition_depend(q, state->executed_transition)){
189             xbt_setset_foreach(state->enabled_transitions, cursor, trans){
190               if((trans->process == q->process) && !xbt_setset_set_belongs(state->done, trans)){
191                 DEBUG3("%s depend with %s at %p", q->name, 
192                        state->executed_transition->name, state);
193
194                 xbt_setset_foreach(state->enabled_transitions, cursor, trans){
195                   if(trans->process == q->process)
196                     xbt_setset_set_insert(state->interleave, trans);    
197                 }
198                 /* FIXME: hack to make it work*/
199                 trans = q;
200                 break;
201               }
202             }
203             if(trans)
204               break;
205           }
206         }
207         if(xbt_setset_set_size(mc_current_state->interleave) > 0){
208           /* We found a back-tracking point, let's loop */
209           xbt_fifo_unshift(mc_stack, mc_current_state);
210           DEBUG1("Back-tracking to depth %d", xbt_fifo_size(mc_stack));
211           MC_replay(mc_stack);
212           MC_UNSET_RAW_MEM;
213           break;
214         }else{
215           MC_state_delete(mc_current_state);
216         }        
217       }
218     }
219   }
220   DEBUG0("We are done");
221   /* We are done, show the statistics and return */
222   MC_print_statistics(mc_stats);
223 }