From 39ef7aeee2f9e1ed7442bbfc2a349f6dddd07861 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 12 Apr 2018 10:45:33 -0700
Subject: [PATCH] chore(util): remove memory_pool

memory_pool object introduces memory contention and unnecessary
complexity. Moreover, it actually reduces performance when we compile
Lean using JEMALLOC.

Here are the numbers for corelib

jemalloc with memory_pool:    13.83 secs
jemalloc without memory_pool: 13.60 secs
---
 src/kernel/expr.cpp           | 59 +++++++++++++----------------------
 src/library/local_context.cpp |  7 ++---
 src/library/parray.h          | 29 +++--------------
 src/library/vm/vm.cpp         |  1 +
 src/tests/library/parray.cpp  |  2 --
 src/util/CMakeLists.txt       |  2 +-
 src/util/init_module.cpp      |  1 -
 src/util/list.h               | 17 +++-------
 src/util/memory_pool.cpp      | 57 ---------------------------------
 src/util/memory_pool.h        | 47 ----------------------------
 src/util/name.cpp             |  7 ++---
 src/util/rb_tree.h            | 15 ++-------
 src/util/sequence.h           | 25 +++------------
 13 files changed, 42 insertions(+), 227 deletions(-)
 delete mode 100644 src/util/memory_pool.cpp
 delete mode 100644 src/util/memory_pool.h

diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index 3e8459b9d5..309543bd81 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -14,7 +14,6 @@ Author: Leonardo de Moura
 #include "util/hash.h"
 #include "util/buffer.h"
 #include "util/object_serializer.h"
-#include "util/memory_pool.h"
 #include "kernel/expr.h"
 #include "kernel/expr_eq_fn.h"
 #include "kernel/expr_sets.h"
@@ -129,7 +128,6 @@ bool is_meta(expr const & e) {
 }
 
 // Expr variables
-DEF_THREAD_MEMORY_POOL(get_var_allocator, sizeof(expr_var));
 expr_var::expr_var(unsigned idx, tag g):
     expr_cell(expr_kind::Var, idx, false, false, false, false, g),
     m_vidx(idx) {
@@ -137,12 +135,10 @@ expr_var::expr_var(unsigned idx, tag g):
         throw exception("invalid free variable index, de Bruijn index is too big");
 }
 void expr_var::dealloc() {
-    this->~expr_var();
-    get_var_allocator().recycle(this);
+    delete this;
 }
 
 // Expr constants
-DEF_THREAD_MEMORY_POOL(get_const_allocator, sizeof(expr_const));
 expr_const::expr_const(name const & n, levels const & ls, tag g):
     expr_cell(expr_kind::Constant, ::lean::hash(n.hash(), hash_levels(ls)), false,
               has_meta(ls), false, has_param(ls), g),
