src/runtime/alloc.cpp linked list optimization

Stream: lean4

[Jad Ghalayini]

From my reading of alloc.cpp, it seems the mutex in

struct heap_manager {
    /* The mutex protects the list of orphan segments. */
    mutex             m_mutex;
    heap *            m_orphans{nullptr};

    void push_orphan(heap * h) {
        /* TODO(Leo): avoid mutex */
        lock_guard<mutex> lock(m_mutex);
        h->m_next_orphan = m_orphans;
        m_orphans = h;
    }

    heap * pop_orphan() {
        /* TODO(Leo): avoid mutex */
        lock_guard<mutex> lock(m_mutex);
        if (m_orphans) {
            heap * h = m_orphans;
            m_orphans = h->m_next_orphan;
            return h;
        } else {
            return nullptr;
        }
    }
};

could be relatively easily replaced with simply an intrusive atomic linked-list, as the comments seem to indicate. Would a PR implementing this be welcome?

[Leonardo de Moura]

Thanks for offering to help. Unfortunately, we don't have the resources to review this kind of PR at the moment.
We are currently focused on porting all Mathlib tactics to Lean 4, and making sure all bugs and missing features have been addressed.
We will probably only have time to review the PR in November. Note that we seldom touch alloc.c, so even if you submit the PR now, it will not get stale. If you are ok with the PR sitting there for a few months, please go ahead.