Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : interleave all enabled processes for each state and apply DPOR only...
[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 xbt_dynar_t visited_states;
12
13 static int is_visited_state(void);
14
15 static int is_visited_state(){
16
17   if(_surf_mc_visited == 0)
18     return 0;
19
20   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
21
22   MC_SET_RAW_MEM;
23
24   mc_snapshot_t new_state = NULL;
25   new_state = MC_take_snapshot();  
26
27   MC_UNSET_RAW_MEM;
28   
29   if(xbt_dynar_is_empty(visited_states)){
30
31     MC_SET_RAW_MEM;
32     xbt_dynar_push(visited_states, &new_state); 
33     MC_UNSET_RAW_MEM;
34
35     if(raw_mem_set)
36       MC_SET_RAW_MEM;
37  
38     return 0;
39
40   }else{
41
42     MC_SET_RAW_MEM;
43     
44     unsigned int cursor = 0;
45     mc_snapshot_t state_test = NULL;
46      
47     xbt_dynar_foreach(visited_states, cursor, state_test){
48       if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug))
49         XBT_DEBUG("****** Pair visited #%d ******", cursor + 1);
50       if(snapshot_compare(new_state, state_test, NULL, NULL) == 0){
51         if(raw_mem_set)
52           MC_SET_RAW_MEM;
53         else
54           MC_UNSET_RAW_MEM;
55         
56         return 1;
57       }   
58     }
59
60     if(xbt_dynar_length(visited_states) == _surf_mc_visited){
61       mc_snapshot_t state_to_remove = NULL;
62       xbt_dynar_shift(visited_states, &state_to_remove);
63       MC_free_snapshot(state_to_remove);
64     }
65
66     xbt_dynar_push(visited_states, &new_state); 
67     
68     MC_UNSET_RAW_MEM;
69
70     if(raw_mem_set)
71       MC_SET_RAW_MEM;
72     
73     return 0;
74     
75   }
76 }
77
78 /**
79  *  \brief Initialize the DPOR exploration algorithm
80  */
81 void MC_dpor_init()
82 {
83   
84   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
85
86   mc_state_t initial_state = NULL;
87   smx_process_t process;
88   
89   /* Create the initial state and push it into the exploration stack */
90   MC_SET_RAW_MEM;
91
92   initial_state = MC_state_new();
93   visited_states = xbt_dynar_new(sizeof(mc_snapshot_t), NULL);
94
95   MC_UNSET_RAW_MEM;
96
97   XBT_DEBUG("**************************************************");
98   XBT_DEBUG("Initial state");
99
100   /* Wait for requests (schedules processes) */
101   MC_wait_for_requests();
102
103   MC_SET_RAW_MEM;
104  
105   /* Get an enabled process and insert it in the interleave set of the initial state */
106   xbt_swag_foreach(process, simix_global->process_list){
107     if(MC_process_is_enabled(process)){
108       MC_state_interleave_process(initial_state, process);
109     }
110   }
111
112   xbt_fifo_unshift(mc_stack_safety, initial_state);
113
114   MC_UNSET_RAW_MEM;
115
116   if(raw_mem_set)
117     MC_SET_RAW_MEM;
118   else
119     MC_UNSET_RAW_MEM;
120   
121 }
122
123
124 /**
125  *   \brief Perform the model-checking operation using a depth-first search exploration
126  *         with Dynamic Partial Order Reductions
127  */
128 void MC_dpor(void)
129 {
130
131   char *req_str;
132   int value;
133   smx_simcall_t req = NULL, prev_req = NULL;
134   mc_state_t state = NULL, prev_state = NULL, next_state = NULL, restore_state=NULL;
135   smx_process_t process = NULL;
136   xbt_fifo_item_t item = NULL;
137   int pos, i;
138   int proc_eval[simix_process_maxpid];
139
140   while (xbt_fifo_size(mc_stack_safety) > 0) {
141
142     /* Get current state */
143     state = (mc_state_t) 
144       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety));
145
146     XBT_DEBUG("**************************************************");
147     XBT_DEBUG("Exploration depth=%d (state=%p)(%u interleave)",
148               xbt_fifo_size(mc_stack_safety), state,
149               MC_state_interleave_size(state));
150
151     /* Update statistics */
152     mc_stats->visited_states++;
153
154     /* If there are processes to interleave and the maximum depth has not been reached
155        then perform one step of the exploration algorithm */
156     if (xbt_fifo_size(mc_stack_safety) < _surf_mc_max_depth &&
157         (req = MC_state_get_request(state, &value))) {
158
159       /* Debug information */
160       if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
161         req_str = MC_request_to_string(req, value);
162         XBT_DEBUG("Execute: %s", req_str);
163         xbt_free(req_str);
164       }
165
166       MC_state_set_executed_request(state, req, value);
167       mc_stats->executed_transitions++;
168
169       /* Answer the request */
170       SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
171
172       /* Wait for requests (schedules processes) */
173       MC_wait_for_requests();
174
175       /* Create the new expanded state */
176       MC_SET_RAW_MEM;
177
178       next_state = MC_state_new();
179
180       if(!is_visited_state()){
181      
182         /* Get an enabled process and insert it in the interleave set of the next state */
183         xbt_swag_foreach(process, simix_global->process_list){
184           if(MC_process_is_enabled(process)){
185             MC_state_interleave_process(next_state, process);
186           }
187         }
188
189         if(_surf_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _surf_mc_checkpoint == 0)){
190           next_state->system_state = MC_take_snapshot();
191         }
192
193       }else{
194
195         XBT_DEBUG("State already visited !");
196         
197       }
198
199       xbt_fifo_unshift(mc_stack_safety, next_state);
200       MC_UNSET_RAW_MEM;
201
202       /* FIXME: Update Statistics
203          mc_stats->state_size +=
204          xbt_setset_set_size(next_state->enabled_transitions);*/
205
206       /* Let's loop again */
207
208       /* The interleave set is empty or the maximum depth is reached, let's back-track */
209     } else {
210
211       if(xbt_fifo_size(mc_stack_safety) == _surf_mc_max_depth)  
212         XBT_WARN("/!\\ Max depth reached ! /!\\ ");
213       else
214         XBT_DEBUG("There are no more processes to interleave.");
215
216       /* Trash the current state, no longer needed */
217       MC_SET_RAW_MEM;
218       xbt_fifo_shift(mc_stack_safety);
219       MC_state_delete(state);
220       MC_UNSET_RAW_MEM;
221
222       /* Check for deadlocks */
223       if(MC_deadlock_check()){
224         MC_show_deadlock(NULL);
225         return;
226       }
227
228       MC_SET_RAW_MEM;
229       /* Traverse the stack backwards until a state with a non empty interleave
230          set is found, deleting all the states that have it empty in the way.
231          For each deleted state, check if the request that has generated it 
232          (from it's predecesor state), depends on any other previous request 
233          executed before it. If it does then add it to the interleave set of the
234          state that executed that previous request. */
235       
236       while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
237
238         for(i=0; i<simix_process_maxpid; i++)
239           proc_eval[i] = 0;
240
241         if(MC_state_interleave_size(state) == 0){
242           req = MC_state_get_internal_request(state);
243           xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
244             if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
245               if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
246                 XBT_DEBUG("Dependent Transitions:");
247                 prev_req = MC_state_get_executed_request(prev_state, &value);
248                 req_str = MC_request_to_string(prev_req, value);
249                 XBT_DEBUG("%s (state=%p)", req_str, prev_state);
250                 xbt_free(req_str);
251                 prev_req = MC_state_get_executed_request(state, &value);
252                 req_str = MC_request_to_string(prev_req, value);
253                 XBT_DEBUG("%s (state=%p)", req_str, state);
254                 xbt_free(req_str);              
255               }
256
257               break;
258
259             }else if(req->issuer == MC_state_get_executed_request(prev_state, &value)->issuer){
260
261               break;
262
263             }else if(proc_eval[MC_state_get_executed_request(prev_state, &value)->issuer->pid] == 0){
264
265               MC_state_remove_interleave_process(prev_state, MC_state_get_executed_request(prev_state, &value)->issuer);
266
267             }
268
269             proc_eval[MC_state_get_executed_request(prev_state, &value)->issuer->pid] = 1;
270
271           }
272         }
273
274         if (MC_state_interleave_size(state)) {
275           /* We found a back-tracking point, let's loop */
276           if(_surf_mc_checkpoint){
277             if(state->system_state != NULL){
278               MC_restore_snapshot(state->system_state);
279               xbt_fifo_unshift(mc_stack_safety, state);
280               XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
281               MC_UNSET_RAW_MEM;
282             }else{
283               pos = xbt_fifo_size(mc_stack_safety);
284               item = xbt_fifo_get_first_item(mc_stack_safety);
285               while(pos>0){
286                 restore_state = (mc_state_t) xbt_fifo_get_item_content(item);
287                 if(restore_state->system_state != NULL){
288                   break;
289                 }else{
290                   item = xbt_fifo_get_next_item(item);
291                   pos--;
292                 }
293               }
294               MC_restore_snapshot(restore_state->system_state);
295               xbt_fifo_unshift(mc_stack_safety, state);
296               XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
297               MC_UNSET_RAW_MEM;
298               MC_replay(mc_stack_safety, pos);
299             }
300           }else{
301             xbt_fifo_unshift(mc_stack_safety, state);
302             XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
303             MC_UNSET_RAW_MEM;
304             MC_replay(mc_stack_safety, -1);
305           }
306           break;
307         } else {
308           MC_state_delete(state);
309         }
310       }
311       MC_UNSET_RAW_MEM;
312     }
313   }
314   MC_print_statistics(mc_stats);
315   MC_UNSET_RAW_MEM;  
316
317   return;
318 }
319
320
321
322