X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/84a3bccd6edd7bbc93648d2646e1413ce8114853..a2a013c0e4ca407feeb7b3d0e85abba7acae2532:/src/mc/compare.cpp

diff --git a/src/mc/compare.cpp b/src/mc/compare.cpp
index e871e48496..1596039cdc 100644
--- a/src/mc/compare.cpp
+++ b/src/mc/compare.cpp
@@ -10,6 +10,7 @@
 
 #include <array>
 #include <memory>
+#include <set>
 #include <utility>
 #include <unordered_set>
 
@@ -48,15 +49,18 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_compare, xbt,
 namespace simgrid {
 namespace mc {
 
+struct HeapLocation;
+typedef std::array<HeapLocation, 2> HeapLocationPair;
+typedef std::set<HeapLocationPair> HeapLocationPairs;
+struct HeapArea;
 struct ProcessComparisonState;
 struct StateComparator;
 
 static int compare_heap_area(
+  StateComparator& state,
   int process_index, const void *area1, const void* area2,
   Snapshot* snapshot1, Snapshot* snapshot2,
-  xbt_dynar_t previous, Type* type, int pointer_level);
-
-static void reset_heap_information(void);
+  HeapLocationPairs* previous, Type* type, int pointer_level);
 
 }
 }
@@ -69,9 +73,47 @@ using simgrid::mc::remote;
 namespace simgrid {
 namespace mc {
 
+struct HeapLocation {
+  int block = 0;
+  int fragment = 0;
+
+  HeapLocation() {}
+  HeapLocation(int block, int fragment = 0) : block(block), fragment(fragment) {}
+
+  bool operator==(HeapLocation const& that) const
+  {
+    return block == that.block && fragment == that.fragment;
+  }
+  bool operator<(HeapLocation const& that) const
+  {
+    return std::make_pair(block, fragment)
+      < std::make_pair(that.block, that.fragment);
+  }
+};
+
+static inline
+HeapLocationPair makeHeapLocationPair(int block1, int fragment1, int block2, int fragment2)
+{
+  return simgrid::mc::HeapLocationPair({
+    simgrid::mc::HeapLocation(block1, fragment1),
+    simgrid::mc::HeapLocation(block2, fragment2)
+  });
+}
+
+struct HeapArea : public HeapLocation {
+  bool valid = false;
+  int block = 0;
+  int fragment = 0;
+  HeapArea() {}
+  HeapArea(int block)
+    : valid(true), block(block) {}
+  HeapArea(int block, int fragment = 0)
+    : valid(true), block(block), fragment(fragment) {}
+};
+
 struct ProcessComparisonState {
   std::vector<simgrid::mc::IgnoredHeapRegion>* to_ignore = nullptr;
-  std::vector<s_heap_area_t> equals_to;
+  std::vector<HeapArea> equals_to;
   std::vector<simgrid::mc::Type*> types;
   std::size_t heapsize = 0;
 
@@ -79,21 +121,49 @@ struct ProcessComparisonState {
                           std::vector<simgrid::mc::IgnoredHeapRegion>* i);
 };
 
+namespace {
+
+/** A hash which works with more stuff
+ *
+ *  It can hash pairs: the standard hash currently doesn't include this.
+ */
+template<class X> struct hash : public std::hash<X> {};
+
+template<class X, class Y>
+struct hash<std::pair<X,Y>> {
+  std::size_t operator()(std::pair<X,Y>const& x) const
+  {
+    struct hash<X> h1;
+    struct hash<X> h2;
+    return h1(x.first) ^ h2(x.second);
+  }
+};
+
+}
+
+
 struct StateComparator {
   s_xbt_mheap_t std_heap_copy;
   std::size_t heaplimit;
   std::array<ProcessComparisonState, 2> processStates;
 
+  std::unordered_set<std::pair<void*, void*>, hash<std::pair<void*, void*>>> compared_pointers;
+
+  void clear()
+  {
+    compared_pointers.clear();
+  }
+
   int initHeapInformation(
     xbt_mheap_t heap1, xbt_mheap_t heap2,
     std::vector<simgrid::mc::IgnoredHeapRegion>* i1,
     std::vector<simgrid::mc::IgnoredHeapRegion>* i2);
 
-  s_heap_area_t& equals_to1_(std::size_t i, std::size_t j)
+  HeapArea& equals_to1_(std::size_t i, std::size_t j)
   {
     return processStates[0].equals_to[ MAX_FRAGMENT_PER_BLOCK * i + j];
   }
-  s_heap_area_t& equals_to2_(std::size_t i, std::size_t j)
+  HeapArea& equals_to2_(std::size_t i, std::size_t j)
   {
     return processStates[1].equals_to[ MAX_FRAGMENT_PER_BLOCK * i + j];
   }
@@ -106,11 +176,11 @@ struct StateComparator {
     return processStates[1].types[ MAX_FRAGMENT_PER_BLOCK * i + j];
   }
 
-  s_heap_area_t const& equals_to1_(std::size_t i, std::size_t j) const
+  HeapArea const& equals_to1_(std::size_t i, std::size_t j) const
   {
     return processStates[0].equals_to[ MAX_FRAGMENT_PER_BLOCK * i + j];
   }
-  s_heap_area_t const& equals_to2_(std::size_t i, std::size_t j) const
+  HeapArea const& equals_to2_(std::size_t i, std::size_t j) const
   {
     return processStates[1].equals_to[ MAX_FRAGMENT_PER_BLOCK * i + j];
   }
@@ -153,59 +223,14 @@ struct StateComparator {
         && this->equals_to2_(b2, f2).fragment == f1;
   }
 
-  void match_equals(xbt_dynar_t list);
+  void match_equals(HeapLocationPairs* list);
 };
 
 }
 }
 
-// TODO, make this a field of ModelChecker or something similar
-static std::unique_ptr<simgrid::mc::StateComparator> mc_diff_info;
-
 /************************************************************************************/
 
-static s_heap_area_t make_heap_area(int block, int fragment)
-{
-  s_heap_area_t area;
-  area.valid = 1;
-  area.block = block;
-  area.fragment = fragment;
-  return area;
-}
-
-static int is_new_heap_area_pair(xbt_dynar_t list, int block1, int fragment1,
-                                 int block2, int fragment2)
-{
-
-  unsigned int cursor = 0;
-  heap_area_pair_t current_pair;
-
-  xbt_dynar_foreach(list, cursor, current_pair)
-    if (current_pair->block1 == block1 && current_pair->block2 == block2
-        && current_pair->fragment1 == fragment1
-        && current_pair->fragment2 == fragment2)
-      return 0;
-
-  return 1;
-}
-
-static int add_heap_area_pair(xbt_dynar_t list, int block1, int fragment1,
-                              int block2, int fragment2)
-{
-
-  if (!is_new_heap_area_pair(list, block1, fragment1, block2, fragment2))
-    return 0;
-
-  heap_area_pair_t pair = nullptr;
-  pair = xbt_new0(s_heap_area_pair_t, 1);
-  pair->block1 = block1;
-  pair->fragment1 = fragment1;
-  pair->block2 = block2;
-  pair->fragment2 = fragment2;
-  xbt_dynar_push(list, &pair);
-  return 1;
-}
-
 static ssize_t heap_comparison_ignore_size(
   std::vector<simgrid::mc::IgnoredHeapRegion>* ignore_list,
   const void *address)
