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

Automatically add subproofs to parallelized execution once they become available #2065

Closed
wants to merge 61 commits into from
Closed

Automatically add subproofs to parallelized execution once they become available #2065

wants to merge 61 commits into from

Conversation

nwatson22
Copy link
Member

No description provided.

tothtamas28
tothtamas28 reviewed Sep 8, 2023
View reviewed changes
kevm-pyk/src/kevm_pyk/utils.py Outdated Show resolved Hide resolved
kevm-pyk/src/kontrol/foundry.py Outdated Show resolved Hide resolved
@nwatson22 nwatson22 mentioned this pull request Sep 13, 2023
Merged
@nwatson22
Copy link
Member Author

nwatson22 commented Sep 14, 2023 •
edited
Loading

Waiting on runtimeverification/pyk#654

nwatson22 and others added 15 commits September 14, 2023 20:10
@nwatson22
Merge branch 'noah/branches-parallelization' of https://github.com/ru…
c3fbee7 
…ntimeverification/evm-semantics into noah/branches-parallelization
@nwatson22
Fix failure reporting to work with split proof
f60c1bc
@nwatson22
Merge master into branch
38126cd
Set Version: 1.0.292
25bf2ad
@nwatson22
Fix merge
cb3dad8
@nwatson22
Merge branch 'noah/branches-parallelization' of https://github.com/ru…
932aad3 
…ntimeverification/evm-semantics into noah/branches-parallelization
@nwatson22
Fix subproofs overwriting each other
269dddc
@nwatson22
Fix formatting
3be4c85
@nwatson22
Make test have 2 long branches
e3e3807
@nwatson22
Remove passing around of failure log
2f8422b
@nwatson22
Remove unused parameter
eb6c48b
@nwatson22
Remove commented lines
55c2331
@nwatson22
Remove commented lines
e598e6c
@nwatson22
Use wait() instead of sleep, remove print statements
17fbcc8
@nwatson22
Fix reporting as failing when pending
ac7e38f
PetarMax added a commit to runtimeverification/pyk that referenced this pull request Sep 18, 2023
@nwatson22 @PetarMax
Make branch extraction more intelligent (#652)
744fbcd 
Closes #632.

Before introducing a branch, simplify each of the would-be new nodes and
see if they simplify to bottom
If there are more than 1 non-bottom node, add all these simplified nodes
to the CFG, creating a split/branch. If not, simply continue
straight-line execution.

This should reduce eliminate some infeasible branching by simplifying
earlier in the process.

Also should eliminate repeated branching encountered in
runtimeverification/evm-semantics#2065 when
creating new proofs from branches.

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: Petar Maksimović <[email protected]>
nwatson22
nwatson22 commented Sep 19, 2023
View reviewed changes
kevm-pyk/pyproject.toml Outdated Show resolved Hide resolved
nwatson22 and others added 21 commits September 20, 2023 18:37
@nwatson22
Merge branch 'noah/branches-parallelization' of https://github.com/ru…
e4b6684 
…ntimeverification/evm-semantics into noah/branches-parallelization
@nwatson22
Merge branch 'master' into noah/branches-parallelization
2137c71
Set Version: 1.0.300
163f835
@nwatson22
Revert LoopsTest expected file
f41c9bb
@nwatson22
Merge branch 'noah/branches-parallelization' of https://github.com/ru…
fcc46c4 
…ntimeverification/evm-semantics into noah/branches-parallelization
@nwatson22
Propogate generate_subproof_name to APRBMCProof constructor
f6ae8c0
@nwatson22
Update poetry lock
42b298c
@nwatson22
Merge master into branch, add test
2ebe0b6
Set Version: 1.0.302
9cf86d8
@nwatson22
Change test selection to use exact match
440a553
@nwatson22
Try adding --subproof argument for selecting which subproof to use (i…
5b738a0 
…ncluding nested)
@nwatson22
Fix subproof path selection
830576e
Set Version: 1.0.303
f56acab
@nwatson22
Merge master into branch
8656742
@nwatson22
Merge branch 'master' into noah/branches-parallelization
dc11c02
Set Version: 1.0.304
921541b
@nwatson22
Merge master into branch
b0d18b2
@nwatson22
Update poetry.lock
0881fb7
Set Version: 1.0.305
4abac54
@nwatson22
Update flake.nix to use branch
39596fc
@nwatson22
Merge branch 'noah/branches-parallelization' of https://github.com/ru…
de03318 
…ntimeverification/evm-semantics into noah/branches-parallelization
@palinatolmach palinatolmach linked an issue Sep 26, 2023 that may be closed by this pull request
Parallelize symbolic execution of tests #2009
Open
Baltoli pushed a commit to runtimeverification/k that referenced this pull request Apr 9, 2024
@nwatson22 @PetarMax
Make branch extraction more intelligent (#652)
620bd5e 
Closes #632.

Before introducing a branch, simplify each of the would-be new nodes and
see if they simplify to bottom
If there are more than 1 non-bottom node, add all these simplified nodes
to the CFG, creating a split/branch. If not, simply continue
straight-line execution.

This should reduce eliminate some infeasible branching by simplifying
earlier in the process.

Also should eliminate repeated branching encountered in
runtimeverification/evm-semantics#2065 when
creating new proofs from branches.

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: Petar Maksimović <[email protected]>
Baltoli pushed a commit to runtimeverification/k that referenced this pull request Apr 9, 2024
@nwatson22 @PetarMax
Make branch extraction more intelligent (runtimeverification/pyk#652)
aed9c7e 
Closes #632.

Before introducing a branch, simplify each of the would-be new nodes and
see if they simplify to bottom
If there are more than 1 non-bottom node, add all these simplified nodes
to the CFG, creating a split/branch. If not, simply continue
straight-line execution.

This should reduce eliminate some infeasible branching by simplifying
earlier in the process.

Also should eliminate repeated branching encountered in
runtimeverification/evm-semantics#2065 when
creating new proofs from branches.

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: Petar Maksimović <[email protected]>
Baltoli pushed a commit to runtimeverification/k that referenced this pull request Apr 9, 2024
@nwatson22 @PetarMax @Baltoli
Make branch extraction more intelligent (runtimeverification/pyk#652)
ee20522 
Closes #632.

Before introducing a branch, simplify each of the would-be new nodes and
see if they simplify to bottom
If there are more than 1 non-bottom node, add all these simplified nodes
to the CFG, creating a split/branch. If not, simply continue
straight-line execution.

This should reduce eliminate some infeasible branching by simplifying
earlier in the process.

Also should eliminate repeated branching encountered in
runtimeverification/evm-semantics#2065 when
creating new proofs from branches.

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: Petar Maksimović <[email protected]>
Baltoli pushed a commit to runtimeverification/k that referenced this pull request Apr 10, 2024
@nwatson22 @PetarMax @Baltoli
Make branch extraction more intelligent (runtimeverification/pyk#652)
d11a628 
Closes #632.

Before introducing a branch, simplify each of the would-be new nodes and
see if they simplify to bottom
If there are more than 1 non-bottom node, add all these simplified nodes
to the CFG, creating a split/branch. If not, simply continue
straight-line execution.

This should reduce eliminate some infeasible branching by simplifying
earlier in the process.

Also should eliminate repeated branching encountered in
runtimeverification/evm-semantics#2065 when
creating new proofs from branches.

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: Petar Maksimović <[email protected]>
Baltoli pushed a commit to runtimeverification/k that referenced this pull request Apr 10, 2024
@nwatson22 @PetarMax @Baltoli
Make branch extraction more intelligent (runtimeverification/pyk#652)
7753cac 
Closes #632.

Before introducing a branch, simplify each of the would-be new nodes and
see if they simplify to bottom
If there are more than 1 non-bottom node, add all these simplified nodes
to the CFG, creating a split/branch. If not, simply continue
straight-line execution.

This should reduce eliminate some infeasible branching by simplifying
earlier in the process.

Also should eliminate repeated branching encountered in
runtimeverification/evm-semantics#2065 when
creating new proofs from branches.

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: Petar Maksimović <[email protected]>
@ehildenb
Copy link
Member

Closing due to age.

@ehildenb ehildenb closed this Jun 25, 2024
@ehildenb ehildenb deleted the noah/branches-parallelization branch June 25, 2024 15:42
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@tothtamas28 tothtamas28 tothtamas28 left review comments

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

Successfully merging this pull request may close these issues.

Parallelize symbolic execution of tests
3 participants
@nwatson22 @ehildenb @tothtamas28