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

refactor(*): minimize dependency on thread local storage, simplify MK_THREAD_LOCAL_GET

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-07 12:15:40 -07:00
parent d9794d8ea4
commit a42856c1d2
6 changed files with 40 additions and 52 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

32
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;
T & new_l_val = get_tlocal1();
T & new_u_val = get_tlocal2();
T new_l_val;
T new_u_val;
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();
T & new_l_val = get_tlocal1();
T & new_u_val = get_tlocal2();
T new_l_val;
T new_u_val;
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()) {
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;
T ad; xnumeral_kind ad_k = XN_NUMERAL;
T bc; xnumeral_kind bc_k = XN_NUMERAL;
T ac; xnumeral_kind ac_k = XN_NUMERAL;
T bd; 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;
T & new_l_val = get_tlocal1();
T & new_u_val = get_tlocal2();
T new_l_val;
T new_u_val;
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;
T & tmp1 = get_tlocal1();
T tmp1;
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;
T & tmp1 = get_tlocal1();
T tmp1;
if (this->is_zero()) {
return *this;
}
@ -872,8 +872,8 @@ void interval<T>::inv(interval_deps & deps) {
using std::swap;
T & new_l_val = get_tlocal1();
T & new_u_val = get_tlocal2();
T new_l_val;
T new_u_val;
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();
T & un1 = get_tlocal1();
T & un2 = get_tlocal2();
T un1;
T un2;
if (compute_intv) {
swap(un1, m_lower);
swap(un2, m_upper);

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

@ -65,13 +65,6 @@ 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);

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

@ -21,11 +21,10 @@ void double_floor(double & v);
// Macro to implement transcendental functions using MPFR
#define LEAN_TRANS_DOUBLE_FUNC(f, v, rnd) \
LEAN_THREAD_PTR(mpfp) t; \
if (!t.get()) t.reset(new mpfp(53)); \
*t = v; \
t->f(rnd); \
v = t->get_double(rnd);
mpfp t(53); \
t = v; \
t.f(rnd); \
v = t.get_double(rnd);
void set_double_rnd(bool plus_inf);
mpfr_rnd_t get_double_rnd();

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

@ -21,11 +21,10 @@ void float_floor(float & v);
// Macro to implement transcendental functions using MPFR
#define LEAN_TRANS_FLOAT_FUNC(f, v, rnd) \
LEAN_THREAD_PTR(mpfp) t; \
if (!t.get()) t.reset(new mpfp(24)); \
*t = v; \
t->f(rnd); \
v = t->get_float(rnd);
mpfp t(24); \
t = v; \
t.f(rnd); \
v = t.get_float(rnd);
void set_float_rnd(bool plus_inf);
mpfr_rnd_t get_float_rnd();

11
src/util/splay_tree.h
View file

@ -8,7 +8,6 @@ Author: Leonardo de Moura
#include <iostream>
#include <algorithm>
#include <utility>
#include <vector>
#include "util/rc.h"
#include "util/pair.h"
#include "util/debug.h"
@ -95,7 +94,7 @@ class splay_tree : public CMP {
entry(bool r, node * n):m_right(r), m_node(n) {}
};
void splay_to_top(std::vector<entry> & path, node * n) {
void splay_to_top(buffer<entry, 32> & path, node * n) {
lean_assert(!n->is_shared());
while (path.size() > 1) {
auto p_entry = path.back(); path.pop_back();
@ -194,7 +193,7 @@ class splay_tree : public CMP {
return true;
}
void update_parent(std::vector<entry> const & path, node * child) {
void update_parent(buffer<entry, 32> const & path, node * child) {
lean_assert(child);
if (path.empty()) {
child->inc_ref();
@ -223,10 +222,8 @@ 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) {
std::vector<entry> & path = get_g_path();
buffer<entry, 32> path;
node * n = m_ptr;
bool found = false;
while (true) {
@ -274,7 +271,7 @@ class splay_tree : public CMP {
void pull_max() {
if (!m_ptr) return;
std::vector<entry> & path = get_g_path();
buffer<entry, 32> path;
node * n = m_ptr;
while (true) {
lean_assert(n);

24
src/util/thread.h
View file

@ -167,20 +167,20 @@ public:
#endif
#if defined(LEAN_USE_BOOST) && defined(LEAN_MULTI_THREAD)
#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(T, GETTER_NAME, DEF_VALUE) \
LEAN_THREAD_PTR(T) GETTER_NAME ## _tlocal; \
static T & GETTER_NAME() { \
if (!(GETTER_NAME ## _tlocal).get()) \
(GETTER_NAME ## _tlocal).reset(new T(DEF_VALUE)); \
return *(GETTER_NAME ## _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; \
#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); \
}
#else
// MK_THREAD_LOCAL_GET_DEF and MK_THREAD_LOCAL_GET when LEAN_USE_BOOST is not defined