From d827b567771df23a66bcced9864042fb1b488871 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 7 Jun 2014 13:05:03 -0700
Subject: [PATCH] fix(util/memory): remove get_thread_allocated_memory, it used
 thread_local

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/tests/util/memory.cpp |  1 -
 src/util/memory.cpp       | 23 -----------------------
 src/util/memory.h         |  5 -----
 3 files changed, 29 deletions(-)

diff --git a/src/tests/util/memory.cpp b/src/tests/util/memory.cpp
index e725cc0b5..e63387a11 100644
--- a/src/tests/util/memory.cpp
+++ b/src/tests/util/memory.cpp
@@ -20,7 +20,6 @@ static void tst1() {
     a = static_cast<int*>(lean::realloc(a, N * 2 * sizeof(N)));
     lean_assert(lean::get_allocated_memory() >= old_mem + N * 2 * sizeof(N));
     std::cout << "Total: "  << static_cast<size_t>(lean::get_allocated_memory()) << "\n";
-    std::cout << "Thread: " << static_cast<size_t>(lean::get_thread_allocated_memory()) << "\n";
 #if !defined(HAS_TCMALLOC) && !defined(LEAN_USE_BOOST)
     // When TCMALLOC is used, there is a problem during initialization, and the value of get_thread_allocated_memory is off.
     lean_assert_eq(lean::get_allocated_memory(), static_cast<size_t>(lean::get_thread_allocated_memory()));
diff --git a/src/util/memory.cpp b/src/util/memory.cpp
index b0f26eddb..b7e30c06b 100644
--- a/src/util/memory.cpp
+++ b/src/util/memory.cpp
@@ -14,10 +14,6 @@ size_t     get_allocated_memory() {
     return 0;
 }
 
-long long  get_thread_allocated_memory() {
-    return 0;
-}
-
 void * malloc(size_t sz)  {
     void * r = ::malloc(sz);
     if (r || sz == 0)
@@ -105,31 +101,15 @@ public:
     size_t size() const { return m_size; }
 };
 
-class thread_alloc_info {
-    size_t m_size; // It can be negative
-public:
-    thread_alloc_info():m_size(0) {}
-    void inc(size_t sz) { m_size += sz; }
-    void dec(size_t sz) { m_size -= sz; }
-    long long size() const { return static_cast<long long>(m_size); }
-};
-
 static alloc_info                          g_global_memory;
-static thread_alloc_info & get_thread_memory() {
-    // we cannot use MK_THREAD_LOCAL_GET here because it depends on new/delete, and the Lean new/delete invokes this procedure
-    static thread_alloc_info LEAN_THREAD_LOCAL g_info;
-    return g_info;
-}
 
 size_t     get_allocated_memory() { return g_global_memory.size(); }
-long long  get_thread_allocated_memory() { return get_thread_memory().size(); }
 
 void * malloc(size_t sz)  {
     void * r = malloc_core(sz);
     if (r || sz == 0) {
         size_t rsz = malloc_size(r);
         g_global_memory.inc(rsz);
-        get_thread_memory().inc(rsz);
         return r;
     } else {
         throw std::bad_alloc();
@@ -145,11 +125,9 @@ void * realloc(void * ptr, size_t sz) {
     }
     size_t old_sz = malloc_size(ptr);
     g_global_memory.dec(old_sz);
-    get_thread_memory().dec(old_sz);
     void * r = realloc_core(ptr, sz);
     size_t new_sz = malloc_size(r);
     g_global_memory.inc(new_sz);
-    get_thread_memory().inc(new_sz);
     if (r || sz == 0)
         return r;
     else
@@ -160,7 +138,6 @@ void free(void * ptr) {
     if (ptr) {
         size_t sz = malloc_size(ptr);
         g_global_memory.dec(sz);
-        get_thread_memory().dec(sz);
     }
     free_core(ptr);
 }
diff --git a/src/util/memory.h b/src/util/memory.h
index 379b319e5..166bc0b48 100644
--- a/src/util/memory.h
+++ b/src/util/memory.h
@@ -8,12 +8,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 size_t get_allocated_memory();
-long long get_thread_allocated_memory();
 void * malloc(size_t sz);
 void * realloc(void * ptr, size_t sz);
 void free(void * ptr);
 }
-
-
-
-