From 516c0c73b9d1a713d77bb9fe36d57049c0ffbd36 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 24 Sep 2014 12:51:04 -0700 Subject: [PATCH] refactor(*): remove dependency to thread_local C++11 keyword, the current compilers have several bugs associated with it We use the simpler __thread (gcc and clang) and __declspec(thread) (visual studio). --- src/init/init.cpp | 3 ++ src/kernel/expr.cpp | 28 +++++------ src/kernel/justification.cpp | 16 +++--- src/library/placeholder.cpp | 7 ++- src/library/tactic/expr_to_tactic.cpp | 15 +++--- src/library/tactic/expr_to_tactic.h | 10 ++-- src/tests/util/thread.cpp | 30 ++++++++++-- src/util/CMakeLists.txt | 2 +- src/util/init_module.cpp | 1 + src/util/interrupt.h | 4 ++ src/util/memory.h | 1 + src/util/memory_pool.h | 30 +++++------- src/util/name.cpp | 2 +- src/util/numerics/mpbq.cpp | 6 +++ src/util/numerics/mpbq.h | 3 +- src/util/numerics/mpq.cpp | 39 ++++----------- src/util/numerics/mpz.cpp | 34 ++++--------- src/util/rb_tree.h | 14 ++++-- src/util/sequence.h | 12 ++--- src/util/sexpr/format.cpp | 10 ++-- src/util/stackinfo.cpp | 16 +++--- src/util/thread.cpp | 37 ++++++++++++++ src/util/thread.h | 70 ++++++++++++++------------- src/util/thread_script_state.cpp | 41 +++++++++++----- 24 files changed, 247 insertions(+), 184 deletions(-) diff --git a/src/init/init.cpp b/src/init/init.cpp index 6d26b7171..de96a4a75 100644 --- a/src/init/init.cpp +++ b/src/init/init.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "util/stackinfo.h" +#include "util/thread.h" #include "util/init_module.h" #include "util/numerics/init_module.h" #include "util/sexpr/init_module.h" @@ -32,6 +33,7 @@ void initialize() { register_modules(); } void finalize() { + run_thread_finalizers(); finalize_frontend_lean_module(); finalize_tactic_module(); finalize_library_module(); @@ -40,6 +42,7 @@ void finalize() { finalize_sexpr_module(); finalize_numerics_module(); finalize_util_module(); + run_post_thread_finalizers(); } initializer::initializer() { diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 42ffa9290..6a324e11f 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -50,7 +50,7 @@ unsigned hash_levels(levels const & ls) { return r; } -MK_THREAD_LOCAL_GET(unsigned, get_hash_alloc_counter, 0) +LEAN_THREAD_VALUE(unsigned, g_hash_alloc_counter, 0); expr_cell::expr_cell(expr_kind k, unsigned h, bool has_expr_mv, bool has_univ_mv, bool has_local, bool has_param_univ): m_flags(0), @@ -68,8 +68,8 @@ expr_cell::expr_cell(expr_kind k, unsigned h, bool has_expr_mv, bool has_univ_mv // Remark: using pointer address as a hash code is not a good idea. // - each execution run will behave differently. // - the hash is not diverse enough - m_hash_alloc = get_hash_alloc_counter(); - get_hash_alloc_counter()++; + m_hash_alloc = g_hash_alloc_counter; + g_hash_alloc_counter++; } void expr_cell::dec_ref(expr & e, buffer & todelete) { @@ -109,7 +109,7 @@ bool is_meta(expr const & e) { } // Expr variables -MK_THREAD_LOCAL_GET(memory_pool, get_var_allocator, sizeof(expr_var)); +DEF_THREAD_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) { @@ -122,7 +122,7 @@ void expr_var::dealloc() { } // Expr constants -MK_THREAD_LOCAL_GET(memory_pool, get_const_allocator, sizeof(expr_const)); +DEF_THREAD_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), @@ -134,7 +134,7 @@ void expr_const::dealloc() { } // Expr metavariables and local variables -MK_THREAD_LOCAL_GET(memory_pool, get_mlocal_allocator, sizeof(expr_mlocal)); +DEF_THREAD_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(), @@ -147,7 +147,7 @@ void expr_mlocal::dealloc(buffer & todelete) { get_mlocal_allocator().recycle(this); } -MK_THREAD_LOCAL_GET(memory_pool, get_local_allocator, sizeof(expr_local)); +DEF_THREAD_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), @@ -166,7 +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 -MK_THREAD_LOCAL_GET(memory_pool, get_app_allocator, sizeof(expr_app)); +DEF_THREAD_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(), @@ -196,7 +196,7 @@ bool operator==(binder_info const & i1, binder_info const & i2) { } // Expr binders (Lambda, Pi) -MK_THREAD_LOCAL_GET(memory_pool, get_binding_allocator, sizeof(expr_binding)); +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): expr_composite(k, ::lean::hash(t.hash(), b.hash()), t.has_expr_metavar() || b.has_expr_metavar(), @@ -218,7 +218,7 @@ void expr_binding::dealloc(buffer & todelete) { } // Expr Sort -MK_THREAD_LOCAL_GET(memory_pool, get_sort_allocator, sizeof(expr_sort)); +DEF_THREAD_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) { @@ -297,15 +297,15 @@ expr_macro::~expr_macro() { #ifdef LEAN_CACHE_EXPRS typedef lru_cache expr_cache; -MK_THREAD_LOCAL_GET(bool, get_expr_cache_enabled, true) +LEAN_THREAD_VALUE(bool, g_expr_cache_enabled, true); MK_THREAD_LOCAL_GET(expr_cache, get_expr_cache, LEAN_INITIAL_EXPR_CACHE_CAPACITY); bool enable_expr_caching(bool f) { - bool r = get_expr_cache_enabled(); - get_expr_cache_enabled() = f; + bool r = g_expr_cache_enabled; + g_expr_cache_enabled = f; return r; } inline expr cache(expr const & e) { - if (get_expr_cache_enabled()) { + if (g_expr_cache_enabled) { if (auto r = get_expr_cache().insert(e)) return *r; } diff --git a/src/kernel/justification.cpp b/src/kernel/justification.cpp index d6f502a63..7e94f0530 100644 --- a/src/kernel/justification.cpp +++ b/src/kernel/justification.cpp @@ -37,7 +37,7 @@ enum class justification_kind { Asserted, Composite, ExtComposite, Assumption, E approx_set get_approx_assumption_set(justification const & j); -MK_THREAD_LOCAL_GET(unsigned, get_hash_alloc_jst_counter, 0) +LEAN_THREAD_VALUE(unsigned, g_hash_alloc_jst_counter, 0); struct justification_cell { MK_LEAN_RC(); @@ -45,8 +45,8 @@ struct justification_cell { unsigned m_hash_alloc; void dealloc(); justification_cell(justification_kind k):m_rc(0), m_kind(k) { - m_hash_alloc = get_hash_alloc_jst_counter(); - get_hash_alloc_jst_counter()++; + m_hash_alloc = g_hash_alloc_jst_counter; + g_hash_alloc_jst_counter++; } bool is_asserted() const { return m_kind == justification_kind::Asserted; } bool is_assumption() const { return m_kind == justification_kind::Assumption || m_kind == justification_kind::ExtAssumption; } @@ -123,11 +123,11 @@ approx_set get_approx_assumption_set(justification const & j) { lean_unreachable(); // LCOV_EXCL_LINE } -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)); +DEF_THREAD_MEMORY_POOL(get_asserted_allocator, sizeof(asserted_cell)); +DEF_THREAD_MEMORY_POOL(get_composite_allocator, sizeof(composite_cell)); +DEF_THREAD_MEMORY_POOL(get_ext_composite_allocator, sizeof(ext_composite_cell)); +DEF_THREAD_MEMORY_POOL(get_assumption_allocator, sizeof(assumption_cell)); +DEF_THREAD_MEMORY_POOL(get_ext_assumption_allocator, sizeof(ext_assumption_cell)); void justification_cell::dealloc() { switch (m_kind) { diff --git a/src/library/placeholder.cpp b/src/library/placeholder.cpp index 15a4c756e..57840009a 100644 --- a/src/library/placeholder.cpp +++ b/src/library/placeholder.cpp @@ -28,11 +28,10 @@ void finalize_placeholder() { delete g_explicit_placeholder_name; } -MK_THREAD_LOCAL_GET(unsigned, get_placeholder_id, 0) +LEAN_THREAD_VALUE(unsigned, g_placeholder_id, 0); static unsigned next_placeholder_id() { - unsigned & c = get_placeholder_id(); - unsigned r = c; - c++; + unsigned r = g_placeholder_id; + g_placeholder_id++; return r; } level mk_level_placeholder() { return mk_global_univ(name(*g_placeholder_name, next_placeholder_id())); } diff --git a/src/library/tactic/expr_to_tactic.cpp b/src/library/tactic/expr_to_tactic.cpp index 18dc03b72..4deb69f49 100644 --- a/src/library/tactic/expr_to_tactic.cpp +++ b/src/library/tactic/expr_to_tactic.cpp @@ -109,11 +109,10 @@ tactic expr_to_tactic(type_checker & tc, expr e, pos_info_provider const * p) { } static name * g_tmp_prefix = nullptr; -MK_THREAD_LOCAL_GET(unsigned, get_expr_tac_id, 0) +LEAN_THREAD_VALUE(unsigned, g_expr_tac_id, 0); static name_generator next_name_generator() { - unsigned & c = get_expr_tac_id(); - unsigned r = c; - c++; + unsigned r = g_expr_tac_id; + g_expr_tac_id++; return name_generator(name(*g_tmp_prefix, r)); } @@ -128,7 +127,7 @@ tactic fixpoint(expr const & b) { }); } -void register_simple_tac(name const & n, std::function const & f) { +void register_simple_tac(name const & n, std::function f) { register_tac(n, [=](type_checker &, expr const & e, pos_info_provider const *) { if (!is_constant(e)) throw expr_to_tactic_exception(e, "invalid constant tactic"); @@ -136,7 +135,7 @@ void register_simple_tac(name const & n, std::function const & f) { }); } -void register_bin_tac(name const & n, std::function const & f) { +void register_bin_tac(name const & n, std::function f) { register_tac(n, [=](type_checker & tc, expr const & e, pos_info_provider const * p) { buffer args; get_app_args(e, args); @@ -147,7 +146,7 @@ void register_bin_tac(name const & n, std::function const & f) { +void register_unary_tac(name const & n, std::function f) { register_tac(n, [=](type_checker & tc, expr const & e, pos_info_provider const * p) { buffer args; get_app_args(e, args); @@ -157,7 +156,7 @@ void register_unary_tac(name const & n, std::function co }); } -void register_unary_num_tac(name const & n, std::function const & f) { +void register_unary_num_tac(name const & n, std::function f) { register_tac(n, [=](type_checker & tc, expr const & e, pos_info_provider const * p) { buffer args; get_app_args(e, args); diff --git a/src/library/tactic/expr_to_tactic.h b/src/library/tactic/expr_to_tactic.h index 6ad59dbbf..efbadfd3a 100644 --- a/src/library/tactic/expr_to_tactic.h +++ b/src/library/tactic/expr_to_tactic.h @@ -58,10 +58,12 @@ typedef std::function const & f); -void register_bin_tac(name const & n, std::function const & f); -void register_unary_tac(name const & n, std::function const & f); -void register_unary_num_tac(name const & n, std::function const & f); +// remark: we can use "const &" in the following procedures, for some obscure reason it produces +// memory leaks when we compile using clang 3.3 +void register_simple_tac(name const & n, std::function f); +void register_bin_tac(name const & n, std::function f); +void register_unary_tac(name const & n, std::function f); +void register_unary_num_tac(name const & n, std::function f); void initialize_expr_to_tactic(); void finalize_expr_to_tactic(); diff --git a/src/tests/util/thread.cpp b/src/tests/util/thread.cpp index 7c5b3da43..8ed8cd448 100644 --- a/src/tests/util/thread.cpp +++ b/src/tests/util/thread.cpp @@ -16,10 +16,19 @@ Author: Leonardo de Moura using namespace lean; #if defined(LEAN_MULTI_THREAD) && !defined(__APPLE__) +LEAN_THREAD_PTR(std::vector, g_v); +void finalize_vector() { + if (g_v) { + delete g_v; + g_v = nullptr; + } +} void foo() { - LEAN_THREAD_PTR(std::vector) v; - if (!v.get()) v.reset(new std::vector(1024)); - if (v->size() != 1024) { + if (!g_v) { + g_v = new std::vector(1024); + register_thread_finalizer(finalize_vector); + } + if (g_v->size() != 1024) { std::cerr << "Error\n"; exit(1); } @@ -28,7 +37,10 @@ void foo() { static void tst1() { unsigned n = 5; for (unsigned i = 0; i < n; i++) { - thread t([](){ foo(); }); + thread t([](){ + foo(); + run_thread_finalizers(); + }); t.join(); } } @@ -175,25 +187,33 @@ static void tst6() { t1.join(); } +static __thread script_state * g_state = nullptr; + static void tst7() { std::cout << "start\n"; system_import("import_test.lua"); system_dostring("print('hello'); x = 10;"); interruptible_thread t1([]() { + g_state = new script_state(); + g_state->dostring("x = 1"); script_state S = get_thread_script_state(); S.dostring("print(x)\n" "for i = 1, 100000 do\n" " x = x + 1\n" "end\n" "print(x)\n"); + delete g_state; }); interruptible_thread t2([]() { + g_state = new script_state(); + g_state->dostring("x = 0"); script_state S = get_thread_script_state(); S.dostring("print(x)\n" "for i = 1, 20000 do\n" " x = x + 1\n" "end\n" "print(x)\n"); + delete g_state; }); t1.join(); t2.join(); std::cout << "done\n"; @@ -224,7 +244,9 @@ int main() { tst6(); tst7(); tst8(); + run_thread_finalizers(); finalize_util_module(); + run_post_thread_finalizers(); return has_violations() ? 1 : 0; } #else diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index 23c037e77..50a1da716 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -4,6 +4,6 @@ add_library(util trace.cpp debug.cpp name.cpp name_set.cpp realpath.cpp script_state.cpp script_exception.cpp rb_map.cpp lua.cpp luaref.cpp lua_named_param.cpp stackinfo.cpp lean_path.cpp serializer.cpp lbool.cpp thread_script_state.cpp bitap_fuzzy_search.cpp - init_module.cpp thread.cpp) + init_module.cpp thread.cpp memory_pool.cpp) target_link_libraries(util ${LEAN_LIBS}) diff --git a/src/util/init_module.cpp b/src/util/init_module.cpp index c17cb5bd5..dad4fd4c6 100644 --- a/src/util/init_module.cpp +++ b/src/util/init_module.cpp @@ -14,6 +14,7 @@ Author: Leonardo de Moura #include "util/name_generator.h" #include "util/lean_path.h" #include "util/thread.h" +#include "util/memory_pool.h" namespace lean { void initialize_util_module() { diff --git a/src/util/interrupt.h b/src/util/interrupt.h index b1d28eb53..90a3d3d4e 100644 --- a/src/util/interrupt.h +++ b/src/util/interrupt.h @@ -56,6 +56,8 @@ public: save_stack_info(false); fun(std::forward(args)...); m_flag_addr.store(&m_dummy_addr); // see comment before m_dummy_addr + run_thread_finalizers(); + run_post_thread_finalizers(); }, std::forward(fun), std::forward(args)...) @@ -69,6 +71,8 @@ private: save_stack_info(false); _this->m_fun(); _this->m_flag_addr.store(&(_this->m_dummy_addr)); // see comment before m_dummy_addr + run_thread_finalizers(); + run_post_thread_finalizers(); } public: template diff --git a/src/util/memory.h b/src/util/memory.h index 166bc0b48..5ceeea47a 100644 --- a/src/util/memory.h +++ b/src/util/memory.h @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once +#include namespace lean { size_t get_allocated_memory(); diff --git a/src/util/memory_pool.h b/src/util/memory_pool.h index 17a3cac53..3be5ea1f0 100644 --- a/src/util/memory_pool.h +++ b/src/util/memory_pool.h @@ -14,27 +14,21 @@ class memory_pool { void * m_free_list; public: memory_pool(unsigned size):m_size(size), m_free_list(nullptr) {} - ~memory_pool() { - while (m_free_list != nullptr) { - void * r = m_free_list; - m_free_list = *(reinterpret_cast(r)); - free(r); - } - } - - void * allocate() { - if (m_free_list != nullptr) { - void * r = m_free_list; - m_free_list = *(reinterpret_cast(r)); - return r; - } else { - return malloc(m_size); - } - } - + ~memory_pool(); + void * allocate(); void recycle(void * ptr) { *(reinterpret_cast(ptr)) = m_free_list; m_free_list = ptr; } }; + +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); \ +} } diff --git a/src/util/name.cpp b/src/util/name.cpp index 3931deb9c..a7bc39a13 100644 --- a/src/util/name.cpp +++ b/src/util/name.cpp @@ -68,7 +68,7 @@ struct name::imp { } }; -MK_THREAD_LOCAL_GET(memory_pool, get_numeric_name_allocator, sizeof(name::imp)); +DEF_THREAD_MEMORY_POOL(get_numeric_name_allocator, sizeof(name::imp)); void name::imp::dealloc() { imp * curr = this; diff --git a/src/util/numerics/mpbq.cpp b/src/util/numerics/mpbq.cpp index 1fa7502ca..38b9c2d44 100644 --- a/src/util/numerics/mpbq.cpp +++ b/src/util/numerics/mpbq.cpp @@ -350,6 +350,12 @@ void display_decimal(std::ostream & out, mpbq const & a, unsigned prec) { } } +MK_THREAD_LOCAL_GET(bool, get_rnd, false); + +bool & numeric_traits::get_rnd() { + return ::lean::get_rnd(); +} + static mpbq * g_zero = nullptr; mpbq const & numeric_traits::zero() { lean_assert(is_zero(*g_zero)); diff --git a/src/util/numerics/mpbq.h b/src/util/numerics/mpbq.h index 7c2fa2110..f1dd1b5f6 100644 --- a/src/util/numerics/mpbq.h +++ b/src/util/numerics/mpbq.h @@ -266,11 +266,12 @@ public: }; }; + template<> class numeric_traits { private: - MK_THREAD_LOCAL_GET(bool, get_rnd, false); public: + static bool & get_rnd(); static bool precise() { return true; } static bool is_zero(mpbq const & v) { return v.is_zero(); } static bool is_pos(mpbq const & v) { return v.is_pos(); } diff --git a/src/util/numerics/mpq.cpp b/src/util/numerics/mpq.cpp index f0bd0e5f6..02ad31fb5 100644 --- a/src/util/numerics/mpq.cpp +++ b/src/util/numerics/mpq.cpp @@ -160,25 +160,6 @@ mpq read_mpq(deserializer & d) { DECL_UDATA(mpq) -template -static mpq const & to_mpq(lua_State * L) { - LEAN_THREAD_PTR(mpq) arg; - if (!arg.get()) - arg.reset(new mpq()); - switch (lua_type(L, idx)) { - case LUA_TNUMBER: *arg = lua_tonumber(L, idx); return *arg; - case LUA_TSTRING: *arg = mpq(lua_tostring(L, idx)); return *arg; - case LUA_TUSERDATA: - if (is_mpz(L, idx)) { - *arg = mpq(to_mpz(L, idx)); - return *arg; - } else { - return *static_cast(luaL_checkudata(L, idx, mpq_mt)); - } - default: throw exception(sstream() << "arg #" << idx << " must be a number, string, mpz or mpq"); - } -} - mpq to_mpq_ext(lua_State * L, int idx) { switch (lua_type(L, idx)) { case LUA_TNUMBER: return mpq(lua_tonumber(L, idx)); @@ -201,43 +182,43 @@ static int mpq_tostring(lua_State * L) { } static int mpq_eq(lua_State * L) { - return push_boolean(L, to_mpq<1>(L) == to_mpq<2>(L)); + return push_boolean(L, to_mpq_ext(L, 1) == to_mpq_ext(L, 2)); } static int mpq_lt(lua_State * L) { - return push_boolean(L, to_mpq<1>(L) < to_mpq<2>(L)); + return push_boolean(L, to_mpq_ext(L, 1) < to_mpq_ext(L, 2)); } static int mpq_add(lua_State * L) { - return push_mpq(L, to_mpq<1>(L) + to_mpq<2>(L)); + return push_mpq(L, to_mpq_ext(L, 1) + to_mpq_ext(L, 2)); } static int mpq_sub(lua_State * L) { - return push_mpq(L, to_mpq<1>(L) - to_mpq<2>(L)); + return push_mpq(L, to_mpq_ext(L, 1) - to_mpq_ext(L, 2)); } static int mpq_mul(lua_State * L) { - return push_mpq(L, to_mpq<1>(L) * to_mpq<2>(L)); + return push_mpq(L, to_mpq_ext(L, 1) * to_mpq_ext(L, 2)); } static int mpq_div(lua_State * L) { - mpq const & arg2 = to_mpq<2>(L); + mpq arg2 = to_mpq_ext(L, 2); if (arg2 == 0) throw exception("division by zero"); - return push_mpq(L, to_mpq<1>(L) / arg2); + return push_mpq(L, to_mpq_ext(L, 1) / arg2); } static int mpq_umn(lua_State * L) { - return push_mpq(L, 0 - to_mpq<1>(L)); + return push_mpq(L, 0 - to_mpq_ext(L, 1)); } static int mpq_power(lua_State * L) { int k = luaL_checkinteger(L, 2); if (k < 0) throw exception("argument #2 must be positive"); - return push_mpq(L, pow(to_mpq<1>(L), k)); + return push_mpq(L, pow(to_mpq_ext(L, 1), k)); } static int mk_mpq(lua_State * L) { - mpq const & arg = to_mpq<1>(L); + mpq arg = to_mpq_ext(L, 1); return push_mpq(L, arg); } diff --git a/src/util/numerics/mpz.cpp b/src/util/numerics/mpz.cpp index 740092900..36f89237d 100644 --- a/src/util/numerics/mpz.cpp +++ b/src/util/numerics/mpz.cpp @@ -104,20 +104,6 @@ mpz read_mpz(deserializer & d) { } DECL_UDATA(mpz) - -template -static mpz const & to_mpz(lua_State * L) { - LEAN_THREAD_PTR(mpz) arg; - if (!arg.get()) - arg.reset(new mpz()); - switch (lua_type(L, idx)) { - case LUA_TNUMBER: *arg = static_cast(lua_tointeger(L, idx)); return *arg; - case LUA_TSTRING: *arg = mpz(lua_tostring(L, idx)); return *arg; - case LUA_TUSERDATA: return *static_cast(luaL_checkudata(L, idx, mpz_mt)); - default: throw exception(sstream() << "arg #" << idx << " must be a number, string or mpz"); - } -} - mpz to_mpz_ext(lua_State * L, int idx) { switch (lua_type(L, idx)) { case LUA_TNUMBER: return mpz(static_cast(lua_tointeger(L, idx))); @@ -135,43 +121,43 @@ static int mpz_tostring(lua_State * L) { } static int mpz_eq(lua_State * L) { - return push_boolean(L, to_mpz<1>(L) == to_mpz<2>(L)); + return push_boolean(L, to_mpz_ext(L, 1) == to_mpz_ext(L, 2)); } static int mpz_lt(lua_State * L) { - return push_boolean(L, to_mpz<1>(L) < to_mpz<2>(L)); + return push_boolean(L, to_mpz_ext(L, 1) < to_mpz_ext(L, 2)); } static int mpz_add(lua_State * L) { - return push_mpz(L, to_mpz<1>(L) + to_mpz<2>(L)); + return push_mpz(L, to_mpz_ext(L, 1) + to_mpz_ext(L, 2)); } static int mpz_sub(lua_State * L) { - return push_mpz(L, to_mpz<1>(L) - to_mpz<2>(L)); + return push_mpz(L, to_mpz_ext(L, 1) - to_mpz_ext(L, 2)); } static int mpz_mul(lua_State * L) { - return push_mpz(L, to_mpz<1>(L) * to_mpz<2>(L)); + return push_mpz(L, to_mpz_ext(L, 1) * to_mpz_ext(L, 2)); } static int mpz_div(lua_State * L) { - mpz const & arg2 = to_mpz<2>(L); + mpz arg2 = to_mpz_ext(L, 2); if (arg2 == 0) throw exception("division by zero"); - return push_mpz(L, to_mpz<1>(L) / arg2); + return push_mpz(L, to_mpz_ext(L, 1) / arg2); } static int mpz_umn(lua_State * L) { - return push_mpz(L, 0 - to_mpz<1>(L)); + return push_mpz(L, 0 - to_mpz_ext(L, 1)); } static int mpz_power(lua_State * L) { int k = luaL_checkinteger(L, 2); if (k < 0) throw exception("argument #2 must be positive"); - return push_mpz(L, pow(to_mpz<1>(L), k)); + return push_mpz(L, pow(to_mpz_ext(L, 1), k)); } static int mk_mpz(lua_State * L) { - mpz const & arg = to_mpz<1>(L); + mpz arg = to_mpz_ext(L, 1); return push_mpz(L, arg); } diff --git a/src/util/rb_tree.h b/src/util/rb_tree.h index b797814f6..5c704db43 100644 --- a/src/util/rb_tree.h +++ b/src/util/rb_tree.h @@ -63,13 +63,20 @@ class rb_tree : public 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; + } + int cmp(T const & v1, T const & v2) const { return CMP::operator()(v1, v2); } static node ensure_unshared(node && n) { if (n.is_shared()) { - return node(new node_cell(*n.m_ptr)); + return node(new (get_allocator().allocate()) node_cell(*n.m_ptr)); } else { return n; } @@ -128,7 +135,7 @@ class rb_tree : public CMP { node insert(node && n, T const & v) { if (!n) { - return node(new node_cell(v)); + return node(new (get_allocator().allocate()) node_cell(v)); } node h = ensure_unshared(n.steal()); @@ -377,7 +384,8 @@ public: template void rb_tree::node_cell::dealloc() { - delete this; + this->~node_cell(); + get_allocator().recycle(this); } template diff --git a/src/util/sequence.h b/src/util/sequence.h index af4d84d9d..d80fbc7c7 100644 --- a/src/util/sequence.h +++ b/src/util/sequence.h @@ -49,16 +49,16 @@ class sequence { }; static memory_pool & get_elem_cell_allocator() { - LEAN_THREAD_PTR(memory_pool) g_allocator; - if (!g_allocator.get()) - g_allocator.reset(new memory_pool(sizeof(elem_cell))); + 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.get()) - g_allocator.reset(new memory_pool(sizeof(join_cell))); + LEAN_THREAD_PTR(memory_pool, g_allocator); + if (!g_allocator) + g_allocator = allocate_thread_memory_pool(sizeof(join_cell)); return *g_allocator; } diff --git a/src/util/sexpr/format.cpp b/src/util/sexpr/format.cpp index e3dbd71ce..fd9bcd423 100644 --- a/src/util/sexpr/format.cpp +++ b/src/util/sexpr/format.cpp @@ -113,7 +113,7 @@ format const & colon() { return *g_colon; } format const & dot() { return *g_dot; } // Auxiliary flag used to mark whether flatten // produce a different sexpr -MK_THREAD_LOCAL_GET(bool, get_g_diff_flatten, false); +LEAN_THREAD_VALUE(bool, g_diff_flatten, false); // sexpr format::flatten(sexpr const & s) { lean_assert(is_cons(s)); @@ -132,10 +132,10 @@ sexpr format::flatten(sexpr const & s) { })); case format_kind::CHOICE: /* flatten (x <|> y) = flatten x */ - get_g_diff_flatten() = true; + g_diff_flatten = true; return flatten(sexpr_choice_1(s)); case format_kind::LINE: - get_g_diff_flatten() = true; + g_diff_flatten = true; return sexpr_text(sexpr(" ")); case format_kind::FLAT_COMPOSE: case format_kind::TEXT: @@ -149,9 +149,9 @@ format flatten(format const & f){ return format(format::flatten(f.m_value)); } format group(format const & f) { - get_g_diff_flatten() = false; + g_diff_flatten = false; format flat_f = flatten(f); - if (get_g_diff_flatten()) { + if (g_diff_flatten) { return choice(flat_f, f); } else { // flat_f and f are essentially the same format object. diff --git a/src/util/stackinfo.cpp b/src/util/stackinfo.cpp index 05eaaacf2..3579418f6 100644 --- a/src/util/stackinfo.cpp +++ b/src/util/stackinfo.cpp @@ -98,32 +98,32 @@ size_t get_stack_size(int main) { #endif static bool g_stack_info_init = false; -MK_THREAD_LOCAL_GET(size_t, get_g_stack_size, 0); -MK_THREAD_LOCAL_GET(size_t, get_g_stack_base, 0); +LEAN_THREAD_VALUE(size_t, g_stack_size, 0); +LEAN_THREAD_VALUE(size_t, g_stack_base, 0); void save_stack_info(bool main) { g_stack_info_init = true; - get_g_stack_size() = get_stack_size(main); + g_stack_size = get_stack_size(main); char x; - get_g_stack_base() = reinterpret_cast(&x); + g_stack_base = reinterpret_cast(&x); } size_t get_used_stack_size() { char y; size_t curr_stack = reinterpret_cast(&y); - return get_g_stack_base() - curr_stack; + return g_stack_base - curr_stack; } size_t get_available_stack_size() { size_t sz = get_used_stack_size(); - if (sz > get_g_stack_size()) + if (sz > g_stack_size) return 0; else - return get_g_stack_size() - sz; + return g_stack_size - sz; } void check_stack(char const * component_name) { - if (g_stack_info_init && get_used_stack_size() + LEAN_MIN_STACK_SPACE > get_g_stack_size()) + if (g_stack_info_init && get_used_stack_size() + LEAN_MIN_STACK_SPACE > g_stack_size) throw stack_space_exception(component_name); } } diff --git a/src/util/thread.cpp b/src/util/thread.cpp index d4ca58ded..102a61561 100644 --- a/src/util/thread.cpp +++ b/src/util/thread.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include #include "util/thread.h" namespace lean { @@ -26,4 +27,40 @@ boost::thread::attributes const & get_thread_attributes() { void initialize_thread() {} void finalize_thread() {} #endif + +typedef std::vector thread_finalizers; +LEAN_THREAD_PTR(thread_finalizers, g_finalizers); +LEAN_THREAD_PTR(thread_finalizers, g_post_finalizers); + +void register_thread_finalizer(thread_finalizer fn) { + if (!g_finalizers) + g_finalizers = new thread_finalizers(); + g_finalizers->push_back(fn); +} + +void register_post_thread_finalizer(thread_finalizer fn) { + if (!g_post_finalizers) + g_post_finalizers = new thread_finalizers(); + g_post_finalizers->push_back(fn); +} + +void run_thread_finalizers(thread_finalizers * fns) { + if (fns) { + unsigned i = fns->size(); + while (i > 0) { + --i; + auto fn = (*fns)[i]; + fn(); + } + delete fns; + } +} + +void run_thread_finalizers() { + run_thread_finalizers(g_finalizers); +} + +void run_post_thread_finalizers() { + run_thread_finalizers(g_post_finalizers); +} } diff --git a/src/util/thread.h b/src/util/thread.h index d1067292c..9b5048e7c 100644 --- a/src/util/thread.h +++ b/src/util/thread.h @@ -161,50 +161,54 @@ public: } #endif -// LEAN_THREAD_PTR macro -#if defined(LEAN_USE_BOOST) - #include - #define LEAN_THREAD_PTR(T) static boost::thread_specific_ptr +#ifdef MSVC +#define LEAN_THREAD_PTR(T, V) static __declspec(thread) T * V = nullptr +#define LEAN_THREAD_VALUE(T, V, VAL) static __declspec(thread) T V = VAL #else - template - class thread_specific_ptr { - T * m_ptr; - public: - thread_specific_ptr():m_ptr(nullptr) {} - ~thread_specific_ptr() { if (m_ptr) delete m_ptr; m_ptr = nullptr; } - T * get() const { return m_ptr; } - void reset(T * ptr) { if (m_ptr) delete m_ptr; m_ptr = ptr; } - T * operator->() const { return m_ptr; } - T & operator*() { return *m_ptr; } - }; - #define LEAN_THREAD_PTR(T) static thread_specific_ptr LEAN_THREAD_LOCAL +#define LEAN_THREAD_PTR(T, V) static __thread T * V = nullptr +#define LEAN_THREAD_VALUE(T, V, VAL) static __thread T V = VAL #endif -#if defined(LEAN_USE_BOOST) && defined(LEAN_MULTI_THREAD) #define MK_THREAD_LOCAL_GET(T, GETTER_NAME, DEF_VALUE) \ -LEAN_THREAD_PTR(T) GETTER_NAME ## _tlocal; \ +LEAN_THREAD_PTR(T, GETTER_NAME ## _tlocal); \ +static void finalize_ ## GETTER_NAME() { \ + if (GETTER_NAME ## _tlocal) { \ + delete GETTER_NAME ## _tlocal; \ + GETTER_NAME ## _tlocal = nullptr; \ + } \ +} \ static T & GETTER_NAME() { \ - if (!(GETTER_NAME ## _tlocal).get()) \ - (GETTER_NAME ## _tlocal).reset(new T(DEF_VALUE)); \ + if (!GETTER_NAME ## _tlocal) { \ + GETTER_NAME ## _tlocal = new T(DEF_VALUE); \ + register_thread_finalizer(finalize_ ## GETTER_NAME); \ + } \ return *(GETTER_NAME ## _tlocal); \ } -#define MK_THREAD_LOCAL_GET_DEF(T, GETTER_NAME) \ -LEAN_THREAD_PTR(T) GETTER_NAME ## _tlocal; \ -static T & GETTER_NAME() { \ - if (!(GETTER_NAME ## _tlocal).get()) \ - (GETTER_NAME ## _tlocal).reset(new T()); \ - return *(GETTER_NAME ## _tlocal); \ +#define MK_THREAD_LOCAL_GET_DEF(T, GETTER_NAME) \ +LEAN_THREAD_PTR(T, GETTER_NAME ## _tlocal); \ +static void finalize_ ## GETTER_NAME() { \ + if (GETTER_NAME ## _tlocal) { \ + delete GETTER_NAME ## _tlocal; \ + GETTER_NAME ## _tlocal = nullptr; \ + } \ +} \ +static T & GETTER_NAME() { \ + if (!GETTER_NAME ## _tlocal) { \ + GETTER_NAME ## _tlocal = new T(); \ + register_thread_finalizer(finalize_ ## GETTER_NAME); \ + } \ + return *(GETTER_NAME ## _tlocal); \ } -#else -// MK_THREAD_LOCAL_GET_DEF and MK_THREAD_LOCAL_GET when LEAN_USE_BOOST is not defined -// REMARK: LEAN_THREAD_LOCAL is a 'blank' when LEAN_MULTI_THREAD is not defined. -// So, the getter is just returning a reference to a global variable if LEAN_MULTI_THREAD is not defined. -#define MK_THREAD_LOCAL_GET(T, GETTER_NAME, DEF_VALUE) static T & GETTER_NAME() { static T LEAN_THREAD_LOCAL r(DEF_VALUE); return r; } -#define MK_THREAD_LOCAL_GET_DEF(T, GETTER_NAME) static T & GETTER_NAME() { static T LEAN_THREAD_LOCAL r; return r; } -#endif + namespace lean { void initialize_thread(); void finalize_thread(); + +typedef void (*thread_finalizer)(); +void register_post_thread_finalizer(thread_finalizer fn); +void register_thread_finalizer(thread_finalizer fn); +void run_post_thread_finalizers(); +void run_thread_finalizers(); } diff --git a/src/util/thread_script_state.cpp b/src/util/thread_script_state.cpp index 7bcfae75e..f0a117b3a 100644 --- a/src/util/thread_script_state.cpp +++ b/src/util/thread_script_state.cpp @@ -120,20 +120,35 @@ struct script_state_ref { ~script_state_ref() { recycle_state(m_state); } }; -// If reset == true, then reset/release the (script_state) thread local storage -// If reset == false, then return (script_state) thread local -static script_state * get_script_state_ref(bool reset) { - LEAN_THREAD_PTR(script_state_ref) g_thread_state; - if (reset) { - g_thread_state.reset(nullptr); - return nullptr; - } else { - if (!g_thread_state.get()) - g_thread_state.reset(new script_state_ref()); - return &((*g_thread_state).m_state); +LEAN_THREAD_PTR(bool, g_registered); +LEAN_THREAD_PTR(script_state_ref, g_thread_state_ref); + +static void finalize_thread_state_ref() { + if (g_thread_state_ref) { + delete g_thread_state_ref; + g_thread_state_ref = nullptr; + } + if (g_registered) { + delete g_registered; + g_registered = nullptr; } } -script_state get_thread_script_state() { return *get_script_state_ref(false); } -void release_thread_script_state() { get_script_state_ref(true); } +script_state get_thread_script_state() { + if (!g_thread_state_ref) { + g_thread_state_ref = new script_state_ref(); + if (!g_registered) { + g_registered = new bool(true); + register_thread_finalizer(finalize_thread_state_ref); + } + } + return g_thread_state_ref->m_state; +} + +void release_thread_script_state() { + if (g_thread_state_ref) { + delete g_thread_state_ref; + g_thread_state_ref = nullptr; + } +} }