1 /* Copyright (c) 2011-2014. The SimGrid Team.
2 * All rights reserved. */
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. */
7 #include "mc_private.h"
11 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_visited, mc,
12 "Logging specific to state equaity detection mechanisms");
14 xbt_dynar_t visited_pairs;
15 xbt_dynar_t visited_states;
17 void visited_state_free(mc_visited_state_t state)
20 MC_free_snapshot(state->system_state);
25 void visited_state_free_voidp(void *s)
27 visited_state_free((mc_visited_state_t) * (void **) s);
31 * \brief Save the current state
32 * \return Snapshot of the current state.
34 static mc_visited_state_t visited_state_new()
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;
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)
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;
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;
66 xbt_dynar_foreach(atomic_propositions, cursor, value)
67 xbt_dynar_push_as(pair->atomic_propositions, int, value);
71 void MC_visited_pair_delete(mc_visited_pair_t p)
73 p->automaton_state = NULL;
74 MC_state_delete(p->graph_state);
75 xbt_dynar_free(&(p->atomic_propositions));
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
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.
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.
96 int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max)
99 int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
103 int cursor = 0, previous_cursor, next_cursor;
104 int nb_processes, heap_bytes_used, nb_processes_test, heap_bytes_used_test;
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;
116 int end = xbt_dynar_length(list) - 1;
118 while (start <= end) {
119 cursor = (start + end) / 2;
122 (mc_visited_state_t) xbt_dynar_get_as(list, cursor,
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) {
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;
132 if (nb_processes_test < nb_processes) {
134 } else if (nb_processes_test > nb_processes) {
137 if (heap_bytes_used_test < heap_bytes_used) {
139 } else if (heap_bytes_used_test > heap_bytes_used) {
142 *min = *max = cursor;
143 previous_cursor = cursor - 1;
144 while (previous_cursor >= 0) {
147 (mc_visited_state_t) xbt_dynar_get_as(list, previous_cursor,
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) {
154 (mc_visited_pair_t) xbt_dynar_get_as(list, previous_cursor,
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;
160 if (nb_processes_test != nb_processes
161 || heap_bytes_used_test != heap_bytes_used)
163 *min = previous_cursor;
166 next_cursor = cursor + 1;
167 while (next_cursor < xbt_dynar_length(list)) {
170 (mc_visited_state_t) xbt_dynar_get_as(list, next_cursor,
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) {
177 (mc_visited_pair_t) xbt_dynar_get_as(list, next_cursor,
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;
183 if (nb_processes_test != nb_processes
184 || heap_bytes_used_test != heap_bytes_used)
204 * \brief Checks whether a given state has already been visited by the algorithm.
206 int is_visited_state()
209 if (_sg_mc_visited == 0)
212 int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
216 mc_visited_state_t new_state = visited_state_new();
218 if (xbt_dynar_is_empty(visited_states)) {
220 xbt_dynar_push(visited_states, &new_state);
229 int min = -1, max = -1, index;
231 mc_visited_state_t state_test;
234 index = get_search_interval(visited_states, new_state, &min, &max);
236 if (min != -1 && max != -1) {
238 // Parallell implementation
239 /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_states, min), (max-min)+1, new_state);
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;
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);
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);
254 return new_state->other_num;
258 while (cursor <= max) {
260 (mc_visited_state_t) xbt_dynar_get_as(visited_states, cursor,
262 if (snapshot_compare(state_test, new_state) == 0) {
263 // The state has been visited:
265 if (state_test->other_num == -1)
266 new_state->other_num = state_test->num;
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);
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);
277 // Replace the old state with the new one (why?):
278 xbt_dynar_remove_at(visited_states, cursor, NULL);
279 xbt_dynar_insert_at(visited_states, cursor, &new_state);
283 return new_state->other_num;
288 // The state has not been visited, add it to the list:
289 xbt_dynar_insert_at(visited_states, min, &new_state);
293 // The state has not been visited: insert the state in the dynamic array.
295 (mc_visited_state_t) xbt_dynar_get_as(visited_states, index,
297 if (state_test->nb_processes < new_state->nb_processes) {
298 xbt_dynar_insert_at(visited_states, index + 1, &new_state);
300 if (state_test->heap_bytes_used < new_state->heap_bytes_used)
301 xbt_dynar_insert_at(visited_states, index + 1, &new_state);
303 xbt_dynar_insert_at(visited_states, index, &new_state);
308 // We have reached the maximum number of stored states;
309 if (xbt_dynar_length(visited_states) > _sg_mc_visited) {
311 // Find the (index of the) older state:
312 int min2 = mc_stats->expanded_states;
313 unsigned int cursor2 = 0;
314 unsigned int index2 = 0;
315 xbt_dynar_foreach(visited_states, cursor2, state_test) {
316 if (state_test->num < min2) {
318 min2 = state_test->num;
323 xbt_dynar_remove_at(visited_states, index2, NULL);
335 * \brief Checks whether a given pair has already been visited by the algorithm.
337 int is_visited_pair(mc_visited_pair_t pair, int pair_num,
338 xbt_automaton_state_t automaton_state,
339 xbt_dynar_t atomic_propositions)
342 if (_sg_mc_visited == 0)
345 int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
349 mc_visited_pair_t new_pair = NULL;
353 MC_visited_pair_new(pair_num, automaton_state, atomic_propositions);
358 if (xbt_dynar_is_empty(visited_pairs)) {
360 xbt_dynar_push(visited_pairs, &new_pair);
364 int min = -1, max = -1, index;
366 mc_visited_pair_t pair_test;
369 index = get_search_interval(visited_pairs, new_pair, &min, &max);
371 if (min != -1 && max != -1) { // Visited pair with same number of processes and same heap bytes used exists
372 /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_pairs, min), (max-min)+1, pair);
374 pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, (min+res)-1, mc_pair_t);
375 if(pair_test->other_num == -1)
376 pair->other_num = pair_test->num;
378 pair->other_num = pair_test->other_num;
379 if(dot_output == NULL)
380 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", pair->num, pair_test->num);
382 XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", pair->num, pair_test->num, pair->other_num);
383 xbt_dynar_remove_at(visited_pairs, (min + res) - 1, NULL);
384 xbt_dynar_insert_at(visited_pairs, (min+res) - 1, &pair);
385 pair_test->visited_removed = 1;
386 if(pair_test->stack_removed && pair_test->visited_removed){
387 if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
388 if(pair_test->acceptance_removed){
389 MC_pair_delete(pair_test);
392 MC_pair_delete(pair_test);
397 return pair->other_num;
400 while (cursor <= max) {
402 (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, cursor,
404 //if(pair_test->acceptance_pair == 0){ /* Acceptance pair have been already checked before */
405 if (xbt_automaton_state_compare
406 (pair_test->automaton_state, new_pair->automaton_state) == 0) {
407 if (xbt_automaton_propositional_symbols_compare_value
408 (pair_test->atomic_propositions,
409 new_pair->atomic_propositions) == 0) {
410 if (snapshot_compare(pair_test, new_pair) == 0) {
411 if (pair_test->other_num == -1)
412 new_pair->other_num = pair_test->num;
414 new_pair->other_num = pair_test->other_num;
415 if (dot_output == NULL)
416 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)",
417 new_pair->num, pair_test->num);
420 ("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))",
421 new_pair->num, pair_test->num, new_pair->other_num);
422 xbt_dynar_remove_at(visited_pairs, cursor, NULL);
423 xbt_dynar_insert_at(visited_pairs, cursor, &new_pair);
424 pair_test->visited_removed = 1;
425 if (pair_test->acceptance_pair) {
426 if (pair_test->acceptance_removed == 1)
427 MC_visited_pair_delete(pair_test);
429 MC_visited_pair_delete(pair_test);
433 return new_pair->other_num;
440 xbt_dynar_insert_at(visited_pairs, min, &new_pair);
443 (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, index,
445 if (pair_test->nb_processes < new_pair->nb_processes) {
446 xbt_dynar_insert_at(visited_pairs, index + 1, &new_pair);
448 if (pair_test->heap_bytes_used < new_pair->heap_bytes_used)
449 xbt_dynar_insert_at(visited_pairs, index + 1, &new_pair);
451 xbt_dynar_insert_at(visited_pairs, index, &new_pair);
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) {
462 min2 = pair_test->num;
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);
471 MC_visited_pair_delete(pair_test);