From 3d4c2c5f59b12b828031bdc940eccf29516e08d3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Petar=20Maksimovi=C4=87?= Date: Tue, 6 Aug 2024 23:03:46 +0200 Subject: [PATCH 1/2] Support for non-immediate proof maintenance (#4563) 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. --------- Co-authored-by: rv-jenkins Co-authored-by: devops Co-authored-by: Noah Watson <107630091+nwatson22@users.noreply.github.com> Co-authored-by: Georgy Lukyanov --- pyk/src/pyk/proof/proof.py | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) diff --git a/pyk/src/pyk/proof/proof.py b/pyk/src/pyk/proof/proof.py index 27adf9721b0..0d1eef04d2e 100644 --- a/pyk/src/pyk/proof/proof.py +++ b/pyk/src/pyk/proof/proof.py @@ -326,6 +326,7 @@ def parallel_advance_proof( fail_fast: bool = False, max_workers: int = 1, callback: Callable[[P], None] = (lambda x: None), + maintenance_rate: int = 1, ) -> None: """Advance proof with multithreaded strategy. @@ -347,7 +348,8 @@ def parallel_advance_proof( fail_fast: If the proof is failing after finishing a step, halt execution even if there are still available steps. max_workers: Maximum number of worker threads the pool can spawn. - callback: Callable to run in between each completed step, useful for getting real-time information about the proof. + callback: Callable to run during proof maintenance, useful for getting real-time information about the proof. + maintenance_rate: Number of iterations between proof maintenance (writing to disk and executing callback). """ pending: set[Future[Any]] = set() explored: set[PS] = set() @@ -376,9 +378,10 @@ def submit_steps(_steps: Iterable[PS]) -> None: proof_results = future.result() for result in proof_results: proof.commit(result) - proof.write_proof_data() - callback(proof) iterations += 1 + if iterations % maintenance_rate == 0: + proof.write_proof_data() + callback(proof) if max_iterations is not None and max_iterations <= iterations: break if fail_fast and proof.failed: @@ -502,6 +505,7 @@ def advance_proof( max_iterations: int | None = None, fail_fast: bool = False, callback: Callable[[P], None] = (lambda x: None), + maintenance_rate: int = 1, ) -> None: """Advance a proof. @@ -513,6 +517,7 @@ def advance_proof( fail_fast: If the proof is failing after finishing a step, halt execution even if there are still available steps. callback: Callable to run in between each completed step, useful for getting real-time information about the proof. + maintenance_rate: Number of iterations between proof maintenance (writing to disk and executing callback). """ iterations = 0 _LOGGER.info(f'Initializing proof: {proof.id}') @@ -533,7 +538,9 @@ def advance_proof( results = self.step_proof(step) for result in results: proof.commit(result) - proof.write_proof_data() - callback(proof) + if iterations % maintenance_rate == 0: + proof.write_proof_data() + callback(proof) + if proof.failed: proof.failure_info = self.failure_info(proof) From a2b5a76d0f3607227f0e63d3019851c8a227a19c Mon Sep 17 00:00:00 2001 From: Noah Watson <107630091+nwatson22@users.noreply.github.com> Date: Wed, 7 Aug 2024 03:00:40 -0500 Subject: [PATCH 2/2] Status bar improvements (#4575) - Adds the number of refuted nodes to the proof status bar. - Adds a separator which separates the one line summary into 3 parts, one which is the proof status, one to do with structure, and one to do with status of the leaves. - Changes the definition of `branches` to mean "how many `Split` and `NDBranch` targets are there?" instead of "how many `Split`s and `NDBranch`es are there?" to more accurately reflect the degree of branching in a proof. --- pyk/src/pyk/proof/reachability.py | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index 53b1b26e586..fab28f6cc60 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -507,14 +507,17 @@ def one_line_summary(self) -> str: nodes = len(self.kcfg.nodes) pending = len(self.pending) failing = len(self.failing) - branches = len(self.kcfg.ndbranches()) + len(self.kcfg.splits()) + branches = 0 + for branch in self.kcfg.ndbranches() + self.kcfg.splits(): + branches += len(branch.targets) vacuous = len(self.kcfg.vacuous) terminal = len(self.terminal) stuck = len(self.kcfg.stuck) passed = len([cover for cover in self.kcfg.covers() if cover.target.id == self.target]) + refuted = len(self.node_refutations) return ( super().one_line_summary - + f'|{nodes} nodes|{pending} pending|{passed} passed|{failing} failing|{branches} branches|{vacuous} vacuous|{terminal} terminal|{stuck} stuck' + + f' --- {nodes} nodes|{branches} branches|{terminal} terminal --- {pending} pending|{passed} passed|{failing} failing|{vacuous} vacuous|{refuted} refuted|{stuck} stuck' ) def get_refutation_id(self, node_id: int) -> str: