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. */
10 #include "mc_comm_pattern.h"
11 #include "mc_safety.h"
12 #include "mc_liveness.h"
13 #include "mc_private.h"
15 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_visited, mc,
16 "Logging specific to state equaity detection mechanisms");
18 xbt_dynar_t visited_pairs;
19 xbt_dynar_t visited_states;
21 void visited_state_free(mc_visited_state_t state)
24 MC_free_snapshot(state->system_state);
29 void visited_state_free_voidp(void *s)
31 visited_state_free((mc_visited_state_t) * (void **) s);
35 * \brief Save the current state
36 * \return Snapshot of the current state.
38 static mc_visited_state_t visited_state_new()
40 mc_process_t process = &(mc_model_checker->process);
41 mc_visited_state_t new_state = NULL;
42 new_state = xbt_new0(s_mc_visited_state_t, 1);
43 new_state->heap_bytes_used = mmalloc_get_bytes_used_remote(
44 MC_process_get_heap(process)->heaplimit,
45 MC_process_get_malloc_info(process));
46 new_state->nb_processes = xbt_swag_size(simix_global->process_list);
47 new_state->system_state = MC_take_snapshot(mc_stats->expanded_states);
48 new_state->num = mc_stats->expanded_states;
49 new_state->other_num = -1;
54 mc_visited_pair_t MC_visited_pair_new(int pair_num,
55 xbt_automaton_state_t automaton_state,
56 xbt_dynar_t atomic_propositions)
58 mc_process_t process = &(mc_model_checker->process);
59 mc_visited_pair_t pair = NULL;
60 pair = xbt_new0(s_mc_visited_pair_t, 1);
61 pair->graph_state = MC_state_new();
62 pair->graph_state->system_state = MC_take_snapshot(pair_num);
63 pair->heap_bytes_used = mmalloc_get_bytes_used_remote(
64 MC_process_get_heap(process)->heaplimit,
65 MC_process_get_malloc_info(process));
66 pair->nb_processes = xbt_swag_size(simix_global->process_list);
67 pair->automaton_state = automaton_state;
70 pair->acceptance_removed = 0;
71 pair->visited_removed = 0;
72 pair->acceptance_pair = 0;
73 pair->atomic_propositions = xbt_dynar_new(sizeof(int), NULL);
74 unsigned int cursor = 0;
76 xbt_dynar_foreach(atomic_propositions, cursor, value)
77 xbt_dynar_push_as(pair->atomic_propositions, int, value);
81 void MC_visited_pair_delete(mc_visited_pair_t p)
83 p->automaton_state = NULL;
84 MC_state_delete(p->graph_state);
85 xbt_dynar_free(&(p->atomic_propositions));
91 * \brief Find a suitable subrange of candidate duplicates for a given state
92 * \param list dynamic array of states/pairs with candidate duplicates of the current state;
93 * \param ref current state/pair;
94 * \param min (output) index of the beginning of the the subrange
95 * \param max (output) index of the enf of the subrange
97 * Given a suitably ordered array of states/pairs, this function extracts a subrange
98 * (with index *min <= i <= *max) with candidate duplicates of the given state/pair.
99 * This function uses only fast discriminating criterions and does not use the
100 * full state/pair comparison algorithms.
102 * The states/pairs in list MUST be ordered using a (given) weak order
103 * (based on nb_processes and heap_bytes_used).
104 * The subrange is the subrange of "equivalence" of the given state/pair.
106 int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max)
109 xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
111 int cursor = 0, previous_cursor, next_cursor;
112 int nb_processes, heap_bytes_used, nb_processes_test, heap_bytes_used_test;
115 if (_sg_mc_liveness) {
116 nb_processes = ((mc_visited_pair_t) ref)->nb_processes;
117 heap_bytes_used = ((mc_visited_pair_t) ref)->heap_bytes_used;
119 nb_processes = ((mc_visited_state_t) ref)->nb_processes;
120 heap_bytes_used = ((mc_visited_state_t) ref)->heap_bytes_used;
124 int end = xbt_dynar_length(list) - 1;
126 while (start <= end) {
127 cursor = (start + end) / 2;
128 if (_sg_mc_liveness) {
130 (mc_visited_pair_t) xbt_dynar_get_as(list, cursor, mc_visited_pair_t);
131 nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
132 heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
135 (mc_visited_state_t) xbt_dynar_get_as(list, cursor,
137 nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
138 heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
140 if (nb_processes_test < nb_processes) {
142 } else if (nb_processes_test > nb_processes) {
145 if (heap_bytes_used_test < heap_bytes_used) {
147 } else if (heap_bytes_used_test > heap_bytes_used) {
150 *min = *max = cursor;
151 previous_cursor = cursor - 1;
152 while (previous_cursor >= 0) {
153 if (_sg_mc_liveness) {
155 (mc_visited_pair_t) xbt_dynar_get_as(list, previous_cursor,
157 nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
158 heap_bytes_used_test =
159 ((mc_visited_pair_t) ref_test)->heap_bytes_used;
162 (mc_visited_state_t) xbt_dynar_get_as(list, previous_cursor,
164 nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
165 heap_bytes_used_test =
166 ((mc_visited_state_t) ref_test)->heap_bytes_used;
168 if (nb_processes_test != nb_processes
169 || heap_bytes_used_test != heap_bytes_used)
171 *min = previous_cursor;
174 next_cursor = cursor + 1;
175 while (next_cursor < xbt_dynar_length(list)) {
176 if (_sg_mc_liveness) {
178 (mc_visited_pair_t) xbt_dynar_get_as(list, next_cursor,
180 nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
181 heap_bytes_used_test =
182 ((mc_visited_pair_t) ref_test)->heap_bytes_used;
185 (mc_visited_state_t) xbt_dynar_get_as(list, next_cursor,
187 nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
188 heap_bytes_used_test =
189 ((mc_visited_state_t) ref_test)->heap_bytes_used;
191 if (nb_processes_test != nb_processes
192 || heap_bytes_used_test != heap_bytes_used)
197 mmalloc_set_current_heap(heap);
203 mmalloc_set_current_heap(heap);
209 * \brief Checks whether a given state has already been visited by the algorithm.
212 mc_visited_state_t is_visited_state()
215 if (_sg_mc_visited == 0)
218 /* If comm determinism verification, we cannot stop the exploration if some
219 communications are not finished (at least, data are transfered). These communications
220 are incomplete and they cannot be analyzed and compared with the initial pattern */
221 if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
222 int current_process = 1;
223 while (current_process < simix_process_maxpid) {
224 if (!xbt_dynar_is_empty((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t)))
230 xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
232 mc_visited_state_t new_state = visited_state_new();
234 if (xbt_dynar_is_empty(visited_states)) {
236 xbt_dynar_push(visited_states, &new_state);
237 mmalloc_set_current_heap(heap);
242 int min = -1, max = -1, index;
244 mc_visited_state_t state_test;
247 index = get_search_interval(visited_states, new_state, &min, &max);
249 if (min != -1 && max != -1) {
251 // Parallell implementation
252 /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_states, min), (max-min)+1, new_state);
254 state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, (min+res)-1, mc_visited_state_t);
255 if(state_test->other_num == -1)
256 new_state->other_num = state_test->num;
258 new_state->other_num = state_test->other_num;
259 if(dot_output == NULL)
260 XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
262 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);
263 xbt_dynar_remove_at(visited_states, (min + res) - 1, NULL);
264 xbt_dynar_insert_at(visited_states, (min+res) - 1, &new_state);
267 return new_state->other_num;
271 while (cursor <= max) {
273 (mc_visited_state_t) xbt_dynar_get_as(visited_states, cursor,
275 if (snapshot_compare(state_test, new_state) == 0) {
276 // The state has been visited:
278 if (state_test->other_num == -1)
279 new_state->other_num = state_test->num;
281 new_state->other_num = state_test->other_num;
282 if (dot_output == NULL)
283 XBT_DEBUG("State %d already visited ! (equal to state %d)",
284 new_state->num, state_test->num);
287 ("State %d already visited ! (equal to state %d (state %d in dot_output))",
288 new_state->num, state_test->num, new_state->other_num);
290 /* Replace the old state with the new one (with a bigger num)
291 (when the max number of visited states is reached, the oldest
292 one is removed according to its number (= with the min number) */
293 xbt_dynar_remove_at(visited_states, cursor, NULL);
294 xbt_dynar_insert_at(visited_states, cursor, &new_state);
296 mmalloc_set_current_heap(heap);
302 // The state has not been visited: insert the state in the dynamic array.
303 xbt_dynar_insert_at(visited_states, min, &new_state);
307 // The state has not been visited: insert the state in the dynamic array.
309 (mc_visited_state_t) xbt_dynar_get_as(visited_states, index,
311 if (state_test->nb_processes < new_state->nb_processes) {
312 xbt_dynar_insert_at(visited_states, index + 1, &new_state);
314 if (state_test->heap_bytes_used < new_state->heap_bytes_used)
315 xbt_dynar_insert_at(visited_states, index + 1, &new_state);
317 xbt_dynar_insert_at(visited_states, index, &new_state);
322 // We have reached the maximum number of stored states;
323 if (xbt_dynar_length(visited_states) > _sg_mc_visited) {
325 // Find the (index of the) older state (with the smallest num):
326 int min2 = mc_stats->expanded_states;
327 unsigned int cursor2 = 0;
328 unsigned int index2 = 0;
329 xbt_dynar_foreach(visited_states, cursor2, state_test){
330 if (!mc_important_snapshot(state_test->system_state) && state_test->num < min2) {
332 min2 = state_test->num;
337 xbt_dynar_remove_at(visited_states, index2, NULL);
340 mmalloc_set_current_heap(heap);
346 * \brief Checks whether a given pair has already been visited by the algorithm.
348 int is_visited_pair(mc_visited_pair_t pair, int pair_num,
349 xbt_automaton_state_t automaton_state,
350 xbt_dynar_t atomic_propositions)
353 if (_sg_mc_visited == 0)
356 xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
358 mc_visited_pair_t new_pair = NULL;
362 MC_visited_pair_new(pair_num, automaton_state, atomic_propositions);
367 if (xbt_dynar_is_empty(visited_pairs)) {
369 xbt_dynar_push(visited_pairs, &new_pair);
373 int min = -1, max = -1, index;
375 mc_visited_pair_t pair_test;
378 index = get_search_interval(visited_pairs, new_pair, &min, &max);
380 if (min != -1 && max != -1) { // Visited pair with same number of processes and same heap bytes used exists
381 /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_pairs, min), (max-min)+1, pair);
383 pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, (min+res)-1, mc_pair_t);
384 if(pair_test->other_num == -1)
385 pair->other_num = pair_test->num;
387 pair->other_num = pair_test->other_num;
388 if(dot_output == NULL)
389 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", pair->num, pair_test->num);
391 XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", pair->num, pair_test->num, pair->other_num);
392 xbt_dynar_remove_at(visited_pairs, (min + res) - 1, NULL);
393 xbt_dynar_insert_at(visited_pairs, (min+res) - 1, &pair);
394 pair_test->visited_removed = 1;
395 if(pair_test->stack_removed && pair_test->visited_removed){
396 if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
397 if(pair_test->acceptance_removed){
398 MC_pair_delete(pair_test);
401 MC_pair_delete(pair_test);
406 return pair->other_num;
409 while (cursor <= max) {
411 (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, cursor,
413 if (xbt_automaton_state_compare
414 (pair_test->automaton_state, new_pair->automaton_state) == 0) {
415 if (xbt_automaton_propositional_symbols_compare_value
416 (pair_test->atomic_propositions,
417 new_pair->atomic_propositions) == 0) {
418 if (snapshot_compare(pair_test, new_pair) == 0) {
419 if (pair_test->other_num == -1)
420 new_pair->other_num = pair_test->num;
422 new_pair->other_num = pair_test->other_num;
423 if (dot_output == NULL)
424 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)",
425 new_pair->num, pair_test->num);
428 ("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))",
429 new_pair->num, pair_test->num, new_pair->other_num);
430 xbt_dynar_remove_at(visited_pairs, cursor, NULL);
431 xbt_dynar_insert_at(visited_pairs, cursor, &new_pair);
432 pair_test->visited_removed = 1;
433 if (pair_test->acceptance_pair) {
434 if (pair_test->acceptance_removed == 1)
435 MC_visited_pair_delete(pair_test);
437 MC_visited_pair_delete(pair_test);
439 mmalloc_set_current_heap(heap);
440 return new_pair->other_num;
446 xbt_dynar_insert_at(visited_pairs, min, &new_pair);
449 (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, index,
451 if (pair_test->nb_processes < new_pair->nb_processes) {
452 xbt_dynar_insert_at(visited_pairs, index + 1, &new_pair);
454 if (pair_test->heap_bytes_used < new_pair->heap_bytes_used)
455 xbt_dynar_insert_at(visited_pairs, index + 1, &new_pair);
457 xbt_dynar_insert_at(visited_pairs, index, &new_pair);
461 if (xbt_dynar_length(visited_pairs) > _sg_mc_visited) {
462 int min2 = mc_stats->expanded_pairs;
463 unsigned int cursor2 = 0;
464 unsigned int index2 = 0;
465 xbt_dynar_foreach(visited_pairs, cursor2, pair_test) {
466 if (!mc_important_snapshot(pair_test->graph_state->system_state) && pair_test->num < min2) {
468 min2 = pair_test->num;
471 xbt_dynar_remove_at(visited_pairs, index2, &pair_test);
472 pair_test->visited_removed = 1;
473 if (pair_test->acceptance_pair) {
474 if (pair_test->acceptance_removed)
475 MC_visited_pair_delete(pair_test);
477 MC_visited_pair_delete(pair_test);
483 mmalloc_set_current_heap(heap);