This repository was archived by the owner on Apr 25, 2024. It is now read-only.

Parallel prover implementation for APRProofs - #727

Open

nwatson22 wants to merge 188 commits into

noah/apr-proof-parallel

Commits on Oct 31, 2023

Add interface for Proof and Prover class, test prove_parallel implementation
nwatson22
committed
b21b2fd
Merge branch 'master' into noah/parallel-prover
nwatson22
authored
f9aaba4
Merge f9aaba4dd881dc10f1c8f417083aaa8c9e4169b3 into 12c67b1f9458595ead1d3afb32d35b6cef84fdb0
nwatson22
authored
31e3a95
Set Version: 0.1.489
rv-auditor
committed
71eb0a3
Keep track of begun nodes
nwatson22
committed
fa0f4d0
Merge branch 'noah/parallel-prover' of https://github.com/runtimeverification/pyk into noah/parallel-prover
nwatson22
committed
2f45ff4

Commits on Nov 1, 2023

Commits on Nov 2, 2023

Use steps
nwatson22
committed
68bd89d

Commits on Nov 3, 2023

Update to match new interface plan
nwatson22
committed
34d2442

Commits on Nov 4, 2023

Add testing module
nwatson22
committed
76e239b

Commits on Nov 6, 2023

Change interface to use ProofStep
nwatson22
committed
a60290c

Commits on Nov 7, 2023

Add documentation comments, assertions and tests for TreeExploreProver, and strengthen type signatures
nwatson22
committed
1d3b9af
Update src/pyk/proof/parallel.py
nwatson22
authored
89527d3
Update src/tests/integration/proof/test_parallel_prove.py
nwatson22
authored
a064486
Update src/tests/integration/proof/test_parallel_prove.py
nwatson22
authored
5132864
Merge branch 'master' into noah/parallel-prover
nwatson22
authored
62ac147
Merge 62ac14736b215c604551ae916f767fea7aaaca5c into 11ec5230566ec2b8336000e636a5d814a4dc56d1
nwatson22
authored
05f8d56
Set Version: 0.1.492
rv-auditor
committed
9517856
Remove unused import
nwatson22
committed
08c0e81
Address comments
nwatson22
committed
2c5b42f
Remove unused typevar
nwatson22
committed
ff9d0c8
Address comments
nwatson22
committed
c8072a4
Merge c8072a49d0dde5f5c10ffe5e941f090feb917e1c into 263f2f58fb07a772df4a04bab95b17a6cd4d45fe
nwatson22
authored
9bd1e71
Set Version: 0.1.493
rv-auditor
committed
fdb4233

Commits on Nov 8, 2023

Commits on Nov 9, 2023

Address comments
nwatson22
committed
296e6f8
Merge branch 'noah/parallel-prover' of https://github.com/runtimeverification/pyk into noah/parallel-prover
nwatson22
committed
6e47134
Merge 6e471343e6096866307ba0af38d96bd33e5cf5e7 into edc297774f4ce99d44788aee7a0f6cee044aaf73
nwatson22
authored
6a9d3b5
Set Version: 0.1.495
rv-auditor
committed
7945c7e
Remove log messages
nwatson22
committed
a95458b
Merge branch 'noah/parallel-prover' of https://github.com/runtimeverification/pyk into noah/parallel-prover
nwatson22
committed
b991065
Fix formatting
nwatson22
committed
7c8c538
Add APRProof/Prover implementations of Prover interface
nwatson22
committed
17ea417
Merge branch 'noah/parallel-prover' into noah/experimental
nwatson22
committed
544962e
Address comments
nwatson22
committed
4445d29

Commits on Nov 10, 2023

