From db4b00c7d80e4fa7d5cffd7b0d5ac5727de2a428 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 12 Apr 2018 10:22:07 -0700 Subject: [PATCH] chore(util,library): remove small_object_allocator We use small_object_allocator to allocate vm_obj's. However small_object_allocator is not thread safe. So, we need to copy vm_obj's between threads. Moreover, in our experiments, we observed that JEMALLOC is actually faster than the small_object_allocator. Here are numbers for the reduced corelib. small_object_allocator: 15.62 secs gcc 4.9 allocator: 16.19 secs jemalloc: 13.83 secs --- src/init/init.cpp | 6 +- src/library/tactic/simp_lemmas.cpp | 6 +- src/library/vm/interaction_state_imp.h | 7 +- src/library/vm/vm.cpp | 20 +-- src/library/vm/vm.h | 3 - src/library/vm/vm_array.cpp | 6 +- src/library/vm/vm_declaration.cpp | 6 +- src/library/vm/vm_environment.cpp | 6 +- src/library/vm/vm_exceptional.cpp | 6 +- src/library/vm/vm_expr.cpp | 14 +- src/library/vm/vm_format.cpp | 12 +- src/library/vm/vm_io.cpp | 8 +- src/library/vm/vm_level.cpp | 6 +- src/library/vm/vm_list.cpp | 8 +- src/library/vm/vm_name.cpp | 6 +- src/library/vm/vm_options.cpp | 6 +- src/library/vm/vm_parser.cpp | 6 +- src/library/vm/vm_rb_map.cpp | 12 +- src/library/vm/vm_string.cpp | 6 +- src/library/vm/vm_task.cpp | 4 +- src/util/CMakeLists.txt | 3 +- src/util/memory.h | 2 +- src/util/small_object_allocator.cpp | 211 ------------------------- src/util/small_object_allocator.h | 43 ----- 24 files changed, 71 insertions(+), 342 deletions(-) delete mode 100644 src/util/small_object_allocator.cpp delete mode 100644 src/util/small_object_allocator.h diff --git a/src/init/init.cpp b/src/init/init.cpp index 1369e4054e..7343be7091 100644 --- a/src/init/init.cpp +++ b/src/init/init.cpp @@ -47,7 +47,7 @@ void initialize() { void finalize() { #ifdef LEAN_TRACK_CUSTOM_ALLOCATORS - std::cerr << "memory deallocated by memory_pool and small_object_allocator (before finalization): " << get_memory_deallocated() << "\n"; + std::cerr << "memory deallocated by memory_pool (before finalization): " << get_memory_deallocated() << "\n"; #endif #ifdef LEAN_TRACK_LIVE_EXPRS std::cerr << "number of live expressions (before finalization): " << get_num_live_exprs() << "\n"; @@ -71,14 +71,14 @@ void finalize() { finalize_util_module(); run_post_thread_finalizers(); #ifdef LEAN_TRACK_CUSTOM_ALLOCATORS - std::cerr << "memory deallocated by memory_pool and small_object_allocator (after finalization): " << get_memory_deallocated() << "\n"; + std::cerr << "memory deallocated by memory_pool (after finalization): " << get_memory_deallocated() << "\n"; #endif #ifdef LEAN_TRACK_LIVE_EXPRS std::cerr << "number of live expressions (after finalization): " << get_num_live_exprs() << "\n"; #endif delete_thread_finalizer_manager(); #ifdef LEAN_TRACK_CUSTOM_ALLOCATORS - std::cerr << "memory deallocated by memory_pool and small_object_allocator (after thread finalization): " << get_memory_deallocated() << "\n"; + std::cerr << "memory deallocated by memory_pool (after thread finalization): " << get_memory_deallocated() << "\n"; #endif #ifdef LEAN_TRACK_LIVE_EXPRS std::cerr << "number of live expressions (after thread finalization): " << get_num_live_exprs() << "\n"; diff --git a/src/library/tactic/simp_lemmas.cpp b/src/library/tactic/simp_lemmas.cpp index b09244b1c8..770723d526 100644 --- a/src/library/tactic/simp_lemmas.cpp +++ b/src/library/tactic/simp_lemmas.cpp @@ -1306,9 +1306,9 @@ struct vm_simp_lemmas : public vm_external { simp_lemmas m_val; vm_simp_lemmas(simp_lemmas const & v): m_val(v) {} virtual ~vm_simp_lemmas() {} - virtual void dealloc() override { this->~vm_simp_lemmas(); get_vm_allocator().deallocate(sizeof(vm_simp_lemmas), this); } + virtual void dealloc() override { delete this; } virtual vm_external * ts_clone(vm_clone_fn const &) override { return new vm_simp_lemmas(m_val); } - virtual vm_external * clone(vm_clone_fn const &) override { return new (get_vm_allocator().allocate(sizeof(vm_simp_lemmas))) vm_simp_lemmas(m_val); } + virtual vm_external * clone(vm_clone_fn const &) override { return new vm_simp_lemmas(m_val); } }; bool is_simp_lemmas(vm_obj const & o) { @@ -1321,7 +1321,7 @@ simp_lemmas const & to_simp_lemmas(vm_obj const & o) { } vm_obj to_obj(simp_lemmas const & idx) { - return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_simp_lemmas))) vm_simp_lemmas(idx)); + return mk_vm_external(new vm_simp_lemmas(idx)); } vm_obj simp_lemmas_mk_default(vm_obj const & s) { diff --git a/src/library/vm/interaction_state_imp.h b/src/library/vm/interaction_state_imp.h index 89088395e5..737385d764 100644 --- a/src/library/vm/interaction_state_imp.h +++ b/src/library/vm/interaction_state_imp.h @@ -38,8 +38,7 @@ interaction_monad::vm_State::~vm_State() {} template void interaction_monad::vm_State::dealloc() { - this->~vm_State(); - get_vm_allocator().deallocate(sizeof(vm_State), this); + delete this; } template @@ -55,7 +54,7 @@ vm_external * interaction_monad::vm_State::clone(vm_clone_fn const &) { if (!is_ts_safe(m_val)) { throw exception("Failed to copy state to another thread"); } - return new(get_vm_allocator().allocate(sizeof(vm_State))) vm_State(m_val); + return new vm_State(m_val); } template @@ -71,7 +70,7 @@ auto interaction_monad::to_state(vm_obj const & o) -> State const & { template vm_obj interaction_monad::to_obj(State const & s) { - return mk_vm_external(new(get_vm_allocator().allocate(sizeof(vm_State))) vm_State(s)); + return mk_vm_external(new vm_State(s)); } template diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp index cad7be9d1e..c1dd814213 100644 --- a/src/library/vm/vm.cpp +++ b/src/library/vm/vm.cpp @@ -15,7 +15,6 @@ Author: Leonardo de Moura #include "util/flet.h" #include "util/interrupt.h" #include "util/sstream.h" -#include "util/small_object_allocator.h" #include "util/sexpr/option_declarations.h" #include "util/shared_mutex.h" #include "library/constants.h" @@ -48,12 +47,6 @@ void vm_obj_cell::dec_ref(vm_obj & o, buffer & todelete) { } } -MK_THREAD_LOCAL_GET(small_object_allocator, get_small_allocator, "vm object"); - -small_object_allocator & get_vm_allocator() { - return get_small_allocator(); -} - vm_composite::vm_composite(vm_obj_kind k, unsigned idx, unsigned sz, vm_obj const * data): vm_obj_cell(k), m_idx(idx), m_size(sz) { vm_obj * fields = get_field_ptr(); @@ -62,7 +55,7 @@ vm_composite::vm_composite(vm_obj_kind k, unsigned idx, unsigned sz, vm_obj cons static vm_obj mk_vm_composite(vm_obj_kind k, unsigned idx, unsigned sz, vm_obj const * data) { lean_assert(k == vm_obj_kind::Constructor || k == vm_obj_kind::Closure); - return vm_obj(new (get_small_allocator().allocate(sizeof(vm_composite) + sz * sizeof(vm_obj))) vm_composite(k, idx, sz, data)); + return vm_obj(new (malloc(sizeof(vm_composite) + sz * sizeof(vm_obj))) vm_composite(k, idx, sz, data)); } void vm_composite::dealloc(buffer & todelete) { @@ -72,7 +65,7 @@ void vm_composite::dealloc(buffer & todelete) { dec_ref(fields[i], todelete); } this->~vm_composite(); - get_small_allocator().deallocate(sizeof(vm_composite) + sz * sizeof(vm_obj), this); + free(this); } vm_obj mk_vm_constructor(unsigned cidx, unsigned sz, vm_obj const * data) { @@ -175,12 +168,11 @@ vm_obj mk_vm_simple(unsigned v) { } vm_obj mk_vm_mpz(mpz const & v) { - return vm_obj(new (get_small_allocator().allocate(sizeof(vm_mpz))) vm_mpz(v)); + return vm_obj(new vm_mpz(v)); } void vm_mpz::dealloc() { - this->~vm_mpz(); - get_small_allocator().deallocate(sizeof(vm_mpz), this); + delete this; } /* TODO(Leo, Jared): delete mk_native_closure that takes environment as argument */ @@ -207,11 +199,11 @@ void vm_native_closure::dealloc(buffer & todelete) { dec_ref(args[i], todelete); } this->~vm_native_closure(); - get_small_allocator().deallocate(sizeof(vm_native_closure) + nargs * sizeof(vm_obj), this); + free(this); } vm_obj mk_native_closure(vm_cfunction fn, unsigned arity, unsigned num_args, vm_obj const * args) { - return vm_obj(new (get_small_allocator().allocate(sizeof(vm_native_closure) + num_args * sizeof(vm_obj))) vm_native_closure(fn, arity, num_args, args)); + return vm_obj(new (malloc(sizeof(vm_native_closure) + num_args * sizeof(vm_obj))) vm_native_closure(fn, arity, num_args, args)); } vm_obj mk_native_closure(vm_cfunction fn, unsigned arity, std::initializer_list const & args) { diff --git a/src/library/vm/vm.h b/src/library/vm/vm.h index 56bdaf7735..50f6e7b78c 100644 --- a/src/library/vm/vm.h +++ b/src/library/vm/vm.h @@ -14,7 +14,6 @@ Author: Leonardo de Moura #include "util/compiler_hints.h" #include "util/rc.h" #include "util/interrupt.h" -#include "util/small_object_allocator.h" #include "util/serializer.h" #include "util/numerics/mpz.h" #include "kernel/environment.h" @@ -211,8 +210,6 @@ public: } }; -small_object_allocator & get_vm_allocator(); - // ======================================= // Constructors vm_obj mk_vm_simple(unsigned cidx); diff --git a/src/library/vm/vm_array.cpp b/src/library/vm/vm_array.cpp index dd1184d006..3c7a36b8be 100644 --- a/src/library/vm/vm_array.cpp +++ b/src/library/vm/vm_array.cpp @@ -14,7 +14,7 @@ struct vm_array : public vm_external { parray m_array; vm_array(parray const & a):m_array(a) {} virtual ~vm_array() {} - virtual void dealloc() override { this->~vm_array(); get_vm_allocator().deallocate(sizeof(vm_array), this); } + virtual void dealloc() override { delete this; } virtual vm_external * ts_clone(vm_clone_fn const &) override; virtual vm_external * clone(vm_clone_fn const &) override { lean_unreachable(); } }; @@ -51,7 +51,7 @@ vm_external * vm_array_ts_copy::clone(vm_clone_fn const & fn) { for (vm_obj const & p : m_entries) { array.push_back(fn(p)); } - return new (get_vm_allocator().allocate(sizeof(vm_array))) vm_array(array); + return new vm_array(array); } parray const & to_array(vm_obj const & o) { @@ -60,7 +60,7 @@ parray const & to_array(vm_obj const & o) { } vm_obj to_obj(parray const & a) { - return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_array))) vm_array(a)); + return mk_vm_external(new vm_array(a)); } vm_obj d_array_read(vm_obj const &, vm_obj const &, vm_obj const & a, vm_obj const & i) { diff --git a/src/library/vm/vm_declaration.cpp b/src/library/vm/vm_declaration.cpp index 9cc7dc6f04..0febcfbe60 100644 --- a/src/library/vm/vm_declaration.cpp +++ b/src/library/vm/vm_declaration.cpp @@ -42,9 +42,9 @@ struct vm_declaration : public vm_external { declaration m_val; vm_declaration(declaration const & v):m_val(v) {} virtual ~vm_declaration() {} - virtual void dealloc() override { this->~vm_declaration(); get_vm_allocator().deallocate(sizeof(vm_declaration), this); } + virtual void dealloc() override { delete this; } virtual vm_external * ts_clone(vm_clone_fn const &) override { return new vm_declaration(m_val); } - virtual vm_external * clone(vm_clone_fn const &) override { return new (get_vm_allocator().allocate(sizeof(vm_declaration))) vm_declaration(m_val); } + virtual vm_external * clone(vm_clone_fn const &) override { return new vm_declaration(m_val); } }; bool is_declaration(vm_obj const & o) { @@ -57,7 +57,7 @@ declaration const & to_declaration(vm_obj const & o) { } vm_obj to_obj(declaration const & n) { - return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_declaration))) vm_declaration(n)); + return mk_vm_external(new vm_declaration(n)); } vm_obj declaration_defn(vm_obj const & n, vm_obj const & ls, vm_obj const & type, vm_obj const & value, diff --git a/src/library/vm/vm_environment.cpp b/src/library/vm/vm_environment.cpp index 8fade3685f..67bc183173 100644 --- a/src/library/vm/vm_environment.cpp +++ b/src/library/vm/vm_environment.cpp @@ -34,9 +34,9 @@ struct vm_environment : public vm_external { environment m_val; vm_environment(environment const & v):m_val(v) {} virtual ~vm_environment() {} - virtual void dealloc() override { this->~vm_environment(); get_vm_allocator().deallocate(sizeof(vm_environment), this); } + virtual void dealloc() override { delete this; } virtual vm_external * ts_clone(vm_clone_fn const &) override { return new vm_environment(m_val); } - virtual vm_external * clone(vm_clone_fn const &) override { return new (get_vm_allocator().allocate(sizeof(vm_environment))) vm_environment(m_val); } + virtual vm_external * clone(vm_clone_fn const &) override { return new vm_environment(m_val); } }; bool is_env(vm_obj const & o) { @@ -49,7 +49,7 @@ environment const & to_env(vm_obj const & o) { } vm_obj to_obj(environment const & n) { - return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_environment))) vm_environment(n)); + return mk_vm_external(new vm_environment(n)); } vm_obj environment_mk_std(vm_obj const & l) { diff --git a/src/library/vm/vm_exceptional.cpp b/src/library/vm/vm_exceptional.cpp index 5a305cba2c..b7890a130f 100644 --- a/src/library/vm/vm_exceptional.cpp +++ b/src/library/vm/vm_exceptional.cpp @@ -15,9 +15,9 @@ struct vm_throwable : public vm_external { throwable * m_val; vm_throwable(throwable const & ex):m_val(ex.clone()) {} virtual ~vm_throwable() { delete m_val; } - virtual void dealloc() override { this->~vm_throwable(); get_vm_allocator().deallocate(sizeof(vm_throwable), this); } + virtual void dealloc() override { delete this; } virtual vm_external * ts_clone(vm_clone_fn const &) override { return new vm_throwable(*m_val); } - virtual vm_external * clone(vm_clone_fn const &) override { return new (get_vm_allocator().allocate(sizeof(vm_throwable))) vm_throwable(*m_val); } + virtual vm_external * clone(vm_clone_fn const &) override { return new vm_throwable(*m_val); } }; throwable * to_throwable(vm_obj const & o) { @@ -26,7 +26,7 @@ throwable * to_throwable(vm_obj const & o) { } vm_obj to_obj(throwable const & ex) { - return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_throwable))) vm_throwable(ex)); + return mk_vm_external(new vm_throwable(ex)); } /** Implement two different signatures: diff --git a/src/library/vm/vm_expr.cpp b/src/library/vm/vm_expr.cpp index 71978ab72b..1b7812c807 100644 --- a/src/library/vm/vm_expr.cpp +++ b/src/library/vm/vm_expr.cpp @@ -41,11 +41,9 @@ struct vm_macro_definition : public vm_external { macro_definition m_val; vm_macro_definition(macro_definition const & v):m_val(v) {} virtual ~vm_macro_definition() {} - virtual void dealloc() override { - this->~vm_macro_definition(); get_vm_allocator().deallocate(sizeof(vm_macro_definition), this); - } + virtual void dealloc() override { delete this; } virtual vm_external * ts_clone(vm_clone_fn const &) override { return new vm_macro_definition(m_val); } - virtual vm_external * clone(vm_clone_fn const &) override { return new (get_vm_allocator().allocate(sizeof(vm_macro_definition))) vm_macro_definition(m_val); } + virtual vm_external * clone(vm_clone_fn const &) override { return new vm_macro_definition(m_val); } }; macro_definition const & to_macro_definition(vm_obj const & o) { @@ -54,16 +52,16 @@ macro_definition const & to_macro_definition(vm_obj const & o) { } vm_obj to_obj(macro_definition const & d) { - return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_macro_definition))) vm_macro_definition(d)); + return mk_vm_external(new vm_macro_definition(d)); } struct vm_expr : public vm_external { expr m_val; vm_expr(expr const & v):m_val(v) {} virtual ~vm_expr() {} - virtual void dealloc() override { this->~vm_expr(); get_vm_allocator().deallocate(sizeof(vm_expr), this); } + virtual void dealloc() override { delete this; } virtual vm_external * ts_clone(vm_clone_fn const &) override { return new vm_expr(m_val); } - virtual vm_external * clone(vm_clone_fn const &) override { return new (get_vm_allocator().allocate(sizeof(vm_expr))) vm_expr(m_val); } + virtual vm_external * clone(vm_clone_fn const &) override { return new vm_expr(m_val); } }; bool is_expr(vm_obj const & o) { @@ -76,7 +74,7 @@ expr const & to_expr(vm_obj const & o) { } vm_obj to_obj(expr const & e) { - return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_expr))) vm_expr(e)); + return mk_vm_external(new vm_expr(e)); } vm_obj to_obj(optional const & e) { diff --git a/src/library/vm/vm_format.cpp b/src/library/vm/vm_format.cpp index a0079e52bc..8a765b29da 100644 --- a/src/library/vm/vm_format.cpp +++ b/src/library/vm/vm_format.cpp @@ -21,9 +21,9 @@ struct vm_format : public vm_external { format m_val; vm_format(format const & v):m_val(v) {} virtual ~vm_format() {} - virtual void dealloc() override { this->~vm_format(); get_vm_allocator().deallocate(sizeof(vm_format), this); } + virtual void dealloc() override { delete this; } virtual vm_external * ts_clone(vm_clone_fn const &) override { return new vm_format(m_val); } - virtual vm_external * clone(vm_clone_fn const &) override { return new (get_vm_allocator().allocate(sizeof(vm_format))) vm_format(m_val); } + virtual vm_external * clone(vm_clone_fn const &) override { return new vm_format(m_val); } }; bool is_format(vm_obj const & o) { @@ -36,7 +36,7 @@ format const & to_format(vm_obj const & o) { } vm_obj to_obj(format const & n) { - return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_format))) vm_format(n)); + return mk_vm_external(new vm_format(n)); } vm_obj format_line() { @@ -140,9 +140,9 @@ struct vm_format_thunk : public vm_external { std::function m_val; vm_format_thunk(std::function const & fn):m_val(fn) {} virtual ~vm_format_thunk() {} - virtual void dealloc() override { this->~vm_format_thunk(); get_vm_allocator().deallocate(sizeof(vm_format_thunk), this); } + virtual void dealloc() override { delete this; } virtual vm_external * ts_clone(vm_clone_fn const &) override { return new vm_format_thunk(m_val); } - virtual vm_external * clone(vm_clone_fn const &) override { return new (get_vm_allocator().allocate(sizeof(vm_format_thunk))) vm_format_thunk(m_val); } + virtual vm_external * clone(vm_clone_fn const &) override { return new vm_format_thunk(m_val); } }; std::function const & to_format_thunk(vm_obj const & o) { @@ -151,7 +151,7 @@ std::function const & to_format_thunk(vm_obj const & o) { } vm_obj to_obj(std::function const & fn) { - return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_format_thunk))) vm_format_thunk(fn)); + return mk_vm_external(new vm_format_thunk(fn)); } static unsigned g_apply_format_thunk_idx = -1; diff --git a/src/library/vm/vm_io.cpp b/src/library/vm/vm_io.cpp index 84cc3af7ac..35772428ae 100644 --- a/src/library/vm/vm_io.cpp +++ b/src/library/vm/vm_io.cpp @@ -79,7 +79,7 @@ struct vm_handle : public vm_external { vm_handle(handle_ref const & h):m_handle(h) {} vm_handle(handle_ref && h):m_handle(std::move(h)) {} virtual ~vm_handle() {} - virtual void dealloc() override { this->~vm_handle(); get_vm_allocator().deallocate(sizeof(vm_handle), this); } + virtual void dealloc() override { delete this; } virtual vm_external * clone(vm_clone_fn const &) override { return new vm_handle(m_handle); } virtual vm_external * ts_clone(vm_clone_fn const &) override { lean_unreachable(); } }; @@ -90,7 +90,7 @@ static handle_ref const & to_handle(vm_obj const & o) { } static vm_obj to_obj(handle_ref && h) { - return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_handle))) vm_handle(std::move(h))); + return mk_vm_external(new vm_handle(std::move(h))); } struct vm_child : public vm_external { @@ -98,7 +98,7 @@ struct vm_child : public vm_external { vm_child(std::shared_ptr && h):m_child(std::move(h)) {} vm_child(std::shared_ptr const & h):m_child(h) {} virtual ~vm_child() {} - virtual void dealloc() override { this->~vm_child(); get_vm_allocator().deallocate(sizeof(vm_child), this); } + virtual void dealloc() override { delete this; } virtual vm_external * clone(vm_clone_fn const &) override { return new vm_child(m_child); } virtual vm_external * ts_clone(vm_clone_fn const &) override { lean_unreachable(); } }; @@ -109,7 +109,7 @@ std::shared_ptr const & to_child(vm_obj const & o) { } static vm_obj to_obj(std::shared_ptr && h) { - return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_child))) vm_child(std::move(h))); + return mk_vm_external(new vm_child(std::move(h))); } /* diff --git a/src/library/vm/vm_level.cpp b/src/library/vm/vm_level.cpp index 7b8917acbe..787df00616 100644 --- a/src/library/vm/vm_level.cpp +++ b/src/library/vm/vm_level.cpp @@ -18,9 +18,9 @@ struct vm_level : public vm_external { level m_val; vm_level(level const & v):m_val(v) {} virtual ~vm_level() {} - virtual void dealloc() override { this->~vm_level(); get_vm_allocator().deallocate(sizeof(vm_level), this); } + virtual void dealloc() override { delete this; } virtual vm_external * ts_clone(vm_clone_fn const &) override { return new vm_level(m_val); } - virtual vm_external * clone(vm_clone_fn const &) override { return new (get_vm_allocator().allocate(sizeof(vm_level))) vm_level(m_val); } + virtual vm_external * clone(vm_clone_fn const &) override { return new vm_level(m_val); } }; bool is_level(vm_obj const & o) { @@ -33,7 +33,7 @@ level const & to_level(vm_obj const & o) { } vm_obj to_obj(level const & n) { - return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_level))) vm_level(n)); + return mk_vm_external(new vm_level(n)); } vm_obj level_zero() { diff --git a/src/library/vm/vm_list.cpp b/src/library/vm/vm_list.cpp index 9b4ec7712b..af3c1dd288 100644 --- a/src/library/vm/vm_list.cpp +++ b/src/library/vm/vm_list.cpp @@ -16,16 +16,14 @@ struct vm_list : public vm_external { list m_val; vm_list(list const & v):m_val(v) {} virtual ~vm_list() {} - virtual void dealloc() override { - this->~vm_list(); get_vm_allocator().deallocate(sizeof(vm_list), this); - } + virtual void dealloc() override { delete this; } virtual vm_external * ts_clone(vm_clone_fn const &) override { return new vm_list(m_val); } - virtual vm_external * clone(vm_clone_fn const &) override { return new (get_vm_allocator().allocate(sizeof(vm_list))) vm_list(m_val); } + virtual vm_external * clone(vm_clone_fn const &) override { return new vm_list(m_val); } }; template vm_obj list_to_obj(list const & l) { - return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_list))) vm_list(l)); + return mk_vm_external(new vm_list(l)); } vm_obj to_obj(list const & ls) { return list_to_obj(ls); } diff --git a/src/library/vm/vm_name.cpp b/src/library/vm/vm_name.cpp index 11db799de0..85af19e42e 100644 --- a/src/library/vm/vm_name.cpp +++ b/src/library/vm/vm_name.cpp @@ -18,9 +18,9 @@ struct vm_name : public vm_external { name m_val; vm_name(name const & v):m_val(v) {} virtual ~vm_name() {} - virtual void dealloc() override { this->~vm_name(); get_vm_allocator().deallocate(sizeof(vm_name), this); } + virtual void dealloc() override { delete this; } virtual vm_external * ts_clone(vm_clone_fn const &) override { return new vm_name(m_val); } - virtual vm_external * clone(vm_clone_fn const &) override { return new (get_vm_allocator().allocate(sizeof(vm_name))) vm_name(m_val); } + virtual vm_external * clone(vm_clone_fn const &) override { return new vm_name(m_val); } }; bool is_name(vm_obj const & o) { @@ -33,7 +33,7 @@ name const & to_name(vm_obj const & o) { } vm_obj to_obj(name const & n) { - return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_name))) vm_name(n)); + return mk_vm_external(new vm_name(n)); } vm_obj name_anonymous() { diff --git a/src/library/vm/vm_options.cpp b/src/library/vm/vm_options.cpp index 07923cf3e9..41de7a9e04 100644 --- a/src/library/vm/vm_options.cpp +++ b/src/library/vm/vm_options.cpp @@ -16,9 +16,9 @@ struct vm_options : public vm_external { options m_val; vm_options(options const & v):m_val(v) {} virtual ~vm_options() {} - virtual void dealloc() override { this->~vm_options(); get_vm_allocator().deallocate(sizeof(vm_options), this); } + virtual void dealloc() override { delete this; } virtual vm_external * ts_clone(vm_clone_fn const &) override { return new vm_options(m_val); } - virtual vm_external * clone(vm_clone_fn const &) override { return new (get_vm_allocator().allocate(sizeof(vm_options))) vm_options(m_val); } + virtual vm_external * clone(vm_clone_fn const &) override { return new vm_options(m_val); } }; bool is_options(vm_obj const & o) { @@ -31,7 +31,7 @@ options const & to_options(vm_obj const & o) { } vm_obj to_obj(options const & n) { - return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_options))) vm_options(n)); + return mk_vm_external(new vm_options(n)); } vm_obj options_size(vm_obj const & o) { diff --git a/src/library/vm/vm_parser.cpp b/src/library/vm/vm_parser.cpp index 696cd63e58..55085dacc9 100644 --- a/src/library/vm/vm_parser.cpp +++ b/src/library/vm/vm_parser.cpp @@ -83,9 +83,9 @@ struct vm_decl_attributes : public vm_external { decl_attributes m_val; vm_decl_attributes(decl_attributes const & v):m_val(v) {} virtual ~vm_decl_attributes() {} - virtual void dealloc() override { this->~vm_decl_attributes(); get_vm_allocator().deallocate(sizeof(vm_decl_attributes), this); } + virtual void dealloc() override { delete this; } virtual vm_external * ts_clone(vm_clone_fn const &) override { return new vm_decl_attributes(m_val); } - virtual vm_external * clone(vm_clone_fn const &) override { return new (get_vm_allocator().allocate(sizeof(vm_decl_attributes))) vm_decl_attributes(m_val); } + virtual vm_external * clone(vm_clone_fn const &) override { return new vm_decl_attributes(m_val); } }; static decl_attributes const & to_decl_attributes(vm_obj const & o) { @@ -94,7 +94,7 @@ static decl_attributes const & to_decl_attributes(vm_obj const & o) { } static vm_obj to_obj(decl_attributes const & n) { - return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_decl_attributes))) vm_decl_attributes(n)); + return mk_vm_external(new vm_decl_attributes(n)); } static vm_obj to_obj(decl_modifiers const & mods) { diff --git a/src/library/vm/vm_rb_map.cpp b/src/library/vm/vm_rb_map.cpp index 5527cff7f9..9c1d8d9553 100644 --- a/src/library/vm/vm_rb_map.cpp +++ b/src/library/vm/vm_rb_map.cpp @@ -29,7 +29,7 @@ struct vm_rb_map : public vm_external { vm_obj_map m_map; vm_rb_map(vm_obj_map const & m):m_map(m) {} virtual ~vm_rb_map() {} - virtual void dealloc() override { this->~vm_rb_map(); get_vm_allocator().deallocate(sizeof(vm_rb_map), this); } + virtual void dealloc() override { delete this; } virtual vm_external * ts_clone(vm_clone_fn const &) override; virtual vm_external * clone(vm_clone_fn const &) override { lean_unreachable(); } }; @@ -72,7 +72,7 @@ vm_external * vm_rb_map_ts_copy::clone(vm_clone_fn const & fn) { for (auto const & p : m_entries) { new_map.insert(fn(p.first), fn(p.second)); } - return new (get_vm_allocator().allocate(sizeof(vm_rb_map))) vm_rb_map(new_map); + return new vm_rb_map(new_map); } vm_obj_map const & to_map(vm_obj const & o) { @@ -81,7 +81,7 @@ vm_obj_map const & to_map(vm_obj const & o) { } vm_obj to_obj(vm_rb_map const & n) { - return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_rb_map))) vm_rb_map(n)); + return mk_vm_external(new vm_rb_map(n)); } vm_obj rb_map_mk_core(vm_obj const &, vm_obj const &, vm_obj const & cmp) { @@ -141,9 +141,9 @@ struct vm_name_set : public vm_external { name_set m_val; vm_name_set(name_set const & v):m_val(v) {} virtual ~vm_name_set() {} - virtual void dealloc() override { this->~vm_name_set(); get_vm_allocator().deallocate(sizeof(vm_name_set), this); } + virtual void dealloc() override { delete this; } virtual vm_external * ts_clone(vm_clone_fn const &) override { return new vm_name_set(m_val); } - virtual vm_external * clone(vm_clone_fn const &) override { return new (get_vm_allocator().allocate(sizeof(vm_name_set))) vm_name_set(m_val); } + virtual vm_external * clone(vm_clone_fn const &) override { return new vm_name_set(m_val); } }; bool is_name_set(vm_obj const & o) { @@ -156,7 +156,7 @@ name_set const & to_name_set(vm_obj const & o) { } vm_obj to_obj(name_set const & n) { - return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_name_set))) vm_name_set(n)); + return mk_vm_external(new vm_name_set(n)); } vm_obj mk_name_set() { diff --git a/src/library/vm/vm_string.cpp b/src/library/vm/vm_string.cpp index c03d3b5f67..5231af7670 100644 --- a/src/library/vm/vm_string.cpp +++ b/src/library/vm/vm_string.cpp @@ -17,9 +17,9 @@ struct vm_string : public vm_external { size_t m_length; // number of unicode scalar values vm_string(std::string const & v, size_t len):m_value(v), m_length(len) {} virtual ~vm_string() {} - virtual void dealloc() override { this->~vm_string(); get_vm_allocator().deallocate(sizeof(vm_string), this); } + virtual void dealloc() override { delete this; } virtual vm_external * ts_clone(vm_clone_fn const &) override { return new vm_string(m_value, m_length); } - virtual vm_external * clone(vm_clone_fn const &) override { return new (get_vm_allocator().allocate(sizeof(vm_string))) vm_string(m_value, m_length); } + virtual vm_external * clone(vm_clone_fn const &) override { return new vm_string(m_value, m_length); } }; bool is_string(vm_obj const & o) { @@ -36,7 +36,7 @@ std::string to_string(vm_obj const & o) { } vm_obj to_obj(std::string const & s, size_t len) { - return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_string))) vm_string(s, len)); + return mk_vm_external(new vm_string(s, len)); } vm_obj to_obj(std::string const & s) { diff --git a/src/library/vm/vm_task.cpp b/src/library/vm/vm_task.cpp index 00e5f7737e..729b0a1192 100644 --- a/src/library/vm/vm_task.cpp +++ b/src/library/vm/vm_task.cpp @@ -24,7 +24,7 @@ struct vm_task : public vm_external { task m_val; vm_task(task const & v) : m_val(v) {} virtual ~vm_task() {} - virtual void dealloc() override { this->~vm_task(); get_vm_allocator().deallocate(sizeof(vm_task), this); } + virtual void dealloc() override { delete this; } virtual vm_external * ts_clone(vm_clone_fn const &) override { return new vm_task(m_val); } @@ -43,7 +43,7 @@ task const & to_task(vm_obj const & o) { } vm_obj to_obj(task const & n) { - return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_task))) vm_task(n)); + return mk_vm_external(new vm_task(n)); } vm_obj to_obj(task const & n) { diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index f5a3e32139..c6e0dd6b12 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -5,5 +5,4 @@ add_library(util OBJECT debug.cpp name.cpp name_set.cpp fresh_name.cpp bitap_fuzzy_search.cpp init_module.cpp thread.cpp memory_pool.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 small_object_allocator.cpp subscripted_name_set.cpp - parser_exception.cpp name_generator.cpp) + log_tree.cpp subscripted_name_set.cpp parser_exception.cpp name_generator.cpp) diff --git a/src/util/memory.h b/src/util/memory.h index df4d1f1e5b..ff55f9bf69 100644 --- a/src/util/memory.h +++ b/src/util/memory.h @@ -17,7 +17,7 @@ size_t get_allocated_memory(); #ifdef LEAN_TRACK_CUSTOM_ALLOCATORS /* We use report_memory_deallocated to track memory released by custom allocators such - as memory_pool and small_object_allocator. */ + as memory_pool. */ void report_memory_deallocated(size_t s); size_t get_memory_deallocated(); #define lean_report_memory_deallocated(s) report_memory_deallocated(s) diff --git a/src/util/small_object_allocator.cpp b/src/util/small_object_allocator.cpp deleted file mode 100644 index be154e4e3e..0000000000 --- a/src/util/small_object_allocator.cpp +++ /dev/null @@ -1,211 +0,0 @@ -/* -Copyright (c) 2016 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include -#include -#include "util/memory.h" -#include "util/interrupt.h" -#include "util/small_object_allocator.h" - -namespace lean { -small_object_allocator::small_object_allocator(char const * id) { - for (unsigned i = 0; i < NUM_SLOTS; i++) { - m_chunks[i] = 0; - m_free_list[i] = 0; - } - m_id = id; - m_alloc_size = 0; -} - -small_object_allocator::~small_object_allocator() { - for (unsigned i = 0; i < NUM_SLOTS; i++) { - chunk * c = m_chunks[i]; - while (c) { - chunk * next = c->m_next; - delete c; - lean_report_memory_deallocated(sizeof(chunk)); - c = next; - } - } - DEBUG_CODE({ - if (m_alloc_size > 0) { - std::cerr << "Memory leak detected for small object allocator '" - << m_id << "'. " << m_alloc_size << " bytes leaked" << std::endl; - } - }); -} - -void small_object_allocator::reset() { - for (unsigned i = 0; i < NUM_SLOTS; i++) { - chunk * c = m_chunks[i]; - while (c) { - chunk * next = c->m_next; - delete c; - lean_report_memory_deallocated(sizeof(chunk)); - c = next; - } - m_chunks[i] = 0; - m_free_list[i] = 0; - } - m_alloc_size = 0; -} - -void small_object_allocator::deallocate(size_t size, void * p) { - if (size == 0) return; -#if LEAN_DEBUG || defined(LEAN_NO_CUSTOM_ALLOCATORS) - // Valgrind friendly - delete[] static_cast(p); - return; -#endif - lean_assert(m_alloc_size >= size); - lean_assert(p); - m_alloc_size -= size; - if (size >= SMALL_OBJ_SIZE - (1 << PTR_ALIGNMENT)) { - free(p); - return; - } - unsigned slot_id = static_cast(size >> PTR_ALIGNMENT); - if ((size & MASK) != 0) - slot_id++; - lean_assert(slot_id > 0); - lean_assert(slot_id < NUM_SLOTS); - *(reinterpret_cast(p)) = m_free_list[slot_id]; - m_free_list[slot_id] = p; -} - -void * small_object_allocator::allocate(size_t size) { - if (size == 0) return 0; - inc_heartbeat(); -#if LEAN_DEBUG || defined(LEAN_NO_CUSTOM_ALLOCATORS) - // Valgrind friendly - return new char[size]; -#endif - m_alloc_size += size; - if (size >= SMALL_OBJ_SIZE - (1 << PTR_ALIGNMENT)) - return malloc(size); - unsigned slot_id = static_cast(size >> PTR_ALIGNMENT); - if ((size & MASK) != 0) - slot_id++; - lean_assert(slot_id < NUM_SLOTS); - lean_assert(slot_id > 0); - if (m_free_list[slot_id] != 0) { - void * r = m_free_list[slot_id]; - m_free_list[slot_id] = *(reinterpret_cast(r)); - return r; - } - chunk * c = m_chunks[slot_id]; - size = slot_id << PTR_ALIGNMENT; - if (c != 0) { - char * new_curr = c->m_curr + size; - if (new_curr < c->m_data + CHUNK_SIZE) { - void * r = c->m_curr; - c->m_curr = new_curr; - return r; - } - } - chunk * new_c = new chunk(); - new_c->m_next = c; - m_chunks[slot_id] = new_c; - void * r = new_c->m_curr; - new_c->m_curr += size; - return r; -} - -size_t small_object_allocator::get_wasted_size() const { - size_t r = 0; - for (unsigned slot_id = 0; slot_id < NUM_SLOTS; slot_id++) { - size_t slot_obj_size = slot_id << PTR_ALIGNMENT; - void ** ptr = reinterpret_cast(const_cast(this)->m_free_list[slot_id]); - while (ptr != 0) { - r += slot_obj_size; - ptr = reinterpret_cast(*ptr); - } - } - return r; -} - -size_t small_object_allocator::get_num_free_objs() const { - size_t r = 0; - for (unsigned slot_id = 0; slot_id < NUM_SLOTS; slot_id++) { - void ** ptr = reinterpret_cast(const_cast(this)->m_free_list[slot_id]); - while (ptr != 0) { - r++; - ptr = reinterpret_cast(*ptr); - } - } - return r; -} - -template -struct ptr_lt { - bool operator()(T * p1, T * p2) const { return p1 < p2; } -}; - -void small_object_allocator::consolidate() { - std::vector chunks; - std::vector free_objs; - for (unsigned slot_id = 1; slot_id < NUM_SLOTS; slot_id++) { - if (m_free_list[slot_id] == 0) - continue; - chunks.clear(); - free_objs.clear(); - chunk * c = m_chunks[slot_id]; - while (c != 0) { - chunks.push_back(c); - c = c->m_next; - } - char * ptr = static_cast(m_free_list[slot_id]); - while (ptr != 0) { - free_objs.push_back(ptr); - ptr = *(reinterpret_cast(ptr)); - } - unsigned obj_size = slot_id << PTR_ALIGNMENT; - unsigned num_objs_per_chunk = CHUNK_SIZE / obj_size; - if (free_objs.size() < num_objs_per_chunk) - continue; - lean_assert(!chunks.empty()); - std::sort(chunks.begin(), chunks.end(), ptr_lt()); - std::sort(free_objs.begin(), free_objs.end(), ptr_lt()); - chunk * last_chunk = 0; - void * last_free_obj = 0; - unsigned chunk_idx = 0; - unsigned obj_idx = 0; - unsigned num_chunks = chunks.size(); - unsigned num_objs = free_objs.size(); - while (chunk_idx < num_chunks) { - chunk * curr_chunk = chunks[chunk_idx]; - char * curr_begin = curr_chunk->m_data; - char * curr_end = curr_begin + CHUNK_SIZE; - unsigned num_free_in_chunk = 0; - unsigned saved_obj_idx = obj_idx; - while (obj_idx < num_objs) { - char * free_obj = free_objs[obj_idx]; - if (free_obj > curr_end) - break; - obj_idx++; - num_free_in_chunk++; - } - if (num_free_in_chunk == num_objs_per_chunk) { - delete curr_chunk; - lean_report_memory_deallocated(sizeof(chunk)); - } else { - curr_chunk->m_next = last_chunk; - last_chunk = curr_chunk; - for (unsigned i = saved_obj_idx; i < obj_idx; i++) { - // relink objects - void * free_obj = free_objs[i]; - *(reinterpret_cast(free_obj)) = last_free_obj; - last_free_obj = free_obj; - } - } - chunk_idx++; - } - m_chunks[slot_id] = last_chunk; - m_free_list[slot_id] = last_free_obj; - } -} -} diff --git a/src/util/small_object_allocator.h b/src/util/small_object_allocator.h deleted file mode 100644 index 80f69a2fe7..0000000000 --- a/src/util/small_object_allocator.h +++ /dev/null @@ -1,43 +0,0 @@ -/* -Copyright (c) 2016 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/debug.h" - -namespace lean { -class small_object_allocator { - static const unsigned PTR_ALIGNMENT = (sizeof(unsigned) == sizeof(void*) ? 2 /* 32 bit */ : 3 /* 64 bit */); // NOLINT - static const unsigned CHUNK_SIZE = (8192 - sizeof(void*)*2); // NOLINT - static const unsigned SMALL_OBJ_SIZE = 256; - static const unsigned NUM_SLOTS = (SMALL_OBJ_SIZE >> PTR_ALIGNMENT); - static const unsigned MASK = ((1 << PTR_ALIGNMENT) - 1); - struct chunk { - chunk * m_next; - char * m_curr; - char m_data[CHUNK_SIZE]; - chunk():m_curr(m_data) {} - }; - chunk * m_chunks[NUM_SLOTS]; - void * m_free_list[NUM_SLOTS]; - size_t m_alloc_size; - char const * m_id; -public: - small_object_allocator(char const * id = "unknown"); - ~small_object_allocator(); - void reset(); - void * allocate(size_t size); - void deallocate(size_t size, void * p); - size_t get_allocation_size() const { return m_alloc_size; } - size_t get_wasted_size() const; - size_t get_num_free_objs() const; - void consolidate(); -}; -} - -inline void * operator new(size_t s, lean::small_object_allocator & r) { return r.allocate(s); } -inline void * operator new[](size_t s, lean::small_object_allocator & r) { return r.allocate(s); } -inline void operator delete(void *, lean::small_object_allocator &) { lean_unreachable(); } -inline void operator delete[](void *, lean::small_object_allocator &) { lean_unreachable(); }