Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Apply generalized broadcast to vstd #1023

Merged
merged 9 commits into from
Apr 25, 2024
Merged

Apply generalized broadcast to vstd #1023

merged 9 commits into from
Apr 25, 2024

Conversation

utaal-b
Copy link
Contributor

@utaal-b utaal-b commented Mar 4, 2024 •
edited by utaal
Loading

This PR applies the generalized broadcast mechanism to vstd, and removes the automatic unconditional broadcast (except for pruning) of #[verifier::external_body] broadcast fns. This PR is intended to not make any changes to the externally visible behavior outside vstd, instead it just applied the new mechanism so that the old one can be removed.

@utaal-b utaal-b force-pushed the generalized-broadcast-vstd branch 2 times, most recently from 57f8f6e to d07752c Compare March 4, 2024 09:27
@utaal-b utaal-b mentioned this pull request Mar 4, 2024
Merged
Base automatically changed from generalized-broadcast to main March 27, 2024 19:33
@utaal utaal force-pushed the generalized-broadcast-vstd branch 3 times, most recently from 89cf133 to 7e8be86 Compare April 7, 2024 20:51
@utaal
Copy link
Collaborator

utaal commented Apr 7, 2024 •
edited
Loading

verusfmt will fail because there are a couple of pending PRs and fixes to tune the support for broadcast group / broadcast use but this should be otherwise ready for review.

Edit: just realized there are still a couple of TODOs: working on those.

@utaal utaal marked this pull request as ready for review April 7, 2024 20:52
@utaal utaal force-pushed the generalized-broadcast-vstd branch from e254862 to d525b2d Compare April 7, 2024 21:20
@utaal utaal force-pushed the generalized-broadcast-vstd branch 4 times, most recently from 0033dff to 8c6f3d9 Compare April 21, 2024 05:18
@utaal
Copy link
Collaborator

utaal commented Apr 21, 2024

Ok, now this should be ready for review. cc @Chris-Hawblitzel

@utaal utaal force-pushed the generalized-broadcast-vstd branch from 8c6f3d9 to b6d4997 Compare April 24, 2024 08:50
@utaal
Copy link
Collaborator

utaal commented Apr 24, 2024

veritas report for verus main (270a4d04f74604948c904b48d298e9c8ae0da8d8) with features: singular

project refspec success total verus time (ms) smt run time (ms)
verus-vstd main (270a4d04f74604948c904b48d298e9c8ae0da8d8) true 9231 5401
memory-allocator main (9ee40b614443962b15e7315106568f20a1810ebf) true 68669 48696
page-table page-table (4c8fec30b7997c79d9d4e9520dee27d2bcdc6a2f) true 24686 37097
verified-storage main (5372264cc1616589264adda20829b4e88a09fbd8) true 6190 4554

veritas report for verus generalized-broadcast-vstd (8c6f3d930ffc57b8670cfe1794425d1bbed2d5a5) with features: singular

project refspec success total verus time (ms) smt run time (ms)
verus-vstd generalized-broadcast-vstd (8c6f3d930ffc57b8670cfe1794425d1bbed2d5a5) false 1600 0
memory-allocator main (9ee40b614443962b15e7315106568f20a1810ebf) true 63483 45441
page-table page-table (4c8fec30b7997c79d9d4e9520dee27d2bcdc6a2f) true 22698 34836
verified-storage main (5372264cc1616589264adda20829b4e88a09fbd8) false 6326 5538

Performance is unaffected, but something's not quite right yet (for verified-storage). The failure on vstd may be that veritas needs a different configuration after this PR.

@utaal utaal force-pushed the generalized-broadcast-vstd branch from b6d4997 to a2ebc63 Compare April 24, 2024 14:10
@utaal
support cfg(not(feature = "alloc")) with default vstd broadcast group…
ffb2688 
…, guard verifier attributes with cfg_attr where necessary
@utaal utaal force-pushed the generalized-broadcast-vstd branch from 90a7d5c to ffb2688 Compare April 25, 2024 01:04
@utaal utaal force-pushed the generalized-broadcast-vstd branch from 9118c74 to 7244402 Compare April 25, 2024 01:29
@utaal
Copy link
Collaborator

utaal commented Apr 25, 2024 •
edited
Loading

The project verification times are now unaffected.

veritas report for verus main (f6c8fecf18877b751929de7f6e807daf59ee9c2e) with features: singular

project refspec outcome total verus time (ms) smt run time (ms)
verus-vstd main (f6c8fecf18877b751929de7f6e807daf59ee9c2e) success (609 verified, 0 errors) 9626 5720
memory-allocator main (9ee40b614443962b15e7315106568f20a1810ebf) success (745 verified, 0 errors) 64473 50035
page-table page-table (4c8fec30b7997c79d9d4e9520dee27d2bcdc6a2f) success (294 verified, 0 errors) 25114 38649
verified-storage main (5372264cc1616589264adda20829b4e88a09fbd8) success (188 verified, 0 errors) 6050 4465
node-replication main (5d496003efc39a8e09d90b4147ab95106b76d6aa) success (254 verified, 0 errors) 8141 2734

veritas report for verus generalized-broadcast-vstd (7244402ed08dfa3cf91334a8abf641d456ae222c) with features: singular

project refspec outcome total verus time (ms) smt run time (ms)
verus-vstd generalized-broadcast-vstd (7244402ed08dfa3cf91334a8abf641d456ae222c) success (815 verified, 0 errors) 22026 9764
memory-allocator main (9ee40b614443962b15e7315106568f20a1810ebf) success (745 verified, 0 errors) 66161 48324
page-table page-table (4c8fec30b7997c79d9d4e9520dee27d2bcdc6a2f) success (294 verified, 0 errors) 22442 35394
verified-storage main (5372264cc1616589264adda20829b4e88a09fbd8) success (188 verified, 0 errors) 6002 4231
node-replication main (5d496003efc39a8e09d90b4147ab95106b76d6aa) success (254 verified, 0 errors) 8360 2837

The longer vstd verification time is likely due to using admit() instead of #[verifier::external_body] and due to some axioms now being actual proofs.

@utaal
Copy link
Collaborator

utaal commented Apr 25, 2024 •
edited
Loading

Now that performance matches (@Chris-Hawblitzel asked me offline to check for potential performance degradation) I'm going to land this to prevent vstd from diverging again. Let me know if you have further comments.

@utaal utaal merged commit 52363ae into main Apr 25, 2024
5 checks passed
@utaal utaal deleted the generalized-broadcast-vstd branch April 25, 2024 02:46
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Chris-Hawblitzel Chris-Hawblitzel Awaiting requested review from Chris-Hawblitzel

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@utaal-b @utaal