feat(util): add small object allocator

src/util/CMakeLists.txt

@@ -3,4 +3,5 @@ add_library(util OBJECT debug.cpp name.cpp name_set.cpp fresh_name.cpp
   safe_arith.cpp ascii.cpp memory.cpp shared_mutex.cpp realpath.cpp
   stackinfo.cpp lean_path.cpp serializer.cpp lbool.cpp
   bitap_fuzzy_search.cpp init_module.cpp thread.cpp memory_pool.cpp
-  utf8.cpp name_map.cpp list_fn.cpp null_ostream.cpp file_lock.cpp)
+  utf8.cpp name_map.cpp list_fn.cpp null_ostream.cpp file_lock.cpp
+  small_object_allocator.cpp)

src/util/debug.h

@@ -19,7 +19,7 @@ Author: Leonardo de Moura
 #define DEBUG_CODE(CODE)
 #endif
 
-#define lean_unreachable() DEBUG_CODE({lean::notify_assertion_violation(__FILE__, __LINE__, "UNREACHABLE CODE WAS REACHED."); lean::invoke_debugger();}) throw unreachable_reached();
+#define lean_unreachable() DEBUG_CODE({lean::notify_assertion_violation(__FILE__, __LINE__, "UNREACHABLE CODE WAS REACHED."); lean::invoke_debugger();}) throw lean::unreachable_reached();
 
 #ifdef LEAN_DEBUG
 #define lean_verify(COND) if (!(COND)) { lean::notify_assertion_violation(__FILE__, __LINE__, #COND); lean::invoke_debugger(); }

src/util/small_object_allocator.cpp

@@ -0,0 +1,211 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <iomanip>
+#include <algorithm>
+#include <vector>
+#include "util/memory.h"
+#include "util/small_object_allocator.h"
+
+namespace lean {
+small_object_allocator::small_object_allocator(char const * id) {
+    for (unsigned i = 0; i < NUM_SLOTS; i++) {
+        m_chunks[i] = 0;
+        m_free_list[i] = 0;
+    }
+    m_id         = id;
+    m_alloc_size = 0;
+}
+
+small_object_allocator::~small_object_allocator() {
+    for (unsigned i = 0; i < NUM_SLOTS; i++) {
+        chunk * c = m_chunks[i];
+        while (c) {
+            chunk * next = c->m_next;
+            delete c;
+            c = next;
+        }
+    }
+    DEBUG_CODE({
+        if (m_alloc_size > 0) {
+            std::cerr << "Memory leak detected for small object allocator '"
+                      << m_id << "'. " << m_alloc_size << " bytes leaked" << std::endl;
+        }
+    });
+}
+
+void small_object_allocator::reset() {
+    for (unsigned i = 0; i < NUM_SLOTS; i++) {
+        chunk * c = m_chunks[i];
+        while (c) {
+            chunk * next = c->m_next;
+            delete c;
+            c = next;
+        }
+        m_chunks[i] = 0;
+        m_free_list[i] = 0;
+    }
+    m_alloc_size = 0;
+}
+
+void small_object_allocator::deallocate(size_t size, void * p) {
+    if (size == 0) return;
+#if LEAN_DEBUG
+    // Valgrind friendly
+    delete[] p;
+    return;
+#endif
+    lean_assert(m_alloc_size >= size);
+    lean_assert(p);
+    m_alloc_size -= size;
+    if (size >= SMALL_OBJ_SIZE - (1 << PTR_ALIGNMENT)) {
+        free(p);
+        return;
+    }
+    unsigned slot_id = static_cast<unsigned>(size >> PTR_ALIGNMENT);
+    if ((size & MASK) != 0)
+        slot_id++;
+    lean_assert(slot_id > 0);
+    lean_assert(slot_id < NUM_SLOTS);
+    *(reinterpret_cast<void**>(p)) = m_free_list[slot_id];
+    m_free_list[slot_id] = p;
+}
+
+void * small_object_allocator::allocate(size_t size) {
+    if (size == 0) return 0;
+#if LEAN_DEBUG
+    // Valgrind friendly
+    return new char[size];
+#endif
+    m_alloc_size += size;
+    if (size >= SMALL_OBJ_SIZE - (1 << PTR_ALIGNMENT))
+        return malloc(size);
+#ifdef LEAN_DEBUG
+    size_t osize = size;
+#endif
+    unsigned slot_id = static_cast<unsigned>(size >> PTR_ALIGNMENT);
+    if ((size & MASK) != 0)
+        slot_id++;
+    lean_assert(slot_id < NUM_SLOTS);
+    lean_assert(slot_id > 0);
+    if (m_free_list[slot_id] != 0) {
+        void * r = m_free_list[slot_id];
+        m_free_list[slot_id] = *(reinterpret_cast<void **>(r));
+        return r;
+    }
+    chunk * c = m_chunks[slot_id];
+    size = slot_id << PTR_ALIGNMENT;
+    lean_assert(size >= osize);
+    if (c != 0) {
+        char * new_curr = c->m_curr + size;
+        if (new_curr < c->m_data + CHUNK_SIZE) {
+            void * r = c->m_curr;
+            c->m_curr = new_curr;
+            return r;
+        }
+    }
+    chunk * new_c = new chunk();
+    new_c->m_next = c;
+    m_chunks[slot_id] = new_c;
+    void * r = new_c->m_curr;
+    new_c->m_curr += size;
+    return r;
+}
+
+size_t small_object_allocator::get_wasted_size() const {
+    size_t r = 0;
+    for (unsigned slot_id = 0; slot_id < NUM_SLOTS; slot_id++) {
+        size_t slot_obj_size = slot_id << PTR_ALIGNMENT;
+        void ** ptr = reinterpret_cast<void **>(const_cast<small_object_allocator*>(this)->m_free_list[slot_id]);
+        while (ptr != 0) {
+            r += slot_obj_size;
+            ptr = reinterpret_cast<void**>(*ptr);
+        }
+    }
+    return r;
+}
+
+size_t small_object_allocator::get_num_free_objs() const {
+    size_t r = 0;
+    for (unsigned slot_id = 0; slot_id < NUM_SLOTS; slot_id++) {
+        void ** ptr = reinterpret_cast<void **>(const_cast<small_object_allocator*>(this)->m_free_list[slot_id]);
+        while (ptr != 0) {
+            r ++;
+            ptr = reinterpret_cast<void**>(*ptr);
+        }
+    }
+    return r;
+}
+
+template<typename T>
+struct ptr_lt {
+    bool operator()(T * p1, T * p2) const { return p1 < p2; }
+};
+
+void small_object_allocator::consolidate() {
+    std::vector<chunk*> chunks;
+    std::vector<char*> free_objs;
+    for (unsigned slot_id = 1; slot_id < NUM_SLOTS; slot_id++) {
+        if (m_free_list[slot_id] == 0)
+            continue;
+        chunks.clear();
+        free_objs.clear();
+        chunk * c = m_chunks[slot_id];
+        while (c != 0) {
+            chunks.push_back(c);
+            c = c->m_next;
+        }
+        char * ptr = static_cast<char*>(m_free_list[slot_id]);
+        while (ptr != 0) {
+            free_objs.push_back(ptr);
+            ptr = *(reinterpret_cast<char**>(ptr));
+        }
+        unsigned obj_size = slot_id << PTR_ALIGNMENT;
+        unsigned num_objs_per_chunk = CHUNK_SIZE / obj_size;
+        if (free_objs.size() < num_objs_per_chunk)
+            continue;
+        lean_assert(!chunks.empty());
+        std::sort(chunks.begin(), chunks.end(), ptr_lt<chunk>());
+        std::sort(free_objs.begin(), free_objs.end(), ptr_lt<char>());
+        chunk *   last_chunk = 0;
+        void * last_free_obj = 0;
+        unsigned chunk_idx = 0;
+        unsigned obj_idx   = 0;
+        unsigned num_chunks = chunks.size();
+        unsigned num_objs   = free_objs.size();
+        while (chunk_idx < num_chunks) {
+            chunk * curr_chunk = chunks[chunk_idx];
+            char *  curr_begin = curr_chunk->m_data;
+            char *  curr_end   = curr_begin + CHUNK_SIZE;
+            unsigned num_free_in_chunk = 0;
+            unsigned saved_obj_idx = obj_idx;
+            while (obj_idx < num_objs) {
+                char * free_obj = free_objs[obj_idx];
+                if (free_obj > curr_end)
+                    break;
+                obj_idx++;
+                num_free_in_chunk++;
+            }
+            if (num_free_in_chunk == num_objs_per_chunk) {
+                delete curr_chunk;
+            }
+            else {
+                curr_chunk->m_next = last_chunk;
+                last_chunk = curr_chunk;
+                for (unsigned i = saved_obj_idx; i < obj_idx; i++) {
+                    // relink objects
+                    void * free_obj = free_objs[i];
+                    *(reinterpret_cast<void**>(free_obj)) = last_free_obj;
+                    last_free_obj = free_obj;
+                }
+            }
+            chunk_idx++;
+        }
+        m_chunks[slot_id]    = last_chunk;
+        m_free_list[slot_id] = last_free_obj;
+    }
+}
+}

