From 4ea4b2404304d320445b3aadaf56d6e217806172 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Sat, 1 Aug 2026 09:03:08 +0200 Subject: [PATCH 1/3] Changing strategies during a proof (interaction) may cause reusability of costs to change, avoid wrong caching hits --- .../de/uka/ilkd/key/java/ServiceCaches.java | 6 ++- .../de/uka/ilkd/key/strategy/CostReuse.java | 49 ++++++++++--------- 2 files changed, 31 insertions(+), 24 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ServiceCaches.java b/key.core/src/main/java/de/uka/ilkd/key/java/ServiceCaches.java index 3fe2d7a376f..75ca962199d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ServiceCaches.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ServiceCaches.java @@ -18,6 +18,7 @@ import de.uka.ilkd.key.proof.TermTacletAppIndexCacheSet; import de.uka.ilkd.key.rule.metaconstruct.arith.Monomial; import de.uka.ilkd.key.rule.metaconstruct.arith.Polynomial; +import de.uka.ilkd.key.strategy.CostReuse; import de.uka.ilkd.key.strategy.IfInstantiationCachePool; import de.uka.ilkd.key.strategy.feature.AbstractBetaFeature.TermInfo; import de.uka.ilkd.key.strategy.feature.AppliedRuleAppsNameCache; @@ -126,7 +127,8 @@ public class ServiceCaches implements SessionCaches { * this class (a {@code CostReuse.Eligibility}, or its ineligible sentinel) to keep this package * independent of the strategy package. */ - private final Map costReuseClassificationCache = new ConcurrentHashMap<>(); + private final Map costReuseClassificationCache = + new ConcurrentHashMap<>(); private final Map monomialCache = new ConcurrentLruCache<>(2000); @@ -243,7 +245,7 @@ public final Map getIntroductionTimeCache() { return introductionTimeCache; } - public final Map getCostReuseClassificationCache() { + public final Map getCostReuseClassificationCache() { return costReuseClassificationCache; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/CostReuse.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/CostReuse.java index 16ab6178326..36393fd51d4 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/CostReuse.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/CostReuse.java @@ -21,6 +21,7 @@ import org.key_project.prover.strategy.costbased.feature.StableCost; import org.key_project.prover.strategy.costbased.feature.VolatileCost; import org.key_project.prover.strategy.costbased.feature.WeakStableCost; +import org.key_project.prover.strategy.costbased.termgenerator.TermGenerator; import org.jspecify.annotations.Nullable; @@ -94,8 +95,16 @@ public record Eligibility(Feature[] vetoes, boolean weakStable) { } /** - * @param strategy the goal's strategy; classified against its cost dispatchers (only used to - * obtain those -- never dereferenced beyond {@link #dispatchers}) + * Secondary cache key for cost reuse eligibility is the strategy as a strategy change + * invalidates the previously established eligibility + */ + public record ConditionalEligibility(Strategy strategy, Eligibility verdict) { + } + + /** + * determines the eligibility of a taclet for cost reuse + * + * @param strategy the goal's strategy * @param proof the proof being worked on; supplies the per-proof classification cache * @param taclet the taclet whose cost is a candidate for reuse * @return how the taclet may reuse its cost, or {@code null} if it is not eligible at all. @@ -108,20 +117,16 @@ public record Eligibility(Feature[] vetoes, boolean weakStable) { if (disp.isEmpty()) { return null; } - // The verdict is cached in the PROOF's ServiceCaches, NOT a static map: a taclet's locality - // depends on the cost dispatchers in force (which differ with the taclet options), while - // Taclet#equals is only name + find term. A cache shared across proofs would let one option - // set read another's verdict for a same-named but structurally different taclet -- exactly - // the static-cache hazard ServiceCaches exists to avoid. Per proof, it is also freed with - // the proof. (ELIGIBLE => at least the top-level NonDuplicateApp veto, so the empty-veto - // INELIGIBLE acts as the "not eligible" sentinel, the map forbidding null values.) - final Map cache = proof.getServices().getCaches() + final Map cache = proof.getServices().getCaches() .getCostReuseClassificationCache(); - final Object e = cache.computeIfAbsent(taclet, t -> { - final Eligibility res = classify(disp, t); - return res == null ? INELIGIBLE : res; - }); - return e == INELIGIBLE ? null : (Eligibility) e; + final ConditionalEligibility cached = cache.get(taclet); + if (cached instanceof ConditionalEligibility c && + c.strategy() == strategy) { // cached result only valid if strategy did not change + return c.verdict() == INELIGIBLE ? null : (Eligibility) c.verdict(); + } + final Eligibility res = classify(disp, taclet); + cache.put(taclet, new ConditionalEligibility(strategy, res == null ? INELIGIBLE : res)); + return res; } private static @Nullable Eligibility classify(List dispatchers, @@ -161,8 +166,8 @@ private static void walk(CostClassifiable f, Set vetoes, boolean[] loca } switch (localityOf(f)) { case VOLATILE -> local[0] = false; - // Transparent: recurse into every child component -- a Feature, TermGenerator or - // ProjectionToTerm, all of which receive the goal -- and stay local only if they all + // Transparent: recurse into every child component; a Feature, TermGenerator or + // ProjectionToTerm, all of which receive the goal, and stay local only if they all // are. WEAK_STABLE additionally reads the whole find formula, so reuse is gated on // that formula being unchanged (see Eligibility). Children are discovered reflectively // (see forEachChild), so authors annotate locality and never enumerate children. @@ -221,7 +226,7 @@ private static void follow(@Nullable Object o, follow(e, action); } } - // Everything else is not a cost component and is not traversed -- notably TermFeature (its + // Everything else is not a cost component and is not traversed, notably TermFeature (its // compute() has no goal, so it is stable by construction), plus Name, RuleAppCost, ... } @@ -235,12 +240,12 @@ static void warnMismatch(Taclet taclet, Object reused, Object fresh) { } /** - * The cost dispatchers to classify against, taken from the strategy of the goal being costed. - * Must NOT be cached across strategies: different goals/proofs use different strategy instances + * The cost dispatchers to classify against, taken from the strategy of the goal on which + * the costs should be computed. + * Must not be cached across strategies: different goals/proofs use different strategy instances * (and some are not {@link ModularJavaDLStrategy} at all). A stale or empty cached value would * make the {@link #walk} traverse nothing and thus classify every taclet as (wrongly) local. - * When the strategy exposes no cost dispatchers, the taclet is treated as ineligible (see - * {@link #vetoesIfEligible}) -- never as trivially local. + * When the strategy exposes no cost dispatchers, the taclet is treated as ineligible. */ private static List dispatchers(Strategy strategy) { return strategy instanceof ModularJavaDLStrategy m ? m.costRuleSetDispatchers() : List.of(); From 24839187595a08fb9423903a7852c0cd27d80cbc Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Sat, 1 Aug 2026 09:47:39 +0200 Subject: [PATCH 2/3] Remove unused cache from EqualityConstraint --- .../EqualityConstraint.java | 82 +------------------ .../key/prover/mt/shared-state-allowlist.txt | 2 - 2 files changed, 3 insertions(+), 81 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/EqualityConstraint.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/EqualityConstraint.java index 9ad4e6611da..b2fff404d74 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/EqualityConstraint.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/EqualityConstraint.java @@ -42,9 +42,6 @@ @Deprecated public class EqualityConstraint implements Constraint { - /** contains a boolean value */ - private static final BooleanContainer CONSTRAINTBOOLEANCONTAINER = new BooleanContainer(); - /** * stores constraint content as a mapping from Metavariable to Term */ @@ -209,7 +206,7 @@ private JTerm instantiate(JTerm p, Services services) { */ @Override public Constraint unify(JTerm t1, JTerm t2, Services services) { - return unify(t1, t2, services, CONSTRAINTBOOLEANCONTAINER); + return unify(t1, t2, services, new BooleanContainer()); } /** @@ -651,7 +648,7 @@ public boolean isAsWeakAs(Constraint co) { */ @Override public Constraint join(Constraint co, Services services) { - return join(co, services, CONSTRAINTBOOLEANCONTAINER); + return join(co, services, new BooleanContainer()); } @@ -683,40 +680,9 @@ public synchronized Constraint join(Constraint co, Services services, return co.join(this, services); } - final ECPair cacheKey; - - lookup: synchronized (joinCacheMonitor) { - ecPair0.set(this, co); - Constraint res = joinCache.get(ecPair0); - - if (res == null) { - cacheKey = ecPair0.copy(); - res = joinCacheOld.get(cacheKey); - if (res == null) { - break lookup; - } - joinCache.put(cacheKey, res); - } - - unchanged.setVal(this == res); - return res; - } - final Constraint res = joinHelp((EqualityConstraint) co, services); - unchanged.setVal(res == this); - - synchronized (joinCacheMonitor) { - if (joinCache.size() > 1000) { - joinCacheOld.clear(); - final Map t = joinCacheOld; - joinCacheOld = joinCache; - joinCache = t; - } - - joinCache.put(cacheKey, res); - return res; - } + return res; } @@ -825,48 +791,6 @@ public String toString() { } - private static final class ECPair { - private Constraint first; - private Constraint second; - private int hash; - - public boolean equals(Object o) { - if (!(o instanceof ECPair e)) { - return false; - } - return first == e.first && second == e.second; - } - - public void set(Constraint first, Constraint second) { - this.first = first; - this.second = second; - this.hash = first.hashCode() + second.hashCode(); - } - - public int hashCode() { - return hash; - } - - public ECPair copy() { - return new ECPair(first, second, hash); - } - - public ECPair(Constraint first, Constraint second, int hash) { - this.first = first; - this.second = second; - this.hash = hash; - } - } - - private static final Object joinCacheMonitor = new Object(); - - // the methods using these caches seem not to be used anymore otherwise refactor and move it - // into ServiceCaches - private static Map joinCache = new ConcurrentLruCache<>(0); - private static Map joinCacheOld = new ConcurrentLruCache<>(0); - - private static final ECPair ecPair0 = new ECPair(null, null, 0); - @Override public int hashCode() { if (hashCode == null) { diff --git a/key.core/src/test/resources/de/uka/ilkd/key/prover/mt/shared-state-allowlist.txt b/key.core/src/test/resources/de/uka/ilkd/key/prover/mt/shared-state-allowlist.txt index 4564b76f6c3..f0b4c717ea9 100644 --- a/key.core/src/test/resources/de/uka/ilkd/key/prover/mt/shared-state-allowlist.txt +++ b/key.core/src/test/resources/de/uka/ilkd/key/prover/mt/shared-state-allowlist.txt @@ -28,8 +28,6 @@ de.uka.ilkd.key.logic.op.QualifierWrapper#INSTANCES # de.uka.ilkd.key.proof.calculus.JavaDLSequentKit#INSTANCE # assigned once at class-init; reads via synchronized getInstance() de.uka.ilkd.key.proof.init.JavaProfile#defaultInstance # lazy singleton; every access inside synchronized getDefaultInstance() de.uka.ilkd.key.proof.init.JavaProfile#defaultInstancePermissions # lazy singleton; every access inside synchronized getDefaultInstance() -de.uka.ilkd.key.strategy.quantifierHeuristics.EqualityConstraint#joinCache # every read/write inside synchronized(joinCacheMonitor) -de.uka.ilkd.key.strategy.quantifierHeuristics.EqualityConstraint#joinCacheOld # every read/write inside synchronized(joinCacheMonitor) # --- written only during single-threaded setup/loading, never by proof-search workers --- de.uka.ilkd.key.logic.sort.ArraySort#aSH # mutated only via getArraySort during type modeling at load time; NOT safe for callers during proving From 2cc76a74a73df76e918053415ebdb675c4772dc2 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Sat, 1 Aug 2026 09:47:39 +0200 Subject: [PATCH 3/3] Use LinkedHashMaps instead of HashMaps for determinism --- .../java/de/uka/ilkd/key/macros/ApplyScriptsMacro.java | 4 ++-- .../java/de/uka/ilkd/key/speclang/LoopContractImpl.java | 6 +++--- .../strategy/quantifierHeuristics/EqualityConstraint.java | 1 - .../strategy/termgenerator/TriggeredInstantiations.java | 7 ++++--- .../java/de/uka/ilkd/key/util/InfFlowProgVarRenamer.java | 5 ++--- 5 files changed, 11 insertions(+), 12 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/ApplyScriptsMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/ApplyScriptsMacro.java index 25b49309cab..9fd345eaf09 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/ApplyScriptsMacro.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/ApplyScriptsMacro.java @@ -176,7 +176,7 @@ private static JmlAssert getJmlAssert(Node node) { Term appliedOn = ruleApp.posInOccurrence().subTerm(); if (appliedOn.op() instanceof UpdateApplication) { var update = UpdateApplication.getUpdate((JTerm) appliedOn); - Map updates = new HashMap<>(); + Map updates = new LinkedHashMap<>(); Services services = goal.proof().getServices(); collectUpdates(update, updates, services); return new OpReplacer(updates, services.getTermFactory()); @@ -311,7 +311,7 @@ private JTerm correctSelfVar(int index, JavaBlock javaBlock, private Map makeObtainVarMap( ImmutableList locationVariables) { - HashMap result = new HashMap<>(); + HashMap result = new LinkedHashMap<>(); for (LocationVariable lv : locationVariables) { result.put(lv, null); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopContractImpl.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopContractImpl.java index 89b0053817e..355028b62a4 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopContractImpl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopContractImpl.java @@ -339,7 +339,7 @@ public static LoopContract combine(ImmutableSet contracts, Service */ private static OpReplacer createOpReplacer(final ProgramVariable index, final ProgramVariable values, Services services) { - final Map replacementMap = new HashMap<>(); + final Map replacementMap = new LinkedHashMap<>(); if (index != null) { replacementMap.put(services.getTermBuilder().index(), services.getTermBuilder().var(index)); @@ -624,8 +624,8 @@ public BlockContract toBlockContract() { if (head != null) { - Map preReplacementMap = new HashMap<>(); - Map postReplacementMap = new HashMap<>(); + Map preReplacementMap = new LinkedHashMap<>(); + Map postReplacementMap = new LinkedHashMap<>(); for (int i = 0; i < head.getStatementCount(); ++i) { Statement stmt = head.getStatementAt(i); if (stmt instanceof LocalVariableDeclaration decl) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/EqualityConstraint.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/EqualityConstraint.java index b2fff404d74..6f1364e26b0 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/EqualityConstraint.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/EqualityConstraint.java @@ -22,7 +22,6 @@ import org.key_project.logic.op.QuantifiableVariable; import org.key_project.logic.op.sv.SchemaVariable; import org.key_project.logic.sort.Sort; -import org.key_project.util.ConcurrentLruCache; import org.key_project.util.collection.DefaultImmutableSet; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSet; diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/termgenerator/TriggeredInstantiations.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/termgenerator/TriggeredInstantiations.java index d491fc665c6..54cc0fb3f4c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/termgenerator/TriggeredInstantiations.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/termgenerator/TriggeredInstantiations.java @@ -5,6 +5,7 @@ import java.util.HashSet; import java.util.Iterator; +import java.util.LinkedHashSet; import java.util.Set; import de.uka.ilkd.key.java.Services; @@ -88,8 +89,8 @@ public Iterator generate(RuleApp app, PosInOccurrenc final Sequent seq = goal.sequent(); final CandidateCache cached = candidateCache.get(); if (seq != cached.last()) { - terms = new HashSet<>(); - axiomSet = new HashSet<>(); + terms = new LinkedHashSet<>(); + axiomSet = new LinkedHashSet<>(); computeAxiomAndCandidateSets(seq, terms, axiomSet, services); for (JTerm axiom : axiomSet) { axioms = axioms.add(axiom); @@ -184,7 +185,7 @@ private HashSet computeInstances(Services services, ImmutableSet axioms, TacletApp app) { - final HashSet instances = new HashSet<>(); + final LinkedHashSet instances = new LinkedHashSet<>(); final HashSet alreadyChecked = new HashSet<>(); // The axioms are fixed for the sequent, so the congruence and the normalization are // built once here instead of once per avoid condition per candidate. diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/InfFlowProgVarRenamer.java b/key.core/src/main/java/de/uka/ilkd/key/util/InfFlowProgVarRenamer.java index 2be39b71306..bd94d9ce13c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/util/InfFlowProgVarRenamer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/util/InfFlowProgVarRenamer.java @@ -3,7 +3,6 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.util; -import java.util.HashMap; import java.util.Map; import de.uka.ilkd.key.java.Services; @@ -54,7 +53,7 @@ public InfFlowProgVarRenamer(JTerm[] terms, Map preInitialisedRepl this.postfix = postfix; this.goalForVariableRegistration = goalForVariableRegistration; if (preInitialisedReplaceMap == null) { - this.replaceMap = new HashMap<>(); + this.replaceMap = new LinkedHashMap<>(); } else { this.replaceMap = preInitialisedReplaceMap; } @@ -241,7 +240,7 @@ private JavaBlock renameJavaBlock(Map progVa private Map restrictToProgramVariables( Map replaceMap) { Map progVarReplaceMap = - new HashMap<>(); + new LinkedHashMap<>(); for (final JTerm t : replaceMap.keySet()) { if (t.op() instanceof LocationVariable lv) { progVarReplaceMap.put(lv,