@@ -247,22 +272,19 @@ static bool is_block_stack(int block)
 namespace simgrid {
 namespace mc {
 
-void StateComparator::match_equals(xbt_dynar_t list)
+void StateComparator::match_equals(HeapLocationPairs* list)
 {
-  unsigned int cursor = 0;
-  heap_area_pair_t current_pair;
-
-  xbt_dynar_foreach(list, cursor, current_pair) {
-    if (current_pair->fragment1 != -1) {
-      this->equals_to1_(current_pair->block1, current_pair->fragment1) =
-          make_heap_area(current_pair->block2, current_pair->fragment2);
-      this->equals_to2_(current_pair->block2, current_pair->fragment2) =
-          make_heap_area(current_pair->block1, current_pair->fragment1);
+  for (auto const& pair : *list) {
+    if (pair[0].fragment != -1) {
+      this->equals_to1_(pair[0].block, pair[0].fragment) =
+          simgrid::mc::HeapArea(pair[1].block, pair[1].fragment);
+      this->equals_to2_(pair[1].block, pair[1].fragment) =
+          simgrid::mc::HeapArea(pair[0].block, pair[0].fragment);
     } else {
-      this->equals_to1_(current_pair->block1, 0) =
-          make_heap_area(current_pair->block2, current_pair->fragment2);
-      this->equals_to2_(current_pair->block2, 0) =
-          make_heap_area(current_pair->block1, current_pair->fragment1);
+      this->equals_to1_(pair[0].block, 0) =
+          simgrid::mc::HeapArea(pair[1].block, pair[1].fragment);
+      this->equals_to2_(pair[1].block, 0) =
+          simgrid::mc::HeapArea(pair[0].block, pair[0].fragment);
     }
   }
 }
@@ -273,7 +295,7 @@ void ProcessComparisonState::initHeapInformation(xbt_mheap_t heap,
   auto heaplimit = ((struct mdesc *) heap)->heaplimit;
   this->heapsize = ((struct mdesc *) heap)->heapsize;
   this->to_ignore = i;
-  this->equals_to.assign(heaplimit * MAX_FRAGMENT_PER_BLOCK, s_heap_area {0, 0, 0});
+  this->equals_to.assign(heaplimit * MAX_FRAGMENT_PER_BLOCK, HeapArea());
   this->types.assign(heaplimit * MAX_FRAGMENT_PER_BLOCK, nullptr);
 }
 
@@ -294,22 +316,6 @@ int StateComparator::initHeapInformation(xbt_mheap_t heap1, xbt_mheap_t heap2,
   return 0;
 }
 
-static
-int init_heap_information(xbt_mheap_t heap1, xbt_mheap_t heap2,
-                          std::vector<simgrid::mc::IgnoredHeapRegion>* i1,
-                          std::vector<simgrid::mc::IgnoredHeapRegion>* i2)
-{
-  if (mc_diff_info == nullptr)
-    mc_diff_info = std::unique_ptr<StateComparator>(new StateComparator());
-  return mc_diff_info->initHeapInformation(heap1, heap2, i1, i2);
-}
-
-static inline
-void reset_heap_information()
-{
-
-}
-
 // TODO, have a robust way to find it in O(1)
 static inline
 mc_mem_region_t MC_get_heap_region(simgrid::mc::Snapshot* snapshot)
@@ -321,10 +327,10 @@ mc_mem_region_t MC_get_heap_region(simgrid::mc::Snapshot* snapshot)
 }
 
 static
-int mmalloc_compare_heap(simgrid::mc::Snapshot* snapshot1, simgrid::mc::Snapshot* snapshot2)
+int mmalloc_compare_heap(
+  simgrid::mc::StateComparator& state, simgrid::mc::Snapshot* snapshot1, simgrid::mc::Snapshot* snapshot2)
 {
   simgrid::mc::Process* process = &mc_model_checker->process();
-  simgrid::mc::StateComparator *state = mc_diff_info.get();
 
   /* Start comparison */
   size_t i1, i2, j1, j2, k;
@@ -352,7 +358,7 @@ int mmalloc_compare_heap(simgrid::mc::Snapshot* snapshot1, simgrid::mc::Snapshot
   const malloc_info* heapinfos2 = snapshot2->read<malloc_info*>(
     (std::uint64_t)heapinfo_address, simgrid::mc::ProcessIndexMissing);
 
-  while (i1 < state->heaplimit) {
+  while (i1 < state.heaplimit) {
 
     const malloc_info* heapinfo1 = (const malloc_info*) MC_region_read(heap_region1, &heapinfo_temp1, &heapinfos1[i1], sizeof(malloc_info));
     const malloc_info* heapinfo2 = (const malloc_info*) MC_region_read(heap_region2, &heapinfo_temp2, &heapinfos2[i1], sizeof(malloc_info));
@@ -369,20 +375,20 @@ int mmalloc_compare_heap(simgrid::mc::Snapshot* snapshot1, simgrid::mc::Snapshot
 
     addr_block1 =
         ((void *) (((ADDR2UINT(i1)) - 1) * BLOCKSIZE +
-                   (char *) state->std_heap_copy.heapbase));
+                   (char *) state.std_heap_copy.heapbase));
 
     if (heapinfo1->type == MMALLOC_TYPE_UNFRAGMENTED) {       /* Large block */
 
       if (is_stack(addr_block1)) {
         for (k = 0; k < heapinfo1->busy_block.size; k++)
-          state->equals_to1_(i1 + k, 0) = make_heap_area(i1, -1);
+          state.equals_to1_(i1 + k, 0) = HeapArea(i1, -1);
         for (k = 0; k < heapinfo2->busy_block.size; k++)
-          state->equals_to2_(i1 + k, 0) = make_heap_area(i1, -1);
+          state.equals_to2_(i1 + k, 0) = HeapArea(i1, -1);
         i1 += heapinfo1->busy_block.size;
         continue;
       }
 
-      if (state->equals_to1_(i1, 0).valid) {
+      if (state.equals_to1_(i1, 0).valid) {
         i1++;
         continue;
       }
@@ -393,26 +399,26 @@ int mmalloc_compare_heap(simgrid::mc::Snapshot* snapshot1, simgrid::mc::Snapshot
 
       /* Try first to associate to same block in the other heap */
       if (heapinfo2->type == heapinfo1->type
-        && state->equals_to2_(i1, 0).valid == 0) {
+        && state.equals_to2_(i1, 0).valid == 0) {
         addr_block2 = (ADDR2UINT(i1) - 1) * BLOCKSIZE +
-                       (char *) state->std_heap_copy.heapbase;
-        res_compare =
-            compare_heap_area(simgrid::mc::ProcessIndexMissing, addr_block1, addr_block2, snapshot1, snapshot2,
-                              nullptr, nullptr, 0);
+                       (char *) state.std_heap_copy.heapbase;
+        res_compare = compare_heap_area(state, simgrid::mc::ProcessIndexMissing,
+            addr_block1, addr_block2, snapshot1, snapshot2,
+            nullptr, nullptr, 0);
         if (res_compare != 1) {
           for (k = 1; k < heapinfo2->busy_block.size; k++)
-            state->equals_to2_(i1 + k, 0) = make_heap_area(i1, -1);
+            state.equals_to2_(i1 + k, 0) = HeapArea(i1, -1);
           for (k = 1; k < heapinfo1->busy_block.size; k++)
-            state->equals_to1_(i1 + k, 0) = make_heap_area(i1, -1);
+            state.equals_to1_(i1 + k, 0) = HeapArea(i1, -1);
           equal = 1;
           i1 += heapinfo1->busy_block.size;
         }
       }
 
-      while (i2 < state->heaplimit && !equal) {
+      while (i2 < state.heaplimit && !equal) {
 
         addr_block2 = (ADDR2UINT(i2) - 1) * BLOCKSIZE +
-                       (char *) state->std_heap_copy.heapbase;
+                       (char *) state.std_heap_copy.heapbase;
 
         if (i2 == i1) {
           i2++;
@@ -426,20 +432,20 @@ int mmalloc_compare_heap(simgrid::mc::Snapshot* snapshot1, simgrid::mc::Snapshot
           continue;
         }
 
-        if (state->equals_to2_(i2, 0).valid) {
+        if (state.equals_to2_(i2, 0).valid) {
           i2++;
           continue;
         }
 
-        res_compare =
-            compare_heap_area(simgrid::mc::ProcessIndexMissing, addr_block1, addr_block2, snapshot1, snapshot2,
-                              nullptr, nullptr, 0);
+        res_compare = compare_heap_area(state, simgrid::mc::ProcessIndexMissing,
+            addr_block1, addr_block2, snapshot1, snapshot2,
+            nullptr, nullptr, 0);
 
         if (res_compare != 1) {
           for (k = 1; k < heapinfo2b->busy_block.size; k++)
-            state->equals_to2_(i2 + k, 0) = make_heap_area(i1, -1);
+            state.equals_to2_(i2 + k, 0) = HeapArea(i1, -1);
           for (k = 1; k < heapinfo1->busy_block.size; k++)
-            state->equals_to1_(i1 + k, 0) = make_heap_area(i2, -1);
+            state.equals_to1_(i1 + k, 0) = HeapArea(i2, -1);
           equal = 1;
           i1 += heapinfo1->busy_block.size;
         }
@@ -451,7 +457,7 @@ int mmalloc_compare_heap(simgrid::mc::Snapshot* snapshot1, simgrid::mc::Snapshot
       if (!equal) {
         XBT_DEBUG("Block %zu not found (size_used = %zu, addr = %p)", i1,
                   heapinfo1->busy_block.busy_size, addr_block1);
-        i1 = state->heaplimit + 1;
+        i1 = state.heaplimit + 1;
         nb_diff1++;
         //i1++;
       }
@@ -463,7 +469,7 @@ int mmalloc_compare_heap(simgrid::mc::Snapshot* snapshot1, simgrid::mc::Snapshot
         if (heapinfo1->busy_frag.frag_size[j1] == -1) /* Free fragment */
           continue;
 
-        if (state->equals_to1_(i1, j1).valid)
+        if (state.equals_to1_(i1, j1).valid)
           continue;
 
         addr_frag1 =
@@ -474,22 +480,22 @@ int mmalloc_compare_heap(simgrid::mc::Snapshot* snapshot1, simgrid::mc::Snapshot
 
         /* Try first to associate to same fragment in the other heap */
         if (heapinfo2->type == heapinfo1->type
-            && state->equals_to2_(i1, j1).valid == 0) {
+            && !state.equals_to2_(i1, j1).valid) {
           addr_block2 = (ADDR2UINT(i1) - 1) * BLOCKSIZE +
-                         (char *) state->std_heap_copy.heapbase;
+                         (char *) state.std_heap_copy.heapbase;
           addr_frag2 =
               (void *) ((char *) addr_block2 +
                         (j1 << heapinfo2->type));
-          res_compare =
-              compare_heap_area(simgrid::mc::ProcessIndexMissing, addr_frag1, addr_frag2, snapshot1, snapshot2,
-                                nullptr, nullptr, 0);
+          res_compare = compare_heap_area(state, simgrid::mc::ProcessIndexMissing,
+              addr_frag1, addr_frag2, snapshot1, snapshot2,
+              nullptr, nullptr, 0);
           if (res_compare != 1)
             equal = 1;
         }
 
 
 
-        while (i2 < state->heaplimit && !equal) {
+        while (i2 < state.heaplimit && !equal) {
 
           const malloc_info* heapinfo2b = (const malloc_info*) MC_region_read(
             heap_region2, &heapinfo_temp2b, &heapinfos2[i2],
@@ -517,19 +523,19 @@ int mmalloc_compare_heap(simgrid::mc::Snapshot* snapshot1, simgrid::mc::Snapshot
             if (i2 == i1 && j2 == j1)
               continue;
 
-            if (state->equals_to2_(i2, j2).valid)
+            if (state.equals_to2_(i2, j2).valid)
               continue;
 
             addr_block2 = (ADDR2UINT(i2) - 1) * BLOCKSIZE +
-                           (char *) state->std_heap_copy.heapbase;
+                           (char *) state.std_heap_copy.heapbase;
             addr_frag2 =
                 (void *) ((char *) addr_block2 +
                           (j2 << heapinfo2b->type));
 
-            res_compare =
-                compare_heap_area(simgrid::mc::ProcessIndexMissing, addr_frag1, addr_frag2, snapshot2, snapshot2,
-                                  nullptr, nullptr, 0);
-
+            res_compare = compare_heap_area(
+                state, simgrid::mc::ProcessIndexMissing,
+                addr_frag1, addr_frag2, snapshot2, snapshot2,
+                nullptr, nullptr, 0);
             if (res_compare != 1) {
               equal = 1;
               break;
@@ -546,8 +552,8 @@ int mmalloc_compare_heap(simgrid::mc::Snapshot* snapshot1, simgrid::mc::Snapshot
               ("Block %zu, fragment %zu not found (size_used = %zd, address = %p)\n",
                i1, j1, heapinfo1->busy_frag.frag_size[j1],
                addr_frag1);
-          i2 = state->heaplimit + 1;
-          i1 = state->heaplimit + 1;
+          i2 = state.heaplimit + 1;
+          i1 = state.heaplimit + 1;
           nb_diff1++;
           break;
         }
@@ -563,14 +569,14 @@ int mmalloc_compare_heap(simgrid::mc::Snapshot* snapshot1, simgrid::mc::Snapshot
   /* All blocks/fragments are equal to another block/fragment ? */
   size_t i = 1, j = 0;
 
-  for(i = 1; i < state->heaplimit; i++) {
+  for(i = 1; i < state.heaplimit; i++) {
     const malloc_info* heapinfo1 = (const malloc_info*) MC_region_read(
       heap_region1, &heapinfo_temp1, &heapinfos1[i], sizeof(malloc_info));
 
     if (heapinfo1->type == MMALLOC_TYPE_UNFRAGMENTED
-        && i1 == state->heaplimit
+        && i1 == state.heaplimit
         && heapinfo1->busy_block.busy_size > 0
-        && state->equals_to1_(i, 0).valid == 0) {
+        && !state.equals_to1_(i, 0).valid) {
       XBT_DEBUG("Block %zu not found (size used = %zu)", i,
                 heapinfo1->busy_block.busy_size);
       nb_diff1++;
@@ -579,25 +585,25 @@ int mmalloc_compare_heap(simgrid::mc::Snapshot* snapshot1, simgrid::mc::Snapshot
     if (heapinfo1->type <= 0)
       continue;
     for (j = 0; j < (size_t) (BLOCKSIZE >> heapinfo1->type); j++)
-      if (i1 == state->heaplimit
+      if (i1 == state.heaplimit
           && heapinfo1->busy_frag.frag_size[j] > 0
-          && state->equals_to1_(i, j).valid == 0) {
+          && !state.equals_to1_(i, j).valid) {
         XBT_DEBUG("Block %zu, Fragment %zu not found (size used = %zd)",
           i, j, heapinfo1->busy_frag.frag_size[j]);
         nb_diff1++;
       }
   }
 
-  if (i1 == state->heaplimit)
+  if (i1 == state.heaplimit)
     XBT_DEBUG("Number of blocks/fragments not found in heap1 : %d", nb_diff1);
 
-  for (i=1; i < state->heaplimit; i++) {
+  for (i=1; i < state.heaplimit; i++) {
     const malloc_info* heapinfo2 = (const malloc_info*) MC_region_read(
       heap_region2, &heapinfo_temp2, &heapinfos2[i], sizeof(malloc_info));
     if (heapinfo2->type == MMALLOC_TYPE_UNFRAGMENTED
-        && i1 == state->heaplimit
+        && i1 == state.heaplimit
         && heapinfo2->busy_block.busy_size > 0
-        && state->equals_to2_(i, 0).valid == 0) {
+        && !state.equals_to2_(i, 0).valid) {
       XBT_DEBUG("Block %zu not found (size used = %zu)", i,
                 heapinfo2->busy_block.busy_size);
       nb_diff2++;
@@ -607,9 +613,9 @@ int mmalloc_compare_heap(simgrid::mc::Snapshot* snapshot1, simgrid::mc::Snapshot
       continue;
 
     for (j = 0; j < (size_t) (BLOCKSIZE >> heapinfo2->type); j++)
-      if (i1 == state->heaplimit
+      if (i1 == state.heaplimit
           && heapinfo2->busy_frag.frag_size[j] > 0
-          && state->equals_to2_(i, j).valid == 0) {
+          && !state.equals_to2_(i, j).valid) {
         XBT_DEBUG("Block %zu, Fragment %zu not found (size used = %zd)",
           i, j, heapinfo2->busy_frag.frag_size[j]);
         nb_diff2++;
@@ -617,7 +623,7 @@ int mmalloc_compare_heap(simgrid::mc::Snapshot* snapshot1, simgrid::mc::Snapshot
 
   }
 
-  if (i1 == state->heaplimit)
+  if (i1 == state.heaplimit)
     XBT_DEBUG("Number of blocks/fragments not found in heap2 : %d", nb_diff2);
 
   return nb_diff1 > 0 || nb_diff2 > 0;
@@ -635,11 +641,11 @@ int mmalloc_compare_heap(simgrid::mc::Snapshot* snapshot1, simgrid::mc::Snapshot
  * @param check_ignore
  */
 static int compare_heap_area_without_type(
-  simgrid::mc::StateComparator *state, int process_index,
+  simgrid::mc::StateComparator& state, int process_index,
   const void *real_area1, const void *real_area2,
   simgrid::mc::Snapshot* snapshot1,
   simgrid::mc::Snapshot* snapshot2,
-  xbt_dynar_t previous, int size,
+  HeapLocationPairs* previous, int size,
   int check_ignore)
 {
   simgrid::mc::Process* process = &mc_model_checker->process();
@@ -650,10 +656,10 @@ static int compare_heap_area_without_type(
 
     if (check_ignore > 0) {
       ssize_t ignore1 = heap_comparison_ignore_size(
-        state->processStates[0].to_ignore, (char *) real_area1 + i);
+        state.processStates[0].to_ignore, (char *) real_area1 + i);
       if (ignore1 != -1) {
         ssize_t ignore2 = heap_comparison_ignore_size(
-          state->processStates[1].to_ignore, (char *) real_area2 + i);
+          state.processStates[1].to_ignore, (char *) real_area2 + i);
         if (ignore2 == ignore1) {
           if (ignore1 == 0) {
             check_ignore--;
@@ -681,14 +687,14 @@ static int compare_heap_area_without_type(
         continue;
       }
 
-      if (addr_pointed1 > state->std_heap_copy.heapbase
+      if (addr_pointed1 > state.std_heap_copy.heapbase
            && addr_pointed1 < mc_snapshot_get_heap_end(snapshot1)
-           && addr_pointed2 > state->std_heap_copy.heapbase
+           && addr_pointed2 > state.std_heap_copy.heapbase
            && addr_pointed2 < mc_snapshot_get_heap_end(snapshot2)) {
         // Both addreses are in the heap:
-        int res_compare =
-            compare_heap_area(process_index, addr_pointed1, addr_pointed2, snapshot1,
-                              snapshot2, previous, nullptr, 0);
+        int res_compare = compare_heap_area(state ,process_index,
+          addr_pointed1, addr_pointed2,
+          snapshot1, snapshot2, previous, nullptr, 0);
         if (res_compare == 1)
           return res_compare;
         i = pointer_align + sizeof(void *);
@@ -719,11 +725,11 @@ static int compare_heap_area_without_type(
  * @return               0 (same), 1 (different), -1 (unknown)
  */
 static int compare_heap_area_with_type(
-  simgrid::mc::StateComparator *state, int process_index,
+  simgrid::mc::StateComparator& state, int process_index,
   const void *real_area1, const void *real_area2,
   simgrid::mc::Snapshot* snapshot1,
   simgrid::mc::Snapshot* snapshot2,
-  xbt_dynar_t previous, simgrid::mc::Type* type,
+  HeapLocationPairs* previous, simgrid::mc::Type* type,
   int area_size, int check_ignore,
   int pointer_level)
 {
@@ -743,10 +749,10 @@ top:
 
   if (check_ignore > 0) {
     ssize_t ignore1 = heap_comparison_ignore_size(
-      state->processStates[0].to_ignore, real_area1);
+      state.processStates[0].to_ignore, real_area1);
     if (ignore1 > 0
         && heap_comparison_ignore_size(
-          state->processStates[1].to_ignore, real_area2) == ignore1)
+          state.processStates[1].to_ignore, real_area2) == ignore1)
       return 0;
   }
 
@@ -844,13 +850,14 @@ top:
     if (pointer_level <= 1) {
       addr_pointed1 = snapshot1->read(remote((void**)real_area1), process_index);
       addr_pointed2 = snapshot2->read(remote((void**)real_area2), process_index);
-      if (addr_pointed1 > state->std_heap_copy.heapbase
+      if (addr_pointed1 > state.std_heap_copy.heapbase
           && addr_pointed1 < mc_snapshot_get_heap_end(snapshot1)
-          && addr_pointed2 > state->std_heap_copy.heapbase
+          && addr_pointed2 > state.std_heap_copy.heapbase
           && addr_pointed2 < mc_snapshot_get_heap_end(snapshot2))
-        return compare_heap_area(process_index, addr_pointed1, addr_pointed2, snapshot1,
-                                 snapshot2, previous, type->subtype,
-                                 pointer_level);
+        return compare_heap_area(state, process_index,
+            addr_pointed1, addr_pointed2, snapshot1,
+            snapshot2, previous, type->subtype,
+            pointer_level);
       else
         return (addr_pointed1 != addr_pointed2);
     }
@@ -861,14 +868,15 @@ top:
       addr_pointed2 = snapshot2->read(
         remote((void**)((char*) real_area2 + i * sizeof(void *))),
         process_index);
-      if (addr_pointed1 > state->std_heap_copy.heapbase
+      if (addr_pointed1 > state.std_heap_copy.heapbase
           && addr_pointed1 < mc_snapshot_get_heap_end(snapshot1)
-          && addr_pointed2 > state->std_heap_copy.heapbase
+          && addr_pointed2 > state.std_heap_copy.heapbase
           && addr_pointed2 < mc_snapshot_get_heap_end(snapshot2))
         res =
-            compare_heap_area(process_index, addr_pointed1, addr_pointed2, snapshot1,
-                              snapshot2, previous, type->subtype,
-                              pointer_level);
+            compare_heap_area(state, process_index,
+              addr_pointed1, addr_pointed2, snapshot1,
+              snapshot2, previous, type->subtype,
+              pointer_level);
       else
         res = (addr_pointed1 != addr_pointed2);
       if (res == 1)
@@ -988,14 +996,15 @@ static simgrid::mc::Type* get_offset_type(void *real_base_address, simgrid::mc::
  * @return 0 (same), 1 (different), -1
  */
 static
-int compare_heap_area(int process_index, const void *area1, const void *area2, simgrid::mc::Snapshot* snapshot1,
-                      simgrid::mc::Snapshot* snapshot2, xbt_dynar_t previous,
+int compare_heap_area(simgrid::mc::StateComparator& state, int process_index,
+                      const void *area1, const void *area2,
+                      simgrid::mc::Snapshot* snapshot1,
+                      simgrid::mc::Snapshot* snapshot2,
+                      HeapLocationPairs* previous,
                       simgrid::mc::Type* type, int pointer_level)
 {
   simgrid::mc::Process* process = &mc_model_checker->process();
 
-  simgrid::mc::StateComparator *state = mc_diff_info.get();
-
   int res_compare;
   ssize_t block1, frag1, block2, frag2;
   ssize_t size;
@@ -1007,7 +1016,7 @@ int compare_heap_area(int process_index, const void *area1, const void *area2, s
   int new_size1 = -1, new_size2 = -1;
   simgrid::mc::Type *new_type1 = nullptr, *new_type2 = nullptr;
 
-  int match_pairs = 0;
+  bool match_pairs = false;
 
   // This is the address of std_heap->heapinfo in the application process:
   void* heapinfo_address = &((xbt_mheap_t) process->heap_address)->heapinfo;
@@ -1019,45 +1028,42 @@ int compare_heap_area(int process_index, const void *area1, const void *area2, s
 
   malloc_info heapinfo_temp1, heapinfo_temp2;
 
+  simgrid::mc::HeapLocationPairs current;
   if (previous == nullptr) {
-    previous = xbt_dynar_new(sizeof(heap_area_pair_t), [](void *d) {
-      xbt_free((heap_area_pair_t) * (void **) d); });
-    match_pairs = 1;
+    previous = &current;
+    match_pairs = true;
   }
 
   // Get block number:
   block1 =
       ((char *) area1 -
-       (char *) state->std_heap_copy.heapbase) / BLOCKSIZE + 1;
+       (char *) state.std_heap_copy.heapbase) / BLOCKSIZE + 1;
   block2 =
       ((char *) area2 -
-       (char *) state->std_heap_copy.heapbase) / BLOCKSIZE + 1;
+       (char *) state.std_heap_copy.heapbase) / BLOCKSIZE + 1;
 
   // If either block is a stack block:
   if (is_block_stack((int) block1) && is_block_stack((int) block2)) {
-    add_heap_area_pair(previous, block1, -1, block2, -1);
-    if (match_pairs) {
-      state->match_equals(previous);
-      xbt_dynar_free(&previous);
-    }
+    previous->insert(simgrid::mc::makeHeapLocationPair(
+      block1, -1, block2, -1));
+    if (match_pairs)
+      state.match_equals(previous);
     return 0;
   }
 
   // If either block is not in the expected area of memory:
-  if (((char *) area1 < (char *) state->std_heap_copy.heapbase)
-      || (block1 > (ssize_t) state->processStates[0].heapsize) || (block1 < 1)
-      || ((char *) area2 < (char *) state->std_heap_copy.heapbase)
-      || (block2 > (ssize_t) state->processStates[1].heapsize) || (block2 < 1)) {
-    if (match_pairs)
-      xbt_dynar_free(&previous);
+  if (((char *) area1 < (char *) state.std_heap_copy.heapbase)
+      || (block1 > (ssize_t) state.processStates[0].heapsize) || (block1 < 1)
+      || ((char *) area2 < (char *) state.std_heap_copy.heapbase)
+      || (block2 > (ssize_t) state.processStates[1].heapsize) || (block2 < 1)) {
     return 1;
   }
 
   // Process address of the block:
   real_addr_block1 = (ADDR2UINT(block1) - 1) * BLOCKSIZE +
-                 (char *) state->std_heap_copy.heapbase;
+                 (char *) state.std_heap_copy.heapbase;
   real_addr_block2 = (ADDR2UINT(block2) - 1) * BLOCKSIZE +
-                 (char *) state->std_heap_copy.heapbase;
+                 (char *) state.std_heap_copy.heapbase;
 
   if (type) {
 
@@ -1089,10 +1095,8 @@ int compare_heap_area(int process_index, const void *area1, const void *area2, s
   if ((heapinfo1->type == MMALLOC_TYPE_FREE || heapinfo1->type==MMALLOC_TYPE_HEAPINFO)
     && (heapinfo2->type == MMALLOC_TYPE_FREE || heapinfo2->type ==MMALLOC_TYPE_HEAPINFO)) {
     /* Free block */
-    if (match_pairs) {
-      state->match_equals(previous);
-      xbt_dynar_free(&previous);
-    }
+    if (match_pairs)
+      state.match_equals(previous);
     return 0;
   }
 
@@ -1105,13 +1109,11 @@ int compare_heap_area(int process_index, const void *area1, const void *area2, s
     offset1 = (char *) area1 - (char *) real_addr_block1;
     offset2 = (char *) area2 - (char *) real_addr_block2;
 
-    if (state->equals_to1_(block1, 0).valid
-        && state->equals_to2_(block2, 0).valid
-        && state->blocksEqual(block1, block2)) {
-      if (match_pairs) {
-        state->match_equals(previous);
-        xbt_dynar_free(&previous);
-      }
+    if (state.equals_to1_(block1, 0).valid
+        && state.equals_to2_(block2, 0).valid
+        && state.blocksEqual(block1, block2)) {
+      if (match_pairs)
+        state.match_equals(previous);
       return 0;
     }
 
@@ -1119,31 +1121,21 @@ int compare_heap_area(int process_index, const void *area1, const void *area2, s
       if (type_size != (ssize_t) heapinfo1->busy_block.busy_size
           && type_size != (ssize_t)   heapinfo2->busy_block.busy_size
           && (type->name.empty() || type->name == "struct s_smx_context")) {
-        if (match_pairs) {
-          state->match_equals(previous);
-          xbt_dynar_free(&previous);
-        }
+        if (match_pairs)
+          state.match_equals(previous);
         return -1;
       }
     }
 
-    if (heapinfo1->busy_block.size != heapinfo2->busy_block.size) {
-      if (match_pairs)
-        xbt_dynar_free(&previous);
+    if (heapinfo1->busy_block.size != heapinfo2->busy_block.size)
       return 1;
-    }
-
-    if (heapinfo1->busy_block.busy_size != heapinfo2->busy_block.busy_size) {
-      if (match_pairs)
-        xbt_dynar_free(&previous);
+    if (heapinfo1->busy_block.busy_size != heapinfo2->busy_block.busy_size)
       return 1;
-    }
 
-    if (!add_heap_area_pair(previous, block1, -1, block2, -1)) {
-      if (match_pairs) {
-        state->match_equals(previous);
-        xbt_dynar_free(&previous);
-      }
+    if (!previous->insert(simgrid::mc::makeHeapLocationPair(
+        block1, -1, block2, -1)).second) {
+      if (match_pairs)
+        state.match_equals(previous);
       return 0;
     }
 
@@ -1152,15 +1144,13 @@ int compare_heap_area(int process_index, const void *area1, const void *area2, s
     // Remember (basic) type inference.
     // The current data structure only allows us to do this for the whole block.
     if (type != nullptr && area1 == real_addr_block1)
-      state->types1_(block1, 0) = type;
+      state.types1_(block1, 0) = type;
     if (type != nullptr && area2 == real_addr_block2)
-      state->types2_(block2, 0) = type;
+      state.types2_(block2, 0) = type;
 
     if (size <= 0) {
-      if (match_pairs) {
-        state->match_equals(previous);
-        xbt_dynar_free(&previous);
-      }
+      if (match_pairs)
+        state.match_equals(previous);
       return 0;
     }
 
@@ -1191,31 +1181,25 @@ int compare_heap_area(int process_index, const void *area1, const void *area2, s
     if (type_size != -1) {
       if (heapinfo1->busy_frag.frag_size[frag1] == -1
           || heapinfo2->busy_frag.frag_size[frag2] == -1) {
-        if (match_pairs) {
-          state->match_equals(previous);
-          xbt_dynar_free(&previous);
-        }
+        if (match_pairs)
+          state.match_equals(previous);
         return -1;
       }
       // ?
       if (type_size != heapinfo1->busy_frag.frag_size[frag1]
           || type_size != heapinfo2->busy_frag.frag_size[frag2]) {
-        if (match_pairs) {
-          state->match_equals(previous);
-          xbt_dynar_free(&previous);
-        }
+        if (match_pairs)
+          state.match_equals(previous);
         return -1;
       }
     }
 
     // Check if the blocks are already matched together:
-    if (state->equals_to1_(block1, frag1).valid
-        && state->equals_to2_(block2, frag2).valid) {
-      if (offset1==offset2 && state->fragmentsEqual(block1, frag1, block2, frag2)) {
-        if (match_pairs) {
-          state->match_equals(previous);
-          xbt_dynar_free(&previous);
-        }
+    if (state.equals_to1_(block1, frag1).valid
+        && state.equals_to2_(block2, frag2).valid) {
+      if (offset1==offset2 && state.fragmentsEqual(block1, frag1, block2, frag2)) {
+        if (match_pairs)
+          state.match_equals(previous);
         return 0;
       }
     }
@@ -1223,16 +1207,11 @@ int compare_heap_area(int process_index, const void *area1, const void *area2, s
     if (heapinfo1->busy_frag.frag_size[frag1] !=
         heapinfo2->busy_frag.frag_size[frag2]) {
       if (type_size == -1) {
-        if (match_pairs) {
-          state->match_equals(previous);
-          xbt_dynar_free(&previous);
-        }
-        return -1;
-      } else {
         if (match_pairs)
-          xbt_dynar_free(&previous);
+          state.match_equals(previous);
+        return -1;
+      } else
         return 1;
-      }
     }
 
     // Size of the fragment:
@@ -1241,9 +1220,9 @@ int compare_heap_area(int process_index, const void *area1, const void *area2, s
     // Remember (basic) type inference.
     // The current data structure only allows us to do this for the whole fragment.
     if (type != nullptr && area1 == real_addr_frag1)
-      state->types1_(block1, frag1) = type;
+      state.types1_(block1, frag1) = type;
     if (type != nullptr && area2 == real_addr_frag2)
-      state->types2_(block2, frag2) = type;
+      state.types2_(block2, frag2) = type;
 
     // The type of the variable is already known:
     if (type) {
@@ -1251,39 +1230,37 @@ int compare_heap_area(int process_index, const void *area1, const void *area2, s
       new_type2 = type;
     }
     // Type inference from the block type.
-    else if (state->types1_(block1, frag1) != nullptr
-             || state->types2_(block2, frag2) != nullptr) {
+    else if (state.types1_(block1, frag1) != nullptr
+             || state.types2_(block2, frag2) != nullptr) {
 
       offset1 = (char *) area1 - (char *) real_addr_frag1;
       offset2 = (char *) area2 - (char *) real_addr_frag2;
 
-      if (state->types1_(block1, frag1) != nullptr
-          && state->types2_(block2, frag2) != nullptr) {
+      if (state.types1_(block1, frag1) != nullptr
+          && state.types2_(block2, frag2) != nullptr) {
         new_type1 =
-            get_offset_type(real_addr_frag1, state->types1_(block1, frag1),
+            get_offset_type(real_addr_frag1, state.types1_(block1, frag1),
                             offset1, size, snapshot1, process_index);
         new_type2 =
-            get_offset_type(real_addr_frag2, state->types2_(block2, frag2),
+            get_offset_type(real_addr_frag2, state.types2_(block2, frag2),
                             offset1, size, snapshot2, process_index);
-      } else if (state->types1_(block1, frag1) != nullptr) {
+      } else if (state.types1_(block1, frag1) != nullptr) {
         new_type1 =
-            get_offset_type(real_addr_frag1, state->types1_(block1, frag1),
+            get_offset_type(real_addr_frag1, state.types1_(block1, frag1),
                             offset1, size, snapshot1, process_index);
         new_type2 =
-            get_offset_type(real_addr_frag2, state->types1_(block1, frag1),
+            get_offset_type(real_addr_frag2, state.types1_(block1, frag1),
                             offset2, size, snapshot2, process_index);
-      } else if (state->types2_(block2, frag2) != nullptr) {
+      } else if (state.types2_(block2, frag2) != nullptr) {
         new_type1 =
-            get_offset_type(real_addr_frag1, state->types2_(block2, frag2),
+            get_offset_type(real_addr_frag1, state.types2_(block2, frag2),
                             offset1, size, snapshot1, process_index);
         new_type2 =
-            get_offset_type(real_addr_frag2, state->types2_(block2, frag2),
+            get_offset_type(real_addr_frag2, state.types2_(block2, frag2),
                             offset2, size, snapshot2, process_index);
       } else {
-        if (match_pairs) {
-          state->match_equals(previous);
-          xbt_dynar_free(&previous);
-        }
+        if (match_pairs)
+          state.match_equals(previous);
         return -1;
       }
 
@@ -1300,10 +1277,8 @@ int compare_heap_area(int process_index, const void *area1, const void *area2, s
         new_size2 = type->byte_size;
 
       } else {
-        if (match_pairs) {
-          state->match_equals(previous);
-          xbt_dynar_free(&previous);
-        }
+        if (match_pairs)
+          state.match_equals(previous);
         return -1;
       }
     }
@@ -1314,19 +1289,16 @@ int compare_heap_area(int process_index, const void *area1, const void *area2, s
     }
 
     if (offset1 == 0 && offset2 == 0
-      && !add_heap_area_pair(previous, block1, frag1, block2, frag2)) {
-        if (match_pairs) {
-          state->match_equals(previous);
-          xbt_dynar_free(&previous);
-        }
+      && !previous->insert(simgrid::mc::makeHeapLocationPair(
+        block1, frag1, block2, frag2)).second) {
+        if (match_pairs)
+          state.match_equals(previous);
         return 0;
       }
 
     if (size <= 0) {
-      if (match_pairs) {
-        state->match_equals(previous);
-        xbt_dynar_free(&previous);
-      }
+      if (match_pairs)
+        state.match_equals(previous);
       return 0;
     }
 
@@ -1335,11 +1307,8 @@ int compare_heap_area(int process_index, const void *area1, const void *area2, s
             heapinfo1->busy_frag.ignore[frag1]))
       check_ignore = heapinfo1->busy_frag.ignore[frag1];
 
-  } else {
-    if (match_pairs)
-      xbt_dynar_free(&previous);
+  } else
     return 1;
-  }
 
 
   /* Start comparison */
@@ -1353,55 +1322,21 @@ int compare_heap_area(int process_index, const void *area1, const void *area2, s
         compare_heap_area_without_type(state, process_index, area1, area2, snapshot1, snapshot2,
                                        previous, size, check_ignore);
 
-  if (res_compare == 1) {
-    if (match_pairs)
-      xbt_dynar_free(&previous);
+  if (res_compare == 1)
     return res_compare;
-  }
-
-  if (match_pairs) {
-    state->match_equals(previous);
-    xbt_dynar_free(&previous);
-  }
 
+  if (match_pairs)
+    state.match_equals(previous);
   return 0;
 }
 
 }
 }
 
-namespace simgrid {
-namespace mc {
-
-/** A hash which works with more stuff
- *
- *  It can hash pairs: the standard hash currently doesn't include this.
- */
-template<class X> struct hash : public std::hash<X> {};
-
-template<class X, class Y>
-struct hash<std::pair<X,Y>> {
-  std::size_t operator()(std::pair<X,Y>const& x) const
-  {
-    struct hash<X> h1;
-    struct hash<X> h2;
-    return h1(x.first) ^ h2(x.second);
-  }
-};
-
-struct ComparisonState {
-  std::unordered_set<std::pair<void*, void*>, hash<std::pair<void*, void*>>> compared_pointers;
-};
-
-}
-}
-
-using simgrid::mc::ComparisonState;
-
 /************************** Snapshot comparison *******************************/
 /******************************************************************************/
 
-static int compare_areas_with_type(ComparisonState& state,
+static int compare_areas_with_type(simgrid::mc::StateComparator& state,
                                    int process_index,
                                    void* real_area1, simgrid::mc::Snapshot* snapshot1, mc_mem_region_t region1,
                                    void* real_area2, simgrid::mc::Snapshot* snapshot2, mc_mem_region_t region2,
@@ -1503,8 +1438,9 @@ static int compare_areas_with_type(ComparisonState& state,
              && addr_pointed2 < mc_snapshot_get_heap_end(snapshot2)))
           return 1;
         // The pointers are both in the heap:
-        return simgrid::mc::compare_heap_area(process_index, addr_pointed1, addr_pointed2, snapshot1,
-                                 snapshot2, nullptr, type->subtype, pointer_level);
+        return simgrid::mc::compare_heap_area(state,
+          process_index, addr_pointed1, addr_pointed2, snapshot1,
+          snapshot2, nullptr, type->subtype, pointer_level);
       }
 
       // The pointers are both in the current object R/W segment:
@@ -1557,11 +1493,12 @@ static int compare_areas_with_type(ComparisonState& state,
   return 0;
 }
 
-static int compare_global_variables(simgrid::mc::ObjectInformation* object_info,
-                                    int process_index,
-                                    mc_mem_region_t r1,
-                                    mc_mem_region_t r2, simgrid::mc::Snapshot* snapshot1,
-                                    simgrid::mc::Snapshot* snapshot2)
+static int compare_global_variables(
+  simgrid::mc::StateComparator& state,
+  simgrid::mc::ObjectInformation* object_info,
+  int process_index,
+  mc_mem_region_t r1, mc_mem_region_t r2,
+  simgrid::mc::Snapshot* snapshot1, simgrid::mc::Snapshot* snapshot2)
 {
   xbt_assert(r1 && r2, "Missing region.");
 
@@ -1577,7 +1514,8 @@ static int compare_global_variables(simgrid::mc::ObjectInformation* object_info,
 
     // Compare the global variables separately for each simulates process:
     for (size_t process_index = 0; process_index < process_count; process_index++) {
-      int is_diff = compare_global_variables(object_info, process_index,
+      int is_diff = compare_global_variables(state,
+        object_info, process_index,
         &r1->privatized_data()[process_index],
         &r2->privatized_data()[process_index],
         snapshot1, snapshot2);
@@ -1590,8 +1528,6 @@ static int compare_global_variables(simgrid::mc::ObjectInformation* object_info,
 #endif
   xbt_assert(r2->storage_type() != simgrid::mc::StorageType::Privatized);
 
-  ComparisonState state;
-
   std::vector<simgrid::mc::Variable>& variables = object_info->global_variables;
 
   for (simgrid::mc::Variable& current_var : variables) {
@@ -1604,8 +1540,7 @@ static int compare_global_variables(simgrid::mc::ObjectInformation* object_info,
       continue;
 
     simgrid::mc::Type* bvariable_type = current_var.type;
-    int res =
-        compare_areas_with_type(state, process_index,
+    int res = compare_areas_with_type(state, process_index,
                                 (char *) current_var.address, snapshot1, r1,
                                 (char *) current_var.address, snapshot2, r2,
                                 bvariable_type, 0);
@@ -1622,14 +1557,13 @@ static int compare_global_variables(simgrid::mc::ObjectInformation* object_info,
 
 }
 
-static int compare_local_variables(int process_index,
+static int compare_local_variables(simgrid::mc::StateComparator& state,
+                                   int process_index,
                                    simgrid::mc::Snapshot* snapshot1,
                                    simgrid::mc::Snapshot* snapshot2,
                                    mc_snapshot_stack_t stack1,
                                    mc_snapshot_stack_t stack2)
 {
-  ComparisonState state;
-
   if (stack1->local_variables.size() != stack2->local_variables.size()) {
     XBT_VERB("Different number of local variables");
     return 1;
@@ -1683,8 +1617,17 @@ static int compare_local_variables(int process_index,
 namespace simgrid {
 namespace mc {
 
+static std::unique_ptr<simgrid::mc::StateComparator> state_comparator;
+
 int snapshot_compare(int num1, simgrid::mc::Snapshot* s1, int num2, simgrid::mc::Snapshot* s2)
 {
+  // TODO, make this a field of ModelChecker or something similar
+
+  if (state_comparator == nullptr)
+    state_comparator = std::unique_ptr<StateComparator>(new StateComparator());
+  else
+    state_comparator->clear();
+
   simgrid::mc::Process* process = &mc_model_checker->process();
 
   int errors = 0;
@@ -1743,7 +1686,9 @@ int snapshot_compare(int num1, simgrid::mc::Snapshot* s1, int num2, simgrid::mc:
     alloca(sizeof(struct mdesc)), sizeof(struct mdesc),
     remote(process->heap_address),
     simgrid::mc::ProcessIndexMissing, simgrid::mc::ReadOptions::lazy());
-  res_init = simgrid::mc::init_heap_information(heap1, heap2, &s1->to_ignore, &s2->to_ignore);
+  res_init = state_comparator->initHeapInformation(
+    heap1, heap2, &s1->to_ignore, &s2->to_ignore);
+
   if (res_init == -1) {
 #ifdef MC_DEBUG
     XBT_DEBUG("(%d - %d) Different heap information", num1, num2);
@@ -1773,8 +1718,8 @@ int snapshot_compare(int num1, simgrid::mc::Snapshot* s1, int num2, simgrid::mc:
       XBT_DEBUG("(%d - %d) Stacks with different process index (%i vs %i)", num1, num2,
         stack1->process_index, stack2->process_index);
     }
-    else diff_local =
-        compare_local_variables(stack1->process_index, s1, s2, stack1, stack2);
+    else diff_local = compare_local_variables(*state_comparator,
+      stack1->process_index, s1, s2, stack1, stack2);
     if (diff_local > 0) {
 #ifdef MC_DEBUG
       XBT_DEBUG("(%d - %d) Different local variables between stacks %d", num1,
@@ -1788,8 +1733,6 @@ int snapshot_compare(int num1, simgrid::mc::Snapshot* s1, int num2, simgrid::mc:
                num2, cursor + 1);
 #endif
 
-      simgrid::mc::reset_heap_information();
-
       return 1;
 #endif
     }
@@ -1816,10 +1759,9 @@ int snapshot_compare(int num1, simgrid::mc::Snapshot* s1, int num2, simgrid::mc:
 
     /* Compare global variables */
     is_diff =
-      compare_global_variables(region1->object_info(),
-        simgrid::mc::ProcessIndexDisabled,
-        region1, region2,
-        s1, s2);
+      compare_global_variables(*state_comparator,
+        region1->object_info(), simgrid::mc::ProcessIndexDisabled,
+        region1, region2, s1, s2);
 
     if (is_diff != 0) {
 #ifdef MC_DEBUG
@@ -1838,7 +1780,7 @@ int snapshot_compare(int num1, simgrid::mc::Snapshot* s1, int num2, simgrid::mc:
   }
 
   /* Compare heap */
-  if (simgrid::mc::mmalloc_compare_heap(s1, s2) > 0) {
+  if (simgrid::mc::mmalloc_compare_heap(*state_comparator, s1, s2) > 0) {
 
 #ifdef MC_DEBUG
     XBT_DEBUG("(%d - %d) Different heap (mmalloc_compare)", num1, num2);
@@ -1853,8 +1795,6 @@ int snapshot_compare(int num1, simgrid::mc::Snapshot* s1, int num2, simgrid::mc:
 #endif
   }
 
-  simgrid::mc::reset_heap_information();
-
 #ifdef MC_VERBOSE
   if (errors || hash_result)
     XBT_VERB("(%d - %d) Difference found", num1, num2);