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

fix(util/rb_tree): do not use thread local storage in template when compiling on OSX with clang++ without Boost

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-26 12:46:24 -07:00
parent 4ab0dd4700
commit 11711a2409
2 changed files with 22 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/CMakeLists.txt
View file

@ -93,6 +93,7 @@ if ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU")
message(FATAL_ERROR "${PROJECT_NAME} requires g++ 4.8 or greater.") message(FATAL_ERROR "${PROJECT_NAME} requires g++ 4.8 or greater.")
endif () endif ()
elseif ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") elseif ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang")
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -D__CLANG__")
if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin") if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
# In OSX, clang requires "-stdlib=libc++" to support C++11 # In OSX, clang requires "-stdlib=libc++" to support C++11
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -stdlib=libc++") set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -stdlib=libc++")

22
src/util/rb_tree.h
View file

@ -14,6 +14,11 @@ Author: Leonardo de Moura
#include "util/memory_pool.h" #include "util/memory_pool.h"
namespace lean { namespace lean {
#if defined(__CLANG__) && defined(__APPLE__) && !defined(LEAN_USE_BOOST)
// TODO(Leo): remove when problen on clang++ OSX thread local storage implementation is fixed
#define LEAN_TEMPLATE_THREAD_LOCAL_UNSAFE
#endif
/** /**
\brief Left-leaning Red-Black Trees \brief Left-leaning Red-Black Trees
@ -63,6 +68,7 @@ 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) {} 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) {}
}; };
#if !defined(LEAN_TEMPLATE_THREAD_LOCAL_UNSAFE)
typedef memory_pool<sizeof(node_cell)> node_allocator; typedef memory_pool<sizeof(node_cell)> node_allocator;
static node_allocator & get_node_allocator() { static node_allocator & get_node_allocator() {
LEAN_THREAD_PTR(node_allocator) g_allocator; LEAN_THREAD_PTR(node_allocator) g_allocator;
@ -70,6 +76,7 @@ class rb_tree : public CMP {
g_allocator.reset(new node_allocator()); g_allocator.reset(new node_allocator());
return *g_allocator; return *g_allocator;
} }
#endif
int cmp(T const & v1, T const & v2) const { int cmp(T const & v1, T const & v2) const {
return CMP::operator()(v1, v2); return CMP::operator()(v1, v2);
@ -77,7 +84,11 @@ class rb_tree : public CMP {
static node ensure_unshared(node && n) { static node ensure_unshared(node && n) {
if (n.is_shared()) { if (n.is_shared()) {
#if defined(LEAN_TEMPLATE_THREAD_LOCAL_UNSAFE)
return node(new node_cell(*n.m_ptr));
#else
return node(new (get_node_allocator().allocate()) node_cell(*n.m_ptr)); return node(new (get_node_allocator().allocate()) node_cell(*n.m_ptr));
#endif
} else { } else {
return n; return n;
} }
@ -135,8 +146,13 @@ class rb_tree : public CMP {
} }
node insert(node && n, T const & v) { node insert(node && n, T const & v) {
if (!n) if (!n) {
#if defined(LEAN_TEMPLATE_THREAD_LOCAL_UNSAFE)
return node(new node_cell(v));
#else
return node(new (get_node_allocator().allocate()) node_cell(v)); return node(new (get_node_allocator().allocate()) node_cell(v));
#endif
}
node h = ensure_unshared(n.steal()); node h = ensure_unshared(n.steal());
int c = cmp(v, h->m_value); int c = cmp(v, h->m_value);
@ -374,8 +390,12 @@ public:
template<typename T, typename CMP> template<typename T, typename CMP>
void rb_tree<T, CMP>::node_cell::dealloc() { void rb_tree<T, CMP>::node_cell::dealloc() {
#if defined(LEAN_TEMPLATE_THREAD_LOCAL_UNSAFE)
delete this;
#else
this->~node_cell(); this->~node_cell();
get_node_allocator().recycle(this); get_node_allocator().recycle(this);
#endif
} }
template<typename T, typename CMP> template<typename T, typename CMP>