Add a unified codegen cache - #4313
Conversation
github-actions
Bot
added
Z-EndToEndBenchCI
|
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. |
|
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] |
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 <felisous@amazon.com>
@AlexanderPortland Please let us know whether you think you could still find the time to do this. Thanks! |
|
Hey @tautschnig! Sorry for the delay, classwork is picking up and I just got sick lol. I did the fxhash change and I'll likely have a free day to sit down and do the CI job too as long as you're okay to wait another few weeks (but I can't make any promises). If it's time critical to have this land, feel free to merge as is! |
There was a problem hiding this comment.
Pull request overview
This PR introduces a unified, extensible codegen cache for Kani’s CProver/GOTO-C backend to avoid repeatedly regenerating identical or equivalent codegen artifacts (notably Ty→Type and Span→Location), improving overall compilation performance.
Changes:
- Add a thread-local unified cache API (
cache_entry,CacheEntry) with two implementations (stats in debug builds, lean in release builds). - Integrate caching into
codegen_ty_stableandcodegen_span_stable, and clear per-harness cache state in the codegen backend. - Add supporting helpers to reduce repeated work (interned readable function name;
Location::try_set_functionmutator).
Reviewed changes
Copilot reviewed 10 out of 10 changed files in this pull request and generated 5 comments.
Show a summary per file
| File | Description |
|---|---|
| kani-compiler/src/codegen_cprover_gotoc/mod.rs | Re-export clear_codegen_cache for backend use. |
| kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs | Add interned readable name + instance name caching helper for codegen reuse. |
| kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs | Clear codegen cache between harnesses during backend execution. |
| kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs | Cache stable type codegen (Ty→cbmc::Type). |
| kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs | Cache span codegen (Span→cbmc::Location) and adjust function attribution. |
| kani-compiler/src/codegen_cprover_gotoc/codegen/mod.rs | Expose the new cache module to codegen. |
| kani-compiler/src/codegen_cprover_gotoc/codegen/cache/mod.rs | Define unified cache API, traits, thread-local storage, and clear granularity. |
| kani-compiler/src/codegen_cprover_gotoc/codegen/cache/impl_stats.rs | Debug implementation that records cache hit/miss timings and prints stats. |
| kani-compiler/src/codegen_cprover_gotoc/codegen/cache/impl_no_stats.rs | Release implementation with minimal overhead. |
| cprover_bindings/src/goto_program/location.rs | Add try_set_function helper to mutate Location::Loc function field. |
Comments suppressed due to low confidence (1)
kani-compiler/src/codegen_cprover_gotoc/codegen/cache/mod.rs:72
- Doc comment typo: "The the" should be "The type".
/// The the of the value that this cache entry holds.
type EntryVal: CodegenCacheVal;
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| /// Returns the (`name`, `mangled_name`) pair for an [Instance] from the cache, computing it if no entry exists. | ||
| fn instance_names(instance: &Instance) -> (String, String) { | ||
| INSTANCE_NAME_CACHE.with_borrow_mut(|cache| { | ||
| cache.entry(*instance).or_insert_with(|| (instance.name(), instance.mangled_name())).clone() | ||
| }) |
| cache_entry::<Location>(sp) | ||
| .tweak(|res| { | ||
| res.try_set_function(self.current_fn.as_ref().map(|x| x.interned_readable_name())) | ||
| .unwrap(); | ||
| }) | ||
| .or_insert_with(|| self.codegen_span_stable_inner(sp)) |
| pub fn try_set_function(&mut self, new_function: Option<InternedString>) -> Option<()> { | ||
| if let Location::Loc { function, .. } = self { | ||
| if let Some(new_function) = new_function { | ||
| *function = Some(new_function); | ||
| } | ||
|
|
||
| Some(()) | ||
| } else { | ||
| None | ||
| } | ||
| } |
| fn avg_duration(durations: &[Duration]) -> Duration { | ||
| let len = durations.len() as u32; | ||
| let sum: Duration = durations.iter().sum(); | ||
| sum / len | ||
| } |
| /// The thread-local codegen cache. Since currently codegen is constrainted to be done | ||
| /// in a single thread (since the compiler's [TyCtxt](rustc_middle::ty::TyCtxt) isn't `Send`), | ||
| /// we only ever need the cache in that one thread. | ||
| pub static CACHE: RefCell<CodegenCache> = RefCell::new(Default::default()); |
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 intocbmc::Types and turningrustc_public::Spans intocbmc::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 andFnAbis, 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.