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

fix(kernel/level): add workaround for clang++ bug: memory leak at thread_local

Browse source 
The fix has an advantage. There is only one copy of level Zero in the system even when multiple threads are used.
Moreover, it does no require any form of synchronization, and modules can be initialized in any order.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-03 10:37:46 -07:00
parent 076414693a
commit 02df63b85e
1 changed files with 10 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/kernel/level.cpp
View file

@ -241,15 +241,19 @@ level mk_param_univ(name const & n) { return level(new level_param_core(level_ki
level mk_global_univ(name const & n) { return level(new level_param_core(level_kind::Global, n)); }
level mk_meta_univ(name const & n) { return level(new level_param_core(level_kind::Meta, n)); }
static std::unique_ptr<level> g_zero_ptr;
static std::unique_ptr<level> g_one_ptr;
level const & mk_level_zero() {
static LEAN_THREAD_LOCAL level g_zero(new level_cell(level_kind::Zero, 7u));
return g_zero;
if (!g_zero_ptr) g_zero_ptr.reset(new level(new level_cell(level_kind::Zero, 7u)));
return *g_zero_ptr;
}
level const & mk_level_one() {
static LEAN_THREAD_LOCAL level g_one(mk_succ(mk_level_zero()));
return g_one;
level const & mk_level_one() {
if (!g_one_ptr) g_one_ptr.reset(new level(mk_succ(mk_level_zero())));
return *g_one_ptr;
}
// Force g_one_ptr and g_zero_ptr to be created at initialization time.
// Purpose: avoid any kind of synchronization at mk_level_zero and mk_level_one
static level g_dummy(mk_level_one());
bool is_one(level const & l) {
return l == mk_level_one();