Fix working with multiple proofs at once
nwatson22
committed
0cda3c4
Add missing requirements for status
nwatson22
committed
a3c210f
Improve typing on prove_parallel
nwatson22
committed
366e89e
Add fail_fast and max_iterations, and tests for these
nwatson22
committed
199e46f
Remove test cases
nwatson22
committed
0d7e523
Add to AprProofStep exec
nwatson22
committed
5777bc6
Merge noah/parallel-prover into branch
nwatson22
committed
f293736
Merge branch 'master' into noah/parallel-prover
nwatson22
authored
c65709a
Merge c65709a0353b7618cb0b113abbf3d78bdc69ecd8 into dd40fd825827736036b98c534acc7c953d117a0f
nwatson22
authored
7799541
Set Version: 0.1.497
rv-auditor
committed
e659928
Fix possibility of TreeExloreProof to switch status after passing/failing
nwatson22
committed
c2744a5
Merge branch 'noah/parallel-prover' of https://github.com/runtimeverification/pyk into noah/parallel-prover
nwatson22
committed
ed26199
Merge branch 'noah/parallel-prover' into noah/experimental
nwatson22
committed
536d0cf

Commits on Nov 13, 2023

Commits on Nov 14, 2023

Add APRProver Implementations
nwatson22
committed
0f5a6b3
Create interface for ProcessData
nwatson22
committed
1950f60
Switch to using 1 server per prover and sharing between threads, init client and kcfg_explore in exec()
nwatson22
committed
2436234

Commits on Nov 16, 2023

Parameterize imp parallel tests, add test to catch check_terminal order issue
nwatson22
committed
a3db6ee
Fix check_terminal bug
nwatson22
committed
5b86dfb

Commits on Nov 17, 2023

Remove parameters fromm prove_parallel and make shutdown() into destructor
nwatson22
committed
923a8d7
Merge master into branch
nwatson22
committed
75e955d
Merge master into branch
nwatson22
committed
640e3ee
Merge 640e3eeb66c87eb5b345d380c4c92e4604156dc3 into 314a6603716d96c9e6a81c145077bd467072053a
nwatson22
authored
66d321a
Set Version: 0.1.505
rv-auditor
committed
a682b22
Add ParallelAPRBMCProver
nwatson22
committed
1f46262
Display profiling information
nwatson22
committed
e029479
Merge e029479a9e695b6c1b684151114e986e95f35a46 into 714e709aaae4fb4417f9f8266b4ed09edeb561ca
nwatson22
authored
26e162f
Set Version: 0.1.506
rv-auditor
committed
5b82535

Commits on Nov 18, 2023

Commits on Nov 20, 2023

Commits on Nov 21, 2023

Commits on Nov 22, 2023

Merge master into branch
nwatson22
committed
a9cc7e5
Merge a9cc7e532285ab358d5ee44f0c759684d0ea5696 into 0535c6b136a08b9057761f32ce15faa9d0a7eac0
nwatson22
authored
7f8981f
Set Version: 0.1.511
rv-auditor
committed
5c105ca
Add cleanup method to ProcessData
nwatson22
committed
81958c5
Merge branch 'noah/apr-proof-parallel' of https://github.com/runtimeverification/pyk into noah/apr-proof-parallel
nwatson22
committed
10e6391
Add checked attribute to printer
nwatson22
committed
04bfed1

Commits on Dec 3, 2023

Commits on Dec 12, 2023

Merge remote-tracking branch 'origin/master' into update-apr-proof-parallel
h0nzZik
committed
174d0ad
Merge 174d0adc0a4253f295fd82e7d9c41f783fbe6ffb into 04bfed1f4dbe0df52cb5d3169a0fccac27665603
h0nzZik
authored
7a7d965
Set Version: 0.1.512
rv-auditor
committed
4354d19
fix a typo
h0nzZik
committed
a5bd37f
Merge a5bd37f065b8bc63a226a96db0d9723032707ba1 into f9a2da504dd4d4b366973185b7d66f07b00bba12
nwatson22
authored
d3eee58
Set Version: 0.1.544
rv-auditor
committed
c977298

Commits on Dec 18, 2023

Commits on Dec 19, 2023

Commits on Jan 26, 2024

Use single server
nwatson22
committed
cccc706
Fix too many servers being started
nwatson22
committed
3d69680

Commits on Jan 30, 2024

Commits on Feb 3, 2024

