Multithreading for KeY#3842
Open
unp1 wants to merge 15 commits into
Open
Conversation
The active statement (and its position) were eagerly computed when a node's rule application was set, on the proving path. Compute them lazily on first access instead; nodes whose active statement is never inspected do no work.
The loop-invariant rule cached the last instantiation in a static field shared across proofs, which could leak an instantiation between unrelated proofs. Store it on the rule application instead.
Give the MethodCall metaconstruct a fresh per-application copy instead of mutating shared instance state, make the class final to lock in that argument, and make JmlAssert's condition final.
A stored settings value may deserialize as Integer or Long depending on its magnitude and the format, but the numeric property converters assumed a fixed boxed type and threw a ClassCastException on the other -- which could crash KeY on startup while loading the settings. Accept any Number instead.
A recent-file entry whose profile name was never set serialized the null value as the string "null"; reloading it then tried to resolve a profile named "null", failed, and showed an error dialog instead of opening the file. Treat a missing profile name (null or the legacy "null" string) as "use the default profile" on load, and stop writing the "null" placeholder when saving.
After a compound macro finished, the status line kept the partial count from the macro's last internal strategy pass (e.g. "Applied 2 rules, 1 goal" even though the macro had closed thousands) instead of the macro's own aggregate. Display the ProofMacroFinishedInfo's aggregate result when a macro completes.
ConcurrentLruCache (exact-LRU, single-lock, drop-in for synchronizedMap over an LRUCache) for eviction-sensitive caches, StripedLruCache for pure caches, and WeakValueInterner for identity-preserving interning under concurrency, with concurrency tests.
unp1
changed the title
Add the parallelProverEnabled / parallelProverThreadCount settings and a Profile.supportsParallelAutomode() capability: the standard Java profile opts in, the well-definedness, information-flow and symbolic-execution profiles keep the single-core fallback.
Add EssentialProofListener and Proof.suspendNonEssentialListeners(), which detaches every proof-tree and rule-app listener not tagged essential for the duration of a run and re-attaches them afterwards, so nothing unrelated to proving fires on a worker thread.
ParallelProver runs automatic proof search on a worker pool, one open goal per worker, behind the AutoProvers selection seam. A single GoalScheduler monitor hands out goals depth-first; Goal.apply is split into a concurrent compute phase and a commit phase serialized on one lock; fresh names come from a partitioned per-proof allocator (atomic Counter), namespace flushes are deferred, and the merge rule is disabled during parallel runs. The taclet-index cache key is immutable so siblings sharing the cache set cannot race on it. Includes the scheduler unit test and the proof-equivalence gate.
Harden the shared state the workers touch during search: route the matching and cost-path caches through the thread-safe cache utilities, intern parametric operators and elementary updates identity-preservingly, give the per-call instantiation caches and counters safe publication or per-worker copies, and guard the specification repository's proving-time maps. Behaviour-preserving.
Add a settings pane and a clickable status-line indicator to switch between the single-core and multi-core prover, a --threads CLI option, and gating of the single-core-only features: proof caching, slicing and the merge rule are disabled (with explanatory tooltips, updated live) while the multi-core prover is active, and restored when switching back.
Route StrategyProofMacro and TryCloseMacro through the AutoProvers seam. The try-close prune stays safe because start() only returns once every worker has stopped, so no worker is live during the tree mutation; a stress test exercises the prune-and-close path at eight workers.
Add the real-proof speedup benchmark, the synthetic best/worst-case benchmark, a JFR profiling probe, and a high-worker non-closure stress test wired into the CI integration-test matrix. Pin the test suite to the single-core prover by default; opt-in parallel tests override it at runtime.
Member
The idea of a worker pool is to have a fix/max amount of threads, and to dispatch work on them.
|
Member
Author
no that is just the starting idea. Depending on the amounts of threads you configure to use, you have that nr of threads and it is capped at the number of processor cores of your computer. Then there is a worker pool and a lifo queue from which a free worker is assigned the next goal. I'll clarify the description thanks.
not yet. The first milestone was to get to a point where we have for some problems a win and KeY is (at least as far as one can test) race free. The problem is, I did not have any race conditions even under high pressure. But the problem is that other OSes with other schedulers might discover some still existing problems, so if someone has time and can just run it once in a while to get feedback, would be appreciated. For trying out, I recommend the preview integration with the single core improvemnts. It solves some congestions here already. |
Member
|
Could you provide the command to be executed? I could try to get a 64-core machine if we would have proofs having such number of goals. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Intended Change
This pull request adds a multi-core (parallel) prover to KeY: automatic proof
search runs on a worker pool. An open goal is either not yet assigned to a worker or
it has exactly one worker, proving independent
sibling goals concurrently. There are at most as many workers as configured and the number of workers is capped at the number of processor cores. It is a port and modernisation of the 2018
HacKeYthon multithreading prototype, rebuilt on current
main.The legacy single-threaded prover stays the default and the safe fallback;
the multi-core prover is opt-in per the configuration below.
Architecture (conceptual)
The guiding principle is isolation, not locking.
Goal.applyis split into aconcurrent compute phase (rule selection + matching, the expensive part) and a
commit phase (proof-tree mutation) serialized under a single lock. A
single-monitor
GoalSchedulerhands goals to workers depth-first. Non-essentiallisteners are detached for the run, fresh names come from a per-worker partition
of the name allocator, shared matching/cost caches use thread-safe cache
utilities, and rules not yet concurrency-safe (the merge rule) disable themselves
during a multi-worker run. Only the standard Java profile runs in parallel.
Full conceptual write-up: Multi-Core Proving (key-docs).
Problems encountered, fixed and verified
cache key and raced on it → a dropped goal and a nondeterministic non-closure.
Fixed with an immutable per-lookup key. Reproduced in ~50% of 8-worker runs
before, 0 after; guarded by a CI stress test.
single atomic step under the scheduler monitor.
proving state; each is a separate, behaviour-preserving commit.
Goal, outsidethe proof-level suspension) fired on worker threads and touched Swing off the
event-dispatch thread. The suspension now covers them too, and the views refresh
once from the final proof state after a run.
Single-core-only features
Proof caching, proof slicing and the merge rule are switched off while the
multi-core prover is active (GUI greys them out with a tooltip; the status line
shows the mode) and restored when switching back. Loading a proof script and
running macros use the multi-core prover when active and the profile supports it,
with one deliberate exception:
TryClose(and theFull Autopilot that ends init) closes goals one at a time under a tight per-goal step budget and is pinned to
the single-core prover — a single goal offers no parallelism, and several workers
exploring its subtree apply rules less step-efficiently and can exhaust the budget
before the goal closes. Either way a run returns only once all workers stop, so
pruning sees a quiescent proof. These restrictions will be lifted incrementally
with the feature owners once the
subset is confirmed safe. Because the default is single-core, these features
work exactly as before.
Configuration
SC/MT N×status-line indicator.
--threads N.-Dkey.prover.parallel[.threads]overrides.Benchmarks
Measured on a 16-core machine, one isolated run per proof (each proof loaded in a
clean settings state). Cells show wall-clock time with the speedup vs the
single-threaded
mainin parentheses;mainis the single-threaded prover (themulti-core prover does not change the single-threaded path).
Real-world proofs — automode (wall time).
The 4× column is the sweet spot: wide, splitting proofs reach ~2–3×. Narrow
proofs gain little and can regress at 8× (see the shape table).
(
quicksort/sortis omitted — it needs its proof script to close, so it is not apure-automode entry.)
Diagrams. Rendered speedup bar charts are in the dev doc's Combined effect section.
Plan
Type of pull request
Ensuring quality
tests pass; full
key.core+ touched-module unit tests pass.opt-in); see the benchmark section for multi-core speedups.
Separable,
main-relevant fixes (kept as standalone commits for cherry-picking,useful even single-core):
cross-proof leak via a static field)
ClassCastException(present onmain) that can prevent KeY from launching whenloading certain settings files (Cherry-Picked on Fixes for minor regressions on main #3844)
entry without a profile serialized
nullas the string"null", so reloading (Cherry-Picked on Fixes for minor regressions on main #3844)it failed to resolve a profile and showed an error instead of opening the file
kept a macro's last internal-pass count instead of its aggregate result (Cherry-Picked on Fixes for minor regressions on main #3844)
Additional information and contact(s)
This PR provides a clear opt-in benefit (parallel speedup on splitting proofs)
with a safe fallback to the unchanged single-core prover.
This PR has been done with AI tooling support.
The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.