Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Fix lua platform script
[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 = mmalloc_get_chunks_used((xbt_mheap_t)(new_state->system_state)->regions[get_heap_region_index(new_state->system_state)]->data);
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 = mmalloc_get_chunks_used((xbt_mheap_t)(state_test->system_state)->regions[get_heap_region_index(state_test->system_state)]->data);
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, NULL, NULL) == 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 = mmalloc_get_chunks_used((xbt_mheap_t)(state_test->system_state)->regions[get_heap_region_index(state_test->system_state)]->data);
94             if(chunks_used_test != current_chunks_used)
95               break;
96             if(snapshot_compare(new_state->system_state, state_test->system_state, NULL, NULL) == 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 = mmalloc_get_chunks_used((xbt_mheap_t)(state_test->system_state)->regions[get_heap_region_index(state_test->system_state)]->data);
111             if(chunks_used_test != current_chunks_used)
112               break;
113             if(snapshot_compare(new_state->system_state, state_test->system_state, NULL, NULL) == 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 = mmalloc_get_chunks_used((xbt_mheap_t)(state_test->system_state)->regions[get_heap_region_index(state_test->system_state)]->data);
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;
215   smx_simcall_t req = NULL, prev_req = NULL;
216   s_smx_simcall_t req2;
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;
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       /* Answer the request */
253       SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
254
255       /* Wait for requests (schedules processes) */
256       MC_wait_for_requests();
257
258       /* Create the new expanded state */
259       MC_SET_RAW_MEM;
260
261       next_state = MC_state_new();
262
263       if(!is_visited_state()){
264      
265         /* Get an enabled process and insert it in the interleave set of the next state */
266         xbt_swag_foreach(process, simix_global->process_list){
267           if(MC_process_is_enabled(process)){
268             MC_state_interleave_process(next_state, process);
269             XBT_DEBUG("Process %lu enabled with simcall %d", process->pid, process->simcall.call);
270           }
271         }
272
273         if(_sg_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _sg_mc_checkpoint == 0)){
274           next_state->system_state = MC_take_snapshot();
275         }
276
277       }else{
278
279         XBT_DEBUG("State already visited !");
280         
281       }
282
283       xbt_fifo_unshift(mc_stack_safety, next_state);
284       MC_UNSET_RAW_MEM;
285
286       /* Let's loop again */
287
288       /* The interleave set is empty or the maximum depth is reached, let's back-track */
289     } else {
290
291       if(xbt_fifo_size(mc_stack_safety) == _sg_mc_max_depth)  
292         XBT_WARN("/!\\ Max depth reached ! /!\\ ");
293       else
294         XBT_DEBUG("There are no more processes to interleave.");
295
296       /* Trash the current state, no longer needed */
297       MC_SET_RAW_MEM;
298       xbt_fifo_shift(mc_stack_safety);
299       MC_state_delete(state);
300       MC_UNSET_RAW_MEM;
301
302       /* Check for deadlocks */
303       if(MC_deadlock_check()){
304         MC_show_deadlock(NULL);
305         return;
306       }
307
308       MC_SET_RAW_MEM;
309       /* Traverse the stack backwards until a state with a non empty interleave
310          set is found, deleting all the states that have it empty in the way.
311          For each deleted state, check if the request that has generated it 
312          (from it's predecesor state), depends on any other previous request 
313          executed before it. If it does then add it to the interleave set of the
314          state that executed that previous request. */
315       
316       while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
317         req = MC_state_get_internal_request(state);
318         xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
319           if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
320             if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
321               XBT_DEBUG("Dependent Transitions:");
322               prev_req = MC_state_get_executed_request(prev_state, &value);
323               req_str = MC_request_to_string(prev_req, value);
324               XBT_DEBUG("%s (state=%p)", req_str, prev_state);
325               xbt_free(req_str);
326               prev_req = MC_state_get_executed_request(state, &value);
327               req_str = MC_request_to_string(prev_req, value);
328               XBT_DEBUG("%s (state=%p)", req_str, state);
329               xbt_free(req_str);              
330             }
331
332             break;
333
334           }else if(req->issuer == MC_state_get_internal_request(prev_state)->issuer){
335
336             XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
337             break;
338
339           }else{
340
341             MC_state_remove_interleave_process(prev_state, req->issuer);
342             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);  
343
344           }
345         }
346        
347         if (MC_state_interleave_size(state)) {
348           /* We found a back-tracking point, let's loop */
349           if(_sg_mc_checkpoint){
350             if(state->system_state != NULL){
351               MC_restore_snapshot(state->system_state);
352               xbt_fifo_unshift(mc_stack_safety, state);
353               MC_UNSET_RAW_MEM;
354             }else{
355               pos = xbt_fifo_size(mc_stack_safety);
356               item = xbt_fifo_get_first_item(mc_stack_safety);
357               while(pos>0){
358                 restore_state = (mc_state_t) xbt_fifo_get_item_content(item);
359                 if(restore_state->system_state != NULL){
360                   break;
361                 }else{
362                   item = xbt_fifo_get_next_item(item);
363                   pos--;
364                 }
365               }
366               MC_restore_snapshot(restore_state->system_state);
367               xbt_fifo_unshift(mc_stack_safety, state);
368               MC_UNSET_RAW_MEM;
369               MC_replay(mc_stack_safety, pos);
370             }
371           }else{
372             xbt_fifo_unshift(mc_stack_safety, state);
373             MC_UNSET_RAW_MEM;
374             MC_replay(mc_stack_safety, -1);
375           }
376
377           MC_SET_RAW_MEM;
378           req2 = *req;
379           for(i=0; i<simix_process_maxpid; i++)
380             interleave_proc[i] = 0;
381           i=0;
382           while((i < MC_state_interleave_size(state))){
383             i++;
384             prev_req = MC_state_get_request(state, &value);
385             if(prev_req != NULL){
386               MC_state_set_executed_request(state, prev_req, value);
387               prev_req = MC_state_get_internal_request(state);
388               if(MC_request_depend(&req2, prev_req)){
389                 XBT_DEBUG("Simcall %d in process %lu dependant with simcall %d in process %lu", req2.call, req2.issuer->pid, prev_req->call, prev_req->issuer->pid);  
390                 interleave_proc[prev_req->issuer->pid] = 1;
391               }else{
392                 XBT_DEBUG("Simcall %d in process %lu independant with simcall %d in process %lu", req2.call, req2.issuer->pid, prev_req->call, prev_req->issuer->pid); 
393                 MC_state_remove_interleave_process(state, prev_req->issuer);
394               }
395             }
396           }
397           xbt_swag_foreach(process, simix_global->process_list){
398             if(interleave_proc[process->pid] == 1)
399               MC_state_interleave_process(state, process);
400           }
401           XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
402           MC_UNSET_RAW_MEM;
403           break;
404         } else {
405           MC_state_delete(state);
406         }
407       }
408       MC_UNSET_RAW_MEM;
409     }
410   }
411   MC_print_statistics(mc_stats);
412   MC_UNSET_RAW_MEM;  
413
414   return;
415 }
416
417
418
419