michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(util/memory_pool): simplify memory_pool, it is not a template anymore

Browse source
This commit is contained in:
Leonardo de Moura 2014-09-24 10:48:32 -07:00
parent 41433a4002
commit ca1b8ca80f
5 changed files with 24 additions and 38 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
src/kernel/expr.cpp
View file

@ -109,8 +109,7 @@ bool is_meta(expr const & e) {
} }
// Expr variables // Expr variables
typedef memory_pool<sizeof(expr_var)> var_allocator; MK_THREAD_LOCAL_GET(memory_pool, get_var_allocator, sizeof(expr_var));
MK_THREAD_LOCAL_GET_DEF(var_allocator, get_var_allocator);
expr_var::expr_var(unsigned idx): expr_var::expr_var(unsigned idx):
expr_cell(expr_kind::Var, idx, false, false, false, false), expr_cell(expr_kind::Var, idx, false, false, false, false),
m_vidx(idx) { m_vidx(idx) {
@ -123,8 +122,7 @@ void expr_var::dealloc() {
} }
// Expr constants // Expr constants
typedef memory_pool<sizeof(expr_const)> const_allocator; MK_THREAD_LOCAL_GET(memory_pool, get_const_allocator, sizeof(expr_const));
MK_THREAD_LOCAL_GET_DEF(const_allocator, get_const_allocator);
expr_const::expr_const(name const & n, levels const & ls): 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)), expr_cell(expr_kind::Constant, ::lean::hash(n.hash(), hash_levels(ls)), false, has_meta(ls), false, has_param(ls)),
m_name(n), m_name(n),
@ -136,8 +134,7 @@ void expr_const::dealloc() {
} }
// Expr metavariables and local variables // Expr metavariables and local variables
typedef memory_pool<sizeof(expr_mlocal)> mlocal_allocator; MK_THREAD_LOCAL_GET(memory_pool, get_mlocal_allocator, sizeof(expr_mlocal));
MK_THREAD_LOCAL_GET_DEF(mlocal_allocator, get_mlocal_allocator);
expr_mlocal::expr_mlocal(bool is_meta, name const & n, expr const & t): 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(), 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(), !is_meta || t.has_local(), t.has_param_univ(),
@ -150,8 +147,7 @@ void expr_mlocal::dealloc(buffer<expr_cell*> & todelete) {
get_mlocal_allocator().recycle(this); get_mlocal_allocator().recycle(this);
} }
typedef memory_pool<sizeof(expr_local)> local_allocator; MK_THREAD_LOCAL_GET(memory_pool, get_local_allocator, sizeof(expr_local));
MK_THREAD_LOCAL_GET_DEF(local_allocator, get_local_allocator);
expr_local::expr_local(name const & n, name const & pp_name, expr const & t, binder_info const & bi): expr_local::expr_local(name const & n, name const & pp_name, expr const & t, binder_info const & bi):
expr_mlocal(false, n, t), expr_mlocal(false, n, t),
m_pp_name(pp_name), 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) {} m_free_var_range(fv_range) {}
// Expr applications // Expr applications
typedef memory_pool<sizeof(expr_app)> app_allocator; MK_THREAD_LOCAL_GET(memory_pool, get_app_allocator, sizeof(expr_app));
MK_THREAD_LOCAL_GET_DEF(app_allocator, get_app_allocator);
expr_app::expr_app(expr const & fn, expr const & arg): expr_app::expr_app(expr const & fn, expr const & arg):
expr_composite(expr_kind::App, ::lean::hash(fn.hash(), arg.hash()), expr_composite(expr_kind::App, ::lean::hash(fn.hash(), arg.hash()),
fn.has_expr_metavar() || arg.has_expr_metavar(), 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) // Expr binders (Lambda, Pi)
typedef memory_pool<sizeof(expr_binding)> binding_allocator; MK_THREAD_LOCAL_GET(memory_pool, get_binding_allocator, sizeof(expr_binding));
MK_THREAD_LOCAL_GET_DEF(binding_allocator, get_binding_allocator);
expr_binding::expr_binding(expr_kind k, name const & n, expr const & t, expr const & b, binder_info const & i): 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()), expr_composite(k, ::lean::hash(t.hash(), b.hash()),
t.has_expr_metavar() || b.has_expr_metavar(), t.has_expr_metavar() || b.has_expr_metavar(),
@ -224,8 +218,7 @@ void expr_binding::dealloc(buffer<expr_cell*> & todelete) {
} }
// Expr Sort // Expr Sort
typedef memory_pool<sizeof(expr_sort)> sort_allocator; MK_THREAD_LOCAL_GET(memory_pool, get_sort_allocator, sizeof(expr_sort));
MK_THREAD_LOCAL_GET_DEF(sort_allocator, get_sort_allocator);
expr_sort::expr_sort(level const & l): expr_sort::expr_sort(level const & l):
expr_cell(expr_kind::Sort, ::lean::hash(l), false, has_meta(l), false, has_param(l)), expr_cell(expr_kind::Sort, ::lean::hash(l), false, has_meta(l), false, has_param(l)),
m_level(l) { m_level(l) {

15
src/kernel/justification.cpp
View file

@ -123,16 +123,11 @@ approx_set get_approx_assumption_set(justification const & j) {
lean_unreachable(); // LCOV_EXCL_LINE lean_unreachable(); // LCOV_EXCL_LINE
} }
typedef memory_pool<sizeof(asserted_cell)> asserted_allocator; MK_THREAD_LOCAL_GET(memory_pool, get_asserted_allocator, sizeof(asserted_cell));
typedef memory_pool<sizeof(composite_cell)> composite_allocator; MK_THREAD_LOCAL_GET(memory_pool, get_composite_allocator, sizeof(composite_cell));
typedef memory_pool<sizeof(ext_composite_cell)> ext_composite_allocator; MK_THREAD_LOCAL_GET(memory_pool, get_ext_composite_allocator, sizeof(ext_composite_cell));
typedef memory_pool<sizeof(assumption_cell)> assumption_allocator; MK_THREAD_LOCAL_GET(memory_pool, get_assumption_allocator, sizeof(assumption_cell));
typedef memory_pool<sizeof(ext_assumption_cell)> ext_assumption_allocator; MK_THREAD_LOCAL_GET(memory_pool, get_ext_assumption_allocator, sizeof(ext_assumption_cell));
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);
void justification_cell::dealloc() { void justification_cell::dealloc() {
switch (m_kind) { switch (m_kind) {

6
src/util/memory_pool.h
View file

@ -9,11 +9,11 @@ Author: Leonardo de Moura
namespace lean { namespace lean {
/** \brief Auxiliary object for "recycling" allocated memory of fixed size */ /** \brief Auxiliary object for "recycling" allocated memory of fixed size */
template<unsigned Size>
class memory_pool { class memory_pool {
unsigned m_size;
void * m_free_list; void * m_free_list;
public: public:
memory_pool():m_free_list(nullptr) {} memory_pool(unsigned size):m_size(size), m_free_list(nullptr) {}
~memory_pool() { ~memory_pool() {
while (m_free_list != nullptr) { while (m_free_list != nullptr) {
void * r = m_free_list; void * r = m_free_list;
@ -28,7 +28,7 @@ public:
m_free_list = *(reinterpret_cast<void **>(r)); m_free_list = *(reinterpret_cast<void **>(r));
return r; return r;
} else { } else {
return malloc(Size); return malloc(m_size);
} }
} }

3
src/util/name.cpp
View file

@ -68,8 +68,7 @@ struct name::imp {
} }
}; };
typedef memory_pool<sizeof(name::imp)> numeric_name_allocator; MK_THREAD_LOCAL_GET(memory_pool, get_numeric_name_allocator, sizeof(name::imp));
MK_THREAD_LOCAL_GET_DEF(numeric_name_allocator, get_numeric_name_allocator);
void name::imp::dealloc() { void name::imp::dealloc() {
imp * curr = this; imp * curr = this;

15
src/util/sequence.h
View file

@ -48,21 +48,20 @@ class sequence {
join_cell(node const & f, node const & s):cell(true), m_first(f), m_second(s) {} join_cell(node const & f, node const & s):cell(true), m_first(f), m_second(s) {}
}; };
typedef memory_pool<sizeof(elem_cell)> elem_cell_allocator; static memory_pool & get_elem_cell_allocator() {
typedef memory_pool<sizeof(join_cell)> join_cell_allocator; LEAN_THREAD_PTR(memory_pool) g_allocator;
static elem_cell_allocator & get_elem_cell_allocator() {
LEAN_THREAD_PTR(elem_cell_allocator) g_allocator;
if (!g_allocator.get()) if (!g_allocator.get())
g_allocator.reset(new elem_cell_allocator()); g_allocator.reset(new memory_pool(sizeof(elem_cell)));
return *g_allocator; return *g_allocator;
} }
static join_cell_allocator & get_join_cell_allocator() { static memory_pool & get_join_cell_allocator() {
LEAN_THREAD_PTR(join_cell_allocator) g_allocator; LEAN_THREAD_PTR(memory_pool) g_allocator;
if (!g_allocator.get()) if (!g_allocator.get())
g_allocator.reset(new join_cell_allocator()); g_allocator.reset(new memory_pool(sizeof(join_cell)));
return *g_allocator; return *g_allocator;
} }
private: private:
node m_node; node m_node;
public: public: