Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Missing space, and more zu -> PRIu64 conversions.
[simgrid.git] / src / mc / mc_dpor.c
1 /* Copyright (c) 2008-2013. The SimGrid Team.
2  * All rights reserved.                                                     */
3
4 /* This program is free software; you can redistribute it and/or modify it
5  * under the terms of the license (GNU LGPL) which comes with this package. */
6
7 #include "mc_private.h"
8
9 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dpor, mc,
10                                 "Logging specific to MC DPOR exploration");
11
12 /********** Global variables **********/
13
14 xbt_dynar_t visited_states;
15 xbt_dict_t first_enabled_state;
16
17 /********** Static functions ***********/
18
19 static void visited_state_free(mc_visited_state_t state){
20   if(state){
21     MC_free_snapshot(state->system_state);
22     xbt_free(state);
23   }
24 }
25
26 static void visited_state_free_voidp(void *s){
27   visited_state_free((mc_visited_state_t) * (void **) s);
28 }
29
30 static mc_visited_state_t visited_state_new(){
31
32   mc_visited_state_t new_state = NULL;
33   new_state = xbt_new0(s_mc_visited_state_t, 1);
34   new_state->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
35   new_state->nb_processes = xbt_swag_size(simix_global->process_list);
36   new_state->system_state = MC_take_snapshot();
37   new_state->num = mc_stats->expanded_states;
38   new_state->other_num = -1;
39
40   return new_state;
41   
42 }
43
44 static int get_search_interval(xbt_dynar_t all_states, mc_visited_state_t state, int *min, int *max){
45
46   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
47
48   MC_SET_RAW_MEM;
49
50   int cursor = 0, previous_cursor, next_cursor;
51   mc_visited_state_t state_test;
52   int start = 0;
53   int end = xbt_dynar_length(all_states) - 1;
54   
55   while(start <= end){
56     cursor = (start + end) / 2;
57     state_test = (mc_visited_state_t)xbt_dynar_get_as(all_states, cursor, mc_visited_state_t);
58     if(state_test->nb_processes < state->nb_processes){
59       start = cursor + 1;
60     }else if(state_test->nb_processes > state->nb_processes){
61       end = cursor - 1;
62     }else{
63       if(state_test->heap_bytes_used < state->heap_bytes_used){
64         start = cursor +1;
65       }else if(state_test->heap_bytes_used > state->heap_bytes_used){
66         end = cursor - 1;
67       }else{
68         *min = *max = cursor;
69         previous_cursor = cursor - 1;
70         while(previous_cursor >= 0){
71           state_test = (mc_visited_state_t)xbt_dynar_get_as(all_states, previous_cursor, mc_visited_state_t);
72           if(state_test->nb_processes != state->nb_processes || state_test->heap_bytes_used != state->heap_bytes_used)
73             break;
74           *min = previous_cursor;
75           previous_cursor--;
76         }
77         next_cursor = cursor + 1;
78         while(next_cursor < xbt_dynar_length(all_states)){
79           state_test = (mc_visited_state_t)xbt_dynar_get_as(all_states, next_cursor, mc_visited_state_t);
80           if(state_test->nb_processes != state->nb_processes || state_test->heap_bytes_used != state->heap_bytes_used)
81             break;
82           *max = next_cursor;
83           next_cursor++;
84         }
85         if(!raw_mem_set)
86           MC_UNSET_RAW_MEM;
87         return -1;
88       }
89      }
90   }
91
92   if(!raw_mem_set)
93     MC_UNSET_RAW_MEM;
94
95   return cursor;
96 }
97
98 static int is_visited_state(){
99
100   if(_sg_mc_visited == 0)
101     return -1;
102
103   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
104
105   MC_SET_RAW_MEM;
106
107   mc_visited_state_t new_state = visited_state_new();
108   
109   if(xbt_dynar_is_empty(visited_states)){
110
111     xbt_dynar_push(visited_states, &new_state); 
112
113     if(!raw_mem_set)
114       MC_UNSET_RAW_MEM;
115
116     return -1;
117
118   }else{
119
120     int min = -1, max = -1, index;
121     //int res;
122     mc_visited_state_t state_test;
123     int cursor;
124
125     index = get_search_interval(visited_states, new_state, &min, &max);
126
127     if(min != -1 && max != -1){
128       /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_states, min), (max-min)+1, new_state);
129       if(res != -1){
130         state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, (min+res)-1, mc_visited_state_t);
131         if(state_test->other_num == -1)
132           new_state->other_num = state_test->num;
133         else
134           new_state->other_num = state_test->other_num;
135         if(dot_output == NULL)
136           XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
137         else
138           XBT_DEBUG("State %d already visited ! (equal to state %d (state %d in dot_output))", new_state->num, state_test->num, new_state->other_num);
139         xbt_dynar_remove_at(visited_states, (min + res) - 1, NULL);
140         xbt_dynar_insert_at(visited_states, (min+res) - 1, &new_state);
141         if(!raw_mem_set)
142           MC_UNSET_RAW_MEM;
143         return new_state->other_num;
144         }*/
145       cursor = min;
146       while(cursor <= max){
147         state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t);
148         if(snapshot_compare(state_test, new_state) == 0){
149           if(state_test->other_num == -1)
150             new_state->other_num = state_test->num;
151           else
152             new_state->other_num = state_test->other_num;
153           if(dot_output == NULL)
154             XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
155           else
156             XBT_DEBUG("State %d already visited ! (equal to state %d (state %d in dot_output))", new_state->num, state_test->num, new_state->other_num);
157           xbt_dynar_remove_at(visited_states, cursor, NULL);
158           xbt_dynar_insert_at(visited_states, cursor, &new_state);
159           if(!raw_mem_set)
160             MC_UNSET_RAW_MEM;
161           return new_state->other_num;
162         }
163         cursor++;
164       }
165       xbt_dynar_insert_at(visited_states, min, &new_state);
166     }else{
167       state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, index, mc_visited_state_t);
168       if(state_test->nb_processes < new_state->nb_processes){
169         xbt_dynar_insert_at(visited_states, index+1, &new_state);
170       }else{
171         if(state_test->heap_bytes_used < new_state->heap_bytes_used)
172           xbt_dynar_insert_at(visited_states, index + 1, &new_state);
173         else
174           xbt_dynar_insert_at(visited_states, index, &new_state);
175       }
176     }
177
178     if(xbt_dynar_length(visited_states) > _sg_mc_visited){
179       int min2 = mc_stats->expanded_states;
180       unsigned int cursor2 = 0;
181       unsigned int index2 = 0;
182       xbt_dynar_foreach(visited_states, cursor2, state_test){
183         if(state_test->num < min2){
184           index2 = cursor2;
185           min2 = state_test->num;
186         }
187       }
188       xbt_dynar_remove_at(visited_states, index2, NULL);
189     }
190
191     if(!raw_mem_set)
192       MC_UNSET_RAW_MEM;
193     
194     return -1;
195     
196   }
197 }
198
199 /**
200  *  \brief Initialize the DPOR exploration algorithm
201  */
202 void MC_dpor_init()
203 {
204   
205   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
206
207   mc_state_t initial_state = NULL;
208   smx_process_t process;
209   
210   /* Create the initial state and push it into the exploration stack */
211   MC_SET_RAW_MEM;
212
213   initial_state = MC_state_new();
214   if(_sg_mc_visited > 0)
215     visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
216
217   first_enabled_state = xbt_dict_new_homogeneous(&xbt_free_f);
218
219   MC_UNSET_RAW_MEM;
220
221   XBT_DEBUG("**************************************************");
222   XBT_DEBUG("Initial state");
223
224   /* Wait for requests (schedules processes) */
225   MC_wait_for_requests();
226
227   MC_ignore_heap(simix_global->process_to_run->data, 0);
228   MC_ignore_heap(simix_global->process_that_ran->data, 0);
229
230   MC_SET_RAW_MEM;
231  
232   /* Get an enabled process and insert it in the interleave set of the initial state */
233   xbt_swag_foreach(process, simix_global->process_list){
234     if(MC_process_is_enabled(process)){
235       MC_state_interleave_process(initial_state, process);
236       if(mc_reduce_kind != e_mc_reduce_none)
237         break;
238     }
239   }
240
241   xbt_fifo_unshift(mc_stack_safety, initial_state);
242
243   /* To ensure the soundness of DPOR, we have to keep a list of 
244      processes which are still enabled at each step of the exploration. 
245      If max depth is reached, we interleave them in the state in which they have 
246      been enabled for the first time. */
247   xbt_swag_foreach(process, simix_global->process_list){
248     if(MC_process_is_enabled(process)){
249       char *key = bprintf("%lu", process->pid);
250       char *data = bprintf("%d", xbt_fifo_size(mc_stack_safety));
251       xbt_dict_set(first_enabled_state, key, data, NULL);
252       xbt_free(key);
253     }
254   }
255
256   MC_UNSET_RAW_MEM;
257
258   if(raw_mem_set)
259     MC_SET_RAW_MEM;
260   else
261     MC_UNSET_RAW_MEM;
262   
263 }
264
265
266 /**
267  *   \brief Perform the model-checking operation using a depth-first search exploration
268  *         with Dynamic Partial Order Reductions
269  */
270 void MC_dpor(void)
271 {
272
273   char *req_str = NULL;
274   int value;
275   smx_simcall_t req = NULL, prev_req = NULL;
276   mc_state_t state = NULL, prev_state = NULL, next_state = NULL, restore_state=NULL;
277   smx_process_t process = NULL;
278   xbt_fifo_item_t item = NULL;
279   int pos;
280   int visited_state = -1;
281   int enabled = 0;
282
283   while (xbt_fifo_size(mc_stack_safety) > 0) {
284
285     /* Get current state */
286     state = (mc_state_t) 
287       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety));
288
289     XBT_DEBUG("**************************************************");
290     XBT_DEBUG("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d)",
291               xbt_fifo_size(mc_stack_safety), state, state->num,
292               MC_state_interleave_size(state), user_max_depth_reached);
293       
294     /* Update statistics */
295     mc_stats->visited_states++;
296
297     /* If there are processes to interleave and the maximum depth has not been reached
298        then perform one step of the exploration algorithm */
299     if (xbt_fifo_size(mc_stack_safety) <= _sg_mc_max_depth && !user_max_depth_reached &&
300         (req = MC_state_get_request(state, &value)) && visited_state == -1) {
301
302       /* Debug information */
303       if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
304         req_str = MC_request_to_string(req, value);
305         XBT_DEBUG("Execute: %s", req_str);
306         xbt_free(req_str);
307       }
308       
309       MC_SET_RAW_MEM;
310       if(dot_output != NULL)
311         req_str = MC_request_get_dot_output(req, value);
312       MC_UNSET_RAW_MEM;
313
314       MC_state_set_executed_request(state, req, value);
315       mc_stats->executed_transitions++;
316
317       MC_SET_RAW_MEM;
318       char *key = bprintf("%lu", req->issuer->pid);
319       xbt_dict_remove(first_enabled_state, key); 
320       xbt_free(key);
321       MC_UNSET_RAW_MEM;
322
323       /* Answer the request */
324       SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
325
326       /* Wait for requests (schedules processes) */
327       MC_wait_for_requests();
328
329       /* Create the new expanded state */
330       MC_SET_RAW_MEM;
331
332       next_state = MC_state_new();
333
334       if((visited_state = is_visited_state()) == -1){
335      
336         /* Get an enabled process and insert it in the interleave set of the next state */
337         xbt_swag_foreach(process, simix_global->process_list){
338           if(MC_process_is_enabled(process)){
339             MC_state_interleave_process(next_state, process);
340             if(mc_reduce_kind != e_mc_reduce_none)
341               break;
342           }
343         }
344
345         if(_sg_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _sg_mc_checkpoint == 0)){
346           next_state->system_state = MC_take_snapshot();
347         }
348
349         if(dot_output != NULL)
350           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
351
352       }else{
353
354         if(dot_output != NULL)
355           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state, req_str);
356
357       }
358
359       xbt_fifo_unshift(mc_stack_safety, next_state);
360
361       /* Insert in dict all enabled processes, if not included yet */
362       xbt_swag_foreach(process, simix_global->process_list){
363         if(MC_process_is_enabled(process)){
364           char *key = bprintf("%lu", process->pid);
365           if(xbt_dict_get_or_null(first_enabled_state, key) == NULL){
366             char *data = bprintf("%d", xbt_fifo_size(mc_stack_safety));
367             xbt_dict_set(first_enabled_state, key, data, NULL); 
368           }
369           xbt_free(key);
370         }
371       }
372       
373       if(dot_output != NULL)
374         xbt_free(req_str);
375
376       MC_UNSET_RAW_MEM;
377
378       /* Let's loop again */
379
380       /* The interleave set is empty or the maximum depth is reached, let's back-track */
381     } else {
382
383       if((xbt_fifo_size(mc_stack_safety) > _sg_mc_max_depth) || user_max_depth_reached || visited_state != -1){  
384
385         if(user_max_depth_reached && visited_state == -1)
386           XBT_DEBUG("User max depth reached !");
387         else if(visited_state == -1)
388           XBT_WARN("/!\\ Max depth reached ! /!\\ ");
389
390         visited_state = -1;
391
392         /* Interleave enabled processes in the state in which they have been enabled for the first time */
393         xbt_swag_foreach(process, simix_global->process_list){
394           if(MC_process_is_enabled(process)){
395             char *key = bprintf("%lu", process->pid);
396             enabled = (int)strtoul(xbt_dict_get_or_null(first_enabled_state, key), 0, 10);
397             xbt_free(key);
398             mc_state_t state_test = NULL;
399             xbt_fifo_item_t item = NULL;
400             int cursor = xbt_fifo_size(mc_stack_safety);
401             xbt_fifo_foreach(mc_stack_safety, item, state_test, mc_state_t){
402               if(cursor-- == enabled){ 
403                 if(!MC_state_process_is_done(state_test, process) && state_test->num != state->num){ 
404                   XBT_DEBUG("Interleave process %lu in state %d", process->pid, state_test->num);
405                   MC_state_interleave_process(state_test, process);
406                   break;
407                 }
408               }
409             } 
410           }
411         }
412
413       }else{
414
415         XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack_safety) + 1);
416
417       }
418
419       /* Trash the current state, no longer needed */
420       MC_SET_RAW_MEM;
421       xbt_fifo_shift(mc_stack_safety);
422       MC_state_delete(state);
423       XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
424       MC_UNSET_RAW_MEM;        
425       
426       /* Check for deadlocks */
427       if(MC_deadlock_check()){
428         MC_show_deadlock(NULL);
429         return;
430       }
431
432       MC_SET_RAW_MEM;
433       /* Traverse the stack backwards until a state with a non empty interleave
434          set is found, deleting all the states that have it empty in the way.
435          For each deleted state, check if the request that has generated it 
436          (from it's predecesor state), depends on any other previous request 
437          executed before it. If it does then add it to the interleave set of the
438          state that executed that previous request. */
439       
440       while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
441         if(mc_reduce_kind != e_mc_reduce_none){
442           req = MC_state_get_internal_request(state);
443           xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
444             if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
445               if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
446                 XBT_DEBUG("Dependent Transitions:");
447                 prev_req = MC_state_get_executed_request(prev_state, &value);
448                 req_str = MC_request_to_string(prev_req, value);
449                 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
450                 xbt_free(req_str);
451                 prev_req = MC_state_get_executed_request(state, &value);
452                 req_str = MC_request_to_string(prev_req, value);
453                 XBT_DEBUG("%s (state=%d)", req_str, state->num);
454                 xbt_free(req_str);              
455               }
456
457               if(!MC_state_process_is_done(prev_state, req->issuer))
458                 MC_state_interleave_process(prev_state, req->issuer);
459               else
460                 XBT_DEBUG("Process %p is in done set", req->issuer);
461
462               break;
463
464             }else if(req->issuer == MC_state_get_internal_request(prev_state)->issuer){
465
466               XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
467               break;
468
469             }else{
470
471               XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant", req->call, req->issuer->pid, state->num, MC_state_get_internal_request(prev_state)->call, MC_state_get_internal_request(prev_state)->issuer->pid, prev_state->num);
472
473             }
474           }
475         }
476              
477         if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack_safety) < _sg_mc_max_depth) {
478           /* We found a back-tracking point, let's loop */
479           XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
480           if(_sg_mc_checkpoint){
481             if(state->system_state != NULL){
482               MC_restore_snapshot(state->system_state);
483               xbt_fifo_unshift(mc_stack_safety, state);
484               MC_UNSET_RAW_MEM;
485             }else{
486               pos = xbt_fifo_size(mc_stack_safety);
487               item = xbt_fifo_get_first_item(mc_stack_safety);
488               while(pos>0){
489                 restore_state = (mc_state_t) xbt_fifo_get_item_content(item);
490                 if(restore_state->system_state != NULL){
491                   break;
492                 }else{
493                   item = xbt_fifo_get_next_item(item);
494                   pos--;
495                 }
496               }
497               MC_restore_snapshot(restore_state->system_state);
498               xbt_fifo_unshift(mc_stack_safety, state);
499               MC_UNSET_RAW_MEM;
500               MC_replay(mc_stack_safety, pos);
501             }
502           }else{
503             xbt_fifo_unshift(mc_stack_safety, state);
504             MC_UNSET_RAW_MEM;
505             MC_replay(mc_stack_safety, -1);
506           }
507           XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety));
508           break;
509         } else {
510           XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1); 
511           MC_state_delete(state);
512         }
513       }
514       MC_UNSET_RAW_MEM;
515     }
516   }
517   MC_print_statistics(mc_stats);
518   MC_UNSET_RAW_MEM;  
519
520   return;
521 }
522
523
524
525