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
This commit is contained in:
parent
1dd7165694
commit
39ef7aeee2
13 changed files with 42 additions and 227 deletions
|
|
@ -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)));
|
||||
}
|
||||
// =======================================
|
||||
|
||||
|
|
|
|||
|
|
@ -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):
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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"
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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"
|
||||
|
||||
|
|
|
|||
|
|
@ -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); }
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
}
|
||||
}
|
||||
|
|
@ -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); \
|
||||
}
|
||||
}
|
||||
|
|
@ -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);
|
||||
|
|
|
|||
|
|
@ -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>
|
||||
|
|
|
|||
|
|
@ -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();
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue