Skip to content

perf: coalescing of RC ops within one basic block#13136

Merged
hargoniX merged 3 commits intomasterfrom
hbv/coalesce_rc
Mar 27, 2026
Merged

perf: coalescing of RC ops within one basic block#13136
hargoniX merged 3 commits intomasterfrom
hbv/coalesce_rc

Conversation

@hargoniX
Copy link
Copy Markdown
Contributor

@hargoniX hargoniX commented Mar 26, 2026

This PR introduces coalescing of RC operations to the RC optimizer. Whenever we perform multiple incs for a single value within one basic block it is legal to instead perform all of these incs at once at the first inc side. This is the case because the value will stay alive until at least the last inc and was thus never observable with RC=1. Hence, this change of inc location never destroys reuse opportunities.

@hargoniX
Copy link
Copy Markdown
Contributor Author

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Mar 26, 2026

Benchmark results for 5cd1000 against a8bbc95 are in. Significant changes detected! @hargoniX

  • build//instructions: -941.6M (-0.01%)

Large changes (2✅)

  • compiled/deriv//instructions: -72.6M (-0.95%)
  • size/libleanshared.so//bytes: -1MiB (-0.97%)

Medium changes (4✅)

  • compiled/rbmap//instructions: -8.0M (-0.08%)
  • size/Init/.olean//bytes: -391kiB (-0.43%)
  • size/all/.ir//bytes: -2MiB (-0.50%)
  • size/compile/.out//bytes: -9MiB (-0.53%)

Small changes (6✅, 1🟥)

  • 🟥 build/profile/compilation (LCNF impure)//wall-clock: +1s (+4.47%)
  • compiled/rbmap_checkpoint//instructions: -8.2M (-0.06%)
  • compiled/rbmap_checkpoint2//instructions: -7.0M (-0.07%)
  • compiled/rbmap_fbip//instructions: -7.5M (-0.10%)
  • size/all/.c//lines: -39.6k (-0.36%)
  • size/all/.olean//bytes: -838kiB (-0.26%)
  • size/install//bytes: -6MiB (-0.23%)

@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Mar 26, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing bot commented Mar 26, 2026

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a8bbc95d9fe665255a5c98fb402546233e760636 --onto e6df474dd9c3ad0e21771eaa808c53f66222216d. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-26 14:57:00)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 439c3c55448290dd0b0b4b205afde4229a7cee4d --onto 4786e082dca22873d14d2a5b9b7c8843380c6e78. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-27 10:50:51)

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Mar 26, 2026

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase a8bbc95d9fe665255a5c98fb402546233e760636 --onto cfa8c5a036d6990635c6ec50b02d0e806995cec3. You can force reference manual CI using the force-manual-ci label. (2026-03-26 14:57:03)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 439c3c55448290dd0b0b4b205afde4229a7cee4d --onto cfa8c5a036d6990635c6ec50b02d0e806995cec3. You can force reference manual CI using the force-manual-ci label. (2026-03-27 10:50:52)

@hargoniX hargoniX added the changelog-compiler Compiler, runtime, and FFI label Mar 27, 2026
@hargoniX hargoniX marked this pull request as ready for review March 27, 2026 10:02
@hargoniX hargoniX requested a review from leodemoura as a code owner March 27, 2026 10:02
@hargoniX hargoniX enabled auto-merge March 27, 2026 10:02
@hargoniX hargoniX added this pull request to the merge queue Mar 27, 2026
Merged via the queue into master with commit c71a0ea Mar 27, 2026
26 checks passed
@hargoniX hargoniX deleted the hbv/coalesce_rc branch March 27, 2026 10:47
volodeyka pushed a commit that referenced this pull request Apr 16, 2026
This PR introduces coalescing of RC operations to the RC optimizer.
Whenever we perform multiple `inc`s for a single value within one basic
block it is legal to instead perform all of these `inc`s at once at the
first `inc` side. This is the case because the value will stay alive
until at least the last `inc` and was thus never observable with `RC=1`.
Hence, this change of `inc` location never destroys reuse opportunities.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-compiler Compiler, runtime, and FFI toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants