From 15f0899efb9cbe3af46e82f35853eb15f6c1b9c0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 7 Jun 2014 10:18:32 -0700 Subject: [PATCH] refactor(*): replace LEAN_THREAD_LOCAL with MK_THREAD_LOCAL_GET, the new macro uses the Boost thread_local_ptr instead of 'thread_local' directive Motivation: clang++ on OSX does not support 'thread_local'. Signed-off-by: Leonardo de Moura --- src/kernel/expr.cpp | 27 +++++++++---------- src/library/decl_macros.h | 28 ++++++++++--------- src/library/placeholder.cpp | 12 ++++++--- src/library/resolve_macro.cpp | 2 +- src/tests/util/thread.cpp | 5 ++-- src/util/exception.cpp | 5 ++-- src/util/interrupt.cpp | 10 +++---- src/util/interval/interval.cpp | 46 ++++++++++++++++---------------- src/util/interval/interval.h | 7 +++++ src/util/memory.cpp | 16 ++++++----- src/util/numerics/double.cpp | 7 +++-- src/util/numerics/double.h | 9 ++++--- src/util/numerics/float.cpp | 7 +++-- src/util/numerics/float.h | 9 ++++--- src/util/numerics/mpbq.cpp | 23 ++++++++-------- src/util/numerics/mpbq.h | 4 +-- src/util/numerics/mpfp.cpp | 6 ++--- src/util/numerics/mpfp.h | 16 +++++------ src/util/numerics/mpq.cpp | 15 ++++++----- src/util/numerics/mpz.cpp | 10 ++++--- src/util/script_exception.cpp | 10 ++++--- src/util/sexpr/format.cpp | 10 +++---- src/util/splay_tree.h | 6 +++-- src/util/stackinfo.cpp | 16 +++++------ src/util/thread.h | 29 +++++++++++++++++++- src/util/thread_script_state.cpp | 26 +++++++++--------- 26 files changed, 212 insertions(+), 149 deletions(-) diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 48d922123..fb51d2655 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -34,6 +34,8 @@ unsigned hash_levels(levels const & ls) { return r; } +MK_THREAD_LOCAL_GET(unsigned, get_hash_alloc_counter, 0) + expr_cell::expr_cell(expr_kind k, unsigned h, bool has_mv, bool has_local, bool has_param_univ): m_flags(0), m_kind(static_cast(k)), @@ -49,9 +51,8 @@ expr_cell::expr_cell(expr_kind k, unsigned h, bool has_mv, bool has_local, bool // 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 - static LEAN_THREAD_LOCAL unsigned g_hash_alloc_counter = 0; - m_hash_alloc = g_hash_alloc_counter; - g_hash_alloc_counter++; + m_hash_alloc = get_hash_alloc_counter(); + get_hash_alloc_counter()++; } void expr_cell::dec_ref(expr & e, buffer & todelete) { @@ -267,23 +268,21 @@ expr_macro::~expr_macro() { // Constructors #ifdef LEAN_CACHE_EXPRS -static bool LEAN_THREAD_LOCAL g_expr_cache_enabled = true; typedef lru_cache expr_cache; +MK_THREAD_LOCAL_GET(bool, get_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; + return r; +} inline expr cache(expr const & e) { - if (g_expr_cache_enabled) { - LEAN_THREAD_PTR(expr_cache) g_expr_cache; - if (!g_expr_cache.get()) - g_expr_cache.reset(new expr_cache(LEAN_INITIAL_EXPR_CACHE_CAPACITY)); - if (auto r = g_expr_cache->insert(e)) + if (get_expr_cache_enabled()) { + if (auto r = get_expr_cache().insert(e)) return *r; } return e; } -bool enable_expr_caching(bool f) { - bool r = g_expr_cache_enabled; - g_expr_cache_enabled = f; - return r; -} #else inline expr cache(expr && e) { return e; } bool enable_expr_caching(bool) { return true; } // NOLINT diff --git a/src/library/decl_macros.h b/src/library/decl_macros.h index 21eec3861..543a2c11b 100644 --- a/src/library/decl_macros.h +++ b/src/library/decl_macros.h @@ -8,23 +8,27 @@ Author: Leonardo de Moura /** \brief Helper macro for defining constants such as bool_type, int_type, int_add, etc. */ -#define MK_BUILTIN(Name, ClassName) \ -expr mk_##Name() { \ - static LEAN_THREAD_LOCAL expr r = mk_value(*(new ClassName())); \ - return r; \ +#define MK_BUILTIN(Name, ClassName) \ +expr mk_##Name() { \ + LEAN_THREAD_PTR(expr) r; \ + if (!r.get()) \ + r.reset(new expr(mk_value(*(new ClassName())))); \ + return *r; \ } /** \brief Helper macro for generating "defined" constants. */ -#define MK_CONSTANT(Name, NameObj) \ -static name Name ## _name = NameObj; \ -expr mk_##Name() { \ - static LEAN_THREAD_LOCAL expr r = mk_constant(Name ## _name); \ - return r ; \ -} \ -bool is_ ## Name(expr const & e) { \ - return is_constant(e) && const_name(e) == Name ## _name; \ +#dEFINE MK_CONSTANT(Name, NameObj) \ +static name Name ## _name = NameObj; \ +expr mk_##Name() { \ + LEAN_THREAD_PTR(expr) r; \ + if (!r.get()) \ + r.reset(new expr(mk_constant(Name ## _name))); \ + return *r; \ +} \ +bool is_ ## Name(expr const & e) { \ + return is_constant(e) && const_name(e) == Name ## _name; \ } #define MK_IS_BUILTIN(Name, Builtin) \ diff --git a/src/library/placeholder.cpp b/src/library/placeholder.cpp index 52e70af05..06e6a385f 100644 --- a/src/library/placeholder.cpp +++ b/src/library/placeholder.cpp @@ -11,9 +11,15 @@ Author: Leonardo de Moura namespace lean { static name g_placeholder_name = name(name::mk_internal_unique_name(), "_"); -static unsigned LEAN_THREAD_LOCAL g_placeholder_counter = 0; -level mk_level_placeholder() { return mk_global_univ(name(g_placeholder_name, g_placeholder_counter++)); } -expr mk_expr_placeholder() { return mk_constant(name(g_placeholder_name, g_placeholder_counter++)); } +MK_THREAD_LOCAL_GET(unsigned, get_placeholder_id, 0) +static unsigned next_placeholder_id() { + unsigned & c = get_placeholder_id(); + unsigned r = c; + c++; + return r; +} +level mk_level_placeholder() { return mk_global_univ(name(g_placeholder_name, next_placeholder_id())); } +expr mk_expr_placeholder() { return mk_constant(name(g_placeholder_name, next_placeholder_id())); } static bool is_placeholder(name const & n) { return !n.is_atomic() && n.get_prefix() == g_placeholder_name; } bool is_placeholder(level const & e) { return is_global(e) && is_placeholder(global_id(e)); } bool is_placeholder(expr const & e) { return is_constant(e) && is_placeholder(const_name(e)); } diff --git a/src/library/resolve_macro.cpp b/src/library/resolve_macro.cpp index 06a3ac888..dfe144357 100644 --- a/src/library/resolve_macro.cpp +++ b/src/library/resolve_macro.cpp @@ -282,7 +282,7 @@ public: virtual void write(serializer & s) const { s.write_string(g_resolve_opcode); } }; -static macro_definition LEAN_THREAD_LOCAL g_resolve_macro_definition(new resolve_macro_definition_cell()); +static macro_definition g_resolve_macro_definition(new resolve_macro_definition_cell()); expr mk_resolve_macro(expr const & l, expr const & H1, expr const & H2) { expr args[3] = {l, H1, H2}; diff --git a/src/tests/util/thread.cpp b/src/tests/util/thread.cpp index 959a4015a..c8d496f9d 100644 --- a/src/tests/util/thread.cpp +++ b/src/tests/util/thread.cpp @@ -16,8 +16,9 @@ using namespace lean; #if defined(LEAN_MULTI_THREAD) void foo() { - static LEAN_THREAD_LOCAL std::vector v(1024); - if (v.size() != 1024) { + LEAN_THREAD_PTR(std::vector) v; + if (!v.get()) v.reset(new std::vector(1024)); + if (v->size() != 1024) { std::cerr << "Error\n"; exit(1); } diff --git a/src/util/exception.cpp b/src/util/exception.cpp index 6b6ae5139..ee8e3da7d 100644 --- a/src/util/exception.cpp +++ b/src/util/exception.cpp @@ -24,9 +24,10 @@ parser_exception::parser_exception(std::string const & msg, char const * fname, parser_exception::parser_exception(sstream const & msg, char const * fname, unsigned l, unsigned p): exception(msg), m_fname(fname), m_line(l), m_pos(p) {} parser_exception::~parser_exception() noexcept {} +MK_THREAD_LOCAL_GET_DEF(std::string, get_g_buffer); char const * parser_exception::what() const noexcept { try { - static LEAN_THREAD_LOCAL std::string buffer; + std::string & buffer = get_g_buffer(); std::ostringstream s; s << m_fname << ":" << m_line << ":" << m_pos << ": error: " << m_msg; buffer = s.str(); @@ -38,7 +39,7 @@ char const * parser_exception::what() const noexcept { } char const * stack_space_exception::what() const noexcept { - static LEAN_THREAD_LOCAL std::string buffer; + std::string & buffer = get_g_buffer(); std::ostringstream s; s << "deep recursion was detected at '" << m_component_name << "' (potential solution: increase stack space in your system)"; buffer = s.str(); diff --git a/src/util/interrupt.cpp b/src/util/interrupt.cpp index 0f28603c6..c45a3b618 100644 --- a/src/util/interrupt.cpp +++ b/src/util/interrupt.cpp @@ -9,18 +9,18 @@ Author: Leonardo de Moura #include "util/exception.h" namespace lean { -static LEAN_THREAD_LOCAL atomic_bool g_interrupt; +MK_THREAD_LOCAL_GET(atomic_bool, get_g_interrupt, false); void request_interrupt() { - g_interrupt.store(true); + get_g_interrupt().store(true); } void reset_interrupt() { - g_interrupt.store(false); + get_g_interrupt().store(false); } bool interrupt_requested() { - return g_interrupt.load(); + return get_g_interrupt().load(); } void check_interrupted() { @@ -45,7 +45,7 @@ void sleep_for(unsigned ms, unsigned step_ms) { } atomic_bool * interruptible_thread::get_flag_addr() { - return &g_interrupt; + return &get_g_interrupt(); } bool interruptible_thread::interrupted() const { diff --git a/src/util/interval/interval.cpp b/src/util/interval/interval.cpp index 19694cae4..5ef0e47c6 100644 --- a/src/util/interval/interval.cpp +++ b/src/util/interval/interval.cpp @@ -280,8 +280,8 @@ template interval & interval::sub(interval const & o, interval_deps & deps) { if (compute_intv) { using std::swap; - static LEAN_THREAD_LOCAL T new_l_val; - static LEAN_THREAD_LOCAL T new_u_val; + T & new_l_val = get_tlocal1(); + T & new_u_val = get_tlocal2(); xnumeral_kind new_l_kind, new_u_kind; lean_trace("numerics", tout << "this: " << *this << " o: " << o << "\n";); round_to_minus_inf(); @@ -342,8 +342,8 @@ interval & interval::mul(interval const & o, interval_deps & deps) { bool c_o = i2.is_lower_open(); bool d_o = i2.is_upper_open(); - static LEAN_THREAD_LOCAL T new_l_val; - static LEAN_THREAD_LOCAL T new_u_val; + T & new_l_val = get_tlocal1(); + T & new_u_val = get_tlocal2(); xnumeral_kind new_l_kind, new_u_kind; if (i1.is_N()) { @@ -422,10 +422,10 @@ interval & interval::mul(interval const & o, interval_deps & deps) { deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_LOWER2 | DEP_IN_UPPER2; } } else if (i2.is_M()) { - static LEAN_THREAD_LOCAL T ad; static LEAN_THREAD_LOCAL xnumeral_kind ad_k; - static LEAN_THREAD_LOCAL T bc; static LEAN_THREAD_LOCAL xnumeral_kind bc_k; - static LEAN_THREAD_LOCAL T ac; static LEAN_THREAD_LOCAL xnumeral_kind ac_k; - static LEAN_THREAD_LOCAL T bd; static LEAN_THREAD_LOCAL xnumeral_kind bd_k; + T & ad = get_tlocal3(); xnumeral_kind ad_k = XN_NUMERAL; + T & bc = get_tlocal4(); xnumeral_kind bc_k = XN_NUMERAL; + T & ac = get_tlocal5(); xnumeral_kind ac_k = XN_NUMERAL; + T & bd = get_tlocal6(); xnumeral_kind bd_k = XN_NUMERAL; bool ad_o = a_o || d_o; bool bc_o = b_o || c_o; @@ -586,8 +586,8 @@ interval & interval::div(interval const & o, interval_deps & deps) { bool c_o = i2.m_lower_open; bool d_o = i2.m_upper_open; - static LEAN_THREAD_LOCAL T new_l_val; - static LEAN_THREAD_LOCAL T new_u_val; + T & new_l_val = get_tlocal1(); + T & new_u_val = get_tlocal2(); xnumeral_kind new_l_kind, new_u_kind; if (i1.is_N()) { @@ -795,7 +795,7 @@ interval & interval::operator-=(T const & o) { template interval & interval::operator*=(T const & o) { xnumeral_kind new_l_kind, new_u_kind; - static LEAN_THREAD_LOCAL T tmp1; + T & tmp1 = get_tlocal1(); if (this->is_zero()) { return *this; } @@ -831,7 +831,7 @@ interval & interval::operator*=(T const & o) { template interval & interval::operator/=(T const & o) { xnumeral_kind new_l_kind, new_u_kind; - static LEAN_THREAD_LOCAL T tmp1; + T & tmp1 = get_tlocal1(); if (this->is_zero()) { return *this; } @@ -872,8 +872,8 @@ void interval::inv(interval_deps & deps) { using std::swap; - static LEAN_THREAD_LOCAL T new_l_val; - static LEAN_THREAD_LOCAL T new_u_val; + T & new_l_val = get_tlocal1(); + T & new_u_val = get_tlocal2(); xnumeral_kind new_l_kind, new_u_kind; if (is_P1()) { @@ -1032,8 +1032,8 @@ void interval::power(unsigned n, interval_deps & deps) { // we need both bounds to justify upper bound xnumeral_kind un1_kind = lower_kind(); xnumeral_kind un2_kind = upper_kind(); - static LEAN_THREAD_LOCAL T un1; - static LEAN_THREAD_LOCAL T un2; + T & un1 = get_tlocal1(); + T & un2 = get_tlocal2(); if (compute_intv) { swap(un1, m_lower); swap(un2, m_upper); @@ -1106,7 +1106,7 @@ T a_div_x_n(T a, T const & x, unsigned n, bool to_plus_inf) { numeric_traits::set_rounding(to_plus_inf); a /= x; } else { - static LEAN_THREAD_LOCAL T tmp; + T tmp; numeric_traits::set_rounding(!to_plus_inf); tmp = x; numeric_traits::power(tmp, n); @@ -1141,7 +1141,7 @@ void interval::display(std::ostream & out) const { template void interval::fmod(interval y) { T const & yb = numeric_traits::is_neg(m_lower) ? y.m_lower : y.m_upper; - static LEAN_THREAD_LOCAL T n; + T n; numeric_traits::set_rounding(false); n = m_lower / yb; numeric_traits::floor(n); @@ -1149,7 +1149,7 @@ template void interval::fmod(interval y) { } template void interval::fmod(T y) { - static LEAN_THREAD_LOCAL T n; + T n; numeric_traits::set_rounding(false); n = m_lower / y; numeric_traits::floor(n); @@ -1781,8 +1781,8 @@ void interval::tan(interval_deps & deps) { template template void interval::csc (interval_deps & deps) { - static LEAN_THREAD_LOCAL T l; - static LEAN_THREAD_LOCAL T u; + T l; + T u; if (compute_intv) { l = m_lower; u = m_upper; @@ -1975,8 +1975,8 @@ void interval::sec (interval_deps & deps) { template template void interval::cot (interval_deps & deps) { - static LEAN_THREAD_LOCAL T l; - static LEAN_THREAD_LOCAL T u; + T l; + T u; if (compute_intv) { l = m_lower; u = m_upper; diff --git a/src/util/interval/interval.h b/src/util/interval/interval.h index 914b5a3b7..0803f2a13 100644 --- a/src/util/interval/interval.h +++ b/src/util/interval/interval.h @@ -65,6 +65,13 @@ class interval { void _swap(interval & b); bool _eq(interval const & b) const; + MK_THREAD_LOCAL_GET_DEF(T, get_tlocal1); + MK_THREAD_LOCAL_GET_DEF(T, get_tlocal2); + MK_THREAD_LOCAL_GET_DEF(T, get_tlocal3); + MK_THREAD_LOCAL_GET_DEF(T, get_tlocal4); + MK_THREAD_LOCAL_GET_DEF(T, get_tlocal5); + MK_THREAD_LOCAL_GET_DEF(T, get_tlocal6); + public: template interval & operator=(T2 const & n) { m_lower = n; m_upper = n; set_closed_endpoints(); return *this; } interval & operator=(T const & n); diff --git a/src/util/memory.cpp b/src/util/memory.cpp index 1376c6a28..b0f26eddb 100644 --- a/src/util/memory.cpp +++ b/src/util/memory.cpp @@ -115,17 +115,21 @@ public: }; static alloc_info g_global_memory; -static LEAN_THREAD_LOCAL thread_alloc_info g_thread_memory; +static thread_alloc_info & get_thread_memory() { + // we cannot use MK_THREAD_LOCAL_GET here because it depends on new/delete, and the Lean new/delete invokes this procedure + static thread_alloc_info LEAN_THREAD_LOCAL g_info; + return g_info; +} size_t get_allocated_memory() { return g_global_memory.size(); } -long long get_thread_allocated_memory() { return g_thread_memory.size(); } +long long get_thread_allocated_memory() { return get_thread_memory().size(); } void * malloc(size_t sz) { void * r = malloc_core(sz); if (r || sz == 0) { size_t rsz = malloc_size(r); g_global_memory.inc(rsz); - g_thread_memory.inc(rsz); + get_thread_memory().inc(rsz); return r; } else { throw std::bad_alloc(); @@ -141,11 +145,11 @@ void * realloc(void * ptr, size_t sz) { } size_t old_sz = malloc_size(ptr); g_global_memory.dec(old_sz); - g_thread_memory.dec(old_sz); + get_thread_memory().dec(old_sz); void * r = realloc_core(ptr, sz); size_t new_sz = malloc_size(r); g_global_memory.inc(new_sz); - g_thread_memory.inc(new_sz); + get_thread_memory().inc(new_sz); if (r || sz == 0) return r; else @@ -156,7 +160,7 @@ void free(void * ptr) { if (ptr) { size_t sz = malloc_size(ptr); g_global_memory.dec(sz); - g_thread_memory.dec(sz); + get_thread_memory().dec(sz); } free_core(ptr); } diff --git a/src/util/numerics/double.cpp b/src/util/numerics/double.cpp index ec52abd6f..ba97c6fe7 100644 --- a/src/util/numerics/double.cpp +++ b/src/util/numerics/double.cpp @@ -10,14 +10,13 @@ Author: Soonho Kong #include "util/numerics/double.h" namespace lean { - -static LEAN_THREAD_LOCAL mpfr_rnd_t g_rnd; +MK_THREAD_LOCAL_GET_DEF(mpfr_rnd_t, get_g_rnd); void set_double_rnd(bool plus_inf) { - g_rnd = plus_inf ? MPFR_RNDU : MPFR_RNDD; + get_g_rnd() = plus_inf ? MPFR_RNDU : MPFR_RNDD; } mpfr_rnd_t get_double_rnd() { - return g_rnd; + return get_g_rnd(); } void double_power(double & v, unsigned k) { v = std::pow(v, k); } diff --git a/src/util/numerics/double.h b/src/util/numerics/double.h index d37fae57a..13e326bb3 100644 --- a/src/util/numerics/double.h +++ b/src/util/numerics/double.h @@ -21,10 +21,11 @@ void double_floor(double & v); // Macro to implement transcendental functions using MPFR #define LEAN_TRANS_DOUBLE_FUNC(f, v, rnd) \ - static LEAN_THREAD_LOCAL mpfp t(53); \ - t = v; \ - t.f(rnd); \ - v = t.get_double(rnd); + LEAN_THREAD_PTR(mpfp) t; \ + if (!t.get()) t.reset(new mpfp(53)); \ + *t = v; \ + t->f(rnd); \ + v = t->get_double(rnd); void set_double_rnd(bool plus_inf); mpfr_rnd_t get_double_rnd(); diff --git a/src/util/numerics/float.cpp b/src/util/numerics/float.cpp index b4ae1cb89..04f4d6985 100644 --- a/src/util/numerics/float.cpp +++ b/src/util/numerics/float.cpp @@ -10,14 +10,13 @@ Author: Soonho Kong #include "util/numerics/float.h" namespace lean { - -static LEAN_THREAD_LOCAL mpfr_rnd_t g_rnd; +MK_THREAD_LOCAL_GET_DEF(mpfr_rnd_t, get_g_rnd); void set_float_rnd(bool plus_inf) { - g_rnd = plus_inf ? MPFR_RNDU : MPFR_RNDD; + get_g_rnd() = plus_inf ? MPFR_RNDU : MPFR_RNDD; } mpfr_rnd_t get_float_rnd() { - return g_rnd; + return get_g_rnd(); } void float_power(float & v, unsigned k) { v = std::pow(v, k); } diff --git a/src/util/numerics/float.h b/src/util/numerics/float.h index a2c16d49f..b6c0ef595 100644 --- a/src/util/numerics/float.h +++ b/src/util/numerics/float.h @@ -21,10 +21,11 @@ void float_floor(float & v); // Macro to implement transcendental functions using MPFR #define LEAN_TRANS_FLOAT_FUNC(f, v, rnd) \ - static LEAN_THREAD_LOCAL mpfp t(24); \ - t = v; \ - t.f(rnd); \ - v = t.get_float(rnd); + LEAN_THREAD_PTR(mpfp) t; \ + if (!t.get()) t.reset(new mpfp(24)); \ + *t = v; \ + t->f(rnd); \ + v = t->get_float(rnd); void set_float_rnd(bool plus_inf); mpfr_rnd_t get_float_rnd(); diff --git a/src/util/numerics/mpbq.cpp b/src/util/numerics/mpbq.cpp index 4265d0007..929812979 100644 --- a/src/util/numerics/mpbq.cpp +++ b/src/util/numerics/mpbq.cpp @@ -9,14 +9,15 @@ Author: Leonardo de Moura #include "util/numerics/mpbq.h" namespace lean { - +MK_THREAD_LOCAL_GET_DEF(mpz, get_tlocal1); +MK_THREAD_LOCAL_GET_DEF(mpz, get_tlocal2); bool set(mpbq & a, mpq const & b) { if (b.is_integer()) { numerator(a.m_num, b); a.m_k = 0; return true; } else { - static LEAN_THREAD_LOCAL mpz d; + mpz & d = get_tlocal1(); denominator(d, b); unsigned shift; if (d.is_power_of_two(shift)) { @@ -47,7 +48,7 @@ void mpbq::normalize() { } int cmp(mpbq const & a, mpbq const & b) { - static LEAN_THREAD_LOCAL mpz tmp; + mpz & tmp = get_tlocal1(); if (a.m_k == b.m_k) { return cmp(a.m_num, b.m_num); } else if (a.m_k < b.m_k) { @@ -61,7 +62,7 @@ int cmp(mpbq const & a, mpbq const & b) { } int cmp(mpbq const & a, mpz const & b) { - static LEAN_THREAD_LOCAL mpz tmp; + mpz & tmp = get_tlocal1(); if (a.m_k == 0) { return cmp(a.m_num, b); } else { @@ -74,8 +75,8 @@ int cmp(mpbq const & a, mpq const & b) { if (a.is_integer() && b.is_integer()) { return -cmp(b, a.m_num); } else { - static LEAN_THREAD_LOCAL mpz tmp1; - static LEAN_THREAD_LOCAL mpz tmp2; + mpz & tmp1 = get_tlocal1(); + mpz & tmp2 = get_tlocal2(); // tmp1 <- numerator(a)*denominator(b) denominator(tmp1, b); tmp1 *= a.m_num; // tmp2 <- numerator(b)*denominator(a) @@ -93,7 +94,7 @@ mpbq & mpbq::operator+=(mpbq const & a) { m_num += a.m_num; } else { lean_assert(m_k > a.m_k); - static LEAN_THREAD_LOCAL mpz tmp; + mpz & tmp = get_tlocal1(); mul2k(tmp, a.m_num, m_k - a.m_k); m_num += tmp; } @@ -107,7 +108,7 @@ mpbq & mpbq::add_int(T const & a) { m_num += a; } else { lean_assert(m_k > 0); - static LEAN_THREAD_LOCAL mpz tmp; + mpz & tmp = get_tlocal1(); tmp = a; mul2k(tmp, tmp, m_k); m_num += tmp; @@ -127,7 +128,7 @@ mpbq & mpbq::operator-=(mpbq const & a) { m_num -= a.m_num; } else { lean_assert(m_k > a.m_k); - static LEAN_THREAD_LOCAL mpz tmp; + mpz & tmp = get_tlocal1(); mul2k(tmp, a.m_num, m_k - a.m_k); m_num -= tmp; } @@ -141,7 +142,7 @@ mpbq & mpbq::sub_int(T const & a) { m_num -= a; } else { lean_assert(m_k > 0); - static LEAN_THREAD_LOCAL mpz tmp; + mpz & tmp = get_tlocal1(); tmp = a; mul2k(tmp, tmp, m_k); m_num -= tmp; @@ -303,7 +304,7 @@ bool lt_1div2k(mpbq const & a, unsigned k) { return false; } else { lean_assert(a.m_k > k); - static LEAN_THREAD_LOCAL mpz tmp; + mpz & tmp = get_tlocal1(); tmp = 1; mul2k(tmp, tmp, a.m_k - k); return a.m_num < tmp; diff --git a/src/util/numerics/mpbq.h b/src/util/numerics/mpbq.h index babc903cf..2d809ebd2 100644 --- a/src/util/numerics/mpbq.h +++ b/src/util/numerics/mpbq.h @@ -269,13 +269,13 @@ public: template<> class numeric_traits { private: - static LEAN_THREAD_LOCAL bool rnd; + MK_THREAD_LOCAL_GET(bool, get_rnd, false); public: 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(); } static bool is_neg(mpbq const & v) { return v.is_neg(); } - static void set_rounding(bool plus_inf) { rnd = plus_inf; } + static void set_rounding(bool plus_inf) { get_rnd() = plus_inf; } static void neg(mpbq & v) { v.neg(); } static void reset(mpbq & v) { v = 0; } static mpbq const & zero(); diff --git a/src/util/numerics/mpfp.cpp b/src/util/numerics/mpfp.cpp index be76a5338..538eebc5b 100644 --- a/src/util/numerics/mpfp.cpp +++ b/src/util/numerics/mpfp.cpp @@ -11,18 +11,18 @@ Author: Soonho Kong #include "util/numerics/mpfp.h" namespace lean { -static LEAN_THREAD_LOCAL mpfr_rnd_t g_mpfp_rnd = MPFR_RNDN; +MK_THREAD_LOCAL_GET(mpfr_rnd_t, get_g_mpfp_rnd, MPFR_RNDN); mpfp numeric_traits::pi_l; mpfp numeric_traits::pi_n; mpfp numeric_traits::pi_u; void set_mpfp_rnd(bool plus_inf) { - g_mpfp_rnd = plus_inf ? MPFR_RNDU : MPFR_RNDD; + get_g_mpfp_rnd() = plus_inf ? MPFR_RNDU : MPFR_RNDD; } mpfr_rnd_t get_mpfp_rnd() { - return g_mpfp_rnd; + return get_g_mpfp_rnd(); } /** diff --git a/src/util/numerics/mpfp.h b/src/util/numerics/mpfp.h index 7b9ec087e..d61e3e63b 100644 --- a/src/util/numerics/mpfp.h +++ b/src/util/numerics/mpfp.h @@ -458,21 +458,21 @@ public: void rround(mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_rint_round(m_val, m_val, rnd); } void rtrunc(mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_rint_trunc(m_val, m_val, rnd); } - friend mpfp floor(mpfp const & a) { static LEAN_THREAD_LOCAL mpfp tmp; tmp = a; tmp.floor(); return tmp; } - friend mpfp ceil (mpfp const & a) { static LEAN_THREAD_LOCAL mpfp tmp; tmp = a; tmp.ceil(); return tmp; } - friend mpfp round(mpfp const & a) { static LEAN_THREAD_LOCAL mpfp tmp; tmp = a; tmp.round(); return tmp; } - friend mpfp trunc(mpfp const & a) { static LEAN_THREAD_LOCAL mpfp tmp; tmp = a; tmp.trunc(); return tmp; } + friend mpfp floor(mpfp const & a) { mpfp tmp; tmp = a; tmp.floor(); return tmp; } + friend mpfp ceil (mpfp const & a) { mpfp tmp; tmp = a; tmp.ceil(); return tmp; } + friend mpfp round(mpfp const & a) { mpfp tmp; tmp = a; tmp.round(); return tmp; } + friend mpfp trunc(mpfp const & a) { mpfp tmp; tmp = a; tmp.trunc(); return tmp; } friend mpfp rfloor(mpfp const & a, mpfr_rnd_t rnd = get_mpfp_rnd()) { - static LEAN_THREAD_LOCAL mpfp tmp; tmp = a; tmp.rfloor(rnd); return tmp; + mpfp tmp; tmp = a; tmp.rfloor(rnd); return tmp; } friend mpfp rceil (mpfp const & a, mpfr_rnd_t rnd = get_mpfp_rnd()) { - static LEAN_THREAD_LOCAL mpfp tmp; tmp = a; tmp.rceil(rnd); return tmp; + mpfp tmp; tmp = a; tmp.rceil(rnd); return tmp; } friend mpfp rround(mpfp const & a, mpfr_rnd_t rnd = get_mpfp_rnd()) { - static LEAN_THREAD_LOCAL mpfp tmp; tmp = a; tmp.rround(rnd); return tmp; + mpfp tmp; tmp = a; tmp.rround(rnd); return tmp; } friend mpfp rtrunc(mpfp const & a, mpfr_rnd_t rnd = get_mpfp_rnd()) { - static LEAN_THREAD_LOCAL mpfp tmp; tmp = a; tmp.rtrunc(rnd); return tmp; + mpfp tmp; tmp = a; tmp.rtrunc(rnd); return tmp; } void power(mpfp const & b, mpfr_rnd_t rnd = get_mpfp_rnd()) { mpfr_pow(m_val, m_val, b.m_val, rnd); } diff --git a/src/util/numerics/mpq.cpp b/src/util/numerics/mpq.cpp index 7c309d1c1..a521ece06 100644 --- a/src/util/numerics/mpq.cpp +++ b/src/util/numerics/mpq.cpp @@ -23,11 +23,12 @@ mpq & mpq::operator=(mpbq const & b) { return *this; } +MK_THREAD_LOCAL_GET_DEF(mpz, get_tlocal1); int cmp(mpq const & a, mpz const & b) { if (a.is_integer()) { return mpz_cmp(mpq_numref(a.m_val), mpq::zval(b)); } else { - static LEAN_THREAD_LOCAL mpz tmp; + mpz & tmp = get_tlocal1(); mpz_mul(mpq::zval(tmp), mpq_denref(a.m_val), mpq::zval(b)); return mpz_cmp(mpq_numref(a.m_val), mpq::zval(tmp)); } @@ -140,14 +141,16 @@ DECL_UDATA(mpq) template static mpq const & to_mpq(lua_State * L) { - static LEAN_THREAD_LOCAL mpq arg; + 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_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; + *arg = mpq(to_mpz(L, idx)); + return *arg; } else { return *static_cast(luaL_checkudata(L, idx, mpq_mt)); } diff --git a/src/util/numerics/mpz.cpp b/src/util/numerics/mpz.cpp index 3c695c4ff..1040eaa76 100644 --- a/src/util/numerics/mpz.cpp +++ b/src/util/numerics/mpz.cpp @@ -54,7 +54,7 @@ mpz operator%(mpz const & a, mpz const & b) { } bool root(mpz & root, mpz const & a, unsigned k) { - static LEAN_THREAD_LOCAL mpz rem; + mpz rem; mpz_rootrem(root.m_val, rem.m_val, a.m_val, k); return rem.is_zero(); } @@ -99,10 +99,12 @@ DECL_UDATA(mpz) template static mpz const & to_mpz(lua_State * L) { - static LEAN_THREAD_LOCAL mpz arg; + 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_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"); } diff --git a/src/util/script_exception.cpp b/src/util/script_exception.cpp index 50e46985c..caba673a7 100644 --- a/src/util/script_exception.cpp +++ b/src/util/script_exception.cpp @@ -70,8 +70,10 @@ char const * script_exception::get_msg() const noexcept { return exception::what(); } +MK_THREAD_LOCAL_GET_DEF(std::string, get_g_buffer) + char const * script_exception::what() const noexcept { - static LEAN_THREAD_LOCAL std::string buffer; + std::string & buffer = get_g_buffer(); std::ostringstream strm; char const * msg = get_msg(); char const * space = msg && *msg == ' ' ? "" : " "; @@ -96,11 +98,13 @@ char const * script_nested_exception::what() const noexcept { std::string super_what = script_exception::what(); std::string nested_what = get_exception().what(); { - static LEAN_THREAD_LOCAL std::string buffer; + std::string buffer; std::ostringstream strm; strm << super_what << "\n" << nested_what; buffer = strm.str(); - return buffer.c_str(); + std::string & r_buffer = get_g_buffer(); + r_buffer = buffer; + return r_buffer.c_str(); } } } diff --git a/src/util/sexpr/format.cpp b/src/util/sexpr/format.cpp index 97da3bb71..eded82a94 100644 --- a/src/util/sexpr/format.cpp +++ b/src/util/sexpr/format.cpp @@ -120,7 +120,7 @@ format const & colon() { return g_colon; } format const & dot() { return g_dot; } // Auxiliary flag used to mark whether flatten // produce a different sexpr -static bool LEAN_THREAD_LOCAL g_diff_flatten = false; +MK_THREAD_LOCAL_GET(bool, get_g_diff_flatten, false); // sexpr format::flatten(sexpr const & s) { lean_assert(is_cons(s)); @@ -139,10 +139,10 @@ sexpr format::flatten(sexpr const & s) { })); case format_kind::CHOICE: /* flatten (x <|> y) = flatten x */ - g_diff_flatten = true; + get_g_diff_flatten() = true; return flatten(sexpr_choice_1(s)); case format_kind::LINE: - g_diff_flatten = true; + get_g_diff_flatten() = true; return sexpr_text(sexpr(" ")); case format_kind::FLAT_COMPOSE: case format_kind::TEXT: @@ -156,9 +156,9 @@ format format::flatten(format const & f){ return format(flatten(f.m_value)); } format group(format const & f) { - g_diff_flatten = false; + get_g_diff_flatten() = false; format flat_f = format::flatten(f); - if (g_diff_flatten) { + if (get_g_diff_flatten()) { return choice(flat_f, f); } else { // flat_f and f are essentially the same format object. diff --git a/src/util/splay_tree.h b/src/util/splay_tree.h index 920ec55ed..179519344 100644 --- a/src/util/splay_tree.h +++ b/src/util/splay_tree.h @@ -223,8 +223,10 @@ class splay_tree : public CMP { } } + MK_THREAD_LOCAL_GET_DEF(std::vector, get_g_path); + bool insert_pull(T const & v, bool is_insert) { - static LEAN_THREAD_LOCAL std::vector path; + std::vector & path = get_g_path(); node * n = m_ptr; bool found = false; while (true) { @@ -272,7 +274,7 @@ class splay_tree : public CMP { void pull_max() { if (!m_ptr) return; - static LEAN_THREAD_LOCAL std::vector path; + std::vector & path = get_g_path(); node * n = m_ptr; while (true) { lean_assert(n); diff --git a/src/util/stackinfo.cpp b/src/util/stackinfo.cpp index eed116006..85587df38 100644 --- a/src/util/stackinfo.cpp +++ b/src/util/stackinfo.cpp @@ -91,32 +91,32 @@ size_t get_stack_size(int main) { #endif static bool g_stack_info_init = false; -static LEAN_THREAD_LOCAL size_t g_stack_size; -static LEAN_THREAD_LOCAL size_t g_stack_base; +MK_THREAD_LOCAL_GET(size_t, get_g_stack_size, 0); +MK_THREAD_LOCAL_GET(size_t, get_g_stack_base, 0); void save_stack_info(bool main) { g_stack_info_init = true; - g_stack_size = get_stack_size(main); + get_g_stack_size() = get_stack_size(main); char x; - g_stack_base = reinterpret_cast(&x); + get_g_stack_base() = reinterpret_cast(&x); } size_t get_used_stack_size() { char y; size_t curr_stack = reinterpret_cast(&y); - return g_stack_base - curr_stack; + return get_g_stack_base() - curr_stack; } size_t get_available_stack_size() { size_t sz = get_used_stack_size(); - if (sz > g_stack_size) + if (sz > get_g_stack_size()) return 0; else - return g_stack_size - sz; + return get_g_stack_size() - sz; } void check_stack(char const * component_name) { - if (g_stack_info_init && get_used_stack_size() + LEAN_MIN_STACK_SPACE > g_stack_size) + if (g_stack_info_init && get_used_stack_size() + LEAN_MIN_STACK_SPACE > get_g_stack_size()) throw stack_space_exception(component_name); } } diff --git a/src/util/thread.h b/src/util/thread.h index 2c9511b30..ccbc86245 100644 --- a/src/util/thread.h +++ b/src/util/thread.h @@ -152,5 +152,32 @@ public: #include #define LEAN_THREAD_PTR(T) static boost::thread_specific_ptr #else - #define LEAN_THREAD_PTR(T) static std::unique_ptr LEAN_THREAD_LOCAL + template + class thread_specific_ptr { + T * m_ptr; + public: + thread_specific_ptr():m_ptr(nullptr) {} + ~thread_specific_ptr() { if (m_ptr) delete m_ptr; } + 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 #endif + +#define MK_THREAD_LOCAL_GET(T, GETTER_NAME, DEF_VALUE) \ +static T & GETTER_NAME() { \ + LEAN_THREAD_PTR(T) tlocal; \ + if (!tlocal.get()) \ + tlocal.reset(new T(DEF_VALUE)); \ + return *tlocal; \ +} + +#define MK_THREAD_LOCAL_GET_DEF(T, GETTER_NAME) \ +static T & GETTER_NAME() { \ + LEAN_THREAD_PTR(T) tlocal; \ + if (!tlocal.get()) \ + tlocal.reset(new T()); \ + return *tlocal; \ +} diff --git a/src/util/thread_script_state.cpp b/src/util/thread_script_state.cpp index dd7642a86..b720a1f4b 100644 --- a/src/util/thread_script_state.cpp +++ b/src/util/thread_script_state.cpp @@ -92,18 +92,20 @@ struct script_state_ref { ~script_state_ref() { recycle_state(m_state); } }; -static std::unique_ptr & get_script_state_ref() { - static std::unique_ptr LEAN_THREAD_LOCAL g_thread_state; - if (!g_thread_state) - g_thread_state.reset(new script_state_ref()); - return g_thread_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); + } } -script_state get_thread_script_state() { - return get_script_state_ref()->m_state; -} - -void release_thread_script_state() { - get_script_state_ref().reset(nullptr); -} +script_state get_thread_script_state() { return *get_script_state_ref(false); } +void release_thread_script_state() { get_script_state_ref(true); } }