[unp1]

Intended Change

Improving scaling of the parallel prover. In particular some scripted proofs like verifyThis2026#update had even bad performance regression when scaling from 4 to 8 threads.

This PR improves scaling and avoids the regressions by introducing a generational cache where reading is lock free.
The cache class was implemented using AI and then used for the Term cache and some arithmetics related caches.

Automode time in ms, minimum of 2 rounds, with rep 2 of each JVM as the measurement. JDK 21.

Proof	Nodes	MT4 main	MT4 PR	MT4 Δ	MT8 main	MT8 PR	MT8 Δ	Scaling gain of PR
license	90,411	11,317	10,995	-2.8%	9,856	8,172	-17.1%	1.17×
bet	103,909	14,494	13,841	-4.5%	12,019	9,660	-19.6%	1.19×
jml-information-flow	19,079	1,831	1,764	-3.7%	1,741	1,379	-20.8%	1.22×
symmArray	13,499	1,871	1,650	-11.8%	1,745	1,471	-15.7%	1.05×
verifyThis26 update	94,024	4,432	2,801	-36.8%	7,441	1,948	-73.8%	2.41×
quicksort/sort	50,872	3,840	3,034	-21.0%	3,650	2,165	-40.7%	1.33×
quicksort/split	50,589	2,203	2,001	-9.2%	1,986	1,489	-25.0%	1.21×
Sum		39,988	36,086	-9.8%	38,438	26,284	-31.6%	1.32×

quicksort/sort and quicksort/split replay their proof scripts with the RAP settings. The other proofs run in automode.

Type of pull request

• New feature (non-breaking change which adds functionality)
• Breaking change (fix or feature that would cause existing functionality to change)
• There are changes to the (Java) code

Ensuring quality

• I made sure that introduced/changed code is well documented (javadoc and inline comments).
• I added new test case(s) for new functionality.
• I have checked that runtime performance has not deteriorated.

Additional information and contact(s)

The contributions within this pull request are licensed under GPLv2, or (at your option) any later version, for inclusion in KeY.

Generational cache create with AI tooling (August)