Multithreading for KeY: combined preview with the performance series

.github/workflows/tests.yml

@@ -78,7 +78,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        test: [ testProveRules, testRunAllFunProofs, testRunAllInfProofs, testRunAllWdProofs ]
+        test: [ testProveRules, testRunAllFunProofs, testRunAllInfProofs, testRunAllWdProofs, testMtStress ]
         os: [ ubuntu-latest ]
         java: [ 21 ]
     runs-on: ${{ matrix.os }}

build.gradle

@@ -123,6 +123,11 @@ subprojects {
         systemProperty "RUNALLPROOFS_DIR", layout.buildDirectory.dir("report/runallproves").get().toString()
 
         systemProperty "key.disregardSettings", "true"
+        // Pin the whole test suite to the single-threaded prover, so no test silently runs on the
+        // multi-core prover (e.g. merge-rule, slicing and symbolic-execution tests rely on single
+        // core). Opt-in parallel tests (equivalence, stress, benchmark) set this property at runtime,
+        // which overrides the baseline within their fork.
+        systemProperty "key.prover.parallel", "false"
         maxHeapSize = "4g"
 
         forkEvery = 0 //default

key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/JavaInfFlowProfile.java

@@ -18,6 +18,13 @@ public class JavaInfFlowProfile extends JavaProfile {
     public static final String NAME = "Java InfFlow Profile";
     public static final String PROFILE_ID = "java-infflow";
 
+    @Override
+    public boolean supportsParallelAutomode() {
+        // Information-flow proofs use side-proof machinery that is not thread-safe: keep
+        // single-core.
+        return false;
+    }
+
     @Override
     public String ident() {
         return PROFILE_ID;

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/profile/SimplifyTermProfile.java

@@ -57,6 +57,12 @@ public SimplifyTermProfile() {
     /**
      * {@inheritDoc}
      */
+    @Override
+    public boolean supportsParallelAutomode() {
+        // Symbolic-execution term-simplification profile: keep single-core (not audited).
+        return false;
+    }
+
     @Override
     protected ImmutableList<TermLabelConfiguration> computeTermLabelConfiguration() {
         ImmutableList<TermLabelConfiguration> result = super.computeTermLabelConfiguration();

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/profile/SymbolicExecutionJavaProfile.java

@@ -111,6 +111,13 @@ protected ImmutableSet<GoalChooserFactory<Proof, Goal>> computeSupportedGoalChoo
                 .add(new SymbolicExecutionGoalChooserFactory());
     }
 
+    @Override
+    public boolean supportsParallelAutomode() {
+        // The symbolic-execution debugger profile builds a shared SE tree during search and is not
+        // audited for thread-safety: keep single-core.
+        return false;
+    }
+
     /**
      * {@inheritDoc}
      */

key.core.wd/src/main/java/de/uka/ilkd/key/wd/WdProfile.java

@@ -61,6 +61,12 @@ public WdProfile() {
             defRules.standardBuiltInRules());
     }
 
+    @Override
+    public boolean supportsParallelAutomode() {
+        // Well-definedness checks are not yet audited for thread-safety: keep single-core.
+        return false;
+    }
+
     @Override
     public String ident() {
         return PROFILE_ID;

key.core/build.gradle

@@ -10,6 +10,7 @@ dependencies {
     api project(':key.util')
     api project(':key.ncore')
     api project(':key.ncore.calculus')
+    api project(':key.ncore.compiler')
 
     antlr4 "org.antlr:antlr4:4.13.2"
     api "org.antlr:antlr4-runtime:4.13.2"
@@ -97,6 +98,30 @@ classes.dependsOn << generateSolverPropsList
 
 tasks.withType(Test) {
     enableAssertions = true
+    // The whole suite is pinned to the single-threaded prover in the root build (key.prover.parallel
+    // = false); opt-in parallel tests override it at runtime. The forwarding loop below still lets
+    // the Gradle command line override it (e.g. -Dkey.prover.parallel=true).
+    // Forward the multithreading / parallel-prover properties from the Gradle command line to the
+    // test JVM (Gradle does not propagate -D automatically). Lets one run e.g.
+    //   ./gradlew :key.core:test --tests '*MtSpeedupBenchmark' -Dkey.mt.benchmark=true
+    // or toggle the parallel prover for any test via -Dkey.prover.parallel(.threads).
+    ["key.mt.benchmark", "key.mt.benchmark.threads", "key.mt.benchmark.proofs",
+     "key.mt.benchmark.maxsteps",
+     "key.mt.synth.splits", "key.mt.synth.worksplits", "key.mt.synth.work",
+     "key.mt.synth.linear", "key.mt.synth.loop",
+     "key.mt.jfr.probe", "key.mt.jfr.proof", "key.mt.jfr.workers", "key.mt.jfr.reps",
+     "key.prover.parallel", "key.prover.parallel.threads"].each { p ->
+        if (System.getProperty(p) != null) {
+            systemProperty(p, System.getProperty(p))
+        }
+    }
+    // Record a Flight Recording of the test JVM when -Dkey.mt.jfr=<file> is given. Used to profile
+    // the parallel prover's lock contention and hot paths (see MtJfrProbe).
+    if (System.getProperty("key.mt.jfr") != null) {
+        jvmArgs += ["-XX:StartFlightRecording=filename=${System.getProperty('key.mt.jfr')}," +
+                    "settings=profile,dumponexit=true,disk=true",
+                    "-XX:FlightRecorderOptions=stackdepth=128"]
+    }
     // Forward retention-probe knobs (see MtRetentionProbe) to the test JVM.
     systemProperties += System.properties.findAll { it.key.toString().startsWith("key.mt.retention") }
     if (project.hasProperty("stressHeap")) {
@@ -149,6 +174,26 @@ tasks.register('testStrictSMT', Test) {
     }
 }
 
+// Stress test for the goal-level parallel prover: run a few large splitting proofs many times at a
+// high (over-subscribed) worker count and assert each one closes. Slow (minutes), so it is gated out
+// of the normal unit-test suite and only runs here. Guards against reintroducing a concurrency race
+// that makes proofs nondeterministically fail to close. See MtStressTest.
+tasks.register('testMtStress', Test) {
+    description = 'Stress the parallel prover at high worker counts to catch non-closure races'
+    group = 'verification'
+    systemProperty("key.mt.stress", "true")
+    maxParallelForks = 1
+    // Each class proves many full proofs; give every test class a fresh JVM so global KeY state
+    // (settings, static caches/interners, the script parser) cannot leak between classes -- e.g.
+    // MtScriptStressTest's position-sensitive script must not inherit state from earlier classes.
+    forkEvery = 1
+    filter {
+        includeTestsMatching "MtStressTest"
+        includeTestsMatching "MtMacroStressTest"
+        includeTestsMatching "MtScriptStressTest"
+    }
+}
+
 //Generation of the three version files within the resources by executing `git'.
 tasks.register('generateVersionFiles') {
     def outputFolder = file("build/resources/main/de/uka/ilkd/key/util")
@@ -250,14 +295,21 @@ tasks.register("testRAP", Test) {
     dependsOn('generateRAPUnitTests', 'testClasses')
 
     forkEvery = 1
-    maxParallelForks = 2
+    // run the regression proofs on up to 10 parallel JVMs (overridable with -PrapForks=N);
+    // for clean perfTest timing reproduction use -PrapForks=1
+    maxParallelForks = (project.findProperty('rapForks') ?: '10') as int
     useJUnitPlatform()
     it.filter {
         it.includeTestsMatching "de.uka.ilkd.key.proof.runallproofs.gen.*"
     }
-    // set heap size for the test JVM(s)
+    // forward the compiled-matcher switch to the (in-process) proof runs in each fork; default
+    // off, enable with -Pmatcher.compiled=true (or -Dkey.matcher.compiled=true)
+    systemProperty 'key.matcher.compiled',
+        (project.findProperty('matcher.compiled')
+                ?: System.getProperty('key.matcher.compiled', 'false'))
+    // set heap size for the test JVM(s) (overridable with -PrapHeap=8g for the large examples)
     minHeapSize = "1g"
-    maxHeapSize = "3g"
+    maxHeapSize = (project.findProperty('rapHeap') ?: '3g')
 
     // set JVM arguments for the test JVM(s)
     //jvmArgs('-XX:MaxPermSize=1g')