kani icon indicating copy to clipboard operation
kani copied to clipboard

Add heuristic to order harness codegen

Open AlexanderPortland opened this issue 5 months ago • 2 comments

Motivation

When compiling with more than a single thread (as in #4236), the order in which we codegen harnesses can have a non-negligable impact on performance. Specifically, if we handle harness that will generate a lot of code near the end of compilation, the main compiler thread can get stuck waiting for worker threads to export that code, slowing down overall compilation. If we could ensure that more difficult to export harnesses are handled first, the thread pool will have more time to write them to disk off the critical path of compilation.

Approach

This PR switches reachability analysis for all harnesses to happen before codegen. It can then use the information we gather from reachability to reorder codegen based on the total number of items reachable from each harness (MostReachableItems).

This heuristic was chosen because it is:

  • simple -- only requiring a single field access for each harness, and taking only ~10µs to fully sort a typical CodegenUnit of 66 harnesses (acceptable given it took ~20ms to codegen the fastest harnesses in that same CodegenUnit)
  • seemingly effective -- on the s2n-codec benchmark it only ever places a slower-to-export harness after a faster one if their actual export times were within 10ms (or 7%). Since the goal is just to roughly order harnesses based on order of magnitude, this is a very good result 🎉

Results

This change made a small, but not insignificant 2.9% reduction in the end to end compile time of the standard library (@ commit 177d0fd).

And below is a recreation of the graph of the compiler's per-thread CPU usage from #4248 now that codegen is ordered. Screenshot 2025-07-31 at 12 16 24 PM

While functionally complete on its own, this change will not really make a performance impact until #4236 is merged.

Resolves #4248

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

AlexanderPortland avatar Jul 31 '25 19:07 AlexanderPortland

Let's get #4236 merged first so that this PR can get concrete data points in its PR description.

tautschnig avatar Aug 01 '25 11:08 tautschnig

#4236 has now been merged, so this one should be ready to be acted upon.

tautschnig avatar Aug 04 '25 10:08 tautschnig