Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Fix missing proto for PID functions
[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 static void visited_state_free(mc_safety_visited_state_t state);
15 static void visited_state_free_voidp(void *s);
16
17 static void visited_state_free(mc_safety_visited_state_t state){
18   if(state){
19     MC_free_snapshot(state->system_state);
20     xbt_free(state);
21   }
22 }
23
24 static void visited_state_free_voidp(void *s){
25   visited_state_free((mc_safety_visited_state_t) * (void **) s);
26 }
27
28 static int is_visited_state(){
29
30   if(_sg_mc_visited == 0)
31     return 0;
32
33   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
34
35   MC_SET_RAW_MEM;
36
37   mc_safety_visited_state_t new_state = NULL;
38   new_state = xbt_new0(s_mc_safety_visited_state_t, 1);
39   new_state->system_state = MC_take_snapshot();
40   new_state->num = mc_stats->expanded_states;
41
42   MC_UNSET_RAW_MEM;
43   
44   if(xbt_dynar_is_empty(visited_states)){
45
46     MC_SET_RAW_MEM;
47     xbt_dynar_push(visited_states, &new_state); 
48     MC_UNSET_RAW_MEM;
49
50     if(raw_mem_set)
51       MC_SET_RAW_MEM;
52  
53     return 0;
54
55   }else{
56
57     MC_SET_RAW_MEM;
58     
59     size_t current_chunks_used = new_state->system_state->heap_chunks_used;
60
61     unsigned int cursor = 0;
62     int previous_cursor = 0, next_cursor = 0;
63     int start = 0;
64     int end = xbt_dynar_length(visited_states) - 1;
65
66     mc_safety_visited_state_t state_test = NULL;
67     size_t chunks_used_test;
68     int same_chunks_not_found = 1;
69
70     while(start <= end && same_chunks_not_found){
71       cursor = (start + end) / 2;
72       state_test = (mc_safety_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_safety_visited_state_t);
73       chunks_used_test = state_test->system_state->heap_chunks_used;
74       if(chunks_used_test < current_chunks_used)
75         start = cursor + 1;
76       if(chunks_used_test > current_chunks_used)
77         end = cursor - 1; 
78       if(chunks_used_test == current_chunks_used){
79         same_chunks_not_found = 0;
80         if(snapshot_compare(new_state->system_state, state_test->system_state) == 0){
81           xbt_dynar_remove_at(visited_states, cursor, NULL);
82           xbt_dynar_insert_at(visited_states, cursor, &new_state);
83           if(raw_mem_set)
84             MC_SET_RAW_MEM;
85           else
86             MC_UNSET_RAW_MEM;
87           return 1;
88         }else{
89           /* Search another state with same number of chunks used */
90           previous_cursor = cursor - 1;
91           while(previous_cursor >= 0){
92             state_test = (mc_safety_visited_state_t)xbt_dynar_get_as(visited_states, previous_cursor, mc_safety_visited_state_t);
93             chunks_used_test = state_test->system_state->heap_chunks_used;
94             if(chunks_used_test != current_chunks_used)
95               break;
96             if(snapshot_compare(new_state->system_state, state_test->system_state) == 0){
97               xbt_dynar_remove_at(visited_states, previous_cursor, NULL);
98               xbt_dynar_insert_at(visited_states, previous_cursor, &new_state);
99               if(raw_mem_set)
100                 MC_SET_RAW_MEM;
101               else
102                 MC_UNSET_RAW_MEM;
103               return 1;
104             }
105             previous_cursor--;
106           }
107           next_cursor = cursor + 1;
108           while(next_cursor < xbt_dynar_length(visited_states)){
109             state_test = (mc_safety_visited_state_t)xbt_dynar_get_as(visited_states, next_cursor, mc_safety_visited_state_t);
110             chunks_used_test = state_test->system_state->heap_chunks_used;
111             if(chunks_used_test != current_chunks_used)
112               break;
113             if(snapshot_compare(new_state->system_state, state_test->system_state) == 0){
114               xbt_dynar_remove_at(visited_states, next_cursor, NULL);
115               xbt_dynar_insert_at(visited_states, next_cursor, &new_state);
116               if(raw_mem_set)
117                 MC_SET_RAW_MEM;
118               else
119                 MC_UNSET_RAW_MEM;
120               return 1;
121             }
122             next_cursor++;
123           }
124         }   
125       }
126     }
127
128     state_test = (mc_safety_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_safety_visited_state_t);
129     chunks_used_test = state_test->system_state->heap_chunks_used;
130
131     if(chunks_used_test < current_chunks_used)
132       xbt_dynar_insert_at(visited_states, cursor + 1, &new_state);
133     else
134       xbt_dynar_insert_at(visited_states, cursor, &new_state);
135
136     if(xbt_dynar_length(visited_states) > _sg_mc_visited){
137       int min = mc_stats->expanded_states;
138       unsigned int cursor2 = 0;
139       unsigned int index = 0;
140       xbt_dynar_foreach(visited_states, cursor2, state_test){
141         if(state_test->num < min){
142           index = cursor2;
143           min = state_test->num;
144         }
145       }
146       xbt_dynar_remove_at(visited_states, index, NULL);
147     }
148     
149     MC_UNSET_RAW_MEM;
150
151     if(raw_mem_set)
152       MC_SET_RAW_MEM;
153     
154     return 0;
155     
156   }
157 }
158
159 /**
160  *  \brief Initialize the DPOR exploration algorithm
161  */
162 void MC_dpor_init()
163 {
164   
165   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
166
167   mc_state_t initial_state = NULL;
168   smx_process_t process;
169   
170   /* Create the initial state and push it into the exploration stack */
171   MC_SET_RAW_MEM;
172
173   initial_state = MC_state_new();
174   visited_states = xbt_dynar_new(sizeof(mc_safety_visited_state_t), visited_state_free_voidp);
175
176   MC_UNSET_RAW_MEM;
177
178   XBT_DEBUG("**************************************************");
179   XBT_DEBUG("Initial state");
180
181   /* Wait for requests (schedules processes) */
182   MC_wait_for_requests();
183
184   MC_SET_RAW_MEM;
185  
186   /* Get an enabled process and insert it in the interleave set of the initial state */
187   xbt_swag_foreach(process, simix_global->process_list){
188     if(MC_process_is_enabled(process)){
189       MC_state_interleave_process(initial_state, process);
190       XBT_DEBUG("Process %lu enabled with simcall %d", process->pid, process->simcall.call);
191     }
192   }
193
194   xbt_fifo_unshift(mc_stack_safety, initial_state);
195
196   MC_UNSET_RAW_MEM;
197
198   if(raw_mem_set)
199     MC_SET_RAW_MEM;
200   else
201     MC_UNSET_RAW_MEM;
202   
203 }
204
205
206 /**
207  *   \brief Perform the model-checking operation using a depth-first search exploration
208  *         with Dynamic Partial Order Reductions
209  */
210 void MC_dpor(void)
211 {
212
213   char *req_str;
214   int value, value2;
215   smx_simcall_t req = NULL, prev_req = NULL, req2 = NULL;
216   s_smx_simcall_t req3;
217   mc_state_t state = NULL, prev_state = NULL, next_state = NULL, restore_state=NULL;
218   smx_process_t process = NULL;
219   xbt_fifo_item_t item = NULL;
220   int pos, i, interleave_size;
221   int interleave_proc[simix_process_maxpid];
222
223   while (xbt_fifo_size(mc_stack_safety) > 0) {
224
225     /* Get current state */
226     state = (mc_state_t) 
227       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety));
228
229     XBT_DEBUG("**************************************************");
230     XBT_DEBUG("Exploration depth=%d (state=%p)(%u interleave)",
231               xbt_fifo_size(mc_stack_safety), state,
232               MC_state_interleave_size(state));
233
234     /* Update statistics */
235     mc_stats->visited_states++;
236
237     /* If there are processes to interleave and the maximum depth has not been reached
238        then perform one step of the exploration algorithm */
239     if (xbt_fifo_size(mc_stack_safety) < _sg_mc_max_depth &&
240         (req = MC_state_get_request(state, &value))) {
241
242       /* Debug information */
243       if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
244         req_str = MC_request_to_string(req, value);
245         XBT_DEBUG("Execute: %s", req_str);
246         xbt_free(req_str);
247       }
248
249       MC_state_set_executed_request(state, req, value);
250       mc_stats->executed_transitions++;
251
252       if(MC_state_interleave_size(state)){
253         MC_SET_RAW_MEM;
254         req2 = MC_state_get_internal_request(state);
255         req3 = *req2;
256         for(i=0; i<simix_process_maxpid; i++)
257           interleave_proc[i] = 0;
258         i=0;
259         interleave_size = MC_state_interleave_size(state);
260         while(i < interleave_size){
261           i++;
262           prev_req = MC_state_get_request(state, &value2);
263           if(prev_req != NULL){
264             MC_state_set_executed_request(state, prev_req, value2);
265             prev_req = MC_state_get_internal_request(state);
266             if(MC_request_depend(&req3, prev_req)){
267               XBT_DEBUG("Simcall %d in process %lu dependant with simcall %d in process %lu", req3.call, req3.issuer->pid, prev_req->call, prev_req->issuer->pid);  
268               interleave_proc[prev_req->issuer->pid] = 1;
269             }else{
270               XBT_DEBUG("Simcall %d in process %lu independant with simcall %d in process %lu", req3.call, req3.issuer->pid, prev_req->call, prev_req->issuer->pid); 
271               MC_state_remove_interleave_process(state, prev_req->issuer);
272             }
273           }
274         }
275         xbt_swag_foreach(process, simix_global->process_list){
276           if(interleave_proc[process->pid] == 1)
277             MC_state_interleave_process(state, process);
278         }
279         MC_UNSET_RAW_MEM;
280       }
281
282       MC_state_set_executed_request(state, req, value);
283
284       /* Answer the request */
285       SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
286
287       /* Wait for requests (schedules processes) */
288       MC_wait_for_requests();
289
290       /* Create the new expanded state */
291       MC_SET_RAW_MEM;
292
293       next_state = MC_state_new();
294
295       if(!is_visited_state()){
296      
297         /* Get an enabled process and insert it in the interleave set of the next state */
298         xbt_swag_foreach(process, simix_global->process_list){
299           if(MC_process_is_enabled(process)){
300             MC_state_interleave_process(next_state, process);
301             XBT_DEBUG("Process %lu enabled with simcall %d", process->pid, process->simcall.call);
302           }
303         }
304
305         if(_sg_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _sg_mc_checkpoint == 0)){
306           next_state->system_state = MC_take_snapshot();
307         }
308
309       }else{
310
311         XBT_DEBUG("State already visited !");
312         
313       }
314
315       xbt_fifo_unshift(mc_stack_safety, next_state);
316       MC_UNSET_RAW_MEM;
317
318       /* Let's loop again */
319
320       /* The interleave set is empty or the maximum depth is reached, let's back-track */
321     } else {
322
323       if(xbt_fifo_size(mc_stack_safety) == _sg_mc_max_depth)  
324         XBT_WARN("/!\\ Max depth reached ! /!\\ ");
325       else
326         XBT_DEBUG("There are no more processes to interleave.");
327
328       /* Trash the current state, no longer needed */
329       MC_SET_RAW_MEM;
330       xbt_fifo_shift(mc_stack_safety);
331       MC_state_delete(state);
332       MC_UNSET_RAW_MEM;
333
334       /* Check for deadlocks */
335       if(MC_deadlock_check()){
336         MC_show_deadlock(NULL);
337         return;
338       }
339
340       MC_SET_RAW_MEM;
341       /* Traverse the stack backwards until a state with a non empty interleave
342          set is found, deleting all the states that have it empty in the way.
343          For each deleted state, check if the request that has generated it 
344          (from it's predecesor state), depends on any other previous request 
345          executed before it. If it does then add it to the interleave set of the
346          state that executed that previous request. */
347       
348       while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
349         req = MC_state_get_internal_request(state);
350         xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
351           if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
352             if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
353               XBT_DEBUG("Dependent Transitions:");
354               prev_req = MC_state_get_executed_request(prev_state, &value);
355               req_str = MC_request_to_string(prev_req, value);
356               XBT_DEBUG("%s (state=%p)", req_str, prev_state);
357               xbt_free(req_str);
358               prev_req = MC_state_get_executed_request(state, &value);
359               req_str = MC_request_to_string(prev_req, value);
360               XBT_DEBUG("%s (state=%p)", req_str, state);
361               xbt_free(req_str);              
362             }
363
364             break;
365
366           }else if(req->issuer == MC_state_get_internal_request(prev_state)->issuer){
367
368             XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
369             break;
370
371           }else{
372
373             MC_state_remove_interleave_process(prev_state, req->issuer);
374             XBT_DEBUG("Simcall %d in process %lu independant with simcall %d process %lu", req->call, req->issuer->pid, MC_state_get_internal_request(prev_state)->call, MC_state_get_internal_request(prev_state)->issuer->pid);  
375
376           }
377         }
378        
379         if (MC_state_interleave_size(state)) {
380           /* We found a back-tracking point, let's loop */
381           if(_sg_mc_checkpoint){
382             if(state->system_state != NULL){
383               MC_restore_snapshot(state->system_state);
384               xbt_fifo_unshift(mc_stack_safety, state);
385               MC_UNSET_RAW_MEM;
386             }else{
387               pos = xbt_fifo_size(mc_stack_safety);
388               item = xbt_fifo_get_first_item(mc_stack_safety);
389               while(pos>0){
390                 restore_state = (mc_state_t) xbt_fifo_get_item_content(item);
391                 if(restore_state->system_state != NULL){
392                   break;
393                 }else{
394                   item = xbt_fifo_get_next_item(item);
395                   pos--;
396                 }
397               }
398               MC_restore_snapshot(restore_state->system_state);
399               xbt_fifo_unshift(mc_stack_safety, state);
400               MC_UNSET_RAW_MEM;
401               MC_replay(mc_stack_safety, pos);
402             }
403           }else{
404             xbt_fifo_unshift(mc_stack_safety, state);
405             MC_UNSET_RAW_MEM;
406             MC_replay(mc_stack_safety, -1);
407           }
408           XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
409           break;
410         } else {
411           MC_state_delete(state);
412         }
413       }
414       MC_UNSET_RAW_MEM;
415     }
416   }
417   MC_print_statistics(mc_stats);
418   MC_UNSET_RAW_MEM;  
419
420   return;
421 }
422
423
424
425