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)
150 int cursor = 0, previous_cursor;
151 int nb_processes, heap_bytes_used, nb_processes_test, heap_bytes_used_test;
154 if (_sg_mc_liveness) {
155 nb_processes = ((mc_visited_pair_t) ref)->nb_processes;
156 heap_bytes_used = ((mc_visited_pair_t) ref)->heap_bytes_used;
158 nb_processes = ((mc_visited_state_t) ref)->nb_processes;
159 heap_bytes_used = ((mc_visited_state_t) ref)->heap_bytes_used;
163 int end = xbt_dynar_length(list) - 1;
165 while (start <= end) {
166 cursor = (start + end) / 2;
167 if (_sg_mc_liveness) {
168 ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, cursor, mc_visited_pair_t);
169 nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
170 heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
172 ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, cursor, mc_visited_state_t);
173 nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
174 heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
176 if (nb_processes_test < nb_processes) {
178 } else if (nb_processes_test > nb_processes) {
181 if (heap_bytes_used_test < heap_bytes_used) {
183 } else if (heap_bytes_used_test > heap_bytes_used) {
186 *min = *max = cursor;
187 previous_cursor = cursor - 1;
188 while (previous_cursor >= 0) {
189 if (_sg_mc_liveness) {
190 ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, previous_cursor, mc_visited_pair_t);
191 nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
192 heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
194 ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, previous_cursor, mc_visited_state_t);
195 nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
196 heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
198 if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used)
200 *min = previous_cursor;
203 size_t next_cursor = cursor + 1;
204 while (next_cursor < xbt_dynar_length(list)) {
205 if (_sg_mc_liveness) {
206 ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, next_cursor, mc_visited_pair_t);
207 nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
208 heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
210 ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, next_cursor, mc_visited_state_t);
211 nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
212 heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
214 if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used)
228 * \brief Checks whether a given state has already been visited by the algorithm.
231 mc_visited_state_t is_visited_state(mc_state_t graph_state)
234 if (_sg_mc_visited == 0)
237 int partial_comm = 0;
239 /* If comm determinism verification, we cannot stop the exploration if some
240 communications are not finished (at least, data are transfered). These communications
241 are incomplete and they cannot be analyzed and compared with the initial pattern. */
242 if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
243 size_t current_process = 1;
244 while (current_process < MC_smx_get_maxpid()) {
245 if (!xbt_dynar_is_empty((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t))){
246 XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
254 mc_visited_state_t new_state = visited_state_new();
255 graph_state->system_state = new_state->system_state;
256 graph_state->in_visited_states = 1;
257 XBT_DEBUG("Snapshot %p of visited state %d (exploration stack state %d)", new_state->system_state, new_state->num, graph_state->num);
259 if (xbt_dynar_is_empty(visited_states)) {
261 xbt_dynar_push(visited_states, &new_state);
266 int min = -1, max = -1, index;
268 mc_visited_state_t state_test;
271 index = get_search_interval(visited_states, new_state, &min, &max);
273 if (min != -1 && max != -1) {
275 // Parallell implementation
276 /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_states, min), (max-min)+1, new_state);
278 state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, (min+res)-1, mc_visited_state_t);
279 if(state_test->other_num == -1)
280 new_state->other_num = state_test->num;
282 new_state->other_num = state_test->other_num;
283 if(dot_output == NULL)
284 XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
286 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);
287 xbt_dynar_remove_at(visited_states, (min + res) - 1, NULL);
288 xbt_dynar_insert_at(visited_states, (min+res) - 1, &new_state);
289 return new_state->other_num;
292 if (_sg_mc_safety || (!partial_comm
293 && initial_global_state->initial_communications_pattern_done)) {
296 while (cursor <= max) {
297 state_test = (mc_visited_state_t) xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t);
298 if (snapshot_compare(state_test, new_state) == 0) {
299 // The state has been visited:
301 if (state_test->other_num == -1)
302 new_state->other_num = state_test->num;
304 new_state->other_num = state_test->other_num;
305 if (dot_output == NULL)
306 XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
308 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);
310 /* Replace the old state with the new one (with a bigger num)
311 (when the max number of visited states is reached, the oldest
312 one is removed according to its number (= with the min number) */
313 xbt_dynar_remove_at(visited_states, cursor, NULL);
314 xbt_dynar_insert_at(visited_states, cursor, &new_state);
315 XBT_DEBUG("Replace visited state %d with the new visited state %d", state_test->num, new_state->num);
323 xbt_dynar_insert_at(visited_states, min, &new_state);
324 XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, xbt_dynar_length(visited_states));
328 // The state has not been visited: insert the state in the dynamic array.
329 state_test = (mc_visited_state_t) xbt_dynar_get_as(visited_states, index, mc_visited_state_t);
330 if (state_test->nb_processes < new_state->nb_processes) {
331 xbt_dynar_insert_at(visited_states, index + 1, &new_state);
333 if (state_test->heap_bytes_used < new_state->heap_bytes_used)
334 xbt_dynar_insert_at(visited_states, index + 1, &new_state);
336 xbt_dynar_insert_at(visited_states, index, &new_state);
339 XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, xbt_dynar_length(visited_states));
343 // We have reached the maximum number of stored states;
344 if ((ssize_t) xbt_dynar_length(visited_states) > _sg_mc_visited) {
346 XBT_DEBUG("Try to remove visited state (maximum number of stored states reached)");
348 // Find the (index of the) older state (with the smallest num):
349 int min2 = mc_stats->expanded_states;
350 unsigned int cursor2 = 0;
351 unsigned int index2 = 0;
352 xbt_dynar_foreach(visited_states, cursor2, state_test){
353 if (state_test->num < min2) {
355 min2 = state_test->num;
360 xbt_dynar_remove_at(visited_states, index2, NULL);
361 XBT_DEBUG("Remove visited state (maximum number of stored states reached)");
369 * \brief Checks whether a given pair has already been visited by the algorithm.
371 int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair) {
373 if (_sg_mc_visited == 0)
376 mc_visited_pair_t new_visited_pair = NULL;
378 if (visited_pair == NULL) {
379 new_visited_pair = MC_visited_pair_new(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state);
381 new_visited_pair = visited_pair;
384 if (xbt_dynar_is_empty(visited_pairs)) {
386 xbt_dynar_push(visited_pairs, &new_visited_pair);
390 int min = -1, max = -1, index;
392 mc_visited_pair_t pair_test;
395 index = get_search_interval(visited_pairs, new_visited_pair, &min, &max);
397 if (min != -1 && max != -1) { // Visited pair with same number of processes and same heap bytes used exists
398 /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_pairs, min), (max-min)+1, pair);
400 pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, (min+res)-1, mc_pair_t);
401 if(pair_test->other_num == -1)
402 pair->other_num = pair_test->num;
404 pair->other_num = pair_test->other_num;
405 if(dot_output == NULL)
406 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", pair->num, pair_test->num);
408 XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", pair->num, pair_test->num, pair->other_num);
409 xbt_dynar_remove_at(visited_pairs, (min + res) - 1, NULL);
410 xbt_dynar_insert_at(visited_pairs, (min+res) - 1, &pair);
411 pair_test->visited_removed = 1;
412 if(pair_test->stack_removed && pair_test->visited_removed){
413 if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
414 if(pair_test->acceptance_removed){
415 MC_pair_delete(pair_test);
418 MC_pair_delete(pair_test);
421 return pair->other_num;
424 while (cursor <= max) {
425 pair_test = (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, cursor, mc_visited_pair_t);
426 if (xbt_automaton_state_compare(pair_test->automaton_state, new_visited_pair->automaton_state) == 0) {
427 if (xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, new_visited_pair->atomic_propositions) == 0) {
428 if (snapshot_compare(pair_test, new_visited_pair) == 0) {
429 if (pair_test->other_num == -1)
430 new_visited_pair->other_num = pair_test->num;
432 new_visited_pair->other_num = pair_test->other_num;
433 if (dot_output == NULL)
434 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_visited_pair->num, pair_test->num);
436 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);
437 xbt_dynar_remove_at(visited_pairs, cursor, &pair_test);
438 xbt_dynar_insert_at(visited_pairs, cursor, &new_visited_pair);
439 pair_test->visited_removed = 1;
440 if (pair_test->acceptance_pair) {
441 if (pair_test->acceptance_removed == 1)
442 MC_visited_pair_delete(pair_test);
444 MC_visited_pair_delete(pair_test);
446 return new_visited_pair->other_num;
452 xbt_dynar_insert_at(visited_pairs, min, &new_visited_pair);
454 pair_test = (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, index, mc_visited_pair_t);
455 if (pair_test->nb_processes < new_visited_pair->nb_processes) {
456 xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
458 if (pair_test->heap_bytes_used < new_visited_pair->heap_bytes_used)
459 xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
461 xbt_dynar_insert_at(visited_pairs, index, &new_visited_pair);
465 if ((ssize_t) xbt_dynar_length(visited_pairs) > _sg_mc_visited) {
466 int min2 = mc_stats->expanded_pairs;
467 unsigned int cursor2 = 0;
468 unsigned int index2 = 0;
469 xbt_dynar_foreach(visited_pairs, cursor2, pair_test) {
470 if (pair_test->num < min2) {
472 min2 = pair_test->num;
475 xbt_dynar_remove_at(visited_pairs, index2, &pair_test);
476 pair_test->visited_removed = 1;
477 if (pair_test->acceptance_pair) {
478 if (pair_test->acceptance_removed)
479 MC_visited_pair_delete(pair_test);
481 MC_visited_pair_delete(pair_test);