diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp
index 67f5b82b3..85d673f7c 100644
--- a/src/util/memory_manager.cpp
+++ b/src/util/memory_manager.cpp
@@ -13,6 +13,11 @@ Copyright (c) 2015 Microsoft Corporation
 #include "util/error_codes.h"
 #include "util/debug.h"
 #include "util/scoped_timer.h"
+#ifdef __GLIBC__
+# include <malloc.h>
+# define HAS_MALLOC_USABLE_SIZE
+#endif
+
 // The following two function are automatically generated by the mk_make.py script.
 // The script collects ADD_INITIALIZER and ADD_FINALIZER commands in the .h files.
 // For example, rational.h contains
@@ -215,7 +220,7 @@ void * memory::allocate(char const* file, int line, char const* obj, size_t s) {
 }
 #endif
 
-#if !defined(SINGLE_THREAD)
+#ifndef SINGLE_THREAD
 // ==================================
 // ==================================
 // THREAD LOCAL VERSION
@@ -258,9 +263,14 @@ static void synchronize_counters(bool allocating) {
 }
 
 void memory::deallocate(void * p) {
+#ifdef HAS_MALLOC_USABLE_SIZE
+    size_t sz      = malloc_usable_size(p);
+    void * real_p  = p;
+#else
     size_t * sz_p  = reinterpret_cast<size_t*>(p) - 1;
     size_t sz      = *sz_p;
     void * real_p  = reinterpret_cast<void*>(sz_p);
+#endif
     g_memory_thread_alloc_size -= sz;
     free(real_p);
     if (g_memory_thread_alloc_size < -SYNCH_THRESHOLD) {
@@ -269,28 +279,41 @@ void memory::deallocate(void * p) {
 }
 
 void * memory::allocate(size_t s) {
+#ifndef HAS_MALLOC_USABLE_SIZE
     s = s + sizeof(size_t); // we allocate an extra field!
-    void * r = malloc(s);
-    if (r == nullptr) {
-        throw_out_of_memory();
-        return nullptr;
-    }
-    *(static_cast<size_t*>(r)) = s;
+#endif
     g_memory_thread_alloc_size += s;
     g_memory_thread_alloc_count += 1;
     if (g_memory_thread_alloc_size > SYNCH_THRESHOLD) {
         synchronize_counters(true);
     }
-
+    void * r = malloc(s);
+    if (r == nullptr) {
+        throw_out_of_memory();
+        return nullptr;
+    }
+#ifdef HAS_MALLOC_USABLE_SIZE
+    g_memory_thread_alloc_size += malloc_usable_size(r) - s;
+    return r;
+#else
+    *(static_cast<size_t*>(r)) = s;
     return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field
+#endif
 }
 
 void* memory::reallocate(void *p, size_t s) {
+#ifdef HAS_MALLOC_USABLE_SIZE
+    size_t sz      = malloc_usable_size(p);
+    void * real_p  = p;
+    // We may be lucky and malloc gave us enough space
+    if (sz >= s)
+        return p;
+#else
     size_t *sz_p = reinterpret_cast<size_t*>(p)-1;
     size_t sz = *sz_p;
     void *real_p = reinterpret_cast<void*>(sz_p);
     s = s + sizeof(size_t); // we allocate an extra field!
-
+#endif
     g_memory_thread_alloc_size += s - sz;
     g_memory_thread_alloc_count += 1;
     if (g_memory_thread_alloc_size > SYNCH_THRESHOLD) {
@@ -302,74 +325,97 @@ void* memory::reallocate(void *p, size_t s) {
         throw_out_of_memory();
         return nullptr;
     }
+#ifdef HAS_MALLOC_USABLE_SIZE
+    g_memory_thread_alloc_size += malloc_usable_size(r) - s;
+    return r;
+#else
     *(static_cast<size_t*>(r)) = s;
     return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field
+#endif
 }
 
 #else
 // ==================================
 // ==================================
-// NO THREAD LOCAL VERSION
+// SINGLE-THREAD MODE
 // ==================================
 // ==================================
-// allocate & deallocate without using thread local storage
+// allocate & deallocate without locking
 
 void memory::deallocate(void * p) {
+#ifdef HAS_MALLOC_USABLE_SIZE
+    size_t sz      = malloc_usable_size(p);
+    void * real_p  = p;
+#else
     size_t * sz_p  = reinterpret_cast<size_t*>(p) - 1;
     size_t sz      = *sz_p;
     void * real_p  = reinterpret_cast<void*>(sz_p);
-    {
-        lock_guard lock(*g_memory_mux);
-        g_memory_alloc_size -= sz;
-    }
+#endif
+    g_memory_alloc_size -= sz;
     free(real_p);
 }
 
 void * memory::allocate(size_t s) {
+#ifndef HAS_MALLOC_USABLE_SIZE
     s = s + sizeof(size_t); // we allocate an extra field!
-    {
-        lock_guard lock(*g_memory_mux);
-        g_memory_alloc_size += s;
-        g_memory_alloc_count += 1;
-        if (g_memory_alloc_size > g_memory_max_used_size)
-            g_memory_max_used_size = g_memory_alloc_size;
-        if (g_memory_max_size != 0 && g_memory_alloc_size > g_memory_max_size)
-            throw_out_of_memory();
-        if (g_memory_max_alloc_count != 0 && g_memory_alloc_count > g_memory_max_alloc_count)
-            throw_alloc_counts_exceeded();
-    }
+#endif
+    g_memory_alloc_size += s;
+    g_memory_alloc_count += 1;
+    if (g_memory_alloc_size > g_memory_max_used_size)
+        g_memory_max_used_size = g_memory_alloc_size;
+    if (g_memory_max_size != 0 && g_memory_alloc_size > g_memory_max_size)
+        throw_out_of_memory();
+    if (g_memory_max_alloc_count != 0 && g_memory_alloc_count > g_memory_max_alloc_count)
+        throw_alloc_counts_exceeded();
+
     void * r = malloc(s);
     if (r == nullptr) {
         throw_out_of_memory();
         return nullptr;
     }
+#ifdef HAS_MALLOC_USABLE_SIZE
+    g_memory_alloc_size += malloc_usable_size(r) - s;
+    return r;
+#else
     *(static_cast<size_t*>(r)) = s;
     return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field
+#endif
 }
 
 void* memory::reallocate(void *p, size_t s) {
+#ifdef HAS_MALLOC_USABLE_SIZE
+    size_t sz      = malloc_usable_size(p);
+    void * real_p  = p;
+    // We may be lucky and malloc gave us enough space
+    if (sz >= s)
+        return p;
+#else
     size_t * sz_p  = reinterpret_cast<size_t*>(p) - 1;
     size_t sz      = *sz_p;
     void * real_p  = reinterpret_cast<void*>(sz_p);
     s = s + sizeof(size_t); // we allocate an extra field!
-    {
-        lock_guard lock(*g_memory_mux);
-        g_memory_alloc_size += s - sz;
-        g_memory_alloc_count += 1;
-        if (g_memory_alloc_size > g_memory_max_used_size)
-            g_memory_max_used_size = g_memory_alloc_size;
-        if (g_memory_max_size != 0 && g_memory_alloc_size > g_memory_max_size)
-            throw_out_of_memory();
-        if (g_memory_max_alloc_count != 0 && g_memory_alloc_count > g_memory_max_alloc_count)
-            throw_alloc_counts_exceeded();
-    }
+#endif
+    g_memory_alloc_size += s - sz;
+    g_memory_alloc_count += 1;
+    if (g_memory_alloc_size > g_memory_max_used_size)
+        g_memory_max_used_size = g_memory_alloc_size;
+    if (g_memory_max_size != 0 && g_memory_alloc_size > g_memory_max_size)
+        throw_out_of_memory();
+    if (g_memory_max_alloc_count != 0 && g_memory_alloc_count > g_memory_max_alloc_count)
+        throw_alloc_counts_exceeded();
+
     void *r = realloc(real_p, s);
     if (r == nullptr) {
         throw_out_of_memory();
         return nullptr;
     }
+#ifdef HAS_MALLOC_USABLE_SIZE
+    g_memory_alloc_size += malloc_usable_size(r) - s;
+    return r;
+#else
     *(static_cast<size_t*>(r)) = s;
     return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field
+#endif
 }
  
 #endif