From cad379333d99ec9d823a38245f25559f682d2007 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 28 Feb 2017 15:04:07 -0800
Subject: [PATCH] feat(util/memory_pool): put limit on the size of memory_pool
 free_lists

See #1405

Memory consumption is still high, but I didn't manage to cross the 2Gb
limit anymore with this commit even after hundreds of modifications.

@gebner I'm not seeing a big difference betwee Lean without memory_pool,
with bounded memory_pool and unbounded memory_pool. We may even consider
removing it in the future after a more careful benchmarking.

In the benchmark (https://gist.github.com/leodemoura/b27fb4203a13a67274b388a602149303),
I'm getting the following numbers:

- No memory_pool: runtimes between 3.532s - 3.556s

- With memory_pool bounded by 8192: runtimes between 3.32s - 3.44s

- With memory_pool (with no limit): runtimes between 3.32s - 3.44s

On the other hand, the small object allocator makes a big difference.
I used your list_rev.lean example.

- with:    2.62s
- without: 3.75s
---
 src/util/memory_pool.cpp |  1 +
 src/util/memory_pool.h   | 14 +++++++++++---
 2 files changed, 12 insertions(+), 3 deletions(-)

diff --git a/src/util/memory_pool.cpp b/src/util/memory_pool.cpp
index 021715f52f..a6d4f23298 100644
--- a/src/util/memory_pool.cpp
+++ b/src/util/memory_pool.cpp
@@ -24,6 +24,7 @@ void * memory_pool::allocate() {
     if (m_free_list != nullptr) {
         void * r = m_free_list;
         m_free_list = *(reinterpret_cast<void **>(r));
+        m_free_list_size--;
         return r;
     } else {
         return malloc(m_size);
diff --git a/src/util/memory_pool.h b/src/util/memory_pool.h
index 1136e565d0..38e7898da4 100644
--- a/src/util/memory_pool.h
+++ b/src/util/memory_pool.h
@@ -7,21 +7,29 @@ Author: Leonardo de Moura
 #pragma once
 #include "util/memory.h"
 
+#define LEAN_FREE_LIST_MAX_SIZE 8192
+
 namespace lean {
 /** \brief Auxiliary object for "recycling" allocated memory of fixed size */
 class memory_pool {
     unsigned m_size;
+    unsigned m_free_list_size;
     void *   m_free_list;
 public:
-    memory_pool(unsigned size):m_size(size), m_free_list(nullptr) {}
+    memory_pool(unsigned size):m_size(size), m_free_list_size(0), m_free_list(nullptr) {}
     ~memory_pool();
     void * allocate();
     void recycle(void * ptr) {
 #ifdef LEAN_NO_CUSTOM_ALLOCATORS
         free(ptr);
 #else
-        *(reinterpret_cast<void**>(ptr)) = m_free_list;
-        m_free_list = ptr;
+        if (m_free_list_size > LEAN_FREE_LIST_MAX_SIZE) {
+            free(ptr);
+        } else {
+            *(reinterpret_cast<void**>(ptr)) = m_free_list;
+            m_free_list = ptr;
+            m_free_list_size++;
+        }
 #endif
     }
 };