@@ -150,8 +146,7 @@ expr_const::expr_const(name const & n, levels const & ls, tag g):
     m_levels(ls) {
 }
 void expr_const::dealloc() {
-    this->~expr_const();
-    get_const_allocator().recycle(this);
+    delete this;
 }
 
 unsigned binder_info::hash() const {
@@ -159,7 +154,6 @@ unsigned binder_info::hash() const {
 }
 
 // Expr metavariables and local variables
-DEF_THREAD_MEMORY_POOL(get_mlocal_allocator, sizeof(expr_mlocal));
 expr_mlocal::expr_mlocal(bool is_meta, name const & n, name const & pp_n, expr const & t, tag g):
     expr_composite(is_meta ? expr_kind::Meta : expr_kind::Local, n.hash(), is_meta || t.has_expr_metavar(), t.has_univ_metavar(),
                    !is_meta || t.has_local(), t.has_param_univ(),
@@ -170,14 +164,12 @@ expr_mlocal::expr_mlocal(bool is_meta, name const & n, name const & pp_n, expr c
 
 void expr_mlocal::dealloc(buffer<expr_cell*> & todelete) {
     dec_ref(m_type, todelete);
-    this->~expr_mlocal();
-    get_mlocal_allocator().recycle(this);
+    delete this;
 }
 
 expr_mlocal::expr_mlocal(expr_mlocal const & src, expr const & new_type):
     expr_composite(src), m_name(src.m_name), m_pp_name(src.m_pp_name), m_type(new_type) {}
 
-DEF_THREAD_MEMORY_POOL(get_local_allocator, sizeof(expr_local));
 expr_local::expr_local(name const & n, name const & pp_n, expr const & t, binder_info const & bi, tag g):
     expr_mlocal(false, n, pp_n, t, g), m_bi(bi) {}
 
@@ -186,8 +178,7 @@ expr_local::expr_local(expr_local const & src, expr const & new_type):
 
 void expr_local::dealloc(buffer<expr_cell*> & todelete) {
     dec_ref(m_type, todelete);
-    this->~expr_local();
-    get_local_allocator().recycle(this);
+    delete this;
 }
 
 expr_composite::expr_composite(expr_composite const & src):
@@ -206,7 +197,6 @@ expr_composite::expr_composite(expr_kind k, unsigned h, bool has_expr_mv, bool h
     m_free_var_range(fv_range) {}
 
 // Expr applications
-DEF_THREAD_MEMORY_POOL(get_app_allocator, sizeof(expr_app));
 expr_app::expr_app(expr const & fn, expr const & arg, tag g):
     expr_composite(expr_kind::App, ::lean::hash(fn.hash(), arg.hash()),
                    fn.has_expr_metavar() || arg.has_expr_metavar(),
@@ -228,8 +218,7 @@ expr_app::expr_app(expr_app const & src, expr const & new_fn, expr const & new_a
 void expr_app::dealloc(buffer<expr_cell*> & todelete) {
     dec_ref(m_fn, todelete);
     dec_ref(m_arg, todelete);
-    this->~expr_app();
-    get_app_allocator().recycle(this);
+    delete this;
 }
 
 static unsigned dec(unsigned k) { return k == 0 ? 0 : k - 1; }
@@ -243,7 +232,6 @@ bool operator==(binder_info const & i1, binder_info const & i2) {
 }
 
 // Expr binders (Lambda, Pi)
-DEF_THREAD_MEMORY_POOL(get_binding_allocator, sizeof(expr_binding));
 expr_binding::expr_binding(expr_kind k, name const & n, expr const & t, expr const & b, binder_info const & i, tag g):
     expr_composite(k, ::lean::hash(t.hash(), b.hash()),
                    t.has_expr_metavar()   || b.has_expr_metavar(),
@@ -267,24 +255,20 @@ expr_binding::expr_binding(expr_binding const & src, expr const & d, expr const
 void expr_binding::dealloc(buffer<expr_cell*> & todelete) {
     dec_ref(m_body, todelete);
     dec_ref(m_binder.m_type, todelete);
-    this->~expr_binding();
-    get_binding_allocator().recycle(this);
+    delete this;
 }
 
 // Expr Sort
-DEF_THREAD_MEMORY_POOL(get_sort_allocator, sizeof(expr_sort));
 expr_sort::expr_sort(level const & l, tag g):
     expr_cell(expr_kind::Sort, ::lean::hash(l), false, has_meta(l), false, has_param(l), g),
     m_level(l) {
 }
 expr_sort::~expr_sort() {}
 void expr_sort::dealloc() {
-    this->~expr_sort();
-    get_sort_allocator().recycle(this);
+    delete this;
 }
 
 // Let expressions
-DEF_THREAD_MEMORY_POOL(get_let_allocator, sizeof(expr_let));
 expr_let::expr_let(name const & n, expr const & t, expr const & v, expr const & b, tag g):
     expr_composite(expr_kind::Let,
                    ::lean::hash(::lean::hash(t.hash(), v.hash()), b.hash()),
@@ -308,8 +292,7 @@ void expr_let::dealloc(buffer<expr_cell*> & todelete) {
     dec_ref(m_body,  todelete);
     dec_ref(m_value, todelete);
     dec_ref(m_type,  todelete);
-    this->~expr_let();
-    get_let_allocator().recycle(this);
+    delete this;
 }
 
 // Macro definition
@@ -423,7 +406,7 @@ struct cache_expr_insert_fn {
         if (is_eqp(new_type, mlocal_type(e))) {
             return e;
         } else {
-            return expr(new (get_mlocal_allocator().allocate()) expr_mlocal(*to_mlocal(e), new_type));
+            return expr(new expr_mlocal(*to_mlocal(e), new_type));
         }
     }
 
@@ -432,7 +415,7 @@ struct cache_expr_insert_fn {
         if (is_eqp(new_type, mlocal_type(e))) {
             return e;
         } else {
-            return expr(new (get_local_allocator().allocate()) expr_local(*to_local(e), new_type));
+            return expr(new expr_local(*to_local(e), new_type));
         }
     }
 
@@ -452,7 +435,7 @@ struct cache_expr_insert_fn {
         if (is_eqp(new_fn, app_fn(e)) && is_eqp(new_arg, app_arg(e))) {
             return e;
         } else {
-            return expr(new (get_app_allocator().allocate()) expr_app(*to_app(e), new_fn, new_arg));
+            return expr(new expr_app(*to_app(e), new_fn, new_arg));
         }
     }
 
@@ -462,7 +445,7 @@ struct cache_expr_insert_fn {
         if (is_eqp(new_domain, binding_domain(e)) && is_eqp(new_body, binding_body(e))) {
             return e;
         } else {
-            return expr(new (get_binding_allocator().allocate()) expr_binding(*to_binding(e), new_domain, new_body));
+            return expr(new expr_binding(*to_binding(e), new_domain, new_body));
         }
     }
 
@@ -473,7 +456,7 @@ struct cache_expr_insert_fn {
         if (is_eqp(new_type, let_type(e)) && is_eqp(new_value, let_value(e)) && is_eqp(new_body, let_body(e))) {
             return e;
         } else {
-            return expr(new (get_let_allocator().allocate()) expr_let(*to_let(e), new_type, new_value, new_body));
+            return expr(new expr_let(*to_let(e), new_type, new_value, new_body));
         }
         return e;
     }
@@ -533,35 +516,35 @@ void flush_expr_cache() {
     clear_instantiate_cache();
 }
 expr mk_var(unsigned idx, tag g) {
-    return cache(expr(new (get_var_allocator().allocate()) expr_var(idx, g)));
+    return cache(expr(new expr_var(idx, g)));
 }
 expr mk_constant(name const & n, levels const & ls, tag g) {
-    return cache(expr(new (get_const_allocator().allocate()) expr_const(n, ls, g)));
+    return cache(expr(new expr_const(n, ls, g)));
 }
 expr mk_macro(macro_definition const & m, unsigned num, expr const * args, tag g) {
     char * mem = new char[sizeof(expr_macro) + num*sizeof(expr const *)];
     return cache(expr(new (mem) expr_macro(m, num, args, g)));
 }
 expr mk_metavar(name const & n, name const & pp_n, expr const & t, tag g) {
-    return cache(expr(new (get_mlocal_allocator().allocate()) expr_mlocal(true, n, pp_n, t, g)));
+    return cache(expr(new expr_mlocal(true, n, pp_n, t, g)));
 }
 expr mk_metavar(name const & n, expr const & t, tag g) {
     return mk_metavar(n, n, t, g);
 }
 expr mk_local(name const & n, name const & pp_n, expr const & t, binder_info const & bi, tag g) {
-    return cache(expr(new (get_local_allocator().allocate()) expr_local(n, pp_n, t, bi, g)));
+    return cache(expr(new expr_local(n, pp_n, t, bi, g)));
 }
 expr mk_app(expr const & f, expr const & a, tag g) {
-    return cache(expr(new (get_app_allocator().allocate()) expr_app(f, a, g)));
+    return cache(expr(new expr_app(f, a, g)));
 }
 expr mk_binding(expr_kind k, name const & n, expr const & t, expr const & e, binder_info const & i, tag g) {
-    return cache(expr(new (get_binding_allocator().allocate()) expr_binding(k, n, t, e, i, g)));
+    return cache(expr(new expr_binding(k, n, t, e, i, g)));
 }
 expr mk_let(name const & n, expr const & t, expr const & v, expr const & b, tag g) {
-    return cache(expr(new (get_let_allocator().allocate()) expr_let(n, t, v, b, g)));
+    return cache(expr(new expr_let(n, t, v, b, g)));
 }
 expr mk_sort(level const & l, tag g) {
-    return cache(expr(new (get_sort_allocator().allocate()) expr_sort(l, g)));
+    return cache(expr(new expr_sort(l, g)));
 }
 // =======================================
 
diff --git a/src/library/local_context.cpp b/src/library/local_context.cpp
index d0310d1a4e..0ccff090c8 100644
--- a/src/library/local_context.cpp
+++ b/src/library/local_context.cpp
@@ -21,18 +21,15 @@ static name *       g_local_prefix;
 static expr *       g_dummy_type;
 static local_decl * g_dummy_decl;
 
-DEF_THREAD_MEMORY_POOL(get_local_decl_allocator, sizeof(local_decl::cell));
-
 void local_decl::cell::dealloc() {
-    this->~cell();
-    get_local_decl_allocator().recycle(this);
+    delete this;
 }
 local_decl::cell::cell(unsigned idx, name const & n, name const & pp_n, expr const & t, optional<expr> const & v, binder_info const & bi):
     m_name(n), m_pp_name(pp_n), m_type(t), m_value(v), m_bi(bi), m_idx(idx), m_rc(1) {}
 
 local_decl::local_decl():local_decl(*g_dummy_decl) {}
 local_decl::local_decl(unsigned idx, name const & n, name const & pp_n, expr const & t, optional<expr> const & v, binder_info const & bi) {
-    m_ptr = new (get_local_decl_allocator().allocate()) cell(idx, n, pp_n, t, v, bi);
+    m_ptr = new cell(idx, n, pp_n, t, v, bi);
 }
 
 local_decl::local_decl(local_decl const & d, expr const & t, optional<expr> const & v):
diff --git a/src/library/parray.h b/src/library/parray.h
index e84ac3bf76..20cc628e80 100644
--- a/src/library/parray.h
+++ b/src/library/parray.h
@@ -8,7 +8,6 @@ Author: Leonardo de Moura
 #include <utility>
 #include <memory>
 #include <algorithm>
-#include "util/memory_pool.h"
 #include "util/debug.h"
 #include "util/buffer.h"
 #include "util/thread.h"
@@ -87,23 +86,8 @@ class parray {
         cell():m_rc(1), m_kind(Root), m_size(0), m_values(nullptr) {}
     };
 
-    static memory_pool & get_allocator() {
-        LEAN_THREAD_PTR(memory_pool, g_allocator);
-        if (!g_allocator)
-            g_allocator = allocate_thread_memory_pool(sizeof(cell) + (ThreadSafe ? sizeof(mutex*) : 0)); // NOLINT
-        return *g_allocator;
-    }
-
-    static memory_pool & get_elem_allocator() {
-        LEAN_THREAD_PTR(memory_pool, g_allocator);
-        if (!g_allocator)
-            g_allocator = allocate_thread_memory_pool(std::max(sizeof(T), sizeof(size_t)));
-        return *g_allocator;
-    }
-
     static void del_elem(T * ptr) {
-        ptr->~T();
-        get_elem_allocator().recycle(ptr);
+        delete ptr;
     }
 
     static void deallocate_cell(cell * c) {
@@ -124,8 +108,7 @@ class parray {
                     delete c->get_mutex();
                 break;
             }
-            c->~cell();
-            get_allocator().recycle(c);
+            delete c;
             if (next == nullptr)
                 return;
             lean_assert(next->m_rc > 0);
@@ -167,11 +150,11 @@ class parray {
     }
 
     static cell * mk_cell() {
-        return new (get_allocator().allocate()) cell();
+        return new cell();
     }
 
     static T * mk_elem_copy(T const & e) {
-        return new (get_elem_allocator().allocate()) T(e);
+        return new T(e);
     }
 
     typedef buffer<cell *, 1024> cell_buffer;
@@ -626,10 +609,6 @@ public:
         return m_cell->m_rc;
     }
 
-    static unsigned sizeof_cell() {
-        return get_allocator().obj_size();
-    }
-
     friend void swap(parray & a1, parray & a2) {
         std::swap(a1.m_cell, a2.m_cell);
     }
diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp
index c1dd814213..6f9e65d1c5 100644
--- a/src/library/vm/vm.cpp
+++ b/src/library/vm/vm.cpp
@@ -17,6 +17,7 @@ Author: Leonardo de Moura
 #include "util/sstream.h"
 #include "util/sexpr/option_declarations.h"
 #include "util/shared_mutex.h"
+#include "util/memory.h"
 #include "library/constants.h"
 #include "library/kernel_serializer.h"
 #include "library/trace.h"
diff --git a/src/tests/library/parray.cpp b/src/tests/library/parray.cpp
index 4d84194463..6c24ffb0fa 100644
--- a/src/tests/library/parray.cpp
+++ b/src/tests/library/parray.cpp
@@ -177,8 +177,6 @@ int main() {
     initialize_library_core_module();
     initialize_library_module();
 
-    std::cout << "sizeof(parray::cell) = " << parray<unsigned>::sizeof_cell() << "\n";
-
     tst1();
     tst2();
     tst3(100000);
diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
index c6e0dd6b12..a773d07c35 100644
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@@ -2,7 +2,7 @@ add_library(util OBJECT debug.cpp name.cpp name_set.cpp fresh_name.cpp
   exception.cpp interrupt.cpp hash.cpp escaped.cpp bit_tricks.cpp
   safe_arith.cpp ascii.cpp memory.cpp shared_mutex.cpp path.cpp
   stackinfo.cpp lean_path.cpp serializer.cpp lbool.cpp
-  bitap_fuzzy_search.cpp init_module.cpp thread.cpp memory_pool.cpp
+  bitap_fuzzy_search.cpp init_module.cpp thread.cpp
   utf8.cpp name_map.cpp list_fn.cpp file_lock.cpp
   timeit.cpp timer.cpp task.cpp task_builder.cpp cancellable.cpp
   log_tree.cpp subscripted_name_set.cpp parser_exception.cpp name_generator.cpp)
diff --git a/src/util/init_module.cpp b/src/util/init_module.cpp
index d6bc4b2ea8..a7b73da14b 100644
--- a/src/util/init_module.cpp
+++ b/src/util/init_module.cpp
@@ -9,7 +9,6 @@ Author: Leonardo de Moura
 #include "util/serializer.h"
 #include "util/name.h"
 #include "util/thread.h"
-#include "util/memory_pool.h"
 #include "util/fresh_name.h"
 #include "util/name_generator.h"
 
diff --git a/src/util/list.h b/src/util/list.h
index f4d0428eb4..112743ffd4 100644
--- a/src/util/list.h
+++ b/src/util/list.h
@@ -10,7 +10,6 @@ Author: Leonardo de Moura
 #include "util/rc.h"
 #include "util/debug.h"
 #include "util/optional.h"
-#include "util/memory_pool.h"
 #include "util/buffer.h"
 
 namespace lean {
@@ -34,19 +33,12 @@ public:
         void dealloc();
     };
 private:
-    static memory_pool & get_allocator() {
-        LEAN_THREAD_PTR(memory_pool, g_allocator);
-        if (!g_allocator)
-            g_allocator = allocate_thread_memory_pool(sizeof(cell));
-        return *g_allocator;
-    }
-
     cell * m_ptr;
     cell * steal_ptr() { cell * r = m_ptr; m_ptr = nullptr; return r; }
 public:
     list():m_ptr(nullptr) {}
-    list(T const & h, list const & t):m_ptr(new (get_allocator().allocate()) cell(h, t)) {}
-    explicit list(T const & h):m_ptr(new (get_allocator().allocate()) cell(h, list())) {}
+    list(T const & h, list const & t):m_ptr(new cell(h, t)) {}
+    explicit list(T const & h):m_ptr(new cell(h, list())) {}
     list(list const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
     list(list&& s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
     list(std::initializer_list<T> const & l):list() {
@@ -113,7 +105,7 @@ public:
 
     template<typename... Args>
     void emplace_front(Args&&... args) {
-        cell * new_ptr = new (get_allocator().allocate()) cell(true, *this, args...);
+        cell * new_ptr = new cell(true, *this, args...);
         if (m_ptr) m_ptr->dec_ref();
         m_ptr = new_ptr;
     }
@@ -161,8 +153,7 @@ public:
 
 template<typename T>
 void list<T>::cell::dealloc() {
-    this->~cell();
-    get_allocator().recycle(this);
+    delete this;
 }
 
 template<typename T> inline list<T>         cons(T const & h, list<T> const & t) { return list<T>(h, t); }
diff --git a/src/util/memory_pool.cpp b/src/util/memory_pool.cpp
deleted file mode 100644
index a6d4f23298..0000000000
--- a/src/util/memory_pool.cpp
+++ /dev/null
@@ -1,57 +0,0 @@
-/*
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include <vector>
-#include "util/interrupt.h"
-#include "util/thread.h"
-#include "util/memory_pool.h"
-
-namespace lean {
-memory_pool::~memory_pool() {
-    while (m_free_list != nullptr) {
-        void * r = m_free_list;
-        m_free_list = *(reinterpret_cast<void **>(r));
-        free(r);
-        lean_report_memory_deallocated(m_size);
-    }
-}
-
-void * memory_pool::allocate() {
-    inc_heartbeat();
-    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);
-    }
-}
-
-typedef std::vector<memory_pool*> memory_pools;
-LEAN_THREAD_PTR(memory_pools, g_thread_pools);
-
-static void thread_finalize_memory_pool(void * p) {
-    std::vector<memory_pool*> * thread_pools = reinterpret_cast<std::vector<memory_pool*>*>(p);
-    unsigned i = thread_pools->size();
-    while (i > 0) {
-        --i;
-        delete (*thread_pools)[i];
-    }
-    delete thread_pools;
-    g_thread_pools = nullptr;
-}
-
-memory_pool * allocate_thread_memory_pool(unsigned sz) {
-    if (!g_thread_pools) {
-        g_thread_pools = new std::vector<memory_pool*>();
-        register_post_thread_finalizer(thread_finalize_memory_pool, g_thread_pools);
-    }
-    memory_pool * r = new memory_pool(sz);
-    g_thread_pools->push_back(r);
-    return r;
-}
-}
diff --git a/src/util/memory_pool.h b/src/util/memory_pool.h
deleted file mode 100644
index dee227819d..0000000000
--- a/src/util/memory_pool.h
+++ /dev/null
@@ -1,47 +0,0 @@
-/*
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-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_size(0), m_free_list(nullptr) {}
-    ~memory_pool();
-    void * allocate();
-    void recycle(void * ptr) {
-#ifdef LEAN_NO_CUSTOM_ALLOCATORS
-        free(ptr);
-#else
-        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
-    }
-    unsigned obj_size() const { return m_size; }
-};
-
-memory_pool * allocate_thread_memory_pool(unsigned sz);
-
-#define DEF_THREAD_MEMORY_POOL(NAME, SZ)                        \
-LEAN_THREAD_PTR(memory_pool, NAME ## _tlocal);                  \
-memory_pool & NAME() {                                          \
-    if (!NAME ## _tlocal)                                       \
-        NAME ## _tlocal = allocate_thread_memory_pool(SZ);      \
-    return *(NAME ## _tlocal);                                  \
-}
-}
diff --git a/src/util/name.cpp b/src/util/name.cpp
index a6d2a5f22b..7810c70586 100644
--- a/src/util/name.cpp
+++ b/src/util/name.cpp
@@ -15,7 +15,6 @@ Author: Leonardo de Moura
 #include "util/sstream.h"
 #include "util/debug.h"
 #include "util/buffer.h"
-#include "util/memory_pool.h"
 #include "util/hash.h"
 #include "util/ascii.h"
 #include "util/utf8.h"
@@ -102,8 +101,6 @@ void copy_limbs(name::imp * p, buffer<name::imp *> & limbs) {
     std::reverse(limbs.begin(), limbs.end());
 }
 
-DEF_THREAD_MEMORY_POOL(get_numeric_name_allocator, sizeof(name::imp));
-
 void name::imp::dealloc() {
     imp * curr = this;
     while (true) {
@@ -112,7 +109,7 @@ void name::imp::dealloc() {
         if (curr->m_is_string)
             delete[] reinterpret_cast<char*>(curr);
         else
-            get_numeric_name_allocator().recycle(curr);
+            delete curr;
         curr = p;
         if (!curr || !curr->dec_ref_core())
             break;
@@ -141,7 +138,7 @@ name::name(name const & prefix, char const * nam) {
 }
 
 name::name(name const & prefix, unsigned k, bool) {
-    m_ptr      = new (get_numeric_name_allocator().allocate()) imp(false, prefix.m_ptr);
+    m_ptr      = new imp(false, prefix.m_ptr);
     m_ptr->m_k = k;
     if (m_ptr->m_prefix)
         m_ptr->m_hash = ::lean::hash(m_ptr->m_prefix->m_hash, k);
diff --git a/src/util/rb_tree.h b/src/util/rb_tree.h
index d8f629d04e..055b77b286 100644
--- a/src/util/rb_tree.h
+++ b/src/util/rb_tree.h
@@ -11,7 +11,6 @@ Author: Leonardo de Moura
 #include "util/debug.h"
 #include "util/buffer.h"
 #include "util/optional.h"
-#include "util/memory_pool.h"
 
 namespace lean {
 /**
@@ -63,13 +62,6 @@ class rb_tree : private CMP {
         node_cell(node_cell const & s):m_left(s.m_left), m_right(s.m_right), m_value(s.m_value), m_red(s.m_red), m_rc(0) {}
     };
 
-    static memory_pool & get_allocator() {
-        LEAN_THREAD_PTR(memory_pool, g_allocator);
-        if (!g_allocator)
-            g_allocator = allocate_thread_memory_pool(sizeof(node_cell));
-        return *g_allocator;
-    }
-
     bool check_cmp_result(T const & DEBUG_CODE(v1), T const & DEBUG_CODE(v2)) const {
         DEBUG_CODE(int n1 = CMP::operator()(v1, v2); int n2 = CMP::operator()(v2, v1););
         lean_assert((n1 < 0  && n2 > 0) || (n1 == 0 && n2 == 0) || (n1 > 0  && n2 < 0));
@@ -83,7 +75,7 @@ class rb_tree : private CMP {
 
     static node ensure_unshared(node && n) {
         if (n.is_shared()) {
-            return node(new (get_allocator().allocate()) node_cell(*n.m_ptr));
+            return node(new node_cell(*n.m_ptr));
         } else {
             return n;
         }
@@ -155,7 +147,7 @@ class rb_tree : private CMP {
 
     node insert(node && n, T const & v) {
         if (!n) {
-            return node(new (get_allocator().allocate()) node_cell(v));
+            return node(new node_cell(v));
         }
         node h = ensure_unshared(n.steal());
 
@@ -590,8 +582,7 @@ bool operator==(rb_tree<T, CMP> const & s1, rb_tree<T, CMP> const & s2) {
 
 template<typename T, typename CMP>
 void rb_tree<T, CMP>::node_cell::dealloc() {
-    this->~node_cell();
-    get_allocator().recycle(this);
+    delete this;
 }
 
 template<typename T, typename CMP>
diff --git a/src/util/sequence.h b/src/util/sequence.h
index d80fbc7c77..8e54fdc249 100644
--- a/src/util/sequence.h
+++ b/src/util/sequence.h
@@ -9,7 +9,6 @@ Author: Leonardo de Moura
 #include "util/debug.h"
 #include "util/buffer.h"
 #include "util/optional.h"
-#include "util/memory_pool.h"
 #include "util/list.h"
 
 namespace lean {
@@ -48,20 +47,6 @@ class sequence {
         join_cell(node const & f, node const & s):cell(true), m_first(f), m_second(s) {}
     };
 
-    static memory_pool & get_elem_cell_allocator() {
-        LEAN_THREAD_PTR(memory_pool, g_allocator);
-        if (!g_allocator)
-            g_allocator = allocate_thread_memory_pool(sizeof(elem_cell));
-        return *g_allocator;
-    }
-
-    static memory_pool & get_join_cell_allocator() {
-        LEAN_THREAD_PTR(memory_pool, g_allocator);
-        if (!g_allocator)
-            g_allocator = allocate_thread_memory_pool(sizeof(join_cell));
-        return *g_allocator;
-    }
-
 private:
     node m_node;
 public:
@@ -116,22 +101,20 @@ template<typename T>
 void sequence<T>::cell::dealloc() {
     if (m_join) {
         join_cell * c = static_cast<join_cell*>(this);
-        c->~join_cell();
-        get_join_cell_allocator().recycle(c);
+        delete c;
     } else {
         elem_cell * c = static_cast<elem_cell*>(this);
-        c->~elem_cell();
-        get_elem_cell_allocator().recycle(c);
+        delete c;
     }
 }
 
 template<typename T>
-sequence<T>::node::node(T const & v):m_ptr(new (get_elem_cell_allocator().allocate()) elem_cell(v)) {}
+sequence<T>::node::node(T const & v):m_ptr(new elem_cell(v)) {}
 
 template<typename T>
 sequence<T>::node::node(node const & f, node const & s) {
     if (f && s) {
-        m_ptr = new (get_join_cell_allocator().allocate()) join_cell(f, s);
+        m_ptr = new join_cell(f, s);
     } else if (f) {
         m_ptr = f.m_ptr;
         m_ptr->inc_ref();