fix(util/thread): make sure threads are finalized when using the Lean C API and threads are created by the host system

src/CMakeLists.txt

@@ -37,6 +37,9 @@ option(INCLUDE_MSYS2_DLLS "INCLUDE_MSYS2_DLLS" OFF)
 option(LEAN_BIN_DEP       "LEAN_BIN_DEP"      ON)
 # When ON we include githash in the version string
 option(USE_GITHASH        "GIT_HASH"          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)
 # Directory that include lean emacs mode dependecies
 set(EMACS_DEPENDENCIES "${CMAKE_SOURCE_DIR}/emacs/dependencies")
 
@@ -83,6 +86,10 @@ if(CACHE_EXPRS)
   set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_CACHE_EXPRS")
 endif()
 
+if(AUTO_THREAD_FINALIZATION)
+  set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_AUTO_THREAD_FINALIZATION")
+endif()
+
 if(CONSERVE_MEMORY AND ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU"))
   message(STATUS "Using compilation flags for minimizing the amount of memory used by gcc")
   set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} --param ggc-min-heapsize=32768 --param ggc-min-expand=20")

src/tests/shared/thread.cpp

@@ -64,6 +64,8 @@ void test_import() {
 
 int main() {
     std::thread t1(test_import);
+    std::thread t2(test_import);
     t1.join();
+    t2.join();
     return 0;
 }

src/util/thread.cpp

@@ -4,7 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include <pthread.h>
 #include <vector>
+#include <iostream>
 #include "util/thread.h"
 
 namespace lean {
@@ -32,18 +34,6 @@ typedef std::vector<thread_finalizer> thread_finalizers;
 LEAN_THREAD_PTR(thread_finalizers, g_finalizers);
 LEAN_THREAD_PTR(thread_finalizers, g_post_finalizers);
 
-void register_thread_finalizer(thread_finalizer fn) {
-    if (!g_finalizers)
-        g_finalizers = new thread_finalizers();
-    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);
-}
-
 void run_thread_finalizers(thread_finalizers * fns) {
     if (fns) {
         unsigned i = fns->size();
@@ -58,9 +48,65 @@ void run_thread_finalizers(thread_finalizers * fns) {
 
 void run_thread_finalizers() {
     run_thread_finalizers(g_finalizers);
+    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<void*>(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);
 }
 }