From 50cfe354bee117c3471abe1bbf54780696674566 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Fri, 20 Jun 2025 10:52:17 +0200 Subject: [PATCH] chore: remove old LEAN_AUTO_THREAD_FINALIZATION workaround (#8885) This PR removes an old workaround around non-implemented C++11 features in the thread finalization. This `ifdef` dates back to approximately 2015 as can be seen [here](https://github.com/leanprover/lean3/blame/master/src/util/thread.cpp#L177), the comments mention that it was originally implemented because not all compilers at the time were able to support the C++11 `thread_local` keyword. 10 years later this is hopefully the case and we can remove this workaround. There is an additional motivation for doing this, `lean::initialize_thread` contains the following allocation: ```cpp g_thread_finalizers_mgr = new thread_finalizers_manager; ``` this is supposed to be freed at some point but: ```cpp // TODO(gabriel): race condition with thread finalizers void delete_thread_finalizer_manager() { // delete g_thread_finalizers_mgr; // g_thread_finalizers_mgr = nullptr; } ``` so `g_thread_finalizers_mgr` leaks upon repeated invocation of `lean::initialize_thread`. Note that Windows has already been using this alternative implementation for a while so the alternative implementation has (hopefully) not rotten away in the meantime. --- script/prepare-llvm-mingw.sh | 1 - src/CMakeLists.txt | 7 --- src/runtime/thread.cpp | 105 ----------------------------------- 3 files changed, 113 deletions(-) diff --git a/script/prepare-llvm-mingw.sh b/script/prepare-llvm-mingw.sh index 4098c7ac10..f07487332e 100644 --- a/script/prepare-llvm-mingw.sh +++ b/script/prepare-llvm-mingw.sh @@ -50,5 +50,4 @@ echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='--sysroot ROOT -L ROOT/lib -Wl,-Bstatic # when not using the above flags, link GMP dynamically/as usual. Always link ICU dynamically. echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-lgmp $(pkg-config --libs libuv) -lucrtbase'" # do not set `LEAN_CC` for tests -echo -n " -DAUTO_THREAD_FINALIZATION=OFF -DSTAGE0_AUTO_THREAD_FINALIZATION=OFF" echo -n " -DLEAN_TEST_VARS=''" diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 0457c08dee..7dcb366bc6 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -58,9 +58,6 @@ option(USE_GITHASH "GIT_HASH" ON) option(INSTALL_LICENSE "INSTALL_LICENSE" ON) # When ON we install a copy of cadical option(INSTALL_CADICAL "Install a copy of cadical" ON) -# When ON thread storage is automatically finalized, it assumes platform support pthreads. -# This option is important when using Lean as library that is invoked from a different programming language (e.g., Haskell). -option(AUTO_THREAD_FINALIZATION "AUTO_THREAD_FINALIZATION" ON) # FLAGS for disabling optimizations and debugging option(FREE_VAR_RANGE_OPT "FREE_VAR_RANGE_OPT" ON) @@ -182,10 +179,6 @@ else() string(APPEND LEAN_EXTRA_CXX_FLAGS " -D LEAN_MULTI_THREAD") endif() -if(AUTO_THREAD_FINALIZATION AND NOT MSVC) - string(APPEND LEAN_EXTRA_CXX_FLAGS " -D LEAN_AUTO_THREAD_FINALIZATION") -endif() - # Set Module Path set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${CMAKE_SOURCE_DIR}/cmake/Modules") diff --git a/src/runtime/thread.cpp b/src/runtime/thread.cpp index cd53bae6ad..7df3d8f2f7 100644 --- a/src/runtime/thread.cpp +++ b/src/runtime/thread.cpp @@ -9,9 +9,6 @@ Author: Leonardo de Moura #include #ifdef LEAN_WINDOWS #include -# ifdef LEAN_AUTO_THREAD_FINALIZATION -#include -# endif #else #include #endif @@ -179,107 +176,6 @@ void run_thread_finalizers_core(thread_finalizers & fns) { 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_thread_finalizers_mgr = nullptr; - -// TODO(gabriel): race condition with thread finalizers -void delete_thread_finalizer_manager() { - // delete g_thread_finalizers_mgr; - // g_thread_finalizers_mgr = nullptr; -} - -void register_thread_finalizer(thread_finalizer fn, void * p) { - g_thread_finalizers_mgr->get_thread_finalizers().emplace_back(fn, p); -} - -void register_post_thread_finalizer(thread_finalizer fn, void * p) { - g_thread_finalizers_mgr->get_post_thread_finalizers().emplace_back(fn, p); -} - -void run_thread_finalizers() { - if (auto p = g_thread_finalizers_mgr->get_pair()) - run_thread_finalizers_core(p->first); -} - -void run_post_thread_finalizers() { - if (auto p = g_thread_finalizers_mgr->get_pair()) - run_thread_finalizers_core(p->second); -} - -void initialize_thread() { - g_thread_finalizers_mgr = new thread_finalizers_manager; - initialize_thread_local_reset_fns(); -} -void finalize_thread() { - finalize_thread_local_reset_fns(); -} -#else -// reference implementation LEAN_THREAD_PTR(thread_finalizers, g_finalizers); LEAN_THREAD_PTR(thread_finalizers, g_post_finalizers); @@ -320,5 +216,4 @@ void initialize_thread() { void finalize_thread() { finalize_thread_local_reset_fns(); } -#endif }