src/util/small_object_allocator.h

@@ -0,0 +1,43 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "util/debug.h"
+
+namespace lean {
+class small_object_allocator {
+    static const unsigned PTR_ALIGNMENT  = (sizeof(unsigned) == sizeof(void*) ? 2 /* 32 bit */ : 3 /* 64 bit */);
+    static const unsigned CHUNK_SIZE     = (8192 - sizeof(void*)*2);
+    static const unsigned SMALL_OBJ_SIZE = 256;
+    static const unsigned NUM_SLOTS      = (SMALL_OBJ_SIZE >> PTR_ALIGNMENT);
+    static const unsigned MASK           = ((1 << PTR_ALIGNMENT) - 1);
+    struct chunk {
+        chunk * m_next;
+        char  * m_curr;
+        char    m_data[CHUNK_SIZE];
+        chunk():m_curr(m_data) {}
+    };
+    chunk *      m_chunks[NUM_SLOTS];
+    void  *      m_free_list[NUM_SLOTS];
+    size_t       m_alloc_size;
+    char const * m_id;
+public:
+    small_object_allocator(char const * id = "unknown");
+    ~small_object_allocator();
+    void reset();
+    void * allocate(size_t size);
+    void deallocate(size_t size, void * p);
+    size_t get_allocation_size() const { return m_alloc_size; }
+    size_t get_wasted_size() const;
+    size_t get_num_free_objs() const;
+    void consolidate();
+};
+}
+
+inline void * operator new(size_t s, lean::small_object_allocator & r) { return r.allocate(s); }
+inline void * operator new[](size_t s, lean::small_object_allocator & r) { return r.allocate(s); }
+inline void operator delete(void *, lean::small_object_allocator &) { lean_unreachable(); }
+inline void operator delete[](void *, lean::small_object_allocator &) { lean_unreachable(); }