search

verus-lang / verus

Verified Rust for low-level systems code
MIT License
1.15k stars 66 forks source link

Prune imported crates before processing VIR #1111

Closed Chris-Hawblitzel closed 4 months ago

Chris-Hawblitzel commented 4 months ago

This adds an earlier pruning stage that prunes imported-crate VIR immediately after importing, saving time on the VIR processing (e.g. ast_simplify) that happens before the existing per-module pruning. In other words, we no longer waste time processing imported VIR from vstd that will go unused. This, together with https://github.com/verus-lang/verus/commit/090b58834caa828826197efbed5fe3454a5d800c , should largely address https://github.com/verus-lang/verus/issues/1076 .

Chris-Hawblitzel commented 4 months ago

Shall we try a veritas run to see the perf impact of the two commits?

It would probably be a good idea just to make sure the commits don't break anything. I expect the commits to mainly affect the performance on small crates for now. As vstd grows the commits may have more of an impact. This pull request by itself seemed to speed up vargo test by about 10% for now.

utaal commented 4 months ago

A bit late, but here are veritas results: before this commit vs current main.

veritas report for verus cb987c8b6773cd5ba9b3ada612a251249cc61e8d (cb987c8b6773cd5ba9b3ada612a251249cc61e8d) with features: singular

project revspec outcome total verus time (ms) smt run time (ms)
verus-vstd cb987c8b6773cd5ba9b3ada612a251249cc61e8d (cb987c8b6773cd5ba9b3ada612a251249cc61e8d) success (755 verified, 0 errors) 22263 8787
page-table page-table (4c8fec30b7997c79d9d4e9520dee27d2bcdc6a2f) success (294 verified, 0 errors) 20956 34588
verified-storage main (bea03b751962752498078e992d1aab8596722f37) success (237 verified, 0 errors) 7241 6054
node-replication main (5d496003efc39a8e09d90b4147ab95106b76d6aa) success (254 verified, 0 errors) 8366 2946

veritas report for verus main (4dbb2c9eb08b9478f758390f823928738828fe48) with features: singular

project revspec outcome total verus time (ms) smt run time (ms)
verus-vstd main (4dbb2c9eb08b9478f758390f823928738828fe48) success (758 verified, 0 errors) 21995 8835
page-table page-table (4c8fec30b7997c79d9d4e9520dee27d2bcdc6a2f) success (294 verified, 0 errors) 20670 33036
verified-storage main (bea03b751962752498078e992d1aab8596722f37) failure (0 verified, 0 errors) 883 0
node-replication main (5d496003efc39a8e09d90b4147ab95106b76d6aa) success (254 verified, 0 errors) 8138 2806
utaal commented 4 months ago

cc @Chris-Hawblitzel other than something breaking verified-storage, the numbers look identical in the noise.