)]}'
{
  "commit": "cc86abf80a932bfd85082583c10f0768c9925ef8",
  "tree": "053816c8d275ffb976f96dd043bc3b1ff951354d",
  "parents": [
    "137a88d9d363d6f0c60de75d4cef02a26f38962e"
  ],
  "author": {
    "name": "Sebastian Ullrich",
    "email": "sebasti@nullri.ch",
    "time": "Tue Sep 01 08:16:56 2026 +0000"
  },
  "committer": {
    "name": "Sebastian Ullrich",
    "email": "sebasti@nullri.ch",
    "time": "Thu Sep 03 16:24:51 2026 +0000"
  },
  "message": "perf: make the small-object allocation fast path a leaf\n\nThis PR shortens `lean_alloc_small_object_core` from 18 to 14 instructions by keeping mimalloc\u0027s generic allocation path out of line, so that the fast path needs no stack frame.\n\nThe entry point now tests `page-\u003efree` itself and tail-jumps to a cold helper on a miss, instead of calling `mi_theap_malloc_small` and checking its result. Only the generic routine can fail, so both the OOM check and the `m_cs_sz` store move to that helper; leaving either at the call site would make the cold call one that has to return, and the fast path would pay a prologue and epilogue on every allocation to serve a path it almost never takes. Restating the callers\u0027 precondition on `sz` (word-aligned, non-zero, at most `MI_SMALL_SIZE_MAX`) additionally folds mimalloc\u0027s bin-index rounding into a plain byte offset and lets the header store drop its mask. That bound is a safety condition in its own right, as a larger `sz` would index `pages_free_direct` out of bounds, so it is also asserted.\n\n```diff\n-push   rbx                            ; frame, only for the generic call below\n mov    rax, [rip+...]                 ; \u0026lean_g_tls\n inc    QWORD PTR fs:[rax]             ; heartbeat++\n mov    rcx, QWORD PTR fs:[rax+0x8]    ; theap\n mov    esi, edi\n-lea    rax, [rsi+0x7]                 ; round sz up to a bin index\n-and    rax, 0xfffffffffffffff8\n-mov    rdx, [rcx+rax*1+0x120]         ; theap-\u003epages_free_direct[..]\n+mov    rdx, [rcx+rsi*1+0x120]         ; sz is the byte offset already\n mov    rax, [rdx+0x8]                 ; page-\u003efree\n test   rax, rax\n-je     .Lcold                         ; inline generic path, ending in pop rbx; ret\n+je     lean_alloc_small_generic_core  ; tail jump, nothing to tear down\n mov    rcx, [rax]                     ; pop the block\n mov    [rdx+0x8], rcx\n inc    WORD PTR [rdx+0x10]            ; page-\u003eused++\n mov    QWORD PTR [rax], 0x0           ; mimalloc\u0027s free-list scrub\n-mov    WORD PTR [rax+0x4], di         ; m_cs_sz, masked to 16 bits\n-pop    rbx\n+mov    DWORD PTR [rax+0x4], edi       ; m_cs_sz, no mask needed\n ret\n```\n\nMeasured by swapping `libleanshared.so` between two full builds, single-threaded with `-DElab.async\u003dfalse` on pinned cores: `tests/elab_bench/big_omega.lean` goes from 18.781G to 18.650G user instructions (-0.694%) and `import Lean` from 1.9356G to 1.9215G (-0.729%), each reproducible to within 0.02%.\n\nLLVM\u0027s hot-cold splitting does not do this: with `-mllvm -hot-cold-split\u003dtrue` the pass fires 27 times elsewhere in the translation unit and leaves this function byte-identical, because it outlines a cold region into a function the original still calls and returns from, which does not remove the frame.\n\nCo-Authored-By: Claude Opus 5 \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "8a0e614c85c40cad1067a99ba3ef51e8b1f35372",
      "old_mode": 33188,
      "old_path": "src/include/lean/lean.h",
      "new_id": "3dc2341b716ab29f9bf01d07497a8ffdda74ccc3",
      "new_mode": 33188,
      "new_path": "src/include/lean/lean.h"
    },
    {
      "type": "modify",
      "old_id": "9a4d944d71115ef0c58e3227081338261369e286",
      "old_mode": 33188,
      "old_path": "src/runtime/mimalloc.cpp",
      "new_id": "1f3e69de7e644c74fedb588c2c6cdb2e8fdfac45",
      "new_mode": 33188,
      "new_path": "src/runtime/mimalloc.cpp"
    }
  ]
}