Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
[mc] Move some SIMIX inspection code in the Process class
[simgrid.git] / src / mc / mc_visited.cpp
1 /* Copyright (c) 2011-2015. 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 <unistd.h>
8 #include <sys/wait.h>
9
10 #include <xbt/automaton.h>
11 #include <xbt/log.h>
12 #include <xbt/sysdep.h>
13 #include <xbt/dynar.h>
14 #include <xbt/fifo.h>
15
16 #include "src/mc/mc_comm_pattern.h"
17 #include "src/mc/mc_safety.h"
18 #include "src/mc/mc_liveness.h"
19 #include "src/mc/mc_private.h"
20 #include "src/mc/Process.hpp"
21 #include "src/mc/mc_smx.h"
22
23 extern "C" {
24
25 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_visited, mc,
26                                 "Logging specific to state equaity detection mechanisms");
27
28 }
29
30 namespace simgrid {
31 namespace mc {
32
33 xbt_dynar_t visited_pairs;
34 xbt_dynar_t visited_states;
35
36 static int is_exploration_stack_state(simgrid::mc::VisitedState* state){
37   xbt_fifo_item_t item = xbt_fifo_get_first_item(mc_stack);
38   while (item) {
39     if (((mc_state_t)xbt_fifo_get_item_content(item))->num == state->num){
40       ((mc_state_t)xbt_fifo_get_item_content(item))->in_visited_states = 0;
41       return 1;
42     }
43     item = xbt_fifo_get_next_item(item);
44   }
45   return 0;
46 }
47
48 /**
49  * \brief Save the current state
50  * \return Snapshot of the current state.
51  */
52 VisitedState::VisitedState()
53 {
54   simgrid::mc::Process* process = &(mc_model_checker->process());
55   this->heap_bytes_used = mmalloc_get_bytes_used_remote(
56     process->get_heap()->heaplimit,
57     process->get_malloc_info());
58
59   this->nb_processes =
60     mc_model_checker->process().simix_processes().size();
61
62   this->num = mc_stats->expanded_states;
63   this->other_num = -1;
64 }
65
66 VisitedState::~VisitedState()
67 {
68   if(!is_exploration_stack_state(this))
69     delete this->system_state;
70 }
71
72 VisitedPair::VisitedPair(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, mc_state_t graph_state)
73 {
74   simgrid::mc::Process* process = &(mc_model_checker->process());
75
76   this->graph_state = graph_state;
77   if(this->graph_state->system_state == nullptr)
78     this->graph_state->system_state = simgrid::mc::take_snapshot(pair_num);
79   this->heap_bytes_used = mmalloc_get_bytes_used_remote(
80     process->get_heap()->heaplimit,
81     process->get_malloc_info());
82
83   this->nb_processes =
84     mc_model_checker->process().simix_processes().size();
85
86   this->automaton_state = automaton_state;
87   this->num = pair_num;
88   this->other_num = -1;
89   this->acceptance_removed = 0;
90   this->visited_removed = 0;
91   this->acceptance_pair = 0;
92   this->atomic_propositions = simgrid::xbt::unique_ptr<s_xbt_dynar_t>(
93     xbt_dynar_new(sizeof(int), nullptr));
94
95   unsigned int cursor = 0;
96   int value;
97   xbt_dynar_foreach(atomic_propositions, cursor, value)
98       xbt_dynar_push_as(this->atomic_propositions.get(), int, value);
99 }
100
101 static int is_exploration_stack_pair(simgrid::mc::VisitedPair* pair){
102   xbt_fifo_item_t item = xbt_fifo_get_first_item(mc_stack);
103   while (item) {
104     if (((simgrid::mc::Pair*)xbt_fifo_get_item_content(item))->num == pair->num){
105       ((simgrid::mc::Pair*)xbt_fifo_get_item_content(item))->visited_pair_removed = 1;
106       return 1;
107     }
108     item = xbt_fifo_get_next_item(item);
109   }
110   return 0;
111 }
112
113 VisitedPair::~VisitedPair()
114 {
115   if( !is_exploration_stack_pair(this))
116     MC_state_delete(this->graph_state, 1);
117 }
118
119 }
120 }
121
122 /**
123  *  \brief Find a suitable subrange of candidate duplicates for a given state
124  *  \param list dynamic array of states/pairs with candidate duplicates of the current state;
125  *  \param ref current state/pair;
126  *  \param min (output) index of the beginning of the the subrange
127  *  \param max (output) index of the enf of the subrange
128  *
129  *  Given a suitably ordered array of states/pairs, this function extracts a subrange
130  *  (with index *min <= i <= *max) with candidate duplicates of the given state/pair.
131  *  This function uses only fast discriminating criterions and does not use the
132  *  full state/pair comparison algorithms.
133  *
134  *  The states/pairs in list MUST be ordered using a (given) weak order
135  *  (based on nb_processes and heap_bytes_used).
136  *  The subrange is the subrange of "equivalence" of the given state/pair.
137  */
138 int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max)
139 {
140   int cursor = 0, previous_cursor;
141   int nb_processes, heap_bytes_used, nb_processes_test, heap_bytes_used_test;
142   void *ref_test;
143
144   if (_sg_mc_liveness) {
145     nb_processes = ((simgrid::mc::VisitedPair*) ref)->nb_processes;
146     heap_bytes_used = ((simgrid::mc::VisitedPair*) ref)->heap_bytes_used;
147   } else {
148     nb_processes = ((simgrid::mc::VisitedState*) ref)->nb_processes;
149     heap_bytes_used = ((simgrid::mc::VisitedState*) ref)->heap_bytes_used;
150   }
151
152   int start = 0;
153   int end = xbt_dynar_length(list) - 1;
154
155   while (start <= end) {
156     cursor = (start + end) / 2;
157     if (_sg_mc_liveness) {
158       ref_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(list, cursor, simgrid::mc::VisitedPair*);
159       nb_processes_test = ((simgrid::mc::VisitedPair*) ref_test)->nb_processes;
160       heap_bytes_used_test = ((simgrid::mc::VisitedPair*) ref_test)->heap_bytes_used;
161     } else {
162       ref_test = (simgrid::mc::VisitedState*) xbt_dynar_get_as(list, cursor, simgrid::mc::VisitedState*);
163       nb_processes_test = ((simgrid::mc::VisitedState*) ref_test)->nb_processes;
164       heap_bytes_used_test = ((simgrid::mc::VisitedState*) ref_test)->heap_bytes_used;
165     }
166     if (nb_processes_test < nb_processes)
167       start = cursor + 1;
168     else if (nb_processes_test > nb_processes)
169       end = cursor - 1;
170     else if (heap_bytes_used_test < heap_bytes_used)
171       start = cursor + 1;
172     else if (heap_bytes_used_test > heap_bytes_used)
173       end = cursor - 1;
174     else {
175         *min = *max = cursor;
176         previous_cursor = cursor - 1;
177         while (previous_cursor >= 0) {
178           if (_sg_mc_liveness) {
179             ref_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(list, previous_cursor, simgrid::mc::VisitedPair*);
180             nb_processes_test = ((simgrid::mc::VisitedPair*) ref_test)->nb_processes;
181             heap_bytes_used_test = ((simgrid::mc::VisitedPair*) ref_test)->heap_bytes_used;
182           } else {
183             ref_test = (simgrid::mc::VisitedState*) xbt_dynar_get_as(list, previous_cursor, simgrid::mc::VisitedState*);
184             nb_processes_test = ((simgrid::mc::VisitedState*) ref_test)->nb_processes;
185             heap_bytes_used_test = ((simgrid::mc::VisitedState*) ref_test)->heap_bytes_used;
186           }
187           if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used)
188             break;
189           *min = previous_cursor;
190           previous_cursor--;
191         }
192         size_t next_cursor = cursor + 1;
193         while (next_cursor < xbt_dynar_length(list)) {
194           if (_sg_mc_liveness) {
195             ref_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(list, next_cursor, simgrid::mc::VisitedPair*);
196             nb_processes_test = ((simgrid::mc::VisitedPair*) ref_test)->nb_processes;
197             heap_bytes_used_test = ((simgrid::mc::VisitedPair*) ref_test)->heap_bytes_used;
198           } else {
199             ref_test = (simgrid::mc::VisitedState*) xbt_dynar_get_as(list, next_cursor, simgrid::mc::VisitedState*);
200             nb_processes_test = ((simgrid::mc::VisitedState*) ref_test)->nb_processes;
201             heap_bytes_used_test = ((simgrid::mc::VisitedState*) ref_test)->heap_bytes_used;
202           }
203           if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used)
204             break;
205           *max = next_cursor;
206           next_cursor++;
207         }
208         return -1;
209     }
210   }
211   return cursor;
212 }
213
214 static
215 void replace_state(
216   simgrid::mc::VisitedState* state_test, simgrid::mc::VisitedState* new_state, int cursor)
217 {
218   if (state_test->other_num == -1)
219     new_state->other_num = state_test->num;
220   else
221     new_state->other_num = state_test->other_num;
222
223   if (dot_output == nullptr)
224     XBT_DEBUG("State %d already visited ! (equal to state %d)",
225       new_state->num, state_test->num);
226   else
227     XBT_DEBUG(
228       "State %d already visited ! (equal to state %d (state %d in dot_output))",
229       new_state->num, state_test->num, new_state->other_num);
230
231   /* Replace the old state with the new one (with a bigger num)
232      (when the max number of visited states is reached,  the oldest
233      one is removed according to its number (= with the min number) */
234   xbt_dynar_remove_at(simgrid::mc::visited_states, cursor, nullptr);
235   xbt_dynar_insert_at(simgrid::mc::visited_states, cursor, &new_state);
236   XBT_DEBUG("Replace visited state %d with the new visited state %d",
237     state_test->num, new_state->num);
238 }
239
240 static
241 bool some_communications_are_not_finished()
242 {
243   for (size_t current_process = 1; current_process < MC_smx_get_maxpid(); current_process++) {
244     xbt_dynar_t pattern = xbt_dynar_get_as(
245       incomplete_communications_pattern, current_process, xbt_dynar_t);
246     if (!xbt_dynar_is_empty(pattern)) {
247       XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
248       return true;
249     }
250   }
251   return false;
252 }
253
254 namespace simgrid {
255 namespace mc {
256
257 /**
258  * \brief Checks whether a given state has already been visited by the algorithm.
259  */
260 simgrid::mc::VisitedState* is_visited_state(mc_state_t graph_state)
261 {
262   if (_sg_mc_visited == 0)
263     return nullptr;
264
265   /* If comm determinism verification, we cannot stop the exploration if some 
266      communications are not finished (at least, data are transfered). These communications 
267      are incomplete and they cannot be analyzed and compared with the initial pattern. */
268   int partial_comm = (_sg_mc_comms_determinism || _sg_mc_send_determinism) &&
269     some_communications_are_not_finished();
270
271   simgrid::mc::VisitedState* new_state = new VisitedState();
272   graph_state->system_state = new_state->system_state;
273   graph_state->in_visited_states = 1;
274   XBT_DEBUG("Snapshot %p of visited state %d (exploration stack state %d)", new_state->system_state, new_state->num, graph_state->num);
275
276   if (xbt_dynar_is_empty(visited_states)) {
277     xbt_dynar_push(visited_states, &new_state);
278     return nullptr;
279   }
280
281     int min = -1, max = -1, index;
282
283     index = get_search_interval(visited_states, new_state, &min, &max);
284
285     if (min != -1 && max != -1) {
286
287       if (_sg_mc_safety || (!partial_comm
288         && initial_global_state->initial_communications_pattern_done)) {
289
290         int cursor = min;
291         while (cursor <= max) {
292           simgrid::mc::VisitedState* state_test = (simgrid::mc::VisitedState*) xbt_dynar_get_as(visited_states, cursor, simgrid::mc::VisitedState*);
293           if (snapshot_compare(state_test, new_state) == 0) {
294             // The state has been visited:
295
296             replace_state(state_test, new_state, cursor);
297             return state_test;
298           }
299           cursor++;
300         }
301       }
302       
303       xbt_dynar_insert_at(visited_states, min, &new_state);
304       XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, xbt_dynar_length(visited_states));
305       
306     } else {
307
308       // The state has not been visited: insert the state in the dynamic array.
309       simgrid::mc::VisitedState* state_test = (simgrid::mc::VisitedState*) xbt_dynar_get_as(visited_states, index, simgrid::mc::VisitedState*);
310       if (state_test->nb_processes < new_state->nb_processes)
311         xbt_dynar_insert_at(visited_states, index + 1, &new_state);
312       else if (state_test->heap_bytes_used < new_state->heap_bytes_used)
313         xbt_dynar_insert_at(visited_states, index + 1, &new_state);
314       else
315         xbt_dynar_insert_at(visited_states, index, &new_state);
316
317        XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, xbt_dynar_length(visited_states));
318
319     }
320
321   if ((ssize_t) xbt_dynar_length(visited_states) <= _sg_mc_visited)
322     return nullptr;
323
324   // We have reached the maximum number of stored states;
325
326       XBT_DEBUG("Try to remove visited state (maximum number of stored states reached)");
327
328       // Find the (index of the) older state (with the smallest num):
329       int min2 = mc_stats->expanded_states;
330       unsigned int cursor2 = 0;
331       unsigned int index2 = 0;
332
333       simgrid::mc::VisitedState* state_test;
334       xbt_dynar_foreach(visited_states, cursor2, state_test)
335         if (!mc_model_checker->is_important_snapshot(*state_test->system_state)
336             && state_test->num < min2) {
337           index2 = cursor2;
338           min2 = state_test->num;
339         }
340
341       // and drop it:
342       xbt_dynar_remove_at(visited_states, index2, nullptr);
343       XBT_DEBUG("Remove visited state (maximum number of stored states reached)");
344
345     return nullptr;
346 }
347
348 /**
349  * \brief Checks whether a given pair has already been visited by the algorithm.
350  */
351 int is_visited_pair(simgrid::mc::VisitedPair* visited_pair, simgrid::mc::Pair* pair) {
352
353   if (_sg_mc_visited == 0)
354     return -1;
355
356   simgrid::mc::VisitedPair* new_visited_pair = nullptr;
357   if (visited_pair == nullptr)
358     new_visited_pair = new simgrid::mc::VisitedPair(
359       pair->num, pair->automaton_state, pair->atomic_propositions.get(),
360       pair->graph_state);
361   else
362     new_visited_pair = visited_pair;
363
364   if (xbt_dynar_is_empty(visited_pairs)) {
365     xbt_dynar_push(visited_pairs, &new_visited_pair);
366     return -1;
367   }
368
369     int min = -1, max = -1, index;
370     //int res;
371     simgrid::mc::VisitedPair* pair_test;
372     int cursor;
373
374     index = get_search_interval(visited_pairs, new_visited_pair, &min, &max);
375
376     if (min != -1 && max != -1) {       // Visited pair with same number of processes and same heap bytes used exists
377       cursor = min;
378       while (cursor <= max) {
379         pair_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(visited_pairs, cursor, simgrid::mc::VisitedPair*);
380         if (xbt_automaton_state_compare(pair_test->automaton_state, new_visited_pair->automaton_state) == 0) {
381           if (xbt_automaton_propositional_symbols_compare_value(
382               pair_test->atomic_propositions.get(),
383               new_visited_pair->atomic_propositions.get()) == 0) {
384             if (snapshot_compare(pair_test, new_visited_pair) == 0) {
385               if (pair_test->other_num == -1)
386                 new_visited_pair->other_num = pair_test->num;
387               else
388                 new_visited_pair->other_num = pair_test->other_num;
389               if (dot_output == nullptr)
390                 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_visited_pair->num, pair_test->num);
391               else
392                 XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", new_visited_pair->num, pair_test->num, new_visited_pair->other_num);
393               xbt_dynar_remove_at(visited_pairs, cursor, &pair_test);
394               xbt_dynar_insert_at(visited_pairs, cursor, &new_visited_pair);
395               pair_test->visited_removed = 1;
396               if (!pair_test->acceptance_pair
397                   || pair_test->acceptance_removed == 1)
398                 delete pair_test;
399               return new_visited_pair->other_num;
400             }
401           }
402         }
403         cursor++;
404       }
405       xbt_dynar_insert_at(visited_pairs, min, &new_visited_pair);
406     } else {
407       pair_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(visited_pairs, index, simgrid::mc::VisitedPair*);
408       if (pair_test->nb_processes < new_visited_pair->nb_processes)
409         xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
410       else if (pair_test->heap_bytes_used < new_visited_pair->heap_bytes_used)
411         xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
412       else
413         xbt_dynar_insert_at(visited_pairs, index, &new_visited_pair);
414     }
415
416     if ((ssize_t) xbt_dynar_length(visited_pairs) > _sg_mc_visited) {
417       int min2 = mc_stats->expanded_pairs;
418       unsigned int cursor2 = 0;
419       unsigned int index2 = 0;
420       xbt_dynar_foreach(visited_pairs, cursor2, pair_test) {
421         if (!mc_model_checker->is_important_snapshot(*pair_test->graph_state->system_state)
422             && pair_test->num < min2) {
423           index2 = cursor2;
424           min2 = pair_test->num;
425         }
426       }
427       xbt_dynar_remove_at(visited_pairs, index2, &pair_test);
428       pair_test->visited_removed = 1;
429       if (!pair_test->acceptance_pair || pair_test->acceptance_removed)
430         delete pair_test;
431     }
432   return -1;
433 }
434
435 }
436 }