chore: update to mimalloc 3.5.0 - #14866
Draft
Kha wants to merge 3 commits into
Draft
Conversation
Member
Author
|
!bench |
|
Benchmark results for 03fb0d9 against 16e77c4 are in. There are significant results. @Kha
Large changes (14✅, 2🟥)
Medium changes (2✅, 5🟥)
Small changes (13✅, 5🟥)
|
github-actions
Bot
added
toolchain-available
leanprover-bot
added
the
builds-manual
Collaborator
|
Reference manual CI status:
|
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@cd03010 against leanprover-community/mathlib4-nightly-testing@5a95bed are in. There are significant results. @Kha
Large changes (1🟥)
Small changes (2✅)
|
mimalloc 3.5.0's `e927d7b0` ("optimize page layout for malloc/free") splits `page->used++` and `--page->used` into a separate load, arithmetic and store, and hoists the load above the free-list null test. The restructuring exists to induce an `ldp` on aarch64 (the commit says so, and pairs it with an `__asm` barrier that `7c66c3f4` later widened to every GNU compiler). On x86-64 it produces no paired load and simply costs two instructions in each of `mi_malloc_small` and `mi_free`: `incw`/`incq` becomes `mov`/`inc`/`mov`.
This patch restores the single read-modify-write everywhere except aarch64, keeping the page-map flattening, the page struct reordering and the `mi_used_t = size_t` widening that the same mimalloc release brought. `mi_malloc_small` goes back to 14 instructions and `mi_free` to 18, three below 3.4.4.
Measured locally against the vendored 3.4.4 and 3.5.0, relinking only `libleanshared.so` (AMD EPYC 9455, `perf stat`, all variants rebuilt adjacently and alternated within each block):
* `compiled/unionfind` instructions -2.19% against 3.4.4 and -2.71% against 3.5.0, so the +0.54% this PR currently costs becomes a 2.2% gain
* `compiled/rbmap_fbip` -4.70% / -3.34%, `compiled/deriv` -2.21% / -1.82%
* retired macro-ops move the same way, and cycles improve 4.4-5.2% against 3.5.0 on `unionfind`
This does not address the separate `compiled/deriv` wall-clock regression, which is a locality effect of the arena and page-map redesign.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
mimalloc 3.5.0 doubled `MI_MAX_EXTEND_SIZE` from 4 KiB to 8 KiB in `932f6e5d`, a commit otherwise about guarding thread-locals against use after they are freed. Extending a page's free list in larger chunks halves the number of `_mi_malloc_generic` refills, which is why it shows up as *fewer* instructions, but it spreads each refill's writes over twice as much memory and costs `compiled/deriv` a tenth of its runtime. Bisecting the 149 first-parent commits between the two mimalloc tags on `compiled/deriv` cycles lands on `932f6e5d` (+9.45% against 3.4.4, parent +0.70%), and reverting this one constant on top of 3.5.0 takes it from +11.58% back to +0.47%. Instruction counts cannot see any of this: the same commit *reduces* `compiled/unionfind` instructions by 25M. With both mimalloc patches applied, against the vendored 3.4.4 (AMD EPYC 9455, min-of-6 interleaved, all variants rebuilt adjacently): * `compiled/deriv` cycles +10.78% -> -0.24%, instructions -0.39% -> -1.65% * `compiled/unionfind` cycles +1.82% -> -0.25%, instructions +0.53% -> -2.07% * `compiled/rbmap_fbip` cycles -1.05% -> +0.22%, instructions -1.40% -> -3.15% `rbmap_fbip` is the one give-back: it has 16x `unionfind`'s page churn and was the main beneficiary of the larger extend size. If radar disagrees on the trade-off across the wider suite, this commit can be dropped on its own. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Member
Author
|
!bench |
|
Benchmark results for 80d0b29 against f8facdb are in. There are significant results. @Kha
Large changes (19✅, 1🟥)
Medium changes (20✅)
Small changes (1327✅, 3🟥)
|
Member
Author
|
!bench |
|
Benchmark results for 66f7f14 against f8facdb are in. There are significant results. @Kha
Large changes (18✅, 1🟥)
Medium changes (17✅)
Small changes (1089✅, 1🟥)
|
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.
No description provided.