-
Notifications
You must be signed in to change notification settings - Fork 447
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
Conversation
Mathlib CI status (docs):
|
!bench |
Here are the benchmark results for commit 76c6249. |
!bench |
1 similar comment
!bench |
Here are the benchmark results for commit 99cbe00. 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 σ) |
Here are the benchmark results for commit 3e32e35. 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 σ) |
Here are the benchmark results for commit 57cf9ae. |
Here are the benchmark results for commit 32adde5.Found no runs to compare against. |
ffec048
to
ed05fb0
Compare
!bench |
Here are the benchmark results for commit ed05fb0. 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 σ) |
There was a problem hiding this 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?
Don't know. Is that something we should look at now, or when it seems to become a problem? |
The latter I think, it would only be an issue if we end up improving this even more. |
Nat.repr
was implemented by generating a list ofChars
, each created by a 10-way if-then-else. This can cause significant slow down in some particular use cases.Now
Nat.repr
isimplemented_by
a faster implementation that uses C++’sstd::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.