From ca1b8ca80fb3b24701f6db0c4c414e4ded3378e8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 24 Sep 2014 10:48:32 -0700 Subject: [PATCH] refactor(util/memory_pool): simplify memory_pool, it is not a template anymore --- src/kernel/expr.cpp | 21 +++++++-------------- src/kernel/justification.cpp | 15 +++++---------- src/util/memory_pool.h | 8 ++++---- src/util/name.cpp | 3 +-- src/util/sequence.h | 15 +++++++-------- 5 files changed, 24 insertions(+), 38 deletions(-) diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 4b93202e6..42ffa9290 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -109,8 +109,7 @@ bool is_meta(expr const & e) { } // Expr variables -typedef memory_pool var_allocator; -MK_THREAD_LOCAL_GET_DEF(var_allocator, get_var_allocator); +MK_THREAD_LOCAL_GET(memory_pool, get_var_allocator, sizeof(expr_var)); expr_var::expr_var(unsigned idx): expr_cell(expr_kind::Var, idx, false, false, false, false), m_vidx(idx) { @@ -123,8 +122,7 @@ void expr_var::dealloc() { } // Expr constants -typedef memory_pool const_allocator; -MK_THREAD_LOCAL_GET_DEF(const_allocator, get_const_allocator); +MK_THREAD_LOCAL_GET(memory_pool, get_const_allocator, sizeof(expr_const)); expr_const::expr_const(name const & n, levels const & ls): expr_cell(expr_kind::Constant, ::lean::hash(n.hash(), hash_levels(ls)), false, has_meta(ls), false, has_param(ls)), m_name(n), @@ -136,8 +134,7 @@ void expr_const::dealloc() { } // Expr metavariables and local variables -typedef memory_pool mlocal_allocator; -MK_THREAD_LOCAL_GET_DEF(mlocal_allocator, get_mlocal_allocator); +MK_THREAD_LOCAL_GET(memory_pool, get_mlocal_allocator, sizeof(expr_mlocal)); expr_mlocal::expr_mlocal(bool is_meta, name const & n, expr const & t): 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(), @@ -150,8 +147,7 @@ void expr_mlocal::dealloc(buffer & todelete) { get_mlocal_allocator().recycle(this); } -typedef memory_pool local_allocator; -MK_THREAD_LOCAL_GET_DEF(local_allocator, get_local_allocator); +MK_THREAD_LOCAL_GET(memory_pool, get_local_allocator, sizeof(expr_local)); expr_local::expr_local(name const & n, name const & pp_name, expr const & t, binder_info const & bi): expr_mlocal(false, n, t), m_pp_name(pp_name), @@ -170,8 +166,7 @@ expr_composite::expr_composite(expr_kind k, unsigned h, bool has_expr_mv, bool h m_free_var_range(fv_range) {} // Expr applications -typedef memory_pool app_allocator; -MK_THREAD_LOCAL_GET_DEF(app_allocator, get_app_allocator); +MK_THREAD_LOCAL_GET(memory_pool, get_app_allocator, sizeof(expr_app)); expr_app::expr_app(expr const & fn, expr const & arg): expr_composite(expr_kind::App, ::lean::hash(fn.hash(), arg.hash()), fn.has_expr_metavar() || arg.has_expr_metavar(), @@ -201,8 +196,7 @@ bool operator==(binder_info const & i1, binder_info const & i2) { } // Expr binders (Lambda, Pi) -typedef memory_pool binding_allocator; -MK_THREAD_LOCAL_GET_DEF(binding_allocator, get_binding_allocator); +MK_THREAD_LOCAL_GET(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): expr_composite(k, ::lean::hash(t.hash(), b.hash()), t.has_expr_metavar() || b.has_expr_metavar(), @@ -224,8 +218,7 @@ void expr_binding::dealloc(buffer & todelete) { } // Expr Sort -typedef memory_pool sort_allocator; -MK_THREAD_LOCAL_GET_DEF(sort_allocator, get_sort_allocator); +MK_THREAD_LOCAL_GET(memory_pool, get_sort_allocator, sizeof(expr_sort)); expr_sort::expr_sort(level const & l): expr_cell(expr_kind::Sort, ::lean::hash(l), false, has_meta(l), false, has_param(l)), m_level(l) { diff --git a/src/kernel/justification.cpp b/src/kernel/justification.cpp index 5d652eb2f..d6f502a63 100644 --- a/src/kernel/justification.cpp +++ b/src/kernel/justification.cpp @@ -123,16 +123,11 @@ approx_set get_approx_assumption_set(justification const & j) { lean_unreachable(); // LCOV_EXCL_LINE } -typedef memory_pool asserted_allocator; -typedef memory_pool composite_allocator; -typedef memory_pool ext_composite_allocator; -typedef memory_pool assumption_allocator; -typedef memory_pool ext_assumption_allocator; -MK_THREAD_LOCAL_GET_DEF(asserted_allocator, get_asserted_allocator); -MK_THREAD_LOCAL_GET_DEF(composite_allocator, get_composite_allocator); -MK_THREAD_LOCAL_GET_DEF(ext_composite_allocator, get_ext_composite_allocator); -MK_THREAD_LOCAL_GET_DEF(assumption_allocator, get_assumption_allocator); -MK_THREAD_LOCAL_GET_DEF(ext_assumption_allocator, get_ext_assumption_allocator); +MK_THREAD_LOCAL_GET(memory_pool, get_asserted_allocator, sizeof(asserted_cell)); +MK_THREAD_LOCAL_GET(memory_pool, get_composite_allocator, sizeof(composite_cell)); +MK_THREAD_LOCAL_GET(memory_pool, get_ext_composite_allocator, sizeof(ext_composite_cell)); +MK_THREAD_LOCAL_GET(memory_pool, get_assumption_allocator, sizeof(assumption_cell)); +MK_THREAD_LOCAL_GET(memory_pool, get_ext_assumption_allocator, sizeof(ext_assumption_cell)); void justification_cell::dealloc() { switch (m_kind) { diff --git a/src/util/memory_pool.h b/src/util/memory_pool.h index 00471a794..17a3cac53 100644 --- a/src/util/memory_pool.h +++ b/src/util/memory_pool.h @@ -9,11 +9,11 @@ Author: Leonardo de Moura namespace lean { /** \brief Auxiliary object for "recycling" allocated memory of fixed size */ -template class memory_pool { - void * m_free_list; + unsigned m_size; + void * m_free_list; public: - memory_pool():m_free_list(nullptr) {} + memory_pool(unsigned size):m_size(size), m_free_list(nullptr) {} ~memory_pool() { while (m_free_list != nullptr) { void * r = m_free_list; @@ -28,7 +28,7 @@ public: m_free_list = *(reinterpret_cast(r)); return r; } else { - return malloc(Size); + return malloc(m_size); } } diff --git a/src/util/name.cpp b/src/util/name.cpp index 91b1f2178..3931deb9c 100644 --- a/src/util/name.cpp +++ b/src/util/name.cpp @@ -68,8 +68,7 @@ struct name::imp { } }; -typedef memory_pool numeric_name_allocator; -MK_THREAD_LOCAL_GET_DEF(numeric_name_allocator, get_numeric_name_allocator); +MK_THREAD_LOCAL_GET(memory_pool, get_numeric_name_allocator, sizeof(name::imp)); void name::imp::dealloc() { imp * curr = this; diff --git a/src/util/sequence.h b/src/util/sequence.h index f6b5e3eb0..af4d84d9d 100644 --- a/src/util/sequence.h +++ b/src/util/sequence.h @@ -48,21 +48,20 @@ class sequence { join_cell(node const & f, node const & s):cell(true), m_first(f), m_second(s) {} }; - typedef memory_pool elem_cell_allocator; - typedef memory_pool join_cell_allocator; - static elem_cell_allocator & get_elem_cell_allocator() { - LEAN_THREAD_PTR(elem_cell_allocator) g_allocator; + static memory_pool & get_elem_cell_allocator() { + LEAN_THREAD_PTR(memory_pool) g_allocator; if (!g_allocator.get()) - g_allocator.reset(new elem_cell_allocator()); + g_allocator.reset(new memory_pool(sizeof(elem_cell))); return *g_allocator; } - static join_cell_allocator & get_join_cell_allocator() { - LEAN_THREAD_PTR(join_cell_allocator) g_allocator; + static memory_pool & get_join_cell_allocator() { + LEAN_THREAD_PTR(memory_pool) g_allocator; if (!g_allocator.get()) - g_allocator.reset(new join_cell_allocator()); + g_allocator.reset(new memory_pool(sizeof(join_cell))); return *g_allocator; } + private: node m_node; public: