Logo AND Algorithmique Numérique Distribuée

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