Skip to content

Conversation

AlexanderPortland
Copy link
Contributor

I’ve noticed that Kani will often repeatedly codegen elements that are similar or exactly the same (sometimes as many as ~500 times) while compiling a crate. The two biggest offenders being codegen-ing rustc_public::Tys into cbmc::Types and turning rustc_public::Spans into cbmc::Locations.

This PR introduces an extensible system for caching portions of Kani’s codegen, using it to speed up both cases mentioned above.

Results

Testing on the standard library shows this cache maintains a >98% cache hit rate, reducing end-to-end compile times by 20%, all while only taking up only ~8MB of memory at peak size (<1% of Kani’s total average use).

Other Ideas

I also tried to cache how we codegen Rvalues and FnAbis, but both failed. The former was far too dependent on the current state of the program, and I think the latter is already cached by the compiler’s query system, so my cache only made it slower when we had to actually query the compiler.

That being said, I’m sure there are more opportunities for caching in our codegen, so I designed the system from the start to try to make it easy to extend the cache with more kinds of elements.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

@AlexanderPortland AlexanderPortland requested a review from a team as a code owner August 21, 2025 19:40
@github-actions github-actions bot added Z-EndToEndBenchCI Tag a PR to run benchmark CI Z-CompilerBenchCI Tag a PR to run benchmark CI labels Aug 21, 2025
@tautschnig
Copy link
Member

Generally looks good to me, but could you please got the extra mile and add a regression test that will measure the caching efficacy (producing basically the numbers that you put in the PR description, but perhaps for some different code base - maybe even Kani itself?). Just like you added end-to-end compile-time measurements it would be good to have caching numbers so that we know when some other, seemingly unrelated, change completely breaks caching.

@AlexanderPortland
Copy link
Contributor Author

AlexanderPortland commented Aug 22, 2025

Hey @tautschnig, would this be best as a CI job (similar to the compiler timing one) or a regression test with a certain cache hit rate hard coded to detect any regression past that? Today's my last day so just trying to plan out what's feasible in the time frame--CI jobs can be very slow to test in my experience. [for my own memory he said a CI job would be best if possible haha]

github-merge-queue bot pushed a commit that referenced this pull request Sep 8, 2025
This PR is a pair of small performance changes. It used to be 4 (and
thus would've been a real combo), but two involved caching so I've moved
them under #4313 instead. These changes include:
1. passing information commonly used by our `GotocHook`s' `hook_applies`
method as arguments, so that each hook doesn't have to recompute it on
it's own
2. a small one-line change to compute a fn instance's name once instead
of twice.

These are both very small, but together with the other two changes now
moved to #4313, made a ~6% decrease in the compile time of the standard
library.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Felipe R. Monteiro <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Z-CompilerBenchCI Tag a PR to run benchmark CI Z-EndToEndBenchCI Tag a PR to run benchmark CI
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants