From 4c6ebdeaf97fc1d6d31c5df184f222f5593a56ef Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 22 Jul 2014 09:18:26 -0700 Subject: [PATCH] perf(util/memory_pool): use memory_pool for hierarchical names and justification objects we get a 8% performance improvement when using multiple threads Signed-off-by: Leonardo de Moura --- src/kernel/expr.cpp | 14 +++++------ src/kernel/justification.cpp | 47 ++++++++++++++++++++++++++++-------- src/util/memory_pool.h | 2 +- src/util/name.cpp | 41 ++++++++++++++++--------------- src/util/name.h | 2 ++ 5 files changed, 69 insertions(+), 37 deletions(-) diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 489c4cd22..c65cf458f 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -104,7 +104,7 @@ expr_var::expr_var(unsigned idx): } void expr_var::dealloc() { this->~expr_var(); - get_var_allocator().recyle(this); + get_var_allocator().recycle(this); } // Expr constants @@ -117,7 +117,7 @@ expr_const::expr_const(name const & n, levels const & ls): } void expr_const::dealloc() { this->~expr_const(); - get_const_allocator().recyle(this); + get_const_allocator().recycle(this); } // Expr metavariables and local variables @@ -132,7 +132,7 @@ expr_mlocal::expr_mlocal(bool is_meta, name const & n, expr const & t): void expr_mlocal::dealloc(buffer & todelete) { dec_ref(m_type, todelete); this->~expr_mlocal(); - get_mlocal_allocator().recyle(this); + get_mlocal_allocator().recycle(this); } typedef memory_pool local_allocator; @@ -144,7 +144,7 @@ expr_local::expr_local(name const & n, name const & pp_name, expr const & t, bin void expr_local::dealloc(buffer & todelete) { dec_ref(m_type, todelete); this->~expr_local(); - get_local_allocator().recyle(this); + get_local_allocator().recycle(this); } // Composite expressions @@ -172,7 +172,7 @@ void expr_app::dealloc(buffer & todelete) { dec_ref(m_fn, todelete); dec_ref(m_arg, todelete); this->~expr_app(); - get_app_allocator().recyle(this); + get_app_allocator().recycle(this); } static unsigned dec(unsigned k) { return k == 0 ? 0 : k - 1; } @@ -205,7 +205,7 @@ void expr_binding::dealloc(buffer & todelete) { dec_ref(m_body, todelete); dec_ref(m_binder.m_type, todelete); this->~expr_binding(); - get_binding_allocator().recyle(this); + get_binding_allocator().recycle(this); } // Expr Sort @@ -218,7 +218,7 @@ expr_sort::expr_sort(level const & l): expr_sort::~expr_sort() {} void expr_sort::dealloc() { this->~expr_sort(); - get_sort_allocator().recyle(this); + get_sort_allocator().recycle(this); } // Macro definition diff --git a/src/kernel/justification.cpp b/src/kernel/justification.cpp index bd9337a14..1247fb56c 100644 --- a/src/kernel/justification.cpp +++ b/src/kernel/justification.cpp @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include #include "util/buffer.h" #include "util/int64.h" +#include "util/memory_pool.h" #include "kernel/justification.h" #include "kernel/metavar.h" @@ -112,13 +113,39 @@ 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); + void justification_cell::dealloc() { switch (m_kind) { - case justification_kind::Asserted: delete to_asserted(this); break; - case justification_kind::Assumption: delete to_assumption(this); break; - case justification_kind::ExtAssumption: delete to_ext_assumption(this); break; - case justification_kind::Composite: delete to_composite(this); break; - case justification_kind::ExtComposite: delete to_ext_composite(this); break; + case justification_kind::Asserted: + to_asserted(this)->~asserted_cell(); + get_asserted_allocator().recycle(this); + break; + case justification_kind::Assumption: + to_assumption(this)->~assumption_cell(); + get_assumption_allocator().recycle(this); + break; + case justification_kind::ExtAssumption: + to_ext_assumption(this)->~ext_assumption_cell(); + get_ext_assumption_allocator().recycle(this); + break; + case justification_kind::Composite: + to_composite(this)->~composite_cell(); + get_composite_allocator().recycle(this); + break; + case justification_kind::ExtComposite: + to_ext_composite(this)->~ext_composite_cell(); + get_ext_composite_allocator().recycle(this); + break; } } @@ -220,23 +247,23 @@ justification mk_composite(justification const & j1, justification const & j2, o return j2; if (j2.is_none()) return j1; - return justification(new ext_composite_cell(j1, j2, fn, s)); + return justification(new (get_ext_composite_allocator().allocate()) ext_composite_cell(j1, j2, fn, s)); } justification mk_composite1(justification const & j1, justification const & j2) { if (j1.is_none()) return j2; if (j2.is_none()) return j1; - return justification(new composite_cell(j1, j2)); + return justification(new (get_composite_allocator().allocate()) composite_cell(j1, j2)); } justification mk_assumption_justification(unsigned idx, optional const & s, pp_jst_fn const & fn) { - return justification(new ext_assumption_cell(idx, fn, s)); + return justification(new (get_ext_assumption_allocator().allocate()) ext_assumption_cell(idx, fn, s)); } justification mk_assumption_justification(unsigned idx) { - return justification(new assumption_cell(idx)); + return justification(new (get_assumption_allocator().allocate()) assumption_cell(idx)); } justification mk_justification(optional const & s, pp_jst_fn const & fn) { - return justification(new asserted_cell(fn, s)); + return justification(new (get_asserted_allocator().allocate()) asserted_cell(fn, s)); } justification mk_justification(optional const & s, pp_jst_sfn const & fn) { return mk_justification(s, [=](formatter const & fmt, pos_info_provider const * p, substitution const & subst) { diff --git a/src/util/memory_pool.h b/src/util/memory_pool.h index 137ffb570..00471a794 100644 --- a/src/util/memory_pool.h +++ b/src/util/memory_pool.h @@ -32,7 +32,7 @@ public: } } - void recyle(void * ptr) { + void recycle(void * ptr) { *(reinterpret_cast(ptr)) = m_free_list; m_free_list = ptr; } diff --git a/src/util/name.cpp b/src/util/name.cpp index 38b6d233b..c291c3c34 100644 --- a/src/util/name.cpp +++ b/src/util/name.cpp @@ -15,6 +15,7 @@ Author: Leonardo de Moura #include "util/debug.h" #include "util/rc.h" #include "util/buffer.h" +#include "util/memory_pool.h" #include "util/hash.h" #include "util/trace.h" #include "util/ascii.h" @@ -23,10 +24,7 @@ Author: Leonardo de Moura namespace lean { constexpr char const * anonymous_str = "[anonymous]"; - -/** - \brief Actual implementation of hierarchical names. -*/ +/** \brief Actual implementation of hierarchical names. */ struct name::imp { MK_LEAN_RC() bool m_is_string; @@ -37,20 +35,7 @@ struct name::imp { unsigned m_k; }; - void dealloc() { - imp * curr = this; - while (true) { - lean_assert(curr->get_rc() == 0); - imp * p = curr->m_prefix; - if (curr->m_is_string) - delete[] reinterpret_cast(curr); - else - delete curr; - curr = p; - if (!curr || !curr->dec_ref_core()) - break; - } - } + void dealloc(); imp(bool s, imp * p):m_rc(1), m_is_string(s), m_hash(0), m_prefix(p) { if (p) p->inc_ref(); } @@ -83,6 +68,24 @@ struct name::imp { } }; +typedef memory_pool numeric_name_allocator; +MK_THREAD_LOCAL_GET_DEF(numeric_name_allocator, get_numeric_name_allocator); + +void name::imp::dealloc() { + imp * curr = this; + while (true) { + lean_assert(curr->get_rc() == 0); + imp * p = curr->m_prefix; + if (curr->m_is_string) + delete[] reinterpret_cast(curr); + else + get_numeric_name_allocator().recycle(curr); + curr = p; + if (!curr || !curr->dec_ref_core()) + break; + } +} + name::name(imp * p) { m_ptr = p; if (m_ptr) @@ -107,7 +110,7 @@ name::name(name const & prefix, char const * name) { } name::name(name const & prefix, unsigned k, bool) { - m_ptr = new imp(false, prefix.m_ptr); + m_ptr = new (get_numeric_name_allocator().allocate()) 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/name.h b/src/util/name.h index 17cddda5a..4112139ec 100644 --- a/src/util/name.h +++ b/src/util/name.h @@ -22,7 +22,9 @@ enum class name_kind { ANONYMOUS, STRING, NUMERAL }; \brief Hierarchical names. */ class name { +public: struct imp; +private: friend int cmp(imp * i1, imp * i2); imp * m_ptr; explicit name(imp * p);