Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : clarify comments
[simgrid.git] / src / mc / mc_visited.c
1 /* Copyright (c) 2011-2014. 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 #include <unistd.h>
9 #include <sys/wait.h>
10
11 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_visited, mc,
12                                 "Logging specific to state equaity detection mechanisms");
13
14 xbt_dynar_t visited_pairs;
15 xbt_dynar_t visited_states;
16
17 void visited_state_free(mc_visited_state_t state)
18 {
19   if (state) {
20     MC_free_snapshot(state->system_state);
21     xbt_free(state);
22   }
23 }
24
25 void visited_state_free_voidp(void *s)
26 {
27   visited_state_free((mc_visited_state_t) * (void **) s);
28 }
29
30 /**
31  * \brief Save the current state
32  * \return Snapshot of the current state.
33  */
34 static mc_visited_state_t visited_state_new()
35 {
36   mc_visited_state_t new_state = NULL;
37   new_state = xbt_new0(s_mc_visited_state_t, 1);
38   new_state->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
39   new_state->nb_processes = xbt_swag_size(simix_global->process_list);
40   new_state->system_state = MC_take_snapshot(mc_stats->expanded_states);
41   new_state->num = mc_stats->expanded_states;
42   new_state->other_num = -1;
43   return new_state;
44 }
45
46
47 mc_visited_pair_t MC_visited_pair_new(int pair_num,
48                                       xbt_automaton_state_t automaton_state,
49                                       xbt_dynar_t atomic_propositions)
50 {
51   mc_visited_pair_t pair = NULL;
52   pair = xbt_new0(s_mc_visited_pair_t, 1);
53   pair->graph_state = MC_state_new();
54   pair->graph_state->system_state = MC_take_snapshot(pair_num);
55   pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
56   pair->nb_processes = xbt_swag_size(simix_global->process_list);
57   pair->automaton_state = automaton_state;
58   pair->num = pair_num;
59   pair->other_num = -1;
60   pair->acceptance_removed = 0;
61   pair->visited_removed = 0;
62   pair->acceptance_pair = 0;
63   pair->atomic_propositions = xbt_dynar_new(sizeof(int), NULL);
64   unsigned int cursor = 0;
65   int value;
66   xbt_dynar_foreach(atomic_propositions, cursor, value)
67       xbt_dynar_push_as(pair->atomic_propositions, int, value);
68   return pair;
69 }
70
71 void MC_visited_pair_delete(mc_visited_pair_t p)
72 {
73   p->automaton_state = NULL;
74   MC_state_delete(p->graph_state);
75   xbt_dynar_free(&(p->atomic_propositions));
76   xbt_free(p);
77   p = NULL;
78 }
79
80 /**
81  *  \brief Find a suitable subrange of candidate duplicates for a given state
82  *  \param list dynamic array of states/pairs with candidate duplicates of the current state;
83  *  \param ref current state/pair;
84  *  \param min (output) index of the beginning of the the subrange
85  *  \param max (output) index of the enf of the subrange
86  *
87  *  Given a suitably ordered array of states/pairs, this function extracts a subrange
88  *  (with index *min <= i <= *max) with candidate duplicates of the given state/pair.
89  *  This function uses only fast discriminating criterions and does not use the
90  *  full state/pair comparison algorithms.
91  *
92  *  The states/pairs in list MUST be ordered using a (given) weak order
93  *  (based on nb_processes and heap_bytes_used).
94  *  The subrange is the subrange of "equivalence" of the given state/pair.
95  */
96 int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max)
97 {
98
99   int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
100
101   MC_SET_MC_HEAP;
102
103   int cursor = 0, previous_cursor, next_cursor;
104   int nb_processes, heap_bytes_used, nb_processes_test, heap_bytes_used_test;
105   void *ref_test;
106
107   if (_sg_mc_safety) {
108     nb_processes = ((mc_visited_state_t) ref)->nb_processes;
109     heap_bytes_used = ((mc_visited_state_t) ref)->heap_bytes_used;
110   } else if (_sg_mc_liveness) {
111     nb_processes = ((mc_visited_pair_t) ref)->nb_processes;
112     heap_bytes_used = ((mc_visited_pair_t) ref)->heap_bytes_used;
113   }
114
115   int start = 0;
116   int end = xbt_dynar_length(list) - 1;
117
118   while (start <= end) {
119     cursor = (start + end) / 2;
120     if (_sg_mc_safety) {
121       ref_test =
122           (mc_visited_state_t) xbt_dynar_get_as(list, cursor,
123                                                 mc_visited_state_t);
124       nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
125       heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
126     } else if (_sg_mc_liveness) {
127       ref_test =
128           (mc_visited_pair_t) xbt_dynar_get_as(list, cursor, mc_visited_pair_t);
129       nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
130       heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
131     }
132     if (nb_processes_test < nb_processes) {
133       start = cursor + 1;
134     } else if (nb_processes_test > nb_processes) {
135       end = cursor - 1;
136     } else {
137       if (heap_bytes_used_test < heap_bytes_used) {
138         start = cursor + 1;
139       } else if (heap_bytes_used_test > heap_bytes_used) {
140         end = cursor - 1;
141       } else {
142         *min = *max = cursor;
143         previous_cursor = cursor - 1;
144         while (previous_cursor >= 0) {
145           if (_sg_mc_safety) {
146             ref_test =
147                 (mc_visited_state_t) xbt_dynar_get_as(list, previous_cursor,
148                                                       mc_visited_state_t);
149             nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
150             heap_bytes_used_test =
151                 ((mc_visited_state_t) ref_test)->heap_bytes_used;
152           } else if (_sg_mc_liveness) {
153             ref_test =
154                 (mc_visited_pair_t) xbt_dynar_get_as(list, previous_cursor,
155                                                      mc_visited_pair_t);
156             nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
157             heap_bytes_used_test =
158                 ((mc_visited_pair_t) ref_test)->heap_bytes_used;
159           }
160           if (nb_processes_test != nb_processes
161               || heap_bytes_used_test != heap_bytes_used)
162             break;
163           *min = previous_cursor;
164           previous_cursor--;
165         }
166         next_cursor = cursor + 1;
167         while (next_cursor < xbt_dynar_length(list)) {
168           if (_sg_mc_safety) {
169             ref_test =
170                 (mc_visited_state_t) xbt_dynar_get_as(list, next_cursor,
171                                                       mc_visited_state_t);
172             nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
173             heap_bytes_used_test =
174                 ((mc_visited_state_t) ref_test)->heap_bytes_used;
175           } else if (_sg_mc_liveness) {
176             ref_test =
177                 (mc_visited_pair_t) xbt_dynar_get_as(list, next_cursor,
178                                                      mc_visited_pair_t);
179             nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
180             heap_bytes_used_test =
181                 ((mc_visited_pair_t) ref_test)->heap_bytes_used;
182           }
183           if (nb_processes_test != nb_processes
184               || heap_bytes_used_test != heap_bytes_used)
185             break;
186           *max = next_cursor;
187           next_cursor++;
188         }
189         if (!mc_mem_set)
190           MC_SET_STD_HEAP;
191         return -1;
192       }
193     }
194   }
195
196   if (!mc_mem_set)
197     MC_SET_STD_HEAP;
198
199   return cursor;
200 }
201
202
203 /**
204  * \brief Checks whether a given state has already been visited by the algorithm.
205  */
206 int is_visited_state()
207 {
208
209   if (_sg_mc_visited == 0)
210     return -1;
211
212   int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
213
214   MC_SET_MC_HEAP;
215
216   mc_visited_state_t new_state = visited_state_new();
217
218   if (xbt_dynar_is_empty(visited_states)) {
219
220     xbt_dynar_push(visited_states, &new_state);
221
222     if (!mc_mem_set)
223       MC_SET_STD_HEAP;
224
225     return -1;
226
227   } else {
228
229     int min = -1, max = -1, index;
230     //int res;
231     mc_visited_state_t state_test;
232     int cursor;
233
234     index = get_search_interval(visited_states, new_state, &min, &max);
235
236     if (min != -1 && max != -1) {
237
238       // Parallell implementation
239       /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_states, min), (max-min)+1, new_state);
240          if(res != -1){
241          state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, (min+res)-1, mc_visited_state_t);
242          if(state_test->other_num == -1)
243          new_state->other_num = state_test->num;
244          else
245          new_state->other_num = state_test->other_num;
246          if(dot_output == NULL)
247          XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
248          else
249          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);
250          xbt_dynar_remove_at(visited_states, (min + res) - 1, NULL);
251          xbt_dynar_insert_at(visited_states, (min+res) - 1, &new_state);
252          if(!raw_mem_set)
253          MC_SET_STD_HEAP;
254          return new_state->other_num;
255          } */
256
257       cursor = min;
258       while (cursor <= max) {
259         state_test =
260             (mc_visited_state_t) xbt_dynar_get_as(visited_states, cursor,
261                                                   mc_visited_state_t);
262         if (snapshot_compare(state_test, new_state) == 0) {
263           // The state has been visited:
264
265           if (state_test->other_num == -1)
266             new_state->other_num = state_test->num;
267           else
268             new_state->other_num = state_test->other_num;
269           if (dot_output == NULL)
270             XBT_DEBUG("State %d already visited ! (equal to state %d)",
271                       new_state->num, state_test->num);
272           else
273             XBT_DEBUG
274                 ("State %d already visited ! (equal to state %d (state %d in dot_output))",
275                  new_state->num, state_test->num, new_state->other_num);
276
277           /* Replace the old state with the new one (with a bigger num) 
278              (when the max number of visited states is reached,  the oldest 
279              one is removed according to its number (= with the min number) */
280           xbt_dynar_remove_at(visited_states, cursor, NULL);
281           xbt_dynar_insert_at(visited_states, cursor, &new_state);
282
283           if (!mc_mem_set)
284             MC_SET_STD_HEAP;
285           return new_state->other_num;
286         }
287         cursor++;
288       }
289
290       // The state has not been visited: insert the state in the dynamic array.
291       xbt_dynar_insert_at(visited_states, min, &new_state);
292
293     } else {
294
295       // The state has not been visited: insert the state in the dynamic array.
296       state_test =
297           (mc_visited_state_t) xbt_dynar_get_as(visited_states, index,
298                                                 mc_visited_state_t);
299       if (state_test->nb_processes < new_state->nb_processes) {
300         xbt_dynar_insert_at(visited_states, index + 1, &new_state);
301       } else {
302         if (state_test->heap_bytes_used < new_state->heap_bytes_used)
303           xbt_dynar_insert_at(visited_states, index + 1, &new_state);
304         else
305           xbt_dynar_insert_at(visited_states, index, &new_state);
306       }
307
308     }
309
310     // We have reached the maximum number of stored states;
311     if (xbt_dynar_length(visited_states) > _sg_mc_visited) {
312
313       // Find the (index of the) older state (with the smallest num):
314       int min2 = mc_stats->expanded_states;
315       unsigned int cursor2 = 0;
316       unsigned int index2 = 0;
317       xbt_dynar_foreach(visited_states, cursor2, state_test) {
318         if (state_test->num < min2) {
319           index2 = cursor2;
320           min2 = state_test->num;
321         }
322       }
323
324       // and drop it:
325       xbt_dynar_remove_at(visited_states, index2, NULL);
326     }
327
328     if (!mc_mem_set)
329       MC_SET_STD_HEAP;
330
331     return -1;
332
333   }
334 }
335
336 /**
337  * \brief Checks whether a given pair has already been visited by the algorithm.
338  */
339 int is_visited_pair(mc_visited_pair_t pair, int pair_num,
340                     xbt_automaton_state_t automaton_state,
341                     xbt_dynar_t atomic_propositions)
342 {
343
344   if (_sg_mc_visited == 0)
345     return -1;
346
347   int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
348
349   MC_SET_MC_HEAP;
350
351   mc_visited_pair_t new_pair = NULL;
352
353   if (pair == NULL) {
354     new_pair =
355         MC_visited_pair_new(pair_num, automaton_state, atomic_propositions);
356   } else {
357     new_pair = pair;
358   }
359
360   if (xbt_dynar_is_empty(visited_pairs)) {
361
362     xbt_dynar_push(visited_pairs, &new_pair);
363
364   } else {
365
366     int min = -1, max = -1, index;
367     //int res;
368     mc_visited_pair_t pair_test;
369     int cursor;
370
371     index = get_search_interval(visited_pairs, new_pair, &min, &max);
372
373     if (min != -1 && max != -1) {       // Visited pair with same number of processes and same heap bytes used exists
374       /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_pairs, min), (max-min)+1, pair);
375          if(res != -1){
376          pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, (min+res)-1, mc_pair_t);
377          if(pair_test->other_num == -1)
378          pair->other_num = pair_test->num;
379          else
380          pair->other_num = pair_test->other_num;
381          if(dot_output == NULL)
382          XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", pair->num, pair_test->num);
383          else
384          XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", pair->num, pair_test->num, pair->other_num);
385          xbt_dynar_remove_at(visited_pairs, (min + res) - 1, NULL);
386          xbt_dynar_insert_at(visited_pairs, (min+res) - 1, &pair);
387          pair_test->visited_removed = 1;
388          if(pair_test->stack_removed && pair_test->visited_removed){
389          if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
390          if(pair_test->acceptance_removed){
391          MC_pair_delete(pair_test);
392          }
393          }else{
394          MC_pair_delete(pair_test);
395          }
396          }
397          if(!raw_mem_set)
398          MC_SET_STD_HEAP;
399          return pair->other_num;
400          } */
401       cursor = min;
402       while (cursor <= max) {
403         pair_test =
404             (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, cursor,
405                                                  mc_visited_pair_t);
406         if (xbt_automaton_state_compare
407             (pair_test->automaton_state, new_pair->automaton_state) == 0) {
408           if (xbt_automaton_propositional_symbols_compare_value
409               (pair_test->atomic_propositions,
410                new_pair->atomic_propositions) == 0) {
411             if (snapshot_compare(pair_test, new_pair) == 0) {
412               if (pair_test->other_num == -1)
413                 new_pair->other_num = pair_test->num;
414               else
415                 new_pair->other_num = pair_test->other_num;
416               if (dot_output == NULL)
417                 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)",
418                           new_pair->num, pair_test->num);
419               else
420                 XBT_DEBUG
421                     ("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))",
422                      new_pair->num, pair_test->num, new_pair->other_num);
423               xbt_dynar_remove_at(visited_pairs, cursor, NULL);
424               xbt_dynar_insert_at(visited_pairs, cursor, &new_pair);
425               pair_test->visited_removed = 1;
426               if (pair_test->acceptance_pair) {
427                 if (pair_test->acceptance_removed == 1)
428                   MC_visited_pair_delete(pair_test);
429               } else {
430                 MC_visited_pair_delete(pair_test);
431               }
432               if (!mc_mem_set)
433                 MC_SET_STD_HEAP;
434               return new_pair->other_num;
435             }
436           }
437         }
438         cursor++;
439       }
440       xbt_dynar_insert_at(visited_pairs, min, &new_pair);
441     } else {
442       pair_test =
443           (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, index,
444                                                mc_visited_pair_t);
445       if (pair_test->nb_processes < new_pair->nb_processes) {
446         xbt_dynar_insert_at(visited_pairs, index + 1, &new_pair);
447       } else {
448         if (pair_test->heap_bytes_used < new_pair->heap_bytes_used)
449           xbt_dynar_insert_at(visited_pairs, index + 1, &new_pair);
450         else
451           xbt_dynar_insert_at(visited_pairs, index, &new_pair);
452       }
453     }
454
455     if (xbt_dynar_length(visited_pairs) > _sg_mc_visited) {
456       int min2 = mc_stats->expanded_pairs;
457       unsigned int cursor2 = 0;
458       unsigned int index2 = 0;
459       xbt_dynar_foreach(visited_pairs, cursor2, pair_test) {
460         if (pair_test->num < min2) {
461           index2 = cursor2;
462           min2 = pair_test->num;
463         }
464       }
465       xbt_dynar_remove_at(visited_pairs, index2, &pair_test);
466       pair_test->visited_removed = 1;
467       if (pair_test->acceptance_pair) {
468         if (pair_test->acceptance_removed)
469           MC_visited_pair_delete(pair_test);
470       } else {
471         MC_visited_pair_delete(pair_test);
472       }
473     }
474
475   }
476
477   if (!mc_mem_set)
478     MC_SET_STD_HEAP;
479
480   return -1;
481 }