From 4e9035d4b9f7b42b9cb1f07b2d901ae80fd83fba Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nlopes@microsoft.com>
Date: Sat, 24 Oct 2020 12:46:50 +0100
Subject: [PATCH] cleanup thread pool of scoped_timer on memory finalize but
 keep it alive on Z3_memory_reset()

---
 src/api/api_context.cpp     |  2 +-
 src/util/memory_manager.cpp |  7 ++++++-
 src/util/memory_manager.h   |  2 +-
 src/util/scoped_timer.cpp   | 42 +++++++++++++++++++++++++------------
 src/util/scoped_timer.h     |  6 ------
 5 files changed, 37 insertions(+), 22 deletions(-)

diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp
index f113744b4..9ec6f708f 100644
--- a/src/api/api_context.cpp
+++ b/src/api/api_context.cpp
@@ -426,7 +426,7 @@ extern "C" {
 
     void Z3_API Z3_reset_memory(void) {
         LOG_Z3_reset_memory();
-        memory::finalize();
+        memory::finalize(false);
         memory::initialize(0);
     }
 
diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp
index a325afca7..37b2ea716 100644
--- a/src/util/memory_manager.cpp
+++ b/src/util/memory_manager.cpp
@@ -27,6 +27,7 @@ Copyright (c) 2015 Microsoft Corporation
 //    rational::finalize();
 void mem_initialize();
 void mem_finalize();
+void finalize_scoped_timer();
 
 // If PROFILE_MEMORY is defined, Z3 will display the amount of memory used, and the number of synchronization steps during finalization
 // #define PROFILE_MEMORY
@@ -130,7 +131,7 @@ void memory::set_max_alloc_count(size_t max_count) {
 
 static bool g_finalizing = false;
 
-void memory::finalize() {
+void memory::finalize(bool shutdown) {
     if (g_memory_initialized) {
         g_finalizing = true;
         mem_finalize();
@@ -139,6 +140,10 @@ void memory::finalize() {
         //delete g_memory_mux;
         g_memory_initialized = false;
         g_finalizing = false;
+
+        if (shutdown) {
+            finalize_scoped_timer();
+        }
     }
 }
 
diff --git a/src/util/memory_manager.h b/src/util/memory_manager.h
index 3e7626e29..7dab520df 100644
--- a/src/util/memory_manager.h
+++ b/src/util/memory_manager.h
@@ -55,7 +55,7 @@ public:
     static bool above_high_watermark();
     static void set_max_size(size_t max_size);
     static void set_max_alloc_count(size_t max_count);
-    static void finalize();
+    static void finalize(bool shutdown = true);
     static void display_max_usage(std::ostream& os);
     static void display_i_max_usage(std::ostream& os);
     static void deallocate(void* p);
diff --git a/src/util/scoped_timer.cpp b/src/util/scoped_timer.cpp
index 06b10479c..bfef8ba04 100644
--- a/src/util/scoped_timer.cpp
+++ b/src/util/scoped_timer.cpp
@@ -20,6 +20,7 @@ Revision History:
 --*/
 
 #include "util/scoped_timer.h"
+#include "util/mutex.h"
 #include "util/util.h"
 #include "util/vector.h"
 #include <chrono>
@@ -32,20 +33,15 @@ Revision History:
 struct state {
     std::thread * m_thread { nullptr };
     std::timed_mutex m_mutex;
-    unsigned ms { 0 };
-    event_handler * eh { nullptr };
-    int work { 0 };
+    event_handler * eh;
+    unsigned ms;
+    int work;
     std::condition_variable_any cv;
 };
 
-/*
- * NOTE: this implementation deliberately leaks threads when Z3
- * exits. this is preferable to deallocating on exit, because
- * destructing threads blocked on condition variables leads to
- * deadlock.
- */
 static std::vector<state*> available_workers;
 static std::mutex workers;
+static atomic<unsigned> num_workers(0);
 
 static void thread_func(state *s) {
     workers.lock();
@@ -53,6 +49,10 @@ static void thread_func(state *s) {
         s->cv.wait(workers, [=]{ return s->work > 0; });
         workers.unlock();
 
+        // exiting..
+        if (s->work == 2)
+            return;
+
         auto end = std::chrono::steady_clock::now() + std::chrono::milliseconds(s->ms);
 
         while (!s->m_mutex.try_lock_until(end)) {
@@ -81,6 +81,7 @@ public:
         if (available_workers.empty()) {
             workers.unlock();
             s = new state;
+            ++num_workers;
         } 
         else {
             s = available_workers.back();
@@ -93,7 +94,6 @@ public:
         s->work = 1;
         if (!s->m_thread) {
             s->m_thread = new std::thread(thread_func, s);
-            s->m_thread->detach();
         } 
         else {
             s->cv.notify_one();
@@ -117,7 +117,23 @@ scoped_timer::~scoped_timer() {
 }
 
 void finalize_scoped_timer() {
-    // TODO: stub to collect idle allocated timers.
-    // if a timer is not idle, we treat this as abnormal
-    // termination and don't commit to collecting the state.
+    unsigned deleted = 0;
+
+    while (deleted < num_workers) {
+        workers.lock();
+        for (auto w : available_workers) {
+            w->work = 2;
+            w->cv.notify_one();
+        }
+        decltype(available_workers) cleanup_workers;
+        std::swap(available_workers, cleanup_workers);
+        workers.unlock();
+
+        for (auto w : cleanup_workers) {
+            ++deleted;
+            w->m_thread->join();
+            delete w->m_thread;
+            delete w;
+        }
+    }
 }
diff --git a/src/util/scoped_timer.h b/src/util/scoped_timer.h
index 7d44923fe..41dcce7b3 100644
--- a/src/util/scoped_timer.h
+++ b/src/util/scoped_timer.h
@@ -27,9 +27,3 @@ public:
     scoped_timer(unsigned ms, event_handler * eh);
     ~scoped_timer();
 };
-
-/*
-  ADD_FINALIZER('finalize_scoped_timer();')
-*/
-
-void finalize_scoped_timer();