Clean up
nwatson22
committed
be877a3
Merge branch 'noah/apr-proof-parallel' of https://github.com/runtimeverification/pyk into noah/apr-proof-parallel
nwatson22
committed
518273d
Clean up
nwatson22
committed
6e7dde5
Clean up
nwatson22
committed
f53b0a9
Clean up
nwatson22
committed
7307862
Merge master into branch
nwatson22
committed
9eaf1a2
Merge 9eaf1a24adfa959e06e431455936c2b71ebc7456 into 4493d41e3d24de34c0c9155d88fe93c9c617070c
nwatson22
authored
d2b484d
Set Version: 0.1.613
rv-auditor
committed
31dcc46

Commits on Feb 5, 2024

Fix formatting
nwatson22
committed
597d280
Merge branch 'noah/apr-proof-parallel' of https://github.com/runtimeverification/pyk into noah/apr-proof-parallel
nwatson22
committed
66a6dfa
Clean up parallel.py
nwatson22
committed
9f30962

Commits on Feb 6, 2024

Clean up reachability.py
nwatson22
committed
f16161d

Commits on Feb 7, 2024

Remove extra inject_modules
nwatson22
committed
95f560d
Revert formatting changes with specific black version
nwatson22
committed
b4ae907
Revert changes relating to newer flake8-bugbear changes
nwatson22
committed
7bb8775
Revert poetry.lock
nwatson22
committed
dc4d66d
Revert changes relating to newer flake8-bugbear changes
nwatson22
committed
4d67d17
Revert changes relating to newer flake8-bugbear changes
nwatson22
committed
39b7cb1

Commits on Feb 8, 2024

Remove unnecessary class
nwatson22
committed
ab95cbe
Remove print messages
nwatson22
committed
3476c15
Encapsulate profiling info for parallel_prove
nwatson22
committed
58f865b
Remove commented lines
nwatson22
committed
21c1679
Remove commented lines
nwatson22
committed
c1dbe97
Merge master into branch
nwatson22
committed
3330c1c
Merge 3330c1ca4d6f4f1e9e135e0df2016defe31cd4d5 into 03ea742571765dc459d2bce4fbc4d2d8e78ae14f
nwatson22
authored
48039a4
Set Version: 0.1.618
rv-auditor
committed
215514e
Integrate max_iterations into APRParallelProver
nwatson22
committed
e43535c
Merge branch 'noah/apr-proof-parallel' of https://github.com/runtimeverification/pyk into noah/apr-proof-parallel
nwatson22
committed
e8123c1
Fix test case
nwatson22
committed
a8e5041
Implement fail_fast
nwatson22
committed
37df3d1
Merge 37df3d152766d50648dd076ea8932f9eb04c3e9a into e1519523721e84eec783019f7c061121bc50241e
nwatson22
authored
1bcab8b
Set Version: 0.1.619
rv-auditor
committed
e0fda99

Commits on Feb 9, 2024

Commits on Feb 10, 2024

reimplement bmc checking for parallel proofs
nwatson22
committed
fd177cc
Merge branch 'noah/apr-proof-parallel' of https://github.com/runtimeverification/pyk into noah/apr-proof-parallel
nwatson22
committed
d3d24a6
Fix formatting
nwatson22
committed
238ffb0
Set haskell option in the tests
nwatson22
committed
47bfa4a
proof/reachability: inline BMC logic into APRProof and APRProver
ehildenb
committed
4c745a7
proof/{proof,show,__init__}: cleanup remaining references to BMC provers
ehildenb
committed
c155cdc
tests/unit/test_proof: update unit tests for unified BMC prover
ehildenb
committed
220bb7b
tests/integration/proof/test_imp: update for unified BMC prover
ehildenb
committed
b8baa48
tests/integration/proof/test_goto: migrate to unified BMC prover
ehildenb
committed
5dda1cc
Merge 5dda1cc36b45f85679e19059d9e1efdd7de19ce3 into e68db42142d1e03d23cabd4cfff9082a08798f12
ehildenb
authored
d5ace85
Set Version: 0.1.620
rv-auditor
committed
c8ec74c
proof/reachability: inline tiny method
ehildenb
committed
9a5ad26

Commits on Feb 12, 2024

Commits on Feb 13, 2024

Commits on Feb 14, 2024