Logo AND Algorithmique Numérique Distribuée

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