Skip to content

feat: expire idle task pool threads after 5 seconds#13123

Draft
Kha wants to merge 1 commit intoleanprover:masterfrom
Kha:push-mvkzsumxnyrv
Draft

feat: expire idle task pool threads after 5 seconds#13123
Kha wants to merge 1 commit intoleanprover:masterfrom
Kha:push-mvkzsumxnyrv

Conversation

@Kha
Copy link
Member

@Kha Kha commented Mar 25, 2026

This PR makes the task thread pool reclaim idle worker threads after 5 seconds of inactivity. Previously, pool threads were allocated on demand but never freed, which could waste significant memory given the new default 1GB stack size per thread.

Worker threads are now detached immediately after creation instead of being stored in a vector. Each idle thread uses a timed wait and exits if no work arrives within the timeout. The destructor waits on a counter instead of joining stored threads.

This PR makes the task thread pool reclaim idle worker threads after 5
seconds of inactivity. Previously, pool threads were allocated on demand
but never freed, which wastes significant memory given the default 1GB
stack size per thread.

Worker threads are now detached immediately after creation instead of
being stored in a vector. Each idle thread uses a timed wait and exits
if no work arrives within the timeout. The destructor waits on a counter
instead of joining stored threads.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
@Kha
Copy link
Member Author

Kha commented Mar 25, 2026

!bench

@leanprover-radar
Copy link

leanprover-radar commented Mar 25, 2026

Benchmark results for d567797 against 6f98a76 are in. Significant changes detected! @Kha

  • 🟥 build//instructions: +38.6G (+0.31%)

Large changes (2🟥)

  • 🟥 compiled/channel//wall-clock: +3s (+117.07%)
  • 🟥 misc/re-elab Init.Data.List.Basic//task-clock: +2s (+13.89%)

Medium changes (1✅, 7🟥)

  • 🟥 build/module/Std.Data.DTreeMap.Internal.Lemmas//instructions: +1.5G (+0.69%)
  • 🟥 compiled/channel//task-clock: +8s (+83.08%)
  • interpreted/identifier_completion//instructions: -1.2G (-1.63%)
  • 🟥 lake/inundation/build no-op//instructions: +245.5M (+4.24%)
  • 🟥 misc/import Init.Data.List.Sublist//instructions: +129.6M (+1.10%)
  • 🟥 misc/import Init.Prelude//instructions: +223.4M (+1.82%)
  • 🟥 misc/import Std.Data.Internal.List.Associative//instructions: +868.8M (+1.10%)
  • 🟥 misc/re-elab Init.Data.List.Basic//instructions: +6.1G (+3.89%)

Small changes (1✅, 301🟥)

Too many entries to display here. View the full report on radar instead.

@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 25, 2026
@mathlib-lean-pr-testing
Copy link

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 6f98a76d01470ff9aa1d0895cfd2827eaa24ec89 --onto e6df474dd9c3ad0e21771eaa808c53f66222216d. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-25 19:02:43)

@leanprover-bot
Copy link
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 6f98a76d01470ff9aa1d0895cfd2827eaa24ec89 --onto cfa8c5a036d6990635c6ec50b02d0e806995cec3. You can force reference manual CI using the force-manual-ci label. (2026-03-25 19:02:45)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

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