Reduce pvector delta_cell quota on reads. Add example that demonstrates why this is needed.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/tests/util/pvector.cpp

@@ -8,8 +8,11 @@ Author: Leonardo de Moura
 #include <cstdlib>
 #include "test.h"
 #include "pvector.h"
+#include "timeit.h"
 using namespace lean;
 
+// #define PVECTOR_PERF_TEST
+
 static void tst1() {
     pvector<int> v;
     lean_assert(v.empty());
@@ -96,10 +99,21 @@ static void tst2() {
     driver(128, 1000, 10000, 0.2, 0.1);
 }
 
-// #define PVECTOR_PERF_TEST
+static void tst3() {
-#ifdef PVECTOR_PERF_TEST
+    timeit t(std::cout, "tst3");
-#include "timeit.h"
+    unsigned N = 20000;
+    unsigned M = 20000;
+    pvector<int> v;
+    for (unsigned i = 0; i < N; i++) v.push_back(i);
+    pvector<int> v2 = v;
+    for (unsigned i = 0; i < N / 2; i++) v2.push_back(i);
+    // v2 has a long trail of deltas
+    // Now, we only read v2
+    unsigned s = 0;
+    for (unsigned i = 0; i < M; i++) { s += v2[i % v2.size()]; }
+}
 
+#ifdef PVECTOR_PERF_TEST
 static void perf_vector(unsigned n) {
     std::vector<int> q;
     for (unsigned i = 0; i < n; i++) {
@@ -173,6 +187,7 @@ static void tst_perf2() {
 int main() {
     tst1();
     tst2();
+    tst3();
 #ifdef PVECTOR_PERF_TEST
     tst_perf1();
     tst_perf2();

src/util/pvector.h

@@ -30,6 +30,7 @@ class pvector {
         cell_kind m_kind;
         MK_LEAN_RC();
         cell(cell_kind k):m_kind(k), m_rc(0) {}
+        cell(cell const & c):m_kind(c.m_kind), m_rc(0) {}
         void dealloc();
         unsigned size() const;
         /**
@@ -59,6 +60,10 @@ class pvector {
             lean_assert(m_prev);
             m_prev->inc_ref();
         }
+        delta_cell(delta_cell const & c):cell(c), m_size(c.m_size), m_quota(c.m_quota), m_prev(c.m_prev) {
+            lean_assert(m_prev);
+            m_prev->inc_ref();
+        }
         ~delta_cell() { lean_assert(m_prev); m_prev->dec_ref(); }
     };
 
@@ -68,6 +73,7 @@ class pvector {
     */
     struct pop_cell : public delta_cell {
         pop_cell(cell * prev):delta_cell(cell_kind::PopBack, prev->size() - 1, prev) {}
+        pop_cell(pop_cell const & c):delta_cell(c) {}
     };
 
     /**
@@ -77,6 +83,7 @@ class pvector {
     struct push_cell : public delta_cell {
         T m_val;
         push_cell(T const & v, cell * prev):delta_cell(cell_kind::PushBack, prev->size() + 1, prev), m_val(v) {}
+        push_cell(push_cell const & c):delta_cell(c), m_val(c.m_val) {}
     };
 
     /**
@@ -87,6 +94,7 @@ class pvector {
         unsigned m_idx;
         T        m_val;
         set_cell(unsigned i, T const & v, cell * prev):delta_cell(cell_kind::Set, prev->size(), prev), m_idx(i), m_val(v) {}
+        set_cell(set_cell const & c):delta_cell(c), m_idx(c.m_idx), m_val(c.m_val) {}
     };
 
     static push_cell & to_push(cell * c) { lean_assert(c->kind() == cell_kind::PushBack); return *static_cast<push_cell*>(c); }
@@ -101,6 +109,9 @@ class pvector {
     cell * m_ptr;
     pvector(cell * d):m_ptr(d) { lean_assert(m_ptr); m_ptr->inc_ref(); }
 
+    /** \brief Return true iff the cell associated with this vector is shared */
+    bool is_shared() const { return m_ptr->get_rc() > 1; }
+
     /** \brief Update the cell (and reference counters) of this vector */
     void update_cell(cell * new_cell) {
         lean_assert(new_cell);
@@ -110,29 +121,26 @@ class pvector {
         m_ptr = new_cell;
     }
 
-    /** \brief Return true iff the cell associated with this vector is shared */
-    bool is_shared() const { return m_ptr->get_rc() > 1; }
-
     /**
-       \brief Auxiliary method for \c flat_if_needed.
+       \brief Auxiliary method for \c flat
-       Given an empty vector \c r, then <tt>flat(c, r)</tt> will
+       Given an empty vector \c r, then <tt>flat_core(c, r)</tt> will
        store in r the vector represented by cell \c c.
        That is, the vector obtained after finding the root cell (aka wrapper for std::vector),
        and applying all deltas.
     */
-    static void flat(cell * c, std::vector<T> & r) {
+    static void flat_core(cell * c, std::vector<T> & r) {
         lean_assert(r.empty());
         switch(c->kind()) {
         case cell_kind::PushBack:
-            flat(to_push(c).m_prev, r);
+            flat_core(to_push(c).m_prev, r);
             r.push_back(to_push(c).m_val);
             break;
         case cell_kind::PopBack:
-            flat(to_pop(c).m_prev, r);
+            flat_core(to_pop(c).m_prev, r);
             r.pop_back();
             break;
         case cell_kind::Set:
-            flat(to_set(c).m_prev, r);
+            flat_core(to_set(c).m_prev, r);
             r[to_set(c).m_idx] = to_set(c).m_val;
             break;
         case cell_kind::Root:
@@ -141,6 +149,18 @@ class pvector {
         }
     }
 
+    /**
+       \brief Change the representation to a root cell.
+    */
+    void flat() {
+        lean_assert(m_ptr->kind() != cell_kind::Root);
+        std::vector<T> r;
+        flat_core(m_ptr, r);
+        update_cell(new root_cell());
+        to_root(m_ptr).m_vector.swap(r);
+        lean_assert(!is_shared());
+    }
+
     /**
        \brief If the quota associated with m_cell is zero, then
        compute a flat representation. That is, represent the vector
@@ -149,11 +169,29 @@ class pvector {
     void flat_if_needed() {
         lean_assert(m_ptr->kind() != cell_kind::Root);
         if (static_cast<delta_cell*>(m_ptr)->m_quota == 0) {
-            std::vector<T> r;
+            flat();
-            flat(m_ptr, r);
+        }
-            update_cell(new root_cell());
+    }
-            to_root(m_ptr).m_vector.swap(r);
+
-            lean_assert(!is_shared());
+    /** \brief Update quota based on the cost of a read */
+    void update_quota_on_read(unsigned cost) {
+        cost /= 2; // reads are cheaper than writes
+        if (cost > 0) {
+            if (cost >= m_ptr->quota()) {
+                flat();
+            } else {
+                if (is_shared()) {
+                    switch (m_ptr->kind()) {
+                    case cell_kind::PushBack: update_cell(new push_cell(to_push(m_ptr))); break;
+                    case cell_kind::PopBack:  update_cell(new pop_cell(to_pop(m_ptr))); break;
+                    case cell_kind::Set:      update_cell(new set_cell(to_set(m_ptr))); break;
+                    case cell_kind::Root:     lean_unreachable(); break;
+                    }
+                }
+                lean_assert(!is_shared());
+                lean_assert(cost < static_cast<delta_cell*>(m_ptr)->m_quota);
+                static_cast<delta_cell*>(m_ptr)->m_quota -= cost;
+            }
         }
     }
 
@@ -183,30 +221,33 @@ public:
     /**
         \brief Access specified element
         \pre i < size()
-
-        TODO: Consider if we should reduce m_quota
-        reading. Another possibility is to
-        have a maximum number of delta_cells
     */
     T const & operator[](unsigned i) const {
         lean_assert(i < size());
         cell const * it = m_ptr;
+        unsigned cost = 0;
         while (true) {
             switch (it->kind()) {
             case cell_kind::PushBack:
-                if (i + 1 == to_push(it).m_size)
+                if (i + 1 == to_push(it).m_size) {
+                    const_cast<pvector*>(this)->update_quota_on_read(cost);
                     return to_push(it).m_val;
+                }
                 break;
             case cell_kind::PopBack:
                 break;
             case cell_kind::Set:
-                if (to_set(it).m_idx == i)
+                if (to_set(it).m_idx == i) {
+                    const_cast<pvector*>(this)->update_quota_on_read(cost);
                     return to_set(it).m_val;
+                }
                 break;
             case cell_kind::Root:
+                const_cast<pvector*>(this)->update_quota_on_read(cost);
                 return to_root(it).m_vector[i];
             }
             it = static_cast<delta_cell const *>(it)->m_prev;
+            cost++;
         }
     }