X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/862f2dd952fd94f506c357c0a9818cec8b08152b..ff808eaaaeeb05dcbb4a26b7997c975db605b875:/src/mc/mc_visited.cpp?ds=sidebyside

diff --git a/src/mc/mc_visited.cpp b/src/mc/mc_visited.cpp
index f030a59e0a..11687b19d7 100644
--- a/src/mc/mc_visited.cpp
+++ b/src/mc/mc_visited.cpp
@@ -8,11 +8,13 @@
 #include <sys/wait.h>
 
 #include <memory>
+#include <algorithm>
 
 #include <xbt/automaton.h>
 #include <xbt/log.h>
 #include <xbt/sysdep.h>
 #include <xbt/dynar.h>
+#include <xbt/dynar.hpp>
 #include <xbt/fifo.h>
 
 #include "src/mc/mc_comm_pattern.h"
@@ -117,147 +119,6 @@ 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 = ((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<class T>
-int get_search_interval(std::vector<std::unique_ptr<T>> 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()
 {
@@ -275,6 +136,21 @@ bool some_communications_are_not_finished()
 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<simgrid::mc::VisitedState>& a, std::unique_ptr<simgrid::mc::VisitedState>& 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.
  */
@@ -295,27 +171,19 @@ std::unique_ptr<simgrid::mc::VisitedState> is_visited_state(mc_state_t graph_sta
   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;
-  }
-
-    int min = -1, max = -1, index;
-
-    index = get_search_interval(visited_states, new_state.get(), &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) {
-          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<simgrid::mc::VisitedState> old_state =
-              std::move(visited_states[cursor]);
+              std::move(visited_state);
 
             if (old_state->other_num == -1)
               new_state->other_num = old_state->num;
@@ -336,58 +204,16 @@ std::unique_ptr<simgrid::mc::VisitedState> 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;
+  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;
 }
 
 }