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"
14 #include "mc_process.h"
19 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_visited, mc,
20 "Logging specific to state equaity detection mechanisms");
22 xbt_dynar_t visited_pairs;
23 xbt_dynar_t visited_states;
25 static int is_exploration_stack_state(mc_visited_state_t state){
26 xbt_fifo_item_t item = xbt_fifo_get_first_item(mc_stack);
28 if (((mc_state_t)xbt_fifo_get_item_content(item))->num == state->num){
29 ((mc_state_t)xbt_fifo_get_item_content(item))->in_visited_states = 0;
32 item = xbt_fifo_get_next_item(item);
37 void visited_state_free(mc_visited_state_t state)
40 if(!is_exploration_stack_state(state)){
41 MC_free_snapshot(state->system_state);
47 void visited_state_free_voidp(void *s)
49 visited_state_free((mc_visited_state_t) * (void **) s);
53 * \brief Save the current state
54 * \return Snapshot of the current state.
56 static mc_visited_state_t visited_state_new()
58 mc_process_t process = &(mc_model_checker->process);
59 mc_visited_state_t new_state = xbt_new0(s_mc_visited_state_t, 1);
60 new_state->heap_bytes_used = mmalloc_get_bytes_used_remote(
61 MC_process_get_heap(process)->heaplimit,
62 MC_process_get_malloc_info(process));
64 if (MC_process_is_self(&mc_model_checker->process)) {
65 new_state->nb_processes = xbt_swag_size(simix_global->process_list);
67 MC_process_smx_refresh(&mc_model_checker->process);
68 new_state->nb_processes = xbt_dynar_length(
69 mc_model_checker->process.smx_process_infos);
72 new_state->system_state = MC_take_snapshot(mc_stats->expanded_states);
73 new_state->num = mc_stats->expanded_states;
74 new_state->other_num = -1;
78 mc_visited_pair_t MC_visited_pair_new(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, mc_state_t graph_state)
80 mc_process_t process = &(mc_model_checker->process);
81 mc_visited_pair_t pair = NULL;
82 pair = xbt_new0(s_mc_visited_pair_t, 1);
83 pair->graph_state = graph_state;
84 if(pair->graph_state->system_state == NULL)
85 pair->graph_state->system_state = MC_take_snapshot(pair_num);
86 pair->heap_bytes_used = mmalloc_get_bytes_used_remote(
87 MC_process_get_heap(process)->heaplimit,
88 MC_process_get_malloc_info(process));
89 if (MC_process_is_self(&mc_model_checker->process)) {
90 pair->nb_processes = xbt_swag_size(simix_global->process_list);
92 MC_process_smx_refresh(&mc_model_checker->process);
93 pair->nb_processes = xbt_dynar_length(
94 mc_model_checker->process.smx_process_infos);
96 pair->automaton_state = automaton_state;
99 pair->acceptance_removed = 0;
100 pair->visited_removed = 0;
101 pair->acceptance_pair = 0;
102 pair->atomic_propositions = xbt_dynar_new(sizeof(int), NULL);
103 unsigned int cursor = 0;
105 xbt_dynar_foreach(atomic_propositions, cursor, value)
106 xbt_dynar_push_as(pair->atomic_propositions, int, value);
110 static int is_exploration_stack_pair(mc_visited_pair_t pair){
111 xbt_fifo_item_t item = xbt_fifo_get_first_item(mc_stack);
113 if (((mc_pair_t)xbt_fifo_get_item_content(item))->num == pair->num){
114 ((mc_pair_t)xbt_fifo_get_item_content(item))->visited_pair_removed = 1;
117 item = xbt_fifo_get_next_item(item);
122 void MC_visited_pair_delete(mc_visited_pair_t p)
124 p->automaton_state = NULL;
125 if( !is_exploration_stack_pair(p))
126 MC_state_delete(p->graph_state, 1);
127 xbt_dynar_free(&(p->atomic_propositions));
133 * \brief Find a suitable subrange of candidate duplicates for a given state
134 * \param list dynamic array of states/pairs with candidate duplicates of the current state;
135 * \param ref current state/pair;
136 * \param min (output) index of the beginning of the the subrange
137 * \param max (output) index of the enf of the subrange
139 * Given a suitably ordered array of states/pairs, this function extracts a subrange
140 * (with index *min <= i <= *max) with candidate duplicates of the given state/pair.
141 * This function uses only fast discriminating criterions and does not use the
142 * full state/pair comparison algorithms.
144 * The states/pairs in list MUST be ordered using a (given) weak order
145 * (based on nb_processes and heap_bytes_used).
146 * The subrange is the subrange of "equivalence" of the given state/pair.
148 int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max)
151 xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
153 int cursor = 0, previous_cursor;
154 int nb_processes, heap_bytes_used, nb_processes_test, heap_bytes_used_test;
157 if (_sg_mc_liveness) {
158 nb_processes = ((mc_visited_pair_t) ref)->nb_processes;
159 heap_bytes_used = ((mc_visited_pair_t) ref)->heap_bytes_used;
161 nb_processes = ((mc_visited_state_t) ref)->nb_processes;
162 heap_bytes_used = ((mc_visited_state_t) ref)->heap_bytes_used;
166 int end = xbt_dynar_length(list) - 1;
168 while (start <= end) {
169 cursor = (start + end) / 2;
170 if (_sg_mc_liveness) {
171 ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, cursor, mc_visited_pair_t);
172 nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
173 heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
175 ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, cursor, mc_visited_state_t);
176 nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
177 heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
179 if (nb_processes_test < nb_processes) {
181 } else if (nb_processes_test > nb_processes) {
184 if (heap_bytes_used_test < heap_bytes_used) {
186 } else if (heap_bytes_used_test > heap_bytes_used) {
189 *min = *max = cursor;
190 previous_cursor = cursor - 1;
191 while (previous_cursor >= 0) {
192 if (_sg_mc_liveness) {
193 ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, previous_cursor, mc_visited_pair_t);
194 nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
195 heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
197 ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, previous_cursor, mc_visited_state_t);
198 nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
199 heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
201 if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used)
203 *min = previous_cursor;
206 size_t next_cursor = cursor + 1;
207 while (next_cursor < xbt_dynar_length(list)) {
208 if (_sg_mc_liveness) {
209 ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, next_cursor, mc_visited_pair_t);
210 nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
211 heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
213 ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, next_cursor, mc_visited_state_t);
214 nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
215 heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
217 if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used)
222 mmalloc_set_current_heap(heap);
228 mmalloc_set_current_heap(heap);
234 * \brief Checks whether a given state has already been visited by the algorithm.
237 mc_visited_state_t is_visited_state(mc_state_t graph_state)
240 if (_sg_mc_visited == 0)
243 int partial_comm = 0;
245 /* If comm determinism verification, we cannot stop the exploration if some
246 communications are not finished (at least, data are transfered). These communications
247 are incomplete and they cannot be analyzed and compared with the initial pattern. */
248 if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
249 size_t current_process = 1;
250 while (current_process < MC_smx_get_maxpid()) {
251 if (!xbt_dynar_is_empty((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t))){
252 XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
260 xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
262 mc_visited_state_t new_state = visited_state_new();
263 graph_state->system_state = new_state->system_state;
264 graph_state->in_visited_states = 1;
265 XBT_DEBUG("Snapshot %p of visited state %d (exploration stack state %d)", new_state->system_state, new_state->num, graph_state->num);
267 if (xbt_dynar_is_empty(visited_states)) {
269 xbt_dynar_push(visited_states, &new_state);
270 mmalloc_set_current_heap(heap);
275 int min = -1, max = -1, index;
277 mc_visited_state_t state_test;
280 index = get_search_interval(visited_states, new_state, &min, &max);
282 if (min != -1 && max != -1) {
284 // Parallell implementation
285 /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_states, min), (max-min)+1, new_state);
287 state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, (min+res)-1, mc_visited_state_t);
288 if(state_test->other_num == -1)
289 new_state->other_num = state_test->num;
291 new_state->other_num = state_test->other_num;
292 if(dot_output == NULL)
293 XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
295 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);
296 xbt_dynar_remove_at(visited_states, (min + res) - 1, NULL);
297 xbt_dynar_insert_at(visited_states, (min+res) - 1, &new_state);
300 return new_state->other_num;
303 if (_sg_mc_safety || (!partial_comm
304 && initial_global_state->initial_communications_pattern_done)) {
307 while (cursor <= max) {
308 state_test = (mc_visited_state_t) xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t);
309 if (snapshot_compare(state_test, new_state) == 0) {
310 // The state has been visited:
312 if (state_test->other_num == -1)
313 new_state->other_num = state_test->num;
315 new_state->other_num = state_test->other_num;
316 if (dot_output == NULL)
317 XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
319 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);
321 /* Replace the old state with the new one (with a bigger num)
322 (when the max number of visited states is reached, the oldest
323 one is removed according to its number (= with the min number) */
324 xbt_dynar_remove_at(visited_states, cursor, NULL);
325 xbt_dynar_insert_at(visited_states, cursor, &new_state);
326 XBT_DEBUG("Replace visited state %d with the new visited state %d", state_test->num, new_state->num);
328 mmalloc_set_current_heap(heap);
335 xbt_dynar_insert_at(visited_states, min, &new_state);
336 XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, xbt_dynar_length(visited_states));
340 // The state has not been visited: insert the state in the dynamic array.
341 state_test = (mc_visited_state_t) xbt_dynar_get_as(visited_states, index, mc_visited_state_t);
342 if (state_test->nb_processes < new_state->nb_processes) {
343 xbt_dynar_insert_at(visited_states, index + 1, &new_state);
345 if (state_test->heap_bytes_used < new_state->heap_bytes_used)
346 xbt_dynar_insert_at(visited_states, index + 1, &new_state);
348 xbt_dynar_insert_at(visited_states, index, &new_state);
351 XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, xbt_dynar_length(visited_states));
355 // We have reached the maximum number of stored states;
356 if ((ssize_t) xbt_dynar_length(visited_states) > _sg_mc_visited) {
358 XBT_DEBUG("Try to remove visited state (maximum number of stored states reached)");
360 // Find the (index of the) older state (with the smallest num):
361 int min2 = mc_stats->expanded_states;
362 unsigned int cursor2 = 0;
363 unsigned int index2 = 0;
364 xbt_dynar_foreach(visited_states, cursor2, state_test){
365 if (!mc_important_snapshot(state_test->system_state) && state_test->num < min2) {
367 min2 = state_test->num;
372 xbt_dynar_remove_at(visited_states, index2, NULL);
373 XBT_DEBUG("Remove visited state (maximum number of stored states reached)");
376 mmalloc_set_current_heap(heap);
382 * \brief Checks whether a given pair has already been visited by the algorithm.
384 int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair) {
386 if (_sg_mc_visited == 0)
389 xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
391 mc_visited_pair_t new_visited_pair = NULL;
393 if (visited_pair == NULL) {
394 new_visited_pair = MC_visited_pair_new(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state);
396 new_visited_pair = visited_pair;
399 if (xbt_dynar_is_empty(visited_pairs)) {
401 xbt_dynar_push(visited_pairs, &new_visited_pair);
405 int min = -1, max = -1, index;
407 mc_visited_pair_t pair_test;
410 index = get_search_interval(visited_pairs, new_visited_pair, &min, &max);
412 if (min != -1 && max != -1) { // Visited pair with same number of processes and same heap bytes used exists
413 /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_pairs, min), (max-min)+1, pair);
415 pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, (min+res)-1, mc_pair_t);
416 if(pair_test->other_num == -1)
417 pair->other_num = pair_test->num;
419 pair->other_num = pair_test->other_num;
420 if(dot_output == NULL)
421 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", pair->num, pair_test->num);
423 XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", pair->num, pair_test->num, pair->other_num);
424 xbt_dynar_remove_at(visited_pairs, (min + res) - 1, NULL);
425 xbt_dynar_insert_at(visited_pairs, (min+res) - 1, &pair);
426 pair_test->visited_removed = 1;
427 if(pair_test->stack_removed && pair_test->visited_removed){
428 if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
429 if(pair_test->acceptance_removed){
430 MC_pair_delete(pair_test);
433 MC_pair_delete(pair_test);
438 return pair->other_num;
441 while (cursor <= max) {
442 pair_test = (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, cursor, mc_visited_pair_t);
443 if (xbt_automaton_state_compare(pair_test->automaton_state, new_visited_pair->automaton_state) == 0) {
444 if (xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, new_visited_pair->atomic_propositions) == 0) {
445 if (snapshot_compare(pair_test, new_visited_pair) == 0) {
446 if (pair_test->other_num == -1)
447 new_visited_pair->other_num = pair_test->num;
449 new_visited_pair->other_num = pair_test->other_num;
450 if (dot_output == NULL)
451 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_visited_pair->num, pair_test->num);
453 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);
454 xbt_dynar_remove_at(visited_pairs, cursor, &pair_test);
455 xbt_dynar_insert_at(visited_pairs, cursor, &new_visited_pair);
456 pair_test->visited_removed = 1;
457 if (pair_test->acceptance_pair) {
458 if (pair_test->acceptance_removed == 1)
459 MC_visited_pair_delete(pair_test);
461 MC_visited_pair_delete(pair_test);
463 mmalloc_set_current_heap(heap);
464 return new_visited_pair->other_num;
470 xbt_dynar_insert_at(visited_pairs, min, &new_visited_pair);
472 pair_test = (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, index, mc_visited_pair_t);
473 if (pair_test->nb_processes < new_visited_pair->nb_processes) {
474 xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
476 if (pair_test->heap_bytes_used < new_visited_pair->heap_bytes_used)
477 xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
479 xbt_dynar_insert_at(visited_pairs, index, &new_visited_pair);
483 if ((ssize_t) xbt_dynar_length(visited_pairs) > _sg_mc_visited) {
484 int min2 = mc_stats->expanded_pairs;
485 unsigned int cursor2 = 0;
486 unsigned int index2 = 0;
487 xbt_dynar_foreach(visited_pairs, cursor2, pair_test) {
488 if (!mc_important_snapshot(pair_test->graph_state->system_state) && pair_test->num < min2) {
490 min2 = pair_test->num;
493 xbt_dynar_remove_at(visited_pairs, index2, &pair_test);
494 pair_test->visited_removed = 1;
495 if (pair_test->acceptance_pair) {
496 if (pair_test->acceptance_removed)
497 MC_visited_pair_delete(pair_test);
499 MC_visited_pair_delete(pair_test);
505 mmalloc_set_current_heap(heap);