X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/31f6ec7370f6689eed6b87f882dc578c9682b2e8..ff808eaaaeeb05dcbb4a26b7997c975db605b875:/src/mc/mc_visited.cpp diff --git a/src/mc/mc_visited.cpp b/src/mc/mc_visited.cpp index 80525901c7..11687b19d7 100644 --- a/src/mc/mc_visited.cpp +++ b/src/mc/mc_visited.cpp @@ -7,10 +7,14 @@ #include #include +#include +#include + #include #include #include #include +#include #include #include "src/mc/mc_comm_pattern.h" @@ -20,24 +24,15 @@ #include "src/mc/Process.hpp" #include "src/mc/mc_smx.h" -extern "C" { - XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_visited, mc, "Logging specific to state equaity detection mechanisms"); -} - namespace simgrid { namespace mc { -xbt_dynar_t visited_pairs; +std::vector> visited_states; -} -} - -xbt_dynar_t visited_states; - -static int is_exploration_stack_state(mc_visited_state_t state){ +static int is_exploration_stack_state(simgrid::mc::VisitedState* state){ xbt_fifo_item_t item = xbt_fifo_get_first_item(mc_stack); while (item) { if (((mc_state_t)xbt_fifo_get_item_content(item))->num == state->num){ @@ -49,44 +44,30 @@ static int is_exploration_stack_state(mc_visited_state_t state){ return 0; } -void visited_state_free(mc_visited_state_t state) -{ - if (!state) - return; - if(!is_exploration_stack_state(state)) - delete state->system_state; - xbt_free(state); -} - -void visited_state_free_voidp(void *s) -{ - visited_state_free((mc_visited_state_t) * (void **) s); -} - /** * \brief Save the current state * \return Snapshot of the current state. */ -static mc_visited_state_t visited_state_new() +VisitedState::VisitedState() { simgrid::mc::Process* process = &(mc_model_checker->process()); - mc_visited_state_t new_state = xbt_new0(s_mc_visited_state_t, 1); - new_state->heap_bytes_used = mmalloc_get_bytes_used_remote( + this->heap_bytes_used = mmalloc_get_bytes_used_remote( process->get_heap()->heaplimit, process->get_malloc_info()); - MC_process_smx_refresh(&mc_model_checker->process()); - new_state->nb_processes = - mc_model_checker->process().smx_process_infos.size(); + this->nb_processes = + mc_model_checker->process().simix_processes().size(); - new_state->system_state = simgrid::mc::take_snapshot(mc_stats->expanded_states); - new_state->num = mc_stats->expanded_states; - new_state->other_num = -1; - return new_state; + this->system_state = simgrid::mc::take_snapshot(mc_stats->expanded_states); + this->num = mc_stats->expanded_states; + this->other_num = -1; } -namespace simgrid { -namespace mc { +VisitedState::~VisitedState() +{ + if(!is_exploration_stack_state(this)) + delete this->system_state; +} VisitedPair::VisitedPair(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, mc_state_t graph_state) { @@ -99,9 +80,8 @@ VisitedPair::VisitedPair(int pair_num, xbt_automaton_state_t automaton_state, xb process->get_heap()->heaplimit, process->get_malloc_info()); - MC_process_smx_refresh(&mc_model_checker->process()); this->nb_processes = - mc_model_checker->process().smx_process_infos.size(); + mc_model_checker->process().simix_processes().size(); this->automaton_state = automaton_state; this->num = pair_num; @@ -139,126 +119,8 @@ VisitedPair::~VisitedPair() } } -/** - * \brief Find a suitable subrange of candidate duplicates for a given state - * \param list dynamic array of states/pairs with candidate duplicates of the current state; - * \param ref current state/pair; - * \param min (output) index of the beginning of the the subrange - * \param max (output) index of the enf of the subrange - * - * Given a suitably ordered array of states/pairs, this function extracts a subrange - * (with index *min <= i <= *max) with candidate duplicates of the given state/pair. - * This function uses only fast discriminating criterions and does not use the - * full state/pair comparison algorithms. - * - * The states/pairs in list MUST be ordered using a (given) weak order - * (based on nb_processes and heap_bytes_used). - * The subrange is the subrange of "equivalence" of the given state/pair. - */ -int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max) -{ - int cursor = 0, previous_cursor; - int nb_processes, heap_bytes_used, nb_processes_test, heap_bytes_used_test; - void *ref_test; - - if (_sg_mc_liveness) { - nb_processes = ((simgrid::mc::VisitedPair*) ref)->nb_processes; - heap_bytes_used = ((simgrid::mc::VisitedPair*) ref)->heap_bytes_used; - } else { - nb_processes = ((mc_visited_state_t) ref)->nb_processes; - heap_bytes_used = ((mc_visited_state_t) ref)->heap_bytes_used; - } - - int start = 0; - int end = xbt_dynar_length(list) - 1; - - while (start <= end) { - cursor = (start + end) / 2; - if (_sg_mc_liveness) { - ref_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(list, cursor, simgrid::mc::VisitedPair*); - nb_processes_test = ((simgrid::mc::VisitedPair*) ref_test)->nb_processes; - heap_bytes_used_test = ((simgrid::mc::VisitedPair*) ref_test)->heap_bytes_used; - } else { - ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, cursor, mc_visited_state_t); - nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes; - heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used; - } - if (nb_processes_test < nb_processes) - start = cursor + 1; - else if (nb_processes_test > nb_processes) - end = cursor - 1; - else if (heap_bytes_used_test < heap_bytes_used) - start = cursor + 1; - else if (heap_bytes_used_test > heap_bytes_used) - end = cursor - 1; - else { - *min = *max = cursor; - previous_cursor = cursor - 1; - while (previous_cursor >= 0) { - if (_sg_mc_liveness) { - ref_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(list, previous_cursor, simgrid::mc::VisitedPair*); - nb_processes_test = ((simgrid::mc::VisitedPair*) ref_test)->nb_processes; - heap_bytes_used_test = ((simgrid::mc::VisitedPair*) ref_test)->heap_bytes_used; - } else { - ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, previous_cursor, mc_visited_state_t); - nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes; - heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used; - } - if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used) - break; - *min = previous_cursor; - previous_cursor--; - } - size_t next_cursor = cursor + 1; - while (next_cursor < xbt_dynar_length(list)) { - if (_sg_mc_liveness) { - ref_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(list, next_cursor, simgrid::mc::VisitedPair*); - nb_processes_test = ((simgrid::mc::VisitedPair*) ref_test)->nb_processes; - heap_bytes_used_test = ((simgrid::mc::VisitedPair*) ref_test)->heap_bytes_used; - } else { - ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, next_cursor, mc_visited_state_t); - nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes; - heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used; - } - if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used) - break; - *max = next_cursor; - next_cursor++; - } - return -1; - } - } - return cursor; -} - -static -void replace_state( - mc_visited_state_t state_test, mc_visited_state_t new_state, int cursor) -{ - if (state_test->other_num == -1) - new_state->other_num = state_test->num; - else - new_state->other_num = state_test->other_num; - - if (dot_output == nullptr) - XBT_DEBUG("State %d already visited ! (equal to state %d)", - new_state->num, state_test->num); - else - 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); - - /* Replace the old state with the new one (with a bigger num) - (when the max number of visited states is reached, the oldest - one is removed according to its number (= with the min number) */ - xbt_dynar_remove_at(visited_states, cursor, nullptr); - xbt_dynar_insert_at(visited_states, cursor, &new_state); - XBT_DEBUG("Replace visited state %d with the new visited state %d", - state_test->num, new_state->num); -} - static -bool some_dommunications_are_not_finished() +bool some_communications_are_not_finished() { for (size_t current_process = 1; current_process < MC_smx_get_maxpid(); current_process++) { xbt_dynar_t pattern = xbt_dynar_get_as( @@ -271,11 +133,28 @@ bool some_dommunications_are_not_finished() return false; } +namespace simgrid { +namespace mc { + +static void prune_visited_states() +{ + while (visited_states.size() > (std::size_t) _sg_mc_visited) { + XBT_DEBUG("Try to remove visited state (maximum number of stored states reached)"); + auto min_element = std::min_element(visited_states.begin(), visited_states.end(), + [](std::unique_ptr& a, std::unique_ptr& b) { + return a->num < b->num; + }); + xbt_assert(min_element != visited_states.end()); + // and drop it: + visited_states.erase(min_element); + XBT_DEBUG("Remove visited state (maximum number of stored states reached)"); + } +} + /** * \brief Checks whether a given state has already been visited by the algorithm. */ - -mc_visited_state_t is_visited_state(mc_state_t graph_state) +std::unique_ptr is_visited_state(mc_state_t graph_state) { if (_sg_mc_visited == 0) return nullptr; @@ -284,173 +163,57 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state) communications are not finished (at least, data are transfered). These communications are incomplete and they cannot be analyzed and compared with the initial pattern. */ int partial_comm = (_sg_mc_comms_determinism || _sg_mc_send_determinism) && - some_dommunications_are_not_finished(); + some_communications_are_not_finished(); - mc_visited_state_t new_state = visited_state_new(); + std::unique_ptr new_state = + std::unique_ptr(new VisitedState()); graph_state->system_state = new_state->system_state; graph_state->in_visited_states = 1; XBT_DEBUG("Snapshot %p of visited state %d (exploration stack state %d)", new_state->system_state, new_state->num, graph_state->num); - if (xbt_dynar_is_empty(visited_states)) { - xbt_dynar_push(visited_states, &new_state); - return nullptr; - } - - int min = -1, max = -1, index; - - index = get_search_interval(visited_states, new_state, &min, &max); - - if (min != -1 && max != -1) { + auto range = std::equal_range(visited_states.begin(), visited_states.end(), + new_state.get(), simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap()); if (_sg_mc_safety || (!partial_comm && initial_global_state->initial_communications_pattern_done)) { - int cursor = min; - while (cursor <= max) { - mc_visited_state_t state_test = (mc_visited_state_t) xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t); - if (snapshot_compare(state_test, new_state) == 0) { + for (auto i = range.first; i != range.second; ++i) { + auto& visited_state = *i; + if (snapshot_compare(visited_state.get(), new_state.get()) == 0) { // The state has been visited: - replace_state(state_test, new_state, cursor); - return state_test; + std::unique_ptr old_state = + std::move(visited_state); + + if (old_state->other_num == -1) + new_state->other_num = old_state->num; + else + new_state->other_num = old_state->other_num; + + if (dot_output == nullptr) + XBT_DEBUG("State %d already visited ! (equal to state %d)", + new_state->num, old_state->num); + else + XBT_DEBUG( + "State %d already visited ! (equal to state %d (state %d in dot_output))", + new_state->num, old_state->num, new_state->other_num); + + /* Replace the old state with the new one (with a bigger num) + (when the max number of visited states is reached, the oldest + one is removed according to its number (= with the min number) */ + XBT_DEBUG("Replace visited state %d with the new visited state %d", + old_state->num, new_state->num); + + visited_state = std::move(new_state); + return std::move(old_state); } - cursor++; } } - - xbt_dynar_insert_at(visited_states, min, &new_state); - XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, xbt_dynar_length(visited_states)); - - } else { - - // The state has not been visited: insert the state in the dynamic array. - mc_visited_state_t state_test = (mc_visited_state_t) xbt_dynar_get_as(visited_states, index, mc_visited_state_t); - if (state_test->nb_processes < new_state->nb_processes) - xbt_dynar_insert_at(visited_states, index + 1, &new_state); - else if (state_test->heap_bytes_used < new_state->heap_bytes_used) - xbt_dynar_insert_at(visited_states, index + 1, &new_state); - else - xbt_dynar_insert_at(visited_states, index, &new_state); - - XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, xbt_dynar_length(visited_states)); - - } - - if ((ssize_t) xbt_dynar_length(visited_states) <= _sg_mc_visited) - return nullptr; - - // We have reached the maximum number of stored states; - - XBT_DEBUG("Try to remove visited state (maximum number of stored states reached)"); - - // Find the (index of the) older state (with the smallest num): - int min2 = mc_stats->expanded_states; - unsigned int cursor2 = 0; - unsigned int index2 = 0; - - mc_visited_state_t state_test; - xbt_dynar_foreach(visited_states, cursor2, state_test) - if (!mc_model_checker->is_important_snapshot(*state_test->system_state) - && state_test->num < min2) { - index2 = cursor2; - min2 = state_test->num; - } - - // and drop it: - xbt_dynar_remove_at(visited_states, index2, nullptr); - XBT_DEBUG("Remove visited state (maximum number of stored states reached)"); - return nullptr; -} - -namespace simgrid { -namespace mc { - -/** - * \brief Checks whether a given pair has already been visited by the algorithm. - */ -int is_visited_pair(simgrid::mc::VisitedPair* visited_pair, simgrid::mc::Pair* pair) { - - if (_sg_mc_visited == 0) - return -1; - - simgrid::mc::VisitedPair* new_visited_pair = nullptr; - if (visited_pair == nullptr) - new_visited_pair = new simgrid::mc::VisitedPair( - pair->num, pair->automaton_state, pair->atomic_propositions.get(), - pair->graph_state); - else - new_visited_pair = visited_pair; - - if (xbt_dynar_is_empty(visited_pairs)) { - xbt_dynar_push(visited_pairs, &new_visited_pair); - return -1; - } - - int min = -1, max = -1, index; - //int res; - simgrid::mc::VisitedPair* pair_test; - int cursor; - - index = get_search_interval(visited_pairs, new_visited_pair, &min, &max); - - if (min != -1 && max != -1) { // Visited pair with same number of processes and same heap bytes used exists - cursor = min; - while (cursor <= max) { - pair_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(visited_pairs, cursor, simgrid::mc::VisitedPair*); - if (xbt_automaton_state_compare(pair_test->automaton_state, new_visited_pair->automaton_state) == 0) { - if (xbt_automaton_propositional_symbols_compare_value( - pair_test->atomic_propositions.get(), - new_visited_pair->atomic_propositions.get()) == 0) { - if (snapshot_compare(pair_test, new_visited_pair) == 0) { - if (pair_test->other_num == -1) - new_visited_pair->other_num = pair_test->num; - else - new_visited_pair->other_num = pair_test->other_num; - if (dot_output == nullptr) - XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_visited_pair->num, pair_test->num); - else - 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); - xbt_dynar_remove_at(visited_pairs, cursor, &pair_test); - xbt_dynar_insert_at(visited_pairs, cursor, &new_visited_pair); - pair_test->visited_removed = 1; - if (!pair_test->acceptance_pair - || pair_test->acceptance_removed == 1) - delete pair_test; - return new_visited_pair->other_num; - } - } - } - cursor++; - } - xbt_dynar_insert_at(visited_pairs, min, &new_visited_pair); - } else { - pair_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(visited_pairs, index, simgrid::mc::VisitedPair*); - if (pair_test->nb_processes < new_visited_pair->nb_processes) - xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair); - else if (pair_test->heap_bytes_used < new_visited_pair->heap_bytes_used) - xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair); - else - xbt_dynar_insert_at(visited_pairs, index, &new_visited_pair); - } - - if ((ssize_t) xbt_dynar_length(visited_pairs) > _sg_mc_visited) { - int min2 = mc_stats->expanded_pairs; - unsigned int cursor2 = 0; - unsigned int index2 = 0; - xbt_dynar_foreach(visited_pairs, cursor2, pair_test) { - if (!mc_model_checker->is_important_snapshot(*pair_test->graph_state->system_state) - && pair_test->num < min2) { - index2 = cursor2; - min2 = pair_test->num; - } - } - xbt_dynar_remove_at(visited_pairs, index2, &pair_test); - pair_test->visited_removed = 1; - if (!pair_test->acceptance_pair || pair_test->acceptance_removed) - delete pair_test; - } - return -1; + XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, (unsigned long) visited_states.size()); + visited_states.insert(range.first, std::move(new_state)); + prune_visited_states(); + return nullptr; } }