Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
ebb68bdd94b61dd33a6c30000df8dd895c90f952
[simgrid.git] / src / mc / mc_dpor.c
1 /* Copyright (c) 2008-2012. Da SimGrid Team. All rights reserved.           */
2
3 /* This program is free software; you can redistribute it and/or modify it
4  * under the terms of the license (GNU LGPL) which comes with this package. */
5
6 #include "mc_private.h"
7
8 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dpor, mc,
9                                 "Logging specific to MC DPOR exploration");
10
11 /**
12  *  \brief Initialize the DPOR exploration algorithm
13  */
14 void MC_dpor_init()
15 {
16   mc_state_t initial_state = NULL;
17   smx_process_t process;
18   
19   /* Create the initial state and push it into the exploration stack */
20   MC_SET_RAW_MEM;
21   initial_state = MC_state_new();
22   xbt_fifo_unshift(mc_stack_safety_stateless, initial_state);
23   MC_UNSET_RAW_MEM;
24
25   XBT_DEBUG("**************************************************");
26   XBT_DEBUG("Initial state");
27
28   /* Wait for requests (schedules processes) */
29   MC_wait_for_requests();
30
31   MC_SET_RAW_MEM;
32   /* Get an enabled process and insert it in the interleave set of the initial state */
33   xbt_swag_foreach(process, simix_global->process_list){
34     if(MC_process_is_enabled(process)){
35       MC_state_interleave_process(initial_state, process);
36       break;
37     }
38   }
39   MC_UNSET_RAW_MEM;
40     
41   /* FIXME: Update Statistics 
42   mc_stats->state_size +=
43       xbt_setset_set_size(initial_state->enabled_transitions); */
44 }
45
46
47 /**
48  *      \brief Perform the model-checking operation using a depth-first search exploration
49  *         with Dynamic Partial Order Reductions
50  */
51 void MC_dpor(void)
52 {
53   char *req_str;
54   int value;
55   smx_simcall_t req = NULL, prev_req = NULL;
56   mc_state_t state = NULL, prev_state = NULL, next_state = NULL;
57   smx_process_t process = NULL;
58   xbt_fifo_item_t item = NULL;
59
60   while (xbt_fifo_size(mc_stack_safety_stateless) > 0) {
61
62     /* Get current state */
63     state = (mc_state_t) 
64       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety_stateless));
65
66     XBT_DEBUG("**************************************************");
67     XBT_DEBUG("Exploration depth=%d (state=%p)(%u interleave)",
68            xbt_fifo_size(mc_stack_safety_stateless), state,
69            MC_state_interleave_size(state));
70
71     /* Update statistics */
72     mc_stats->visited_states++;
73
74     /* If there are processes to interleave and the maximum depth has not been reached
75        then perform one step of the exploration algorithm */
76     if (xbt_fifo_size(mc_stack_safety_stateless) < MAX_DEPTH &&
77         (req = MC_state_get_request(state, &value))) {
78
79       /* Debug information */
80       if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
81         req_str = MC_request_to_string(req, value);
82         XBT_DEBUG("Execute: %s", req_str);
83         xbt_free(req_str);
84       }
85
86       MC_state_set_executed_request(state, req, value);
87       mc_stats->executed_transitions++;
88
89       /* Answer the request */
90       SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
91
92       /* Wait for requests (schedules processes) */
93       MC_wait_for_requests();
94
95       /* Create the new expanded state */
96       MC_SET_RAW_MEM;
97       next_state = MC_state_new();
98       xbt_fifo_unshift(mc_stack_safety_stateless, next_state);
99
100       /* Get an enabled process and insert it in the interleave set of the next state */
101       xbt_swag_foreach(process, simix_global->process_list){
102         if(MC_process_is_enabled(process)){
103           MC_state_interleave_process(next_state, process);
104           break;
105         }
106       }
107       MC_UNSET_RAW_MEM;
108
109       /* FIXME: Update Statistics
110       mc_stats->state_size +=
111           xbt_setset_set_size(next_state->enabled_transitions);*/
112
113       /* Let's loop again */
114
115       /* The interleave set is empty or the maximum depth is reached, let's back-track */
116     } else {
117       XBT_DEBUG("There are no more processes to interleave.");
118
119       /* Trash the current state, no longer needed */
120       MC_SET_RAW_MEM;
121       xbt_fifo_shift(mc_stack_safety_stateless);
122       MC_state_delete(state);
123       MC_UNSET_RAW_MEM;
124
125       /* Check for deadlocks */
126       if(MC_deadlock_check()){
127         MC_show_deadlock(NULL);
128         return;
129       }
130
131       MC_SET_RAW_MEM;
132       /* Traverse the stack backwards until a state with a non empty interleave
133          set is found, deleting all the states that have it empty in the way.
134          For each deleted state, check if the request that has generated it 
135          (from it's predecesor state), depends on any other previous request 
136          executed before it. If it does then add it to the interleave set of the
137          state that executed that previous request. */
138       while ((state = xbt_fifo_shift(mc_stack_safety_stateless)) != NULL) {
139         req = MC_state_get_internal_request(state);
140         xbt_fifo_foreach(mc_stack_safety_stateless, item, prev_state, mc_state_t) {
141           if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
142             if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
143               XBT_DEBUG("Dependent Transitions:");
144               prev_req = MC_state_get_executed_request(prev_state, &value);
145               req_str = MC_request_to_string(prev_req, value);
146               XBT_DEBUG("%s (state=%p)", req_str, prev_state);
147               xbt_free(req_str);
148               prev_req = MC_state_get_executed_request(state, &value);
149               req_str = MC_request_to_string(prev_req, value);
150               XBT_DEBUG("%s (state=%p)", req_str, state);
151               xbt_free(req_str);              
152             }
153
154             if(!MC_state_process_is_done(prev_state, req->issuer))
155               MC_state_interleave_process(prev_state, req->issuer);
156             else
157               XBT_DEBUG("Process %p is in done set", req->issuer);
158
159             break;
160           }
161         }
162         if (MC_state_interleave_size(state)) {
163           /* We found a back-tracking point, let's loop */
164           xbt_fifo_unshift(mc_stack_safety_stateless, state);
165           XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety_stateless));
166           MC_UNSET_RAW_MEM;
167           MC_replay(mc_stack_safety_stateless);
168           break;
169         } else {
170           MC_state_delete(state);
171         }
172       }
173       MC_UNSET_RAW_MEM;
174     }
175   }
176   MC_UNSET_RAW_MEM;
177   return;
178 }
179
180
181 /********************* DPOR stateful *********************/
182
183 mc_state_ws_t new_state_ws(mc_snapshot_t s, mc_state_t gs){
184   mc_state_ws_t sws = NULL;
185   sws = xbt_new0(s_mc_state_ws_t, 1);
186   sws->system_state = s;
187   sws->graph_state = gs;
188   return sws;
189 }
190
191 void MC_dpor_stateful_init(){
192
193   XBT_DEBUG("**************************************************");
194   XBT_DEBUG("DPOR (stateful) init");
195   XBT_DEBUG("**************************************************");
196
197   mc_state_t initial_graph_state;
198   smx_process_t process; 
199   mc_snapshot_t initial_system_snapshot;
200   mc_state_ws_t initial_state ;
201   
202   MC_wait_for_requests();
203
204   MC_SET_RAW_MEM;
205
206   initial_system_snapshot = xbt_new0(s_mc_snapshot_t, 1);
207
208   initial_graph_state = MC_state_new();
209   xbt_swag_foreach(process, simix_global->process_list){
210     if(MC_process_is_enabled(process)){
211       MC_state_interleave_process(initial_graph_state, process);
212       break;
213     }
214   }
215
216   MC_take_snapshot(initial_system_snapshot);
217
218   initial_state = new_state_ws(initial_system_snapshot, initial_graph_state);
219   xbt_fifo_unshift(mc_stack_safety_stateful, initial_state);
220
221   MC_UNSET_RAW_MEM;
222
223 }
224
225 void MC_dpor_stateful(){
226
227   smx_process_t process = NULL;
228   
229   if(xbt_fifo_size(mc_stack_safety_stateful) == 0)
230     return;
231
232   int value;
233   mc_state_t next_graph_state = NULL;
234   smx_simcall_t req = NULL, prev_req = NULL;
235   char *req_str;
236   xbt_fifo_item_t item = NULL;
237
238   mc_snapshot_t next_snapshot;
239   mc_state_ws_t current_state;
240   mc_state_ws_t prev_state;
241   mc_state_ws_t next_state;
242  
243   while(xbt_fifo_size(mc_stack_safety_stateful) > 0){
244
245     current_state = (mc_state_ws_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety_stateful));
246
247     
248     XBT_DEBUG("**************************************************");
249     XBT_DEBUG("Depth : %d, State : %p , %u interleave", xbt_fifo_size(mc_stack_safety_stateful),current_state, MC_state_interleave_size(current_state->graph_state));
250
251     mc_stats->visited_states++;
252     if(mc_stats->expanded_states>1100)
253       exit(0);
254     //sleep(1);
255
256     if((xbt_fifo_size(mc_stack_safety_stateful) < MAX_DEPTH) && (req = MC_state_get_request(current_state->graph_state, &value))){
257
258       /* Debug information */
259       if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
260         req_str = MC_request_to_string(req, value);
261         //XBT_INFO("Visited states = %lu",mc_stats->visited_states );
262         XBT_DEBUG("Execute: %s",req_str);
263         xbt_free(req_str);
264       }
265
266       MC_state_set_executed_request(current_state->graph_state, req, value);
267       mc_stats->executed_transitions++;
268       
269       /* Answer the request */
270       SIMIX_simcall_pre(req, value);
271       
272       /* Wait for requests (schedules processes) */
273       MC_wait_for_requests();
274       
275       /* Create the new expanded graph_state */
276       MC_SET_RAW_MEM;
277       
278       next_graph_state = MC_state_new();
279       
280       /* Get an enabled process and insert it in the interleave set of the next graph_state */
281       xbt_swag_foreach(process, simix_global->process_list){
282         if(MC_process_is_enabled(process)){
283           MC_state_interleave_process(next_graph_state, process);
284           break;
285         }
286       }
287
288       next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
289       MC_take_snapshot(next_snapshot);
290
291       next_state = new_state_ws(next_snapshot, next_graph_state);
292       xbt_fifo_unshift(mc_stack_safety_stateful, next_state);
293       
294       MC_UNSET_RAW_MEM;
295
296     }else{
297       XBT_DEBUG("There are no more processes to interleave.");
298       
299       /* Trash the current state, no longer needed */
300       MC_SET_RAW_MEM;
301       xbt_fifo_shift(mc_stack_safety_stateful);
302       MC_UNSET_RAW_MEM;
303
304       /* Check for deadlocks */
305       if(MC_deadlock_check()){
306         MC_show_deadlock_stateful(NULL);
307         return;
308       }
309
310       MC_SET_RAW_MEM;
311       while((current_state = xbt_fifo_shift(mc_stack_safety_stateful)) != NULL){
312         req = MC_state_get_internal_request(current_state->graph_state);
313         xbt_fifo_foreach(mc_stack_safety_stateful, item, prev_state, mc_state_ws_t) {
314           if(MC_request_depend(req, MC_state_get_internal_request(prev_state->graph_state))){
315             if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
316               XBT_DEBUG("Dependent Transitions:");
317               prev_req = MC_state_get_executed_request(prev_state->graph_state, &value);
318               req_str = MC_request_to_string(prev_req, value);
319               XBT_DEBUG("%s (state=%p)", req_str, prev_state->graph_state);
320               xbt_free(req_str);
321               prev_req = MC_state_get_executed_request(current_state->graph_state, &value);
322               req_str = MC_request_to_string(prev_req, value);
323               XBT_DEBUG("%s (state=%p)", req_str, current_state->graph_state);
324               xbt_free(req_str);              
325             }
326
327             if(!MC_state_process_is_done(prev_state->graph_state, req->issuer)){
328               MC_state_interleave_process(prev_state->graph_state, req->issuer);
329               
330             } else {
331               XBT_DEBUG("Process %p is in done set", req->issuer);
332             }
333
334             break;
335           }
336         }
337
338         if(MC_state_interleave_size(current_state->graph_state)){
339           MC_restore_snapshot(current_state->system_state);
340           xbt_fifo_unshift(mc_stack_safety_stateful, current_state);
341           XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety_stateful));
342           MC_UNSET_RAW_MEM;
343           break;
344         }
345       }
346
347       MC_UNSET_RAW_MEM;
348
349     } 
350   }
351   MC_UNSET_RAW_MEM;
352   return;
353 }
354
355
356