perf: make the small-object allocation fast path a leaf - #14998
Draft
Kha wants to merge 1 commit into
Draft
Conversation
Kha
marked this pull request as draft
September 2, 2026 11:59
Member
Author
|
!bench |
|
Benchmark results for 29fe74e against ac0f56e are in. There are significant results. @Kha
Large changes (19✅, 1🟥)
Medium changes (32✅)
Small changes (1855✅, 1🟥)
|
github-actions
Bot
added
the
toolchain-available
Collaborator
|
Reference manual CI status:
|
github-actions
Bot
added
the
mathlib4-nightly-available
mathlib-lean-pr-testing
Bot
added
the
builds-mathlib
|
Mathlib CI status (docs):
|
Member
Author
|
!bench mathlib |
|
Benchmark results for leanprover-community/mathlib4-nightly-testing@81601f8 against leanprover-community/mathlib4-nightly-testing@2415714 are in. There are significant results. @Kha
Large changes (1✅)
Medium changes (1✅)
Small changes (725✅)
|
This PR shortens the fused small-object allocation entry point from 18 to 14 instructions and gives constructor allocation a single merged header store, worth 0.75% of user instructions on the workloads measured below. Three changes, none of which need a patch to mimalloc. The page refill moves into a cold helper that the entry points tail-jump to, so the fast path no longer builds a stack frame for a call it rarely makes; the helper also writes `m_cs_sz`, which is what leaves `sz` dead across the branch and keeps `lean_alloc_small_object_core` a leaf as well. Restating the callers' precondition on `sz` (word-aligned, non-zero, at most `MI_SMALL_SIZE_MAX`) folds mimalloc's bin-index rounding into a plain byte offset and drops the mask before the header store; the bound is a safety condition in its own right, since a larger `sz` would index `pages_free_direct` out of bounds. Finally, a second entry point `lean_alloc_small_object_raw` leaves the whole header to the caller. The fast path of `lean_alloc_small_object_core`: ```diff -push rbx ; frame, only for the refill call below mov rax, [rip+...] ; &lean_g_tls inc QWORD PTR fs:[rax] ; heartbeat++ mov rcx, QWORD PTR fs:[rax+0x8] ; theap mov esi, edi -lea rax, [rsi+0x7] ; round sz up to a bin index -and rax, 0xfffffffffffffff8 -mov rdx, [rcx+rax*1+0x120] ; theap->pages_free_direct[..] +mov rdx, [rcx+rsi*1+0x120] ; sz is the byte offset already mov rax, [rdx+0x8] ; page->free test rax, rax -je .Lcold ; inline cold path, ending in pop rbx; ret +je lean_alloc_small_generic_core ; tail jump, nothing to tear down mov rcx, [rax] ; pop the block mov [rdx+0x8], rcx inc WORD PTR [rdx+0x10] ; page->used++ mov QWORD PTR [rax], 0x0 ; mimalloc's free-list scrub -mov WORD PTR [rax+0x4], di ; m_cs_sz, masked to 16 bits -pop rbx +mov DWORD PTR [rax+0x4], edi ; m_cs_sz, no mask needed ret ``` `lean_alloc_small_object_raw` is what lets `lean_alloc_ctor` write all four header fields with adjacent stores that merge, rather than having the callee store `m_cs_sz` and the caller fill in around it. Allocating a `List.cons`: ```diff mov edi, 0x18 -call lean_alloc_small_object_core ; stores m_cs_sz itself -mov DWORD PTR [rax], 0x1 ; m_rc -mov WORD PTR [rax+0x6], 0x102 ; m_other, m_tag; cannot merge across m_cs_sz +call lean_alloc_small_object_raw ; leaves the header alone +movabs rcx, 0x102001800000001 ; m_rc | m_cs_sz | m_other | m_tag +mov QWORD PTR [rax], rcx ; one store mov QWORD PTR [rax+0x8], r14 mov QWORD PTR [rax+0x10], rbx ``` Measured by swapping `libleanshared.so` between two full builds, single-threaded with `-DElab.async=false` on pinned cores: `tests/elab_bench/big_omega.lean` goes from 18.946G to 18.803G user instructions (-0.754%) and `import Lean` from 1.9365G to 1.9219G (-0.753%), each reproducible to within 0.01%; cycles on the former fall about 1.2%. Heartbeat counts are unchanged. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Kha
force-pushed
the
heartbeat-minimal
branch
from
September 3, 2026 13:56
29fe74e to
f193bda
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR shortens the fused small-object allocation entry point from 18 to 14 instructions and gives constructor allocation a single merged header store, worth 0.75% of user instructions on the workloads measured below.
Three changes, none of which need a patch to mimalloc. The page refill moves into a cold helper that the entry points tail-jump to, so the fast path no longer builds a stack frame for a call it rarely makes; the helper also writes
m_cs_sz, which is what leavesszdead across the branch and keepslean_alloc_small_object_corea leaf as well. Restating the callers' precondition onsz(word-aligned, non-zero, at mostMI_SMALL_SIZE_MAX) folds mimalloc's bin-index rounding into a plain byte offset and drops the mask before the header store; the bound is a safety condition in its own right, since a largerszwould indexpages_free_directout of bounds. Finally, a second entry pointlean_alloc_small_object_rawleaves the whole header to the caller.The fast path of
lean_alloc_small_object_core:lean_alloc_small_object_rawis what letslean_alloc_ctorwrite all four header fields with adjacent stores that merge, rather than having the callee storem_cs_szand the caller fill in around it. Allocating aList.cons:Measured single-threaded with
-DElab.async=falseon pinned cores:tests/elab_bench/big_omega.leangoes from 18.946G to 18.803G user instructions (-0.754%) andimport Leanfrom 1.9365G to 1.9219G (-0.753%), each reproducible to within 0.01%; cycles on the former fall about 1.2%. Heartbeat counts are unchanged.Co-Authored-By: Claude Opus 5 (1M context) noreply@anthropic.com