wip: inline mimalloc's small-alloc fast path (measurement patch, not for merge) This replicates mimalloc's small-allocation fast path inside `lean_alloc_small_object` so that the call, the frame, the argument shuffle and the size rounding (which `lean_alloc_small_object` has already done) all fold away, and the size-class index collapses to a constant displacement. Per-allocation codegen was checked against `mi_malloc_small`'s body instruction for instruction. On `simp_local`, 8 interleaved rounds, with the heartbeat increment already inlined on both sides so this isolates the allocator: instructions -2.88% (t=-225), cycles -1.34% (t=-5.9), task-clock -1.20% (t=-5.5). Elab tests pass 3097/3097 and compile tests 123/124, the one failure being the pre-existing `precompileLink` Lake test. Reading mimalloc's `__mi_theap_default` directly measures a little better, -3.25% instructions, but does not link: that symbol is `mi_decl_hidden`, so it resolves for objects linked into `libleanshared` and not for binaries linking against it, and `bin/leanc` fails with undefined references, which stops any benchmark needing `leanc` from running. The theap is therefore obtained through `mi_theap_get_default()`, which is public API, and cached in a thread-local Lean owns. Getting the cached form to perform took three steps worth recording, since the first two cost more than they looked like they would: - Writing the cache from the inline fast path kept the thread-pointer address live across the slow-path call and pushed callers from two callee-saved spills to four, which ate the entire cycle win. The refresh moved into an out-of-line `lean_mi_malloc_small_slow`. - A null check on the cache cost about 0.6 percentage points of instructions. It cannot simply be dropped: `lean_initialize_thread` has exactly one caller in the tree, `thread_main` for `lthread`-created threads, so the main thread and any FFI or libuv thread never run it and would dereference zero. - Instead the thread-local starts out pointing at a stand-in theap whose every size class resolves to a page with an empty free list, so the existing `block == NULL` test catches the uninitialised case and sends it down the slow path, which installs the real theap. Being a constant initialiser this needs no hook and covers every thread. What makes this unshippable is the layout knowledge: the offsets are read off the vendored mimalloc build (`pages_free_direct` at 0x118 indexed by byte size, `page->free` at 0x8, `page->used` uint16 at 0x10) and hold only because this build sets MI_SECURE=0 and MI_PADDING=0. `mi_theap_t` is opaque in mimalloc's public header and that header has no inline definitions, so the pop cannot be expressed through supported API. Public API covers obtaining the theap (`mi_theap_get_default`) and passing it in (`mi_theap_malloc_small`), just not the fast path itself. The real routes are ThinLTO, post-link inlining with BOLT, or an upstream mimalloc change moving the already-`mi_decl_forceinline` fast path out of `alloc.c` into a header. Worth pursuing independently of any inlining: `lean_alloc_small_object` aligns the size to 8 and `mi_malloc_small` then aligns it to 8 again, about 0.7% of runtime spent on nothing, and no public entry point takes a pre-rounded size. `moreLeancArgs` carries `-DLEAN_MI_INLINE_FASTPATH` to enable the path and `-DLEAN_MI_REV` purely to invalidate Lake's stdlib traces, which do not cover the include tree and would otherwise silently reuse objects compiled against an older `lean.h`. Co-Authored-By: Claude <noreply@anthropic.com>
This is the repository for Lean 4.
See Install Lean.
Please read our Contribution Guidelines first.
See Building Lean.