From 460c3f86a0ab7d24bf02b21f6f66a31d16819306 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Wed, 27 Sep 2023 21:41:47 +0200 Subject: [PATCH 01/19] Proof queue --- kevm-pyk/poetry.lock | 8 +- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/__main__.py | 169 +++++++++++++++++++++++++----- 3 files changed, 145 insertions(+), 34 deletions(-) diff --git a/kevm-pyk/poetry.lock b/kevm-pyk/poetry.lock index 2ca213a5ce..8a6c23314d 100644 --- a/kevm-pyk/poetry.lock +++ b/kevm-pyk/poetry.lock @@ -814,7 +814,7 @@ plugins = ["importlib-metadata"] [[package]] name = "pyk" -version = "0.1.478" +version = "0.1.479" description = "" optional = false python-versions = "^3.10" @@ -834,8 +834,8 @@ tomli = "^2.0.1" [package.source] type = "git" url = "https://github.com/runtimeverification/pyk.git" -reference = "v0.1.478" -resolved_reference = "5d3e77d23cfe46d682f8e2d50e9865287d3729bb" +reference = "v0.1.479" +resolved_reference = "41706ef5081585a4c71f7fccb4dea2d7a3796421" [[package]] name = "pyperclip" @@ -1099,4 +1099,4 @@ testing = ["big-O", "jaraco.functools", "jaraco.itertools", "more-itertools", "p [metadata] lock-version = "2.0" python-versions = "^3.10" -content-hash = "92468f5f87e8f2228e0ac2036b35fee2c198bb92249d8012b03c062b09ed180f" +content-hash = "7ac1ad0f11ec671b9b13ae07c6ed971a06bc8ccbc178e20cc34610cb9e6bb390" diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 91c917cb23..ab75470ad7 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -17,7 +17,7 @@ packages = [ [tool.poetry.dependencies] python = "^3.10" pathos = "*" -pyk = { git = "https://github.com/runtimeverification/pyk.git", tag="v0.1.478" } +pyk = { git = "https://github.com/runtimeverification/pyk.git", tag="v0.1.479" } tomlkit = "^0.11.6" xdg-base-dirs = "^6.0.0" diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index 3df8f0ec30..4c35ca44fc 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -1,17 +1,20 @@ from __future__ import annotations +import abc import contextlib -import graphlib +import dataclasses import json import logging -import os +import multiprocessing import sys +import tempfile import time from argparse import ArgumentParser from pathlib import Path from typing import TYPE_CHECKING -from pathos.pools import ProcessPool # type: ignore +import multiprocess # type: ignore +import pathos # type: ignore from pyk.cli.utils import file_path from pyk.cterm import CTerm from pyk.kast.outer import KApply, KRewrite, KSort, KToken @@ -24,7 +27,7 @@ from pyk.proof.equality import EqualityProof from pyk.proof.show import APRProofShow from pyk.proof.tui import APRProofViewer -from pyk.utils import single +from pyk.utils import single, unique from . import VERSION, config, kdist from .cli import KEVMCLIArgs, node_id_like @@ -43,7 +46,7 @@ if TYPE_CHECKING: from argparse import Namespace from collections.abc import Callable, Iterable, Iterator - from typing import Any, Final, TypeVar + from typing import Any, Final, Mapping, TypeVar from pyk.kast.outer import KClaim from pyk.kcfg.kcfg import NodeIdLike @@ -192,14 +195,50 @@ def map(self, f: Callable[[Any], Any], xs: list[Any]) -> list[Any]: @contextlib.contextmanager -def wrap_process_pool(workers: int) -> Iterator[ZeroProcessPool | ProcessPool]: +def wrap_process_pool(workers: int) -> Iterator[ZeroProcessPool | pathos.pools.ProcessPool]: if workers <= 1: yield ZeroProcessPool() else: - with ProcessPool(ncpus=workers) as pp: + with pathos.pools.ProcessPool(ncpus=workers) as pp: yield pp +class TodoQueueTask(abc.ABC): + ... + + +@dataclasses.dataclass +class TodoQueueProofTask(TodoQueueTask): + proof_id: str + + +@dataclasses.dataclass +class TodoQueueStop(TodoQueueTask): + ... + + +class DoneQueueTask(abc.ABC): + ... + + +@dataclasses.dataclass +class DoneQueueTaskFinished(DoneQueueTask): + proof_id: str + passed: bool + failure_log: list[str] | None + + +class MyEnvironment: + number_of_workers: int + to_do_queue: multiprocessing.Queue # only instances of TodoQueueTask go there + done_queue: multiprocessing.Queue # only instances of DoneQueueTask go there + + def __init__(self, number_of_workers: int): + self.number_of_workers = number_of_workers + self.to_do_queue = multiprocessing.Queue() + self.done_queue = multiprocessing.Queue() + + def exec_prove( spec_file: Path, includes: Iterable[str], @@ -238,6 +277,9 @@ def exec_prove( if smt_retry_limit is None: smt_retry_limit = 10 + if save_directory is None: + save_directory = Path(tempfile.TemporaryDirectory().name) + kevm = KEVM(definition_dir, use_directory=save_directory, bug_report=bug_report) include_dirs = [Path(include) for include in includes] @@ -257,6 +299,7 @@ def is_functional(claim: KClaim) -> bool: llvm_definition_dir = definition_dir / 'llvm-library' if use_booster else None _LOGGER.info(f'Extracting claims from file: {spec_file}') + all_claims = kevm.get_claims( spec_file, spec_module_name=spec_module, @@ -265,11 +308,18 @@ def is_functional(claim: KClaim) -> bool: claim_labels=None, exclude_claim_labels=exclude_claim_labels, ) - if all_claims is None: - raise ValueError(f'No claims found in file: {spec_file}') - all_claims_by_label: dict[str, KClaim] = {c.label: c for c in all_claims} - spec_module_name = spec_module if spec_module is not None else os.path.splitext(spec_file.name)[0].upper() - claims_graph = claim_dependency_dict(all_claims, spec_module_name=spec_module_name) + + spec_modules = kevm.get_claim_modules( + spec_file, spec_module_name=spec_module, include_dirs=include_dirs, md_selector=md_selector + ) + + all_claims_by_id: Mapping[str, KClaim] = {f'{spec_module}.{claim.label}': claim for claim in all_claims} + + claims_graph = claim_dependency_dict(all_claims, spec_module_name=spec_module) + proofs: list[APRProof] = APRProof.from_spec_modules( + kevm.definition, spec_modules, spec_labels=claim_labels, logs={}, proof_dir=save_directory + ) + proofs = list(unique(proofs)) def _init_and_run_proof(claim: KClaim) -> tuple[bool, list[str] | None]: with legacy_explore( @@ -358,29 +408,90 @@ def _init_and_run_proof(claim: KClaim) -> tuple[bool, list[str] | None]: return passed, failure_log - topological_sorter = graphlib.TopologicalSorter(claims_graph) - topological_sorter.prepare() - with wrap_process_pool(workers=workers) as process_pool: - selected_results: list[tuple[bool, list[str] | None]] = [] - selected_claims = [] - while topological_sorter.is_active(): - ready = topological_sorter.get_ready() - _LOGGER.info(f'Discharging proof obligations: {ready}') - curr_claim_list = [all_claims_by_label[label] for label in ready] - results: list[tuple[bool, list[str] | None]] = process_pool.map(_init_and_run_proof, curr_claim_list) - for label in ready: - topological_sorter.done(label) - selected_results.extend(results) - selected_claims.extend(curr_claim_list) + def worker(env: MyEnvironment) -> None: + while True: + msg = env.to_do_queue.get() + match msg: + case TodoQueueStop(): + return + case TodoQueueProofTask(proof_id): + passed, failure_log = _init_and_run_proof(all_claims_by_id[proof_id]) + env.done_queue.put(DoneQueueTaskFinished(proof_id=proof_id, passed=passed, failure_log=failure_log)) + + def coordinator(env: MyEnvironment, proofs_to_do: list[APRProof]) -> list[tuple[bool, list[str] | None]]: + id_to_proof: dict[str, APRProof] = {pf.id: pf for pf in proofs_to_do} + remaining_proof_ids: set[str] = {pf.id for pf in proofs_to_do} + finished_proof_ids: dict[str, tuple[bool, list[str] | None]] = {} + + def get_a_ready_id() -> str | None: + for proof_id in remaining_proof_ids: + if set(id_to_proof[proof_id].subproof_ids).issubset(finished_proof_ids.keys()): + remaining_proof_ids.remove(proof_id) + return proof_id + return None + + def put_all_ready_into_queue() -> int: + n = 0 + while True: + opt_proof_id: str | None = get_a_ready_id() + if opt_proof_id is None: + return n + env.to_do_queue.put(TodoQueueProofTask(opt_proof_id)) + n = n + 1 + + def process_incoming_message(msg: DoneQueueTask) -> bool: + match msg: + case DoneQueueTaskFinished(proof_id=proof_id, passed=passed, failure_log=failure_log): + finished_proof_ids[proof_id] = (passed, failure_log) + return True + return False + + def take_all_proven_from_queue() -> int: + n = 0 + while not env.done_queue.empty(): + msg = env.done_queue.get() + if process_incoming_message(msg): + n = n + 1 + return n + + enqueued_counter: int = 0 + while True: + newly_removed_from_queue = take_all_proven_from_queue() + newly_enqueued = put_all_ready_into_queue() + enqueued_counter = enqueued_counter + newly_enqueued - newly_removed_from_queue + assert enqueued_counter >= 0 + if enqueued_counter == 0: + break + assert enqueued_counter > 0 + # We can wait for some incoming message. + # Unfortunately, a `wait_until_nonempty` primitive is missing, so we have to block using `get`. + msg = env.done_queue.get() + if process_incoming_message(msg): + enqueued_counter = enqueued_counter - 1 + # And now we are going to process all the other incoming messages (if any) + continue + # Now we want to stop all the workers + for _ in range(env.number_of_workers): + env.to_do_queue.put(TodoQueueStop()) + return [finished_proof_ids[p.id] for p in proofs_to_do] + + # ctx = multiprocessing.get_context('spawn') + env = MyEnvironment(number_of_workers=workers) + worker_processes = [multiprocess.Process(target=worker, args=(env,)) for _ in range(workers)] + for w in worker_processes: + w.start() + results = coordinator(env, proofs) + for w in worker_processes: + w.join() failed = 0 - for claim, r in zip(selected_claims, selected_results, strict=True): + for proof, r in zip(proofs, results, strict=True): passed, failure_log = r if passed: - print(f'PROOF PASSED: {claim.label}') + print(f'PROOF PASSED: {proof.id}') else: failed += 1 - print(f'PROOF FAILED: {claim.label}') + print(f'PROOF FAILED: {proof.id}') if failure_info and failure_log is not None: for line in failure_log: print(line) From aef5cb4911f50d26172d6b83f1cc9d5cb91f1b94 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Wed, 25 Oct 2023 18:44:07 +0200 Subject: [PATCH 02/19] remove old code --- kevm-pyk/src/kevm_pyk/__main__.py | 18 +----------------- 1 file changed, 1 insertion(+), 17 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index 4c35ca44fc..4f3f03eb1a 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -1,7 +1,6 @@ from __future__ import annotations import abc -import contextlib import dataclasses import json import logging @@ -14,7 +13,6 @@ from typing import TYPE_CHECKING import multiprocess # type: ignore -import pathos # type: ignore from pyk.cli.utils import file_path from pyk.cterm import CTerm from pyk.kast.outer import KApply, KRewrite, KSort, KToken @@ -45,7 +43,7 @@ if TYPE_CHECKING: from argparse import Namespace - from collections.abc import Callable, Iterable, Iterator + from collections.abc import Callable, Iterable from typing import Any, Final, Mapping, TypeVar from pyk.kast.outer import KClaim @@ -189,20 +187,6 @@ def exec_prove_legacy( raise SystemExit(1) -class ZeroProcessPool: - def map(self, f: Callable[[Any], Any], xs: list[Any]) -> list[Any]: - return [f(x) for x in xs] - - -@contextlib.contextmanager -def wrap_process_pool(workers: int) -> Iterator[ZeroProcessPool | pathos.pools.ProcessPool]: - if workers <= 1: - yield ZeroProcessPool() - else: - with pathos.pools.ProcessPool(ncpus=workers) as pp: - yield pp - - class TodoQueueTask(abc.ABC): ... From a91e921cf1dadcff32c531f15f9329e13de199f9 Mon Sep 17 00:00:00 2001 From: devops Date: Wed, 25 Oct 2023 17:44:58 +0000 Subject: [PATCH 03/19] Set Version: 1.0.328 --- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/__init__.py | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index ab75470ad7..c05f4f6b06 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.327" +version = "1.0.328" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index d27ad28287..90c6120254 100644 --- a/kevm-pyk/src/kevm_pyk/__init__.py +++ b/kevm-pyk/src/kevm_pyk/__init__.py @@ -6,4 +6,4 @@ from typing import Final -VERSION: Final = '1.0.327' +VERSION: Final = '1.0.328' diff --git a/package/version b/package/version index 6698d2ca16..6300eb8079 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.327 +1.0.328 From 8fcc95a81279ae958cb9e72d1ff85f242c467b92 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Wed, 25 Oct 2023 20:29:17 +0200 Subject: [PATCH 04/19] pyupgrade --- kevm-pyk/src/kevm_pyk/__main__.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index 4f3f03eb1a..6b6f4a882a 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -43,8 +43,8 @@ if TYPE_CHECKING: from argparse import Namespace - from collections.abc import Callable, Iterable - from typing import Any, Final, Mapping, TypeVar + from collections.abc import Callable, Iterable, Mapping + from typing import Any, Final, TypeVar from pyk.kast.outer import KClaim from pyk.kcfg.kcfg import NodeIdLike From f679e95ad05227529ef6e6bdbf953bbbdc09e4b0 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Thu, 26 Oct 2023 14:49:11 +0200 Subject: [PATCH 05/19] fix missing module name --- kevm-pyk/src/kevm_pyk/__main__.py | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index 6b6f4a882a..22da2080d7 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -5,6 +5,7 @@ import json import logging import multiprocessing +import os import sys import tempfile import time @@ -284,9 +285,11 @@ def is_functional(claim: KClaim) -> bool: _LOGGER.info(f'Extracting claims from file: {spec_file}') + spec_module_name = spec_module if spec_module is not None else os.path.splitext(spec_file.name)[0].upper() + all_claims = kevm.get_claims( spec_file, - spec_module_name=spec_module, + spec_module_name=spec_module_name, include_dirs=include_dirs, md_selector=md_selector, claim_labels=None, @@ -294,12 +297,12 @@ def is_functional(claim: KClaim) -> bool: ) spec_modules = kevm.get_claim_modules( - spec_file, spec_module_name=spec_module, include_dirs=include_dirs, md_selector=md_selector + spec_file, spec_module_name=spec_module_name, include_dirs=include_dirs, md_selector=md_selector ) - all_claims_by_id: Mapping[str, KClaim] = {f'{spec_module}.{claim.label}': claim for claim in all_claims} + all_claims_by_id: Mapping[str, KClaim] = {f'{spec_module_name}.{claim.label}': claim for claim in all_claims} - claims_graph = claim_dependency_dict(all_claims, spec_module_name=spec_module) + claims_graph = claim_dependency_dict(all_claims, spec_module_name=spec_module_name) proofs: list[APRProof] = APRProof.from_spec_modules( kevm.definition, spec_modules, spec_labels=claim_labels, logs={}, proof_dir=save_directory ) From b953bb76b33456cdc7a6246f12011e5794d10844 Mon Sep 17 00:00:00 2001 From: devops Date: Thu, 26 Oct 2023 12:51:33 +0000 Subject: [PATCH 06/19] Set Version: 1.0.329 --- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/__init__.py | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index c05f4f6b06..688c8fc155 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.328" +version = "1.0.329" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index 90c6120254..73295fdf0a 100644 --- a/kevm-pyk/src/kevm_pyk/__init__.py +++ b/kevm-pyk/src/kevm_pyk/__init__.py @@ -6,4 +6,4 @@ from typing import Final -VERSION: Final = '1.0.328' +VERSION: Final = '1.0.329' diff --git a/package/version b/package/version index 6300eb8079..fa8116d633 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.328 +1.0.329 From 37b03b3a3b9dfa517efa0f5e74b95ebfce7cc515 Mon Sep 17 00:00:00 2001 From: devops Date: Thu, 26 Oct 2023 13:56:26 +0000 Subject: [PATCH 07/19] Set Version: 1.0.329 --- package/version | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/package/version b/package/version index 4cb34c1ea2..fa8116d633 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.330 +1.0.329 From 61a09fe429299f73e09d380e16ce13ef9573f89f Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Thu, 26 Oct 2023 15:57:18 +0200 Subject: [PATCH 08/19] broken string --- kevm-pyk/pyproject.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 2711812e37..a967e85b08 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.330 +version = "1.0.330" description = "" authors = [ "Runtime Verification, Inc. ", From c2c6c7361397d4c88df6932edfdac6b4a415d5b0 Mon Sep 17 00:00:00 2001 From: devops Date: Thu, 26 Oct 2023 13:57:52 +0000 Subject: [PATCH 09/19] Set Version: 1.0.329 --- kevm-pyk/pyproject.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index a967e85b08..688c8fc155 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.330" +version = "1.0.329" description = "" authors = [ "Runtime Verification, Inc. ", From c765a7d7684caecff3b9b0145b504520214452ff Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Thu, 26 Oct 2023 15:58:56 +0200 Subject: [PATCH 10/19] broken string --- kevm-pyk/src/kevm_pyk/__init__.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index 5926f0f8fe..fc225b4d0c 100644 --- a/kevm-pyk/src/kevm_pyk/__init__.py +++ b/kevm-pyk/src/kevm_pyk/__init__.py @@ -6,4 +6,4 @@ from typing import Final -VERSION: Final = '1.0.330 +VERSION: Final = '1.0.330' From a77465794069a465bd800dbd7655d0a07f25f692 Mon Sep 17 00:00:00 2001 From: devops Date: Thu, 26 Oct 2023 13:59:35 +0000 Subject: [PATCH 11/19] Set Version: 1.0.329 --- kevm-pyk/src/kevm_pyk/__init__.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index fc225b4d0c..73295fdf0a 100644 --- a/kevm-pyk/src/kevm_pyk/__init__.py +++ b/kevm-pyk/src/kevm_pyk/__init__.py @@ -6,4 +6,4 @@ from typing import Final -VERSION: Final = '1.0.330' +VERSION: Final = '1.0.329' From f37bd5c6943a6710fc7c54eb12f8e11458f086dd Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Sat, 28 Oct 2023 16:38:52 +0200 Subject: [PATCH 12/19] fix newer poetry complaining about relative paths --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index a4798dc7a7..31a95d43f8 100644 --- a/Makefile +++ b/Makefile @@ -5,7 +5,7 @@ all: poetry # -------- PYTHON_BIN := python3.10 -KEVM_PYK_DIR := ./kevm-pyk +KEVM_PYK_DIR := $(abspath ./kevm-pyk) POETRY := poetry -C $(KEVM_PYK_DIR) POETRY_RUN := $(POETRY) run -- From b3bdbbb2c9967a00961ac856327b5c0f17c858f2 Mon Sep 17 00:00:00 2001 From: devops Date: Sat, 28 Oct 2023 14:39:28 +0000 Subject: [PATCH 13/19] Set Version: 1.0.330 --- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/__init__.py | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 688c8fc155..a967e85b08 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.329" +version = "1.0.330" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index 73295fdf0a..fc225b4d0c 100644 --- a/kevm-pyk/src/kevm_pyk/__init__.py +++ b/kevm-pyk/src/kevm_pyk/__init__.py @@ -6,4 +6,4 @@ from typing import Final -VERSION: Final = '1.0.329' +VERSION: Final = '1.0.330' diff --git a/package/version b/package/version index fa8116d633..4cb34c1ea2 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.329 +1.0.330 From 9eb4125a04fd26672b1011ad616a8622256a820e Mon Sep 17 00:00:00 2001 From: devops Date: Mon, 30 Oct 2023 09:23:32 +0000 Subject: [PATCH 14/19] Set Version: 1.0.330 --- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/__init__.py | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index b59236e6e4..a967e85b08 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.331" +version = "1.0.330" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index 13a6abed14..fc225b4d0c 100644 --- a/kevm-pyk/src/kevm_pyk/__init__.py +++ b/kevm-pyk/src/kevm_pyk/__init__.py @@ -6,4 +6,4 @@ from typing import Final -VERSION: Final = '1.0.331' +VERSION: Final = '1.0.330' diff --git a/package/version b/package/version index 4501612766..4cb34c1ea2 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.331 +1.0.330 From 350f40b14404e9d8ba1fcb8dfe5c652ae7138b6a Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Mon, 30 Oct 2023 14:56:19 +0100 Subject: [PATCH 15/19] fixes; use only multiprocess (instead of multiprocessing) --- kevm-pyk/src/kevm_pyk/__main__.py | 22 +++++++++++++--------- 1 file changed, 13 insertions(+), 9 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index 22da2080d7..252748ee0e 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -4,7 +4,6 @@ import dataclasses import json import logging -import multiprocessing import os import sys import tempfile @@ -215,13 +214,13 @@ class DoneQueueTaskFinished(DoneQueueTask): class MyEnvironment: number_of_workers: int - to_do_queue: multiprocessing.Queue # only instances of TodoQueueTask go there - done_queue: multiprocessing.Queue # only instances of DoneQueueTask go there + #to_do_queue: multiprocessing.Queue # only instances of TodoQueueTask go there + #done_queue: multiprocessing.Queue # only instances of DoneQueueTask go there def __init__(self, number_of_workers: int): self.number_of_workers = number_of_workers - self.to_do_queue = multiprocessing.Queue() - self.done_queue = multiprocessing.Queue() + self.to_do_queue = multiprocess.Queue() + self.done_queue = multiprocess.Queue() def exec_prove( @@ -300,7 +299,9 @@ def is_functional(claim: KClaim) -> bool: spec_file, spec_module_name=spec_module_name, include_dirs=include_dirs, md_selector=md_selector ) - all_claims_by_id: Mapping[str, KClaim] = {f'{spec_module_name}.{claim.label}': claim for claim in all_claims} + #all_claims_by_id: Mapping[str, KClaim] = {f'{spec_module_name}.{claim.label}': claim for claim in all_claims} + all_claims_by_id: Mapping[str, KClaim] = {claim.label: claim for claim in all_claims} + _LOGGER.warning(f'claims by id (keys): {all_claims_by_id.keys()}') claims_graph = claim_dependency_dict(all_claims, spec_module_name=spec_module_name) proofs: list[APRProof] = APRProof.from_spec_modules( @@ -402,8 +403,11 @@ def worker(env: MyEnvironment) -> None: case TodoQueueStop(): return case TodoQueueProofTask(proof_id): - passed, failure_log = _init_and_run_proof(all_claims_by_id[proof_id]) - env.done_queue.put(DoneQueueTaskFinished(proof_id=proof_id, passed=passed, failure_log=failure_log)) + try: + passed, failure_log = _init_and_run_proof(all_claims_by_id[proof_id]) + env.done_queue.put(DoneQueueTaskFinished(proof_id=proof_id, passed=passed, failure_log=failure_log)) + except Exception as e: + env.done_queue.put(DoneQueueTaskFinished(proof_id=proof_id, passed=False, failure_log=[str(e)])) def coordinator(env: MyEnvironment, proofs_to_do: list[APRProof]) -> list[tuple[bool, list[str] | None]]: id_to_proof: dict[str, APRProof] = {pf.id: pf for pf in proofs_to_do} @@ -462,7 +466,7 @@ def take_all_proven_from_queue() -> int: env.to_do_queue.put(TodoQueueStop()) return [finished_proof_ids[p.id] for p in proofs_to_do] - # ctx = multiprocessing.get_context('spawn') + #return None env = MyEnvironment(number_of_workers=workers) worker_processes = [multiprocess.Process(target=worker, args=(env,)) for _ in range(workers)] for w in worker_processes: From d6fe325a0d553ec16872d4d04fd5f1a39caaa808 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Mon, 30 Oct 2023 15:27:09 +0100 Subject: [PATCH 16/19] format --- kevm-pyk/src/kevm_pyk/__main__.py | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index 252748ee0e..5794dd4aa0 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -214,8 +214,8 @@ class DoneQueueTaskFinished(DoneQueueTask): class MyEnvironment: number_of_workers: int - #to_do_queue: multiprocessing.Queue # only instances of TodoQueueTask go there - #done_queue: multiprocessing.Queue # only instances of DoneQueueTask go there + # to_do_queue: multiprocessing.Queue # only instances of TodoQueueTask go there + # done_queue: multiprocessing.Queue # only instances of DoneQueueTask go there def __init__(self, number_of_workers: int): self.number_of_workers = number_of_workers @@ -299,7 +299,7 @@ def is_functional(claim: KClaim) -> bool: spec_file, spec_module_name=spec_module_name, include_dirs=include_dirs, md_selector=md_selector ) - #all_claims_by_id: Mapping[str, KClaim] = {f'{spec_module_name}.{claim.label}': claim for claim in all_claims} + # all_claims_by_id: Mapping[str, KClaim] = {f'{spec_module_name}.{claim.label}': claim for claim in all_claims} all_claims_by_id: Mapping[str, KClaim] = {claim.label: claim for claim in all_claims} _LOGGER.warning(f'claims by id (keys): {all_claims_by_id.keys()}') @@ -405,7 +405,9 @@ def worker(env: MyEnvironment) -> None: case TodoQueueProofTask(proof_id): try: passed, failure_log = _init_and_run_proof(all_claims_by_id[proof_id]) - env.done_queue.put(DoneQueueTaskFinished(proof_id=proof_id, passed=passed, failure_log=failure_log)) + env.done_queue.put( + DoneQueueTaskFinished(proof_id=proof_id, passed=passed, failure_log=failure_log) + ) except Exception as e: env.done_queue.put(DoneQueueTaskFinished(proof_id=proof_id, passed=False, failure_log=[str(e)])) @@ -466,7 +468,7 @@ def take_all_proven_from_queue() -> int: env.to_do_queue.put(TodoQueueStop()) return [finished_proof_ids[p.id] for p in proofs_to_do] - #return None + # return None env = MyEnvironment(number_of_workers=workers) worker_processes = [multiprocess.Process(target=worker, args=(env,)) for _ in range(workers)] for w in worker_processes: From 1917ed2b0c32fd06e29e48e80abe7823ea2a3686 Mon Sep 17 00:00:00 2001 From: devops Date: Mon, 30 Oct 2023 14:27:33 +0000 Subject: [PATCH 17/19] Set Version: 1.0.331 --- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/__init__.py | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index a967e85b08..b59236e6e4 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.330" +version = "1.0.331" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index fc225b4d0c..13a6abed14 100644 --- a/kevm-pyk/src/kevm_pyk/__init__.py +++ b/kevm-pyk/src/kevm_pyk/__init__.py @@ -6,4 +6,4 @@ from typing import Final -VERSION: Final = '1.0.330' +VERSION: Final = '1.0.331' diff --git a/package/version b/package/version index 4cb34c1ea2..4501612766 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.330 +1.0.331 From e9daa414005bcfbd11ecba5d0606d23906c6ccf8 Mon Sep 17 00:00:00 2001 From: devops Date: Mon, 30 Oct 2023 14:37:14 +0000 Subject: [PATCH 18/19] Set Version: 1.0.331 --- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/__init__.py | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 95080548ce..b59236e6e4 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.332" +version = "1.0.331" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index d0cab81dab..13a6abed14 100644 --- a/kevm-pyk/src/kevm_pyk/__init__.py +++ b/kevm-pyk/src/kevm_pyk/__init__.py @@ -6,4 +6,4 @@ from typing import Final -VERSION: Final = '1.0.332' +VERSION: Final = '1.0.331' diff --git a/package/version b/package/version index 51dda02714..4501612766 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.332 +1.0.331 From 3fc73bd720975cbbc0a8e72e07ec342662f20ecd Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Tue, 31 Oct 2023 11:51:13 +0100 Subject: [PATCH 19/19] finish merging until it type checks --- kevm-pyk/src/kevm_pyk/__main__.py | 29 +++++++++++++++-------------- 1 file changed, 15 insertions(+), 14 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index 6c221316d8..ecdc88edec 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -27,7 +27,7 @@ from pyk.proof.equality import EqualityProof from pyk.proof.show import APRProofShow from pyk.proof.tui import APRProofViewer -from pyk.utils import FrozenDict, hash_str, single, unique +from pyk.utils import FrozenDict, hash_str, single from . import VERSION, config, kdist from .cli import KEVMCLIArgs, node_id_like @@ -478,18 +478,20 @@ def worker(env: MyEnvironment) -> None: DoneQueueTaskFinished(claim_label=claim_label, passed=passed, failure_log=failure_log) ) except Exception as e: - env.done_queue.put(DoneQueueTaskFinished(claim_label=claim_label, passed=False, failure_log=[str(e)])) + env.done_queue.put( + DoneQueueTaskFinished(claim_label=claim_label, passed=False, failure_log=[str(e)]) + ) def coordinator(env: MyEnvironment, jobs_to_do: list[KClaimJob]) -> list[tuple[bool, list[str] | None]]: - id_to_job: dict[str, KClaimJob] = {job.claim.label : job for job in jobs_to_do} + id_to_job: dict[str, KClaimJob] = {job.claim.label: job for job in jobs_to_do} remaining_job_labels: set[str] = {job.claim.label for job in jobs_to_do} finished_job_labels: dict[str, tuple[bool, list[str] | None]] = {} def get_a_ready_id() -> str | None: - for proof_id in remaining_job_labels: - if set(id_to_proof[proof_id].subproof_ids).issubset(finished_job_labels.keys()): - remaining_job_labels.remove(proof_id) - return proof_id + for job_label in remaining_job_labels: + if set({d.claim.label for d in id_to_job[job_label].dependencies}).issubset(finished_job_labels.keys()): + remaining_job_labels.remove(job_label) + return job_label return None def put_all_ready_into_queue() -> int: @@ -503,8 +505,8 @@ def put_all_ready_into_queue() -> int: def process_incoming_message(msg: DoneQueueTask) -> bool: match msg: - case DoneQueueTaskFinished(proof_id=proof_id, passed=passed, failure_log=failure_log): - finished_job_labels[proof_id] = (passed, failure_log) + case DoneQueueTaskFinished(claim_label=claim_label, passed=passed, failure_log=failure_log): + finished_job_labels[claim_label] = (passed, failure_log) return True return False @@ -535,20 +537,19 @@ def take_all_proven_from_queue() -> int: # Now we want to stop all the workers for _ in range(env.number_of_workers): env.to_do_queue.put(TodoQueueStop()) - return [finished_job_labels[p.id] for p in proofs_to_do] - + return [finished_job_labels[job.claim.label] for job in jobs_to_do] env = MyEnvironment(number_of_workers=workers) worker_processes = [multiprocess.Process(target=worker, args=(env,)) for _ in range(workers)] for w in worker_processes: w.start() - jobs: list[KClaimJob] = [] - results = coordinator(env, proofs) + all_claim_jobs_list = list(all_claim_jobs) + results = coordinator(env, all_claim_jobs_list) for w in worker_processes: w.join() failed = 0 - for job, r in zip(jobs, results, strict=True): + for job, r in zip(all_claim_jobs_list, results, strict=True): passed, failure_log = r if passed: print(f'PROOF PASSED: {job.claim.label}')