X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/3eb8b6369503c39208fcf754830b6b26dc4186fc..2376a01092173679830310f4d57b267445959f97:/src/mc/mc_visited.cpp diff --git a/src/mc/mc_visited.cpp b/src/mc/mc_visited.cpp index 19a9e2ec4d..ee5d9ee4c4 100644 --- a/src/mc/mc_visited.cpp +++ b/src/mc/mc_visited.cpp @@ -8,16 +8,16 @@ #include #include +#include -#include #include #include #include +#include #include #include "src/mc/mc_comm_pattern.h" #include "src/mc/mc_safety.h" -#include "src/mc/mc_liveness.h" #include "src/mc/mc_private.h" #include "src/mc/Process.hpp" #include "src/mc/mc_smx.h" @@ -28,21 +28,8 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_visited, mc, namespace simgrid { namespace mc { -xbt_dynar_t visited_pairs; std::vector> visited_states; -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){ - ((mc_state_t)xbt_fifo_get_item_content(item))->in_visited_states = 0; - return 1; - } - item = xbt_fifo_get_next_item(item); - } - return 0; -} - /** * \brief Save the current state * \return Snapshot of the current state. @@ -64,259 +51,58 @@ VisitedState::VisitedState() 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) +static void prune_visited_states() { - simgrid::mc::Process* process = &(mc_model_checker->process()); - - this->graph_state = graph_state; - if(this->graph_state->system_state == nullptr) - this->graph_state->system_state = simgrid::mc::take_snapshot(pair_num); - this->heap_bytes_used = mmalloc_get_bytes_used_remote( - process->get_heap()->heaplimit, - process->get_malloc_info()); - - this->nb_processes = - mc_model_checker->process().simix_processes().size(); - - this->automaton_state = automaton_state; - this->num = pair_num; - this->other_num = -1; - this->acceptance_removed = 0; - this->visited_removed = 0; - this->acceptance_pair = 0; - this->atomic_propositions = simgrid::xbt::unique_ptr( - xbt_dynar_new(sizeof(int), nullptr)); - - unsigned int cursor = 0; - int value; - xbt_dynar_foreach(atomic_propositions, cursor, value) - xbt_dynar_push_as(this->atomic_propositions.get(), int, value); -} - -static int is_exploration_stack_pair(simgrid::mc::VisitedPair* pair){ - xbt_fifo_item_t item = xbt_fifo_get_first_item(mc_stack); - while (item) { - if (((simgrid::mc::Pair*)xbt_fifo_get_item_content(item))->num == pair->num){ - ((simgrid::mc::Pair*)xbt_fifo_get_item_content(item))->visited_pair_removed = 1; - return 1; - } - item = xbt_fifo_get_next_item(item); + 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)"); } - return 0; } -VisitedPair::~VisitedPair() +static int snapshot_compare(simgrid::mc::VisitedState* state1, simgrid::mc::VisitedState* state2) { - if( !is_exploration_stack_pair(this)) - MC_state_delete(this->graph_state, 1); -} - -} + simgrid::mc::Snapshot* s1 = state1->system_state.get(); + simgrid::mc::Snapshot* s2 = state2->system_state.get(); + int num1 = state1->num; + int num2 = state2->num; + return snapshot_compare(num1, s1, num2, s2); } -/** - * \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 = ((simgrid::mc::VisitedState*) ref)->nb_processes; - heap_bytes_used = ((simgrid::mc::VisitedState*) 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 = (simgrid::mc::VisitedState*) xbt_dynar_get_as(list, cursor, simgrid::mc::VisitedState*); - nb_processes_test = ((simgrid::mc::VisitedState*) ref_test)->nb_processes; - heap_bytes_used_test = ((simgrid::mc::VisitedState*) 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 = (simgrid::mc::VisitedState*) xbt_dynar_get_as(list, previous_cursor, simgrid::mc::VisitedState*); - nb_processes_test = ((simgrid::mc::VisitedState*) ref_test)->nb_processes; - heap_bytes_used_test = ((simgrid::mc::VisitedState*) 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 = (simgrid::mc::VisitedState*) xbt_dynar_get_as(list, next_cursor, simgrid::mc::VisitedState*); - nb_processes_test = ((simgrid::mc::VisitedState*) ref_test)->nb_processes; - heap_bytes_used_test = ((simgrid::mc::VisitedState*) 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; -} - -// TODO, it would make sense to use std::set instead -template -int get_search_interval(std::vector> const& list, T *ref, int *min, int *max) -{ - int nb_processes = ref->nb_processes; - int heap_bytes_used = ref->heap_bytes_used; - - int cursor = 0; - int start = 0; - int end = list.size() - 1; - while (start <= end) { - cursor = (start + end) / 2; - int nb_processes_test = list[cursor]->nb_processes; - int heap_bytes_used_test = list[cursor]->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; - int previous_cursor = cursor - 1; - while (previous_cursor >= 0) { - nb_processes_test = list[previous_cursor]->nb_processes; - heap_bytes_used_test = list[previous_cursor]->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 < list.size()) { - nb_processes_test = list[next_cursor]->nb_processes; - heap_bytes_used_test = list[next_cursor]->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 -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( - incomplete_communications_pattern, current_process, xbt_dynar_t); - if (!xbt_dynar_is_empty(pattern)) { - XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited."); - return true; - } - } - return false; -} - -namespace simgrid { -namespace mc { - /** * \brief Checks whether a given state has already been visited by the algorithm. */ -std::unique_ptr is_visited_state(mc_state_t graph_state) +std::unique_ptr is_visited_state(simgrid::mc::State* graph_state, bool compare_snpashots) { - if (_sg_mc_visited == 0) - return nullptr; - /* If comm determinism verification, we cannot stop the exploration if some - 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_communications_are_not_finished(); 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 (visited_states.empty()) { - visited_states.push_back(std::move(new_state)); - return nullptr; - } + XBT_DEBUG("Snapshot %p of visited state %d (exploration stack state %d)", + new_state->system_state.get(), new_state->num, graph_state->num); - int min = -1, max = -1, index; + auto range = std::equal_range(visited_states.begin(), visited_states.end(), + new_state.get(), simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap()); - index = get_search_interval(visited_states, new_state.get(), &min, &max); + if (compare_snpashots) { - if (min != -1 && max != -1) { - - if (_sg_mc_safety || (!partial_comm - && initial_global_state->initial_communications_pattern_done)) { - - int cursor = min; - while (cursor <= max) { - if (snapshot_compare(visited_states[cursor].get(), new_state.get()) == 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: std::unique_ptr old_state = - std::move(visited_states[cursor]); + std::move(visited_state); if (old_state->other_num == -1) new_state->other_num = old_state->num; @@ -337,145 +123,16 @@ std::unique_ptr is_visited_state(mc_state_t graph_sta XBT_DEBUG("Replace visited state %d with the new visited state %d", old_state->num, new_state->num); - simgrid::mc::visited_states[cursor] = std::move(new_state); + visited_state = std::move(new_state); return std::move(old_state); } - cursor++; } } - - XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, (unsigned long) visited_states.size()); - visited_states.insert(visited_states.begin() + min, std::move(new_state)); - - } else { - - // The state has not been visited: insert the state in the dynamic array. - simgrid::mc::VisitedState* state_test = &*visited_states[index]; - std::size_t position; - if (state_test->nb_processes < new_state->nb_processes) - position = index + 1; - else if (state_test->heap_bytes_used < new_state->heap_bytes_used) - position = index + 1; - else - position = index; - visited_states.insert(visited_states.begin() + position, std::move(new_state)); - XBT_DEBUG("Insert new visited state %d (total : %lu)", - visited_states[index]->num, - (unsigned long) visited_states.size()); - - } - if (visited_states.size() <= (std::size_t) _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 index2 = 0; - - for (std::size_t cursor2 = 0; cursor2 != visited_states.size(); ++cursor2) - if (!mc_model_checker->is_important_snapshot( - *visited_states[cursor2]->system_state) - && visited_states[cursor2]->num < min2) { - index2 = cursor2; - min2 = visited_states[cursor2]->num; - } - - // and drop it: - visited_states.erase(visited_states.begin() + index2); - XBT_DEBUG("Remove visited state (maximum number of stored states reached)"); - - return nullptr; -} - -/** - * \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; } }