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

refactor(*): replace LEAN_THREAD_LOCAL with MK_THREAD_LOCAL_GET, the new macro uses the Boost thread_local_ptr instead of 'thread_local' directive

Browse source 
Motivation: clang++ on OSX does not support 'thread_local'.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-07 10:18:32 -07:00
parent 91df9a5550
commit 15f0899efb
26 changed files with 212 additions and 149 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

27
src/kernel/expr.cpp
View file

@ -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<unsigned>(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<expr_cell*> & 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, expr_hash, is_bi_equal_proc> 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

28
src/library/decl_macros.h
View file

@ -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) \

12
src/library/placeholder.cpp
View file

@ -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)); }

2
src/library/resolve_macro.cpp
View file

@ -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};

5
src/tests/util/thread.cpp
View file

@ -16,8 +16,9 @@ using namespace lean;
#if defined(LEAN_MULTI_THREAD)
void foo() {
static LEAN_THREAD_LOCAL std::vector<int> v(1024);
if (v.size() != 1024) {
LEAN_THREAD_PTR(std::vector<int>) v;
if (!v.get()) v.reset(new std::vector<int>(1024));
if (v->size() != 1024) {
std::cerr << "Error\n";
exit(1);
}

5
src/util/exception.cpp
View file

@ -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();

10
src/util/interrupt.cpp
View file

@ -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 {

46
src/util/interval/interval.cpp
View file

@ -280,8 +280,8 @@ template<bool compute_intv, bool compute_deps>
interval<T> & interval<T>::sub(interval<T> 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<T> & interval<T>::mul(interval<T> 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<T> & interval<T>::mul(interval<T> 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<T> & interval<T>::div(interval<T> 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<T> & interval<T>::operator-=(T const & o) {
template<typename T>
interval<T> & interval<T>::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<T> & interval<T>::operator*=(T const & o) {
template<typename T>
interval<T> & interval<T>::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<T>::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<T>::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<T>::set_rounding(to_plus_inf);
a /= x;
} else {
static LEAN_THREAD_LOCAL T tmp;
T tmp;
numeric_traits<T>::set_rounding(!to_plus_inf);
tmp = x;
numeric_traits<T>::power(tmp, n);
@ -1141,7 +1141,7 @@ void interval<T>::display(std::ostream & out) const {
template<typename T> void interval<T>::fmod(interval<T> y) {
T const & yb = numeric_traits<T>::is_neg(m_lower) ? y.m_lower : y.m_upper;
static LEAN_THREAD_LOCAL T n;
T n;
numeric_traits<T>::set_rounding(false);
n = m_lower / yb;
numeric_traits<T>::floor(n);
@ -1149,7 +1149,7 @@ template<typename T> void interval<T>::fmod(interval<T> y) {
}
template<typename T> void interval<T>::fmod(T y) {
static LEAN_THREAD_LOCAL T n;
T n;
numeric_traits<T>::set_rounding(false);
n = m_lower / y;
numeric_traits<T>::floor(n);
@ -1781,8 +1781,8 @@ void interval<T>::tan(interval_deps & deps) {
template<typename T>
template<bool compute_intv, bool compute_deps>
void interval<T>::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<T>::sec (interval_deps & deps) {
template<typename T>
template<bool compute_intv, bool compute_deps>
void interval<T>::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;

7
src/util/interval/interval.h
View file

@ -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<typename T2> interval & operator=(T2 const & n) { m_lower = n; m_upper = n; set_closed_endpoints(); return *this; }
interval & operator=(T const & n);

16
src/util/memory.cpp
View file

@ -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);
}

7
src/util/numerics/double.cpp
View file

@ -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); }

9
src/util/numerics/double.h
View file

@ -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();

7
src/util/numerics/float.cpp
View file

@ -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); }

9
src/util/numerics/float.h
View file

@ -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();

23
src/util/numerics/mpbq.cpp
View file

@ -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;

4
src/util/numerics/mpbq.h
View file

@ -269,13 +269,13 @@ public:
template<>
class numeric_traits<mpbq> {
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();

6
src/util/numerics/mpfp.cpp
View file

@ -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<mpfp>::pi_l;
mpfp numeric_traits<mpfp>::pi_n;
mpfp numeric_traits<mpfp>::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();
}
/**

16
src/util/numerics/mpfp.h
View file

@ -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); }

15
src/util/numerics/mpq.cpp
View file

@ -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<int idx>
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<mpq*>(luaL_checkudata(L, idx, mpq_mt));
}

10
src/util/numerics/mpz.cpp
View file

@ -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<int idx>
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<long>(lua_tointeger(L, idx)); return arg;
case LUA_TSTRING: arg = mpz(lua_tostring(L, idx)); return arg;
case LUA_TNUMBER: *arg = static_cast<long>(lua_tointeger(L, idx)); return *arg;
case LUA_TSTRING: *arg = mpz(lua_tostring(L, idx)); return *arg;
case LUA_TUSERDATA: return *static_cast<mpz*>(luaL_checkudata(L, idx, mpz_mt));
default: throw exception(sstream() << "arg #" << idx << " must be a number, string or mpz");
}

10
src/util/script_exception.cpp
View file

@ -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();
}
}
}

10
src/util/sexpr/format.cpp
View file

@ -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.

6
src/util/splay_tree.h
View file

@ -223,8 +223,10 @@ class splay_tree : public CMP {
}
}
MK_THREAD_LOCAL_GET_DEF(std::vector<entry>, get_g_path);
bool insert_pull(T const & v, bool is_insert) {
static LEAN_THREAD_LOCAL std::vector<entry> path;
std::vector<entry> & 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<entry> path;
std::vector<entry> & path = get_g_path();
node * n = m_ptr;
while (true) {
lean_assert(n);

16
src/util/stackinfo.cpp
View file

@ -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<size_t>(&x);
get_g_stack_base() = reinterpret_cast<size_t>(&x);
}
size_t get_used_stack_size() {
char y;
size_t curr_stack = reinterpret_cast<size_t>(&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);
}
}

29
src/util/thread.h
View file

@ -152,5 +152,32 @@ public:
#include <boost/thread/tss.hpp>
#define LEAN_THREAD_PTR(T) static boost::thread_specific_ptr<T>
#else
#define LEAN_THREAD_PTR(T) static std::unique_ptr<T> LEAN_THREAD_LOCAL
template<typename T>
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<T> 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; \
}

26
src/util/thread_script_state.cpp
View file

@ -92,18 +92,20 @@ struct script_state_ref {
~script_state_ref() { recycle_state(m_state); }
};
static std::unique_ptr<script_state_ref> & get_script_state_ref() {
static std::unique_ptr<script_state_ref> 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); }
}