Introduce thread pool for writing goto binaries in parallel

[AlexanderPortland]

Serializing and writing goto binaries is a serious bottleneck for the Kani compiler, with profiling indicating that it takes around half of the total codegen time.

This PR introduces a variable size thread pool specifically for serializing goto binaries and writing them to disk. Now, instead of having to do everything itself, the main compiler thread just has collect all the data needed for serialization (requiring relatively inexpensive clones of some local state) and dispatch it to the thread pool's work queue. This allows the main thread to move on quickly while the pool's worker threads handle generating the binaries off of the critical path of compilation.

Results

The table below shows wall clock end-to-end compile times before and after this change. This metric corresponds to how long a user would have to wait for Kani's compilation to finish before verification can begin.

benchmark	compile time before	compile time now	change
standard library (commit 177d0fd)	328s	233s	-95s (-29%)
prost crate (from #2505)	325s	177s	-148s (-45%)

from local runs on a 12 core M3 Mac

Resolves #2505.

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

[tautschnig]

Running kani autoharness -Z autoharness --list ... for the standard library this command previously took 2:05 hours of wall-clock time (and 11300 seconds of CPU time) on an r5.metal. With the changes in this PR and increasing NUM_FILE_EXPORT_THREADS to 32 (can we please use the value of --jobs for that?) the same command took 1:25 hours (approximately 25% improvement) despite using 13000 seconds of CPU time (some overhead is not unexpected).

[AlexanderPortland]

I also don't think it's unexpected that this introduced regressions on the compile-timer-short CI job. The overhead of spinning up threads and communicating with them is likely not worth it for a workspace with a single proof as the main compiler thread could just as easily write that one file itself.

@tautschnig Does it make sense to cap the number of threads used (taken from the value of --jobs) at # of proof harnesses - 1? For workloads of just a single proof this will force the main thread to just handle everything itself and potentially negate this regression.

[tautschnig]

@tautschnig Does it make sense to cap the number of threads used (taken from the value of --jobs) at # of proof harnesses - 1? For workloads of just a single proof this will force the main thread to just handle everything itself and potentially negate this regression.

Yes, this capping sounds like a good idea!

[AlexanderPortland]

I ended up implementing the full calculation for the size of the thread pool as something along the lines of min(# of harnesses - 1, # of CPU cores - 1, SOME_MAX_SENSIBLE_COUNT) rather than taking it directly from the --jobs Kani argument.

Our compiler generates goto files at a fixed rate (currently around twice as fast as they can be exported), so adding any more than 3-4 threads to the export pool seems to have no real performance benefit as the extra threads are mostly sitting around without work to do.

Since the internal performance of our compiler isn't known by Kani users, it feels like this might be better kept as an internal calculation rather than taking it as an input. Does that seem alright @tautschnig?

[carolynzech]

The inspiration from this change came from #2505, specifically #2505 (comment). @AlexanderPortland can you check if these changes resolve the issue? Of course resolution here is subjective, since we have to decide what reasonable performance is, but let's do some measurements and see if this version of Kani builds in a more reasonable amount of time.

(This repo may serve as a useful benchmark for some of the other compiler perf improvements you've made as well, in addition to the standard library).

[tautschnig]

I'm happy with this, but would appreciate attention to Carolyn's comment with regard to #2505.

[AlexanderPortland]

Just ran the tests and, on my local machine, this change brings the prost crate's end to end compile time down 45%. I've updated the PR description with the full #s from that benchmark and the standard library.