)]}'
{
  "commit": "f200b075e03d4c45ab22fc6625330fffb3e2b1c3",
  "tree": "8952a76d929b7ade767af002dce34d5f2f166aad",
  "parents": [
    "2dbc71d2eb0366cb653a2910f39c64eed724e87c"
  ],
  "author": {
    "name": "Sebastian Ullrich",
    "email": "sebasti@nullri.ch",
    "time": "Mon Aug 03 15:52:21 2026 +0000"
  },
  "committer": {
    "name": "Sebastian Ullrich",
    "email": "sebasti@nullri.ch",
    "time": "Mon Aug 03 20:30:00 2026 +0000"
  },
  "message": "wip: inline mimalloc\u0027s small-alloc fast path (measurement patch, not for merge)\n\nThis replicates mimalloc\u0027s 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`\u0027s body instruction for instruction.\n\nOn `simp_local`, 8 interleaved rounds, with the heartbeat increment already inlined on both sides so this isolates the allocator: instructions -2.88% (t\u003d-225), cycles -1.34% (t\u003d-5.9), task-clock -1.20% (t\u003d-5.5). Elab tests pass 3097/3097 and compile tests 123/124, the one failure being the pre-existing `precompileLink` Lake test.\n\nReading mimalloc\u0027s `__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.\n\nGetting the cached form to perform took three steps worth recording, since the first two cost more than they looked like they would:\n\n- 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`.\n- 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.\n- 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 \u003d\u003d 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.\n\nWhat 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-\u003efree` at 0x8, `page-\u003eused` uint16 at 0x10) and hold only because this build sets MI_SECURE\u003d0 and MI_PADDING\u003d0. `mi_theap_t` is opaque in mimalloc\u0027s 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.\n\nWorth 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.\n\n`moreLeancArgs` carries `-DLEAN_MI_INLINE_FASTPATH` to enable the path and `-DLEAN_MI_REV` purely to invalidate Lake\u0027s stdlib traces, which do not cover the include tree and would otherwise silently reuse objects compiled against an older `lean.h`.\n\nCo-Authored-By: Claude \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "3f57fa7b2ee74e2e8902fa3b65f4cfdb4d7c630f",
      "old_mode": 33188,
      "old_path": "src/include/lean/lean.h",
      "new_id": "8b1a3c41d2b7d70aa805bf8a579709ce7a5bc06e",
      "new_mode": 33188,
      "new_path": "src/include/lean/lean.h"
    },
    {
      "type": "modify",
      "old_id": "59ec466d40d56731370c12eed45f85d0bae33abc",
      "old_mode": 33188,
      "old_path": "src/lakefile.toml.in",
      "new_id": "0112c33b75b619117f484a9925ee1916583b0f60",
      "new_mode": 33188,
      "new_path": "src/lakefile.toml.in"
    },
    {
      "type": "modify",
      "old_id": "23e882896c360910d83a6b552360d93047762f82",
      "old_mode": 33188,
      "old_path": "src/runtime/alloc.cpp",
      "new_id": "8ef20eec4381286ae87fc87d3a4298d321c002ba",
      "new_mode": 33188,
      "new_path": "src/runtime/alloc.cpp"
    }
  ]
}