Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

perf: faster Nat.repr implementation in C #3876

Merged
merged 6 commits into from
Apr 17, 2024
Merged

Conversation

nomeata
Copy link
Collaborator

@nomeata nomeata commented Apr 10, 2024

Nat.repr was implemented by generating a list of Chars, each created by a 10-way if-then-else. This can cause significant slow down in some particular use cases.

Now Nat.repr is implemented_by a faster implementation that uses C++’s std::to_string on small numbers (< USize.size) and maintains an array of pre-allocated strings for the first 128 numbers.

The handling of big numbers (≥ USize.size) remains as before.

@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc April 10, 2024 21:55 Inactive
@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 Apr 10, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Apr 10, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Apr 10, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Apr 10, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

leanprover-community-mathlib4-bot commented Apr 10, 2024

Mathlib CI status (docs):

@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc April 10, 2024 22:26 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Apr 10, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Apr 10, 2024
@nomeata
Copy link
Collaborator Author

nomeata commented Apr 11, 2024

!bench

@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc April 11, 2024 05:57 Inactive
@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 76c6249.
There were no significant changes against commit 892bfe2.

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Apr 11, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Apr 11, 2024
src/Init/Data/Repr.lean Outdated Show resolved Hide resolved
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Apr 11, 2024
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc April 11, 2024 07:18 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Apr 11, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Apr 11, 2024
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc April 11, 2024 14:08 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Apr 11, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Apr 11, 2024
@nomeata
Copy link
Collaborator Author

nomeata commented Apr 11, 2024

!bench

1 similar comment
@nomeata
Copy link
Collaborator Author

nomeata commented Apr 11, 2024

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 99cbe00.
There were significant changes against commit 892bfe2:

  Benchmark                  Metric         Change
  ============================================================
- tests/bench/ interpreted   instructions    80.9% (19859.8 σ)
- tests/bench/ interpreted   task-clock      35.0%    (27.2 σ)
- tests/bench/ interpreted   wall-clock      56.3%    (30.7 σ)

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Apr 11, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Apr 11, 2024
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc April 11, 2024 22:08 Inactive
@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 3e32e35.
There were significant changes against commit 892bfe2:

  Benchmark                  Metric             Change
  ===============================================================
+ stdlib                     tactic execution    -3.5%  (-37.5 σ)
+ stdlib                     type checking       -1.9%  (-31.0 σ)
- tests/bench/ interpreted   instructions        62.4% (1872.7 σ)
- tests/bench/ interpreted   task-clock          26.9%   (20.1 σ)
- tests/bench/ interpreted   wall-clock          43.8%   (37.3 σ)

@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc April 12, 2024 15:36 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Apr 12, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Apr 12, 2024
@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 57cf9ae.
The entire run failed.
Found no significant differences.

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 32adde5.Found no runs to compare against.

@nomeata nomeata force-pushed the joachim/nat.toString branch from ffec048 to ed05fb0 Compare April 12, 2024 19:23
@nomeata
Copy link
Collaborator Author

nomeata commented Apr 12, 2024

!bench

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Apr 12, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Apr 12, 2024
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc April 12, 2024 19:45 Inactive
@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit ed05fb0.
There were significant changes against commit b0183a6:

  Benchmark                  Metric          Change
  ==============================================================
+ nat_repr                   branch-misses    -8.3%    (-10.2 σ)
+ nat_repr                   branches        -69.7% (-81916.4 σ)
+ nat_repr                   instructions    -70.8% (-70325.4 σ)
+ nat_repr                   task-clock      -63.8%    (-62.5 σ)
+ nat_repr                   wall-clock      -63.8%    (-62.3 σ)
+ stdlib                     task-clock       -1.1%    (-22.0 σ)
+ tests/bench/ interpreted   instructions     -3.7%  (-2746.6 σ)

@nomeata nomeata added the awaiting-review Waiting for someone to review the PR label Apr 12, 2024
@nomeata nomeata marked this pull request as ready for review April 12, 2024 21:28
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc April 12, 2024 21:43 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Apr 12, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Apr 12, 2024
@nomeata nomeata changed the base branch from joachim/nat_repr_bench to master April 12, 2024 22:11
@nomeata
Copy link
Collaborator Author

nomeata commented Apr 12, 2024

@nomeata nomeata requested a review from hargoniX April 17, 2024 08:26
Copy link
Contributor

@hargoniX hargoniX left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM, the only thing I'm wondering about is the stddev on our metrics for the nat_repr benchmark, how reliable are they?

@nomeata
Copy link
Collaborator Author

nomeata commented Apr 17, 2024

Don't know. Is that something we should look at now, or when it seems to become a problem?

@hargoniX
Copy link
Contributor

The latter I think, it would only be an issue if we end up improving this even more.

@nomeata nomeata removed the awaiting-review Waiting for someone to review the PR label Apr 17, 2024
@nomeata nomeata added this pull request to the merge queue Apr 17, 2024
Merged via the queue into master with commit 5043368 Apr 17, 2024
14 of 20 checks passed
@nomeata nomeata deleted the joachim/nat.toString branch October 22, 2024 12:39
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
builds-mathlib CI has verified that Mathlib builds against this PR 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.

6 participants