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

Support for non-immediate proof maintenance #4563

Merged
merged 11 commits into from
Aug 6, 2024
Merged

Support for non-immediate proof maintenance #4563

merged 11 commits into from
Aug 6, 2024

Conversation

PetarMax
Copy link
Contributor

@PetarMax PetarMax commented Jul 31, 2024 •
edited
Loading

When doing large real-world proofs with a high degree of parallelism, the bandwidth is overtaken by the writing of the proof to disk on every proof iteration, slowing the process considerably.

This PR introduces the ability to write to disk and perform the callback on every maintenance_iterations of the parallel proof, set by default to 32.

EDIT: Actually, perhaps it's a better idea to write the proof every max_workers iterations.

@PetarMax PetarMax self-assigned this Jul 31, 2024
@rv-jenkins rv-jenkins changed the base branch from master to develop July 31, 2024 10:00
@PetarMax PetarMax marked this pull request as ready for review July 31, 2024 12:43
@nwatson22 nwatson22 mentioned this pull request Aug 5, 2024
Merged
nwatson22
nwatson22 approved these changes Aug 5, 2024
View reviewed changes
Copy link
Member

@nwatson22 nwatson22 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good. Can you make it toggleable with a flag so we can choose to do the disk writing/status bar updating every step?

rv-jenkins and others added 5 commits August 6, 2024 21:33
@rv-jenkins @PetarMax
Update dependency: deps/llvm-backend_release (#4559)
1c43e2e 
Co-authored-by: devops <[email protected]>
@nwatson22 @PetarMax
Display number of terminal nodes in one_line_summary for APRProof (…
dad78b1 
…#4566)

Adds the number of terminal nodes to `one_line_summary` for `APRProof`.
Also changes the display to use `|` as dividers instead of `/`.
@rv-jenkins @PetarMax
Update dependency: deps/haskell-backend_release (#4558)
80a43a8 
Co-authored-by: devops <[email protected]>
@rv-jenkins @PetarMax
Update dependency: deps/haskell-backend_release (#4571)
da797e8 
Co-authored-by: devops <[email protected]>
@geo2a @PetarMax
Remove the deprecated "log-timing" RPC log option (#4573)
bcd3983 
This option is unused and all its use cases are subsumed by the `-l
Timing --log-format json` non-RPC log option.

For reference, here's the Haskell Backend PR that stops emitting the
timing RPC log entries:
runtimeverification/haskell-backend#4015
@PetarMax
Copy link
Contributor Author

PetarMax commented Aug 6, 2024

I think I prefer to have a separate parameter so that we can decouple it from the number of workers, as it is now. Is there anything else to do in pyk?

@nwatson22
Copy link
Member

I think I prefer to have a separate parameter so that we can decouple it from the number of workers, as it is now. Is there anything else to do in pyk?

You could possibly add the same parameter/logic to Prover.advance_proof() and feed the option through to be able to be used with pyk prove, but that could also be done later in a separate PR since this is needed for kontrol now.

nwatson22
nwatson22 approved these changes Aug 6, 2024
View reviewed changes
pyk/src/tests/unit/test-data/pyk_toml_test.toml Outdated
@@ -1,6 +1,6 @@
[coverage]
output = "default-file"
definition = "/tmp"
definition = "/var/folders/ks/1p8zyp5j7xz_v1krhl4l17tm0000gn/T"
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What is this change for?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have not changed that file manually...

@PetarMax
Copy link
Contributor Author

PetarMax commented Aug 6, 2024

I think I prefer to have a separate parameter so that we can decouple it from the number of workers, as it is now. Is there anything else to do in pyk?

You could possibly add the same parameter/logic to Prover.advance_proof() and feed the option through to be able to be used with pyk prove, but that could also be done later in a separate PR since this is needed for kontrol now.

Yes, happy to.

@PetarMax
Copy link
Contributor Author

PetarMax commented Aug 6, 2024

Just to say - I am not sure how to test this, because the final outcome is the same, it's just that the proof should be faster. Happy to go along with any ideas in a follow-up PR.

@PetarMax PetarMax merged commit 3d4c2c5 into develop Aug 6, 2024
17 checks passed
@PetarMax PetarMax deleted the petar/non-immediate-proof-maintenance branch August 6, 2024 21:03
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@nwatson22 nwatson22 nwatson22 approved these changes

@tothtamas28 tothtamas28 Awaiting requested review from tothtamas28

@ehildenb ehildenb Awaiting requested review from ehildenb

Assignees

@PetarMax PetarMax

Labels
enhancement
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@PetarMax @nwatson22 @rv-jenkins @geo2a