Skip to content

perf: Don't hash the key when searching in empty hash tables#2471

Closed
hargoniX wants to merge 1 commit into
leanprover:masterfrom
hargoniX:empty-hash
Closed

perf: Don't hash the key when searching in empty hash tables#2471
hargoniX wants to merge 1 commit into
leanprover:masterfrom
hargoniX:empty-hash

Conversation

@hargoniX

@hargoniX hargoniX commented Aug 28, 2023

Copy link
Copy Markdown
Contributor

Based on: rust-lang/hashbrown#305

Judging from the rustc benchmarks this can save significant amounts of instructions and seems like quite a simple change. It is however unclear to me whether we do have the usage pattern of HashMaps that they do somewhere so it might possibly be useless for us as well. I don't have a local benchmark setup so we have to run performance tests here if we are interested in this. I'm guessing I don't have the privileges for that?

@kim-em

kim-em commented Aug 29, 2023

Copy link
Copy Markdown
Collaborator

@hargoniX, I think anyone is allowed to run

!bench

@kim-em

kim-em commented Aug 29, 2023

Copy link
Copy Markdown
Collaborator

Apparently not! @Kha, I'm presuming you need to sprinkle some magic permissions bits here?

kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request Aug 30, 2023
@leodemoura

Copy link
Copy Markdown
Member

!bench

@leanprover-bot

Copy link
Copy Markdown
Collaborator

Here are the benchmark results for commit 1262a41.
There were no significant changes against commit a7efe5b.

@kim-em kim-em added successful-mathlib-build builds-mathlib CI has verified that Mathlib builds against this PR and removed successful-mathlib-build labels Aug 31, 2023
@kim-em

kim-em commented Aug 31, 2023

Copy link
Copy Markdown
Collaborator
  • ✅ Mathlib branch lean-pr-testing-2471 has successfully built against this PR. (2023-08-31 05:34:45)

@kim-em

kim-em commented Aug 31, 2023

Copy link
Copy Markdown
Collaborator
  • ✅ Mathlib branch lean-pr-testing-2471 has successfully built against this PR. (2023-08-31 06:09:35)

@kim-em

kim-em commented Aug 31, 2023

Copy link
Copy Markdown
Collaborator

Here are the bench results on Mathlib: http://speed.lean-fro.org/mathlib4/compare/93695581-e592-41ad-9a6a-53fe2cce9e75/to/e760a006-736d-49ba-b9b4-d6d79e4f697f.

I think without any interesting performance gain we can put this one to rest?

@hargoniX

Copy link
Copy Markdown
Contributor Author

@digama0 would you like to have this optimization on the std4 HashMap?

@hargoniX hargoniX closed this Aug 31, 2023
@digama0

digama0 commented Aug 31, 2023

Copy link
Copy Markdown
Collaborator

I was planning on it if this landed, but if the performance impact isn't there I'm not sure. The results seem to be slightly negative.

@kim-em kim-em added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan builds-mathlib CI has verified that Mathlib builds against this PR and removed builds-mathlib CI has verified that Mathlib builds against this PR breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Aug 31, 2023
@kim-em

kim-em commented Aug 31, 2023

Copy link
Copy Markdown
Collaborator
  • ✅ Mathlib branch lean-pr-testing-2471 has successfully built against this PR. (2023-08-31 10:59:42)

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

Projects

None yet

Development

Successfully merging this pull request may close these issues.

5 participants