diff --git a/src/tests/shared/thread.cpp b/src/tests/shared/thread.cpp index e1398269b..0964119bd 100644 --- a/src/tests/shared/thread.cpp +++ b/src/tests/shared/thread.cpp @@ -53,7 +53,6 @@ void test_import() { check(lean_options_mk_empty(&o, &ex)); check(lean_ios_mk_std(o, &ios, &ex)); check(lean_env_import(env, ios, ms, &new_env, &ex)); - std::cout << "standard library has been imported\n"; lean_env_del(env); lean_env_del(new_env); lean_name_del(std); diff --git a/src/tests/util/thread.cpp b/src/tests/util/thread.cpp index 07f5d2c56..6ee74c4b6 100644 --- a/src/tests/util/thread.cpp +++ b/src/tests/util/thread.cpp @@ -17,14 +17,13 @@ using namespace lean; #if defined(LEAN_MULTI_THREAD) && !defined(__APPLE__) LEAN_THREAD_PTR(std::vector, g_v); -void finalize_vector() { - delete g_v; - g_v = nullptr; +void finalize_vector(void * p) { + delete reinterpret_cast*>(p); } void foo() { if (!g_v) { g_v = new std::vector(1024); - register_thread_finalizer(finalize_vector); + register_thread_finalizer(finalize_vector, g_v); } if (g_v->size() != 1024) { std::cerr << "Error\n"; diff --git a/src/util/memory_pool.cpp b/src/util/memory_pool.cpp index 45b396a76..a3aa0cef7 100644 --- a/src/util/memory_pool.cpp +++ b/src/util/memory_pool.cpp @@ -30,21 +30,21 @@ void * memory_pool::allocate() { typedef std::vector memory_pools; LEAN_THREAD_PTR(memory_pools, g_thread_pools); -static void thread_finalize_memory_pool() { - if (g_thread_pools) { - unsigned i = g_thread_pools->size(); - while (i > 0) { - --i; - delete (*g_thread_pools)[i]; - } - delete g_thread_pools; +static void thread_finalize_memory_pool(void * p) { + std::vector * thread_pools = reinterpret_cast*>(p); + unsigned i = thread_pools->size(); + while (i > 0) { + --i; + delete (*thread_pools)[i]; } + delete thread_pools; + g_thread_pools = nullptr; } memory_pool * allocate_thread_memory_pool(unsigned sz) { if (!g_thread_pools) { - register_post_thread_finalizer(thread_finalize_memory_pool); g_thread_pools = new std::vector(); + register_post_thread_finalizer(thread_finalize_memory_pool, g_thread_pools); } memory_pool * r = new memory_pool(sz); g_thread_pools->push_back(r); diff --git a/src/util/thread.cpp b/src/util/thread.cpp index 142ba641d..2cfa3bedf 100644 --- a/src/util/thread.cpp +++ b/src/util/thread.cpp @@ -30,83 +30,131 @@ void initialize_thread() {} void finalize_thread() {} #endif -typedef std::vector thread_finalizers; +typedef std::vector> thread_finalizers; + +void run_thread_finalizers_core(thread_finalizers & fns) { + unsigned i = fns.size(); + while (i > 0) { + --i; + auto fn = fns[i].first; + fn(fns[i].second); + } + fns.clear(); +} + +// We have two different implementations of the following procedures. +// +// void register_thread_finalizer(thread_finalizer fn, void * p); +// void register_post_thread_finalizer(thread_finalizer fn, void * p); +// void run_thread_finalizers(); +// +// The implementation is selected by using the LEAN_AUTO_THREAD_FINALIZATION compilation directive. +// We can remove the implementation based on pthreads after the new thread_local C++11 keyword is properly +// implemented in all platforms. +// In the meantime, when LEAN_AUTO_THREAD_FINALIZATION is defined/set, we use a thread finalization +// procedure based on the pthread API. +// Remark: we only need this feature when Lean is being used as a library. +// Example: the C API is being used from Haskell, and the execution threads +// are being created by Haskell. +// Remark: for the threads created by Lean, we explicitly create the thread finalizers. +// The idea is to avoid memory leaks even when LEAN_AUTO_THREAD_FINALIZATION is not used. + +#if defined(LEAN_AUTO_THREAD_FINALIZATION) +// pthread based implementation + +typedef std::pair thread_finalizers_pair; + +class thread_finalizers_manager { + pthread_key_t g_key; +public: + thread_finalizers_manager() { + pthread_key_create(&g_key, finalize_thread); + init_thread(); // initialize main thread + } + + ~thread_finalizers_manager() { + finalize_thread(get_pair()); // finalize main thread + pthread_key_delete(g_key); + } + + thread_finalizers_pair * get_pair() { + return reinterpret_cast(pthread_getspecific(g_key)); + } + + void init_thread() { + if (get_pair() == nullptr) { + thread_finalizers_pair * p = new thread_finalizers_pair(); + pthread_setspecific(g_key, p); + } + } + + thread_finalizers & get_thread_finalizers() { + init_thread(); + return get_pair()->first; + } + + thread_finalizers & get_post_thread_finalizers() { + init_thread(); + return get_pair()->second; + } + + static void finalize_thread(void * d) { + if (d) { + thread_finalizers_pair * p = reinterpret_cast(d); + run_thread_finalizers_core(p->first); + run_thread_finalizers_core(p->second); + delete p; + } + } +}; + +static thread_finalizers_manager g_aux; + +void register_thread_finalizer(thread_finalizer fn, void * p) { + g_aux.get_thread_finalizers().emplace_back(fn, p); +} + +void register_post_thread_finalizer(thread_finalizer fn, void * p) { + g_aux.get_post_thread_finalizers().emplace_back(fn, p); +} + +void run_thread_finalizers() { +} + +void run_post_thread_finalizers() { +} +#else +// reference implementation LEAN_THREAD_PTR(thread_finalizers, g_finalizers); LEAN_THREAD_PTR(thread_finalizers, g_post_finalizers); +void register_thread_finalizer(thread_finalizer fn, void * p) { + if (!g_finalizers) + g_finalizers = new thread_finalizers(); + g_finalizers->emplace_back(fn, p); +} + +void register_post_thread_finalizer(thread_finalizer fn, void * p) { + if (!g_post_finalizers) + g_post_finalizers = new thread_finalizers(); + g_post_finalizers->emplace_back(fn, p); +} + void run_thread_finalizers(thread_finalizers * fns) { if (fns) { - unsigned i = fns->size(); - while (i > 0) { - --i; - auto fn = (*fns)[i]; - fn(); - } + run_thread_finalizers_core(*fns); delete fns; } } void run_thread_finalizers() { run_thread_finalizers(g_finalizers); - g_finalizers = nullptr; + g_finalizers = nullptr; } void run_post_thread_finalizers() { run_thread_finalizers(g_post_finalizers); g_post_finalizers = nullptr; } - -#if defined(LEAN_AUTO_THREAD_FINALIZATION) -// This is an auxiliary class used to finalize thread local storage. -// It can be removed after the new thread_local C++11 keyword is properly -// implemented in all platforms. -// In the meantime, we create a "fake" key that is only used to trigger -// the Lean thread finalization procedures. -// We only need this feature when Lean is being used as a library. -// Example: the C API is being used from Haskell, and the execution threads -// are being created by Haskell. -// Remark: for the threads created by Lean, we explicitly create the thread finalizers. -// The idea is to avoid memory leaks even when LEAN_AUTO_THREAD_FINALIZATION is not used. -class thread_key_init { - pthread_key_t g_key; -public: - static void finalize_thread(void *) { // NOLINT - run_thread_finalizers(); - run_post_thread_finalizers(); - } - - thread_key_init() { - pthread_key_create(&g_key, finalize_thread); - } - - ~thread_key_init() { - pthread_key_delete(g_key); - } - - void init_thread() { - void * p; - if ((p = pthread_getspecific(g_key)) == nullptr) { - pthread_setspecific(g_key, reinterpret_cast(1)); - } - } -}; - -static thread_key_init g_aux; #endif - -void register_thread_finalizer(thread_finalizer fn) { - if (!g_finalizers) { - g_finalizers = new thread_finalizers(); - #if defined(LEAN_AUTO_THREAD_FINALIZATION) - g_aux.init_thread(); - #endif - } - g_finalizers->push_back(fn); -} - -void register_post_thread_finalizer(thread_finalizer fn) { - if (!g_post_finalizers) - g_post_finalizers = new thread_finalizers(); - g_post_finalizers->push_back(fn); -} } diff --git a/src/util/thread.h b/src/util/thread.h index 36dc79da2..4dd8d51bd 100644 --- a/src/util/thread.h +++ b/src/util/thread.h @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once +#include #if defined(LEAN_MULTI_THREAD) #if !defined(LEAN_USE_BOOST) // MULTI THREADING SUPPORT BASED ON THE STANDARD LIBRARY @@ -169,42 +170,41 @@ public: #define LEAN_THREAD_VALUE(T, V, VAL) static __thread T V = VAL #endif -#define MK_THREAD_LOCAL_GET(T, GETTER_NAME, DEF_VALUE) \ -LEAN_THREAD_PTR(T, GETTER_NAME ## _tlocal); \ -static void finalize_ ## GETTER_NAME() { \ - delete GETTER_NAME ## _tlocal; \ - GETTER_NAME ## _tlocal = nullptr; \ -} \ -static T & GETTER_NAME() { \ - if (!GETTER_NAME ## _tlocal) { \ - GETTER_NAME ## _tlocal = new T(DEF_VALUE); \ - register_thread_finalizer(finalize_ ## GETTER_NAME); \ - } \ - return *(GETTER_NAME ## _tlocal); \ +#define MK_THREAD_LOCAL_GET(T, GETTER_NAME, DEF_VALUE) \ +LEAN_THREAD_PTR(T, GETTER_NAME ## _tlocal); \ +static void finalize_ ## GETTER_NAME(void * p) { \ + delete reinterpret_cast(p); \ + GETTER_NAME ## _tlocal = nullptr; \ +} \ +static T & GETTER_NAME() { \ + if (!GETTER_NAME ## _tlocal) { \ + GETTER_NAME ## _tlocal = new T(DEF_VALUE); \ + register_thread_finalizer(finalize_ ## GETTER_NAME, GETTER_NAME ## _tlocal); \ + } \ + return *(GETTER_NAME ## _tlocal); \ } -#define MK_THREAD_LOCAL_GET_DEF(T, GETTER_NAME) \ -LEAN_THREAD_PTR(T, GETTER_NAME ## _tlocal); \ -static void finalize_ ## GETTER_NAME() { \ - delete GETTER_NAME ## _tlocal; \ - GETTER_NAME ## _tlocal = nullptr; \ -} \ -static T & GETTER_NAME() { \ - if (!GETTER_NAME ## _tlocal) { \ - GETTER_NAME ## _tlocal = new T(); \ - register_thread_finalizer(finalize_ ## GETTER_NAME); \ - } \ - return *(GETTER_NAME ## _tlocal); \ +#define MK_THREAD_LOCAL_GET_DEF(T, GETTER_NAME) \ +LEAN_THREAD_PTR(T, GETTER_NAME ## _tlocal); \ +static void finalize_ ## GETTER_NAME(void * p) { \ + delete reinterpret_cast(p); \ + GETTER_NAME ## _tlocal = nullptr; \ +} \ +static T & GETTER_NAME() { \ + if (!GETTER_NAME ## _tlocal) { \ + GETTER_NAME ## _tlocal = new T(); \ + register_thread_finalizer(finalize_ ## GETTER_NAME, GETTER_NAME ## _tlocal); \ + } \ + return *(GETTER_NAME ## _tlocal); \ } - namespace lean { void initialize_thread(); void finalize_thread(); -typedef void (*thread_finalizer)(); -void register_post_thread_finalizer(thread_finalizer fn); -void register_thread_finalizer(thread_finalizer fn); -void run_post_thread_finalizers(); +typedef void (*thread_finalizer)(void *); +void register_post_thread_finalizer(thread_finalizer fn, void * p); +void register_thread_finalizer(thread_finalizer fn, void * p); void run_thread_finalizers(); +void run_post_thread_finalizers(); } diff --git a/src/util/thread_script_state.cpp b/src/util/thread_script_state.cpp index 438214670..e58e3d7c5 100644 --- a/src/util/thread_script_state.cpp +++ b/src/util/thread_script_state.cpp @@ -123,26 +123,25 @@ struct script_state_ref { LEAN_THREAD_PTR(bool, g_registered); LEAN_THREAD_PTR(script_state_ref, g_thread_state_ref); -static void finalize_thread_state_ref() { - delete g_thread_state_ref; - g_thread_state_ref = nullptr; - delete g_registered; +static void finalize_registered(void * p) { + delete reinterpret_cast(p); g_registered = nullptr; } +static void finalize_thread_state_ref(void * p) { + delete reinterpret_cast(p); + g_thread_state_ref = nullptr; +} + script_state get_thread_script_state() { if (!g_thread_state_ref) { g_thread_state_ref = new script_state_ref(); - if (!g_registered) { - g_registered = new bool(true); - register_thread_finalizer(finalize_thread_state_ref); - } + register_thread_finalizer(finalize_thread_state_ref, g_thread_state_ref); + } + if (!g_registered) { + g_registered = new bool(true); + register_thread_finalizer(finalize_registered, g_registered); } return g_thread_state_ref->m_state; } - -void release_thread_script_state() { - delete g_thread_state_ref; - g_thread_state_ref = nullptr; -} } diff --git a/src/util/thread_script_state.h b/src/util/thread_script_state.h index b7b4e408d..ea0fed35a 100644 --- a/src/util/thread_script_state.h +++ b/src/util/thread_script_state.h @@ -25,19 +25,13 @@ void system_dostring(char const * code); void system_import(char const * fname); /** \brief Retrieve a script_state object for the current thread. - The thread has exclusive access until the thread is destroyed, - or the method \c release_thread_script_state is invoked. + The thread has exclusive access until the thread is destroyed. \remark For performance reasons global script_state objects are recycled. So, users should not delete/redefine functions defined using #system_dostring. So, side-effects are discouraged. */ script_state get_thread_script_state(); -/** - \brief Put the thread script_state back on the state pool, - and available for other threads. -*/ -void release_thread_script_state(); void enable_script_state_recycling(bool flag); void initialize_thread_script_state();