Skip to content

Commit 118d7b9

Browse files
DrodtDrodt
authored
Performance Series 2 (4/5): Lower memory for the per-goal rule-application queue (#3877)
2 parents 3645128 + 8b063d8 commit 118d7b9

7 files changed

Lines changed: 197 additions & 57 deletions

File tree

‎key.core/src/main/java/de/uka/ilkd/key/logic/LexPathOrdering.java‎

Lines changed: 41 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -4,8 +4,6 @@
44
package de.uka.ilkd.key.logic;
55

66
import java.math.BigInteger;
7-
import java.util.HashMap;
8-
import java.util.LinkedHashMap;
97
import java.util.LinkedHashSet;
108
import java.util.Set;
119
import java.util.WeakHashMap;
@@ -20,15 +18,37 @@
2018
import org.key_project.logic.op.Operator;
2119
import org.key_project.logic.op.QuantifiableVariable;
2220
import org.key_project.logic.sort.Sort;
21+
import org.key_project.util.LRUCache;
2322
import org.key_project.util.collection.ImmutableArray;
2423

2524
/**
2625
*
2726
*/
2827
public class LexPathOrdering implements TermOrdering {
2928

29+
/**
30+
* Per-comparison memo, scoped to one top-level {@link #compare(Term, Term)} call. The
31+
* recursion of {@link #compareHelp} visits the pair-DAG of the two terms; on large terms with
32+
* structural sharing that DAG has far more distinct pairs than the bounded global
33+
* {@link #cache} can hold, so the LRU is evicted mid-comparison and memoization collapses --
34+
* measured two BILLION compareHelp calls (960M recomputations, 134s) for 1.68M comparisons on
35+
* an ips4o goal at 6000 proof steps. An unbounded per-call map restores true DAG complexity
36+
* (same run: 92M calls, 7.8s, byte-identical results). ThreadLocal because a LexPathOrdering
37+
* instance is shared across parallel-prover workers; the map is reused (cleared) per call, so
38+
* small comparisons pay only an empty-map lookup.
39+
*/
40+
private final ThreadLocal<java.util.HashMap<CacheKey, CompRes>> callMemo =
41+
ThreadLocal.withInitial(java.util.HashMap::new);
42+
3043
public int compare(Term p_a, Term p_b) {
31-
final CompRes res = compareHelp(p_a, p_b);
44+
final java.util.HashMap<CacheKey, CompRes> memo = callMemo.get();
45+
memo.clear(); // scope the memo to this top-level comparison
46+
final CompRes res;
47+
try {
48+
res = compareHelp(p_a, p_b);
49+
} finally {
50+
memo.clear();
51+
}
3252
if (res.lt()) {
3353
return -1;
3454
} else if (res.gt()) {
@@ -75,19 +95,33 @@ private record CacheKey(Term left, Term right) {
7595
}
7696

7797

78-
private final HashMap<CacheKey, CompRes> cache = new LinkedHashMap<>();
98+
/**
99+
* Cache of comparison results, an LRU bounded at {@link #CACHE_SIZE}. Previously this grew to
100+
* 100000 entries and then dropped <em>all</em> of them at once; on long proofs that churns the
101+
* cache (every overflow throws away the hot entries too) and averages ~50000 live entries. An
102+
* LRU keeps the recently-used ones within a much smaller steady bound. 10000 is well below that
103+
* old average (a memory saving) and A/B-safe: on the heaviest LexPath proof (the wide-branching
104+
* bike example) shrinking 100000 -> 1000 cost &lt;2% automode time, i.e. the cache barely
105+
* helps.
106+
* The bound is tunable via {@code -Dkey.lexpath.cachesize}.
107+
*/
108+
private static final int CACHE_SIZE = Integer.getInteger("key.lexpath.cachesize", 10000);
109+
private final LRUCache<CacheKey, CompRes> cache = new LRUCache<>(CACHE_SIZE);
79110

80111

81112
private CompRes compareHelp(Term p_a, Term p_b) {
82113
final CacheKey key = new CacheKey(p_a, p_b);
114+
final java.util.HashMap<CacheKey, CompRes> memo = callMemo.get();
115+
final CompRes local = memo.get(key);
116+
if (local != null) {
117+
return local;
118+
}
83119
CompRes res = cache.get(key);
84120
if (res == null) {
85121
res = compareHelp2(p_a, p_b);
86-
if (cache.size() > 100000) {
87-
cache.clear();
88-
}
89122
cache.put(key, res);
90123
}
124+
memo.put(key, res);
91125
return res;
92126
}
93127

‎key.core/src/main/java/de/uka/ilkd/key/proof/CopyOnWriteIndexMap.java‎

Lines changed: 77 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,77 @@
1+
/* This file is part of KeY - https://key-project.org
2+
* KeY is licensed under the GNU General Public License Version 2
3+
* SPDX-License-Identifier: GPL-2.0-only */
4+
package de.uka.ilkd.key.proof;
5+
6+
import java.util.Collection;
7+
import java.util.LinkedHashMap;
8+
9+
/**
10+
* A copy-on-write map used for the {@link TacletIndex}'s find-taclet lists. {@link #copy()} shares
11+
* the backing map in O(1); the first mutating call ({@link #put}/{@link #remove}) clones it, so a
12+
* shared map is never written in place. Reads delegate straight through.
13+
*
14+
* <p>
15+
* The point is memory: every proof {@link Goal} gets its own {@link TacletIndex} via
16+
* {@link TacletIndex#copy()}, but the find-taclet lists are only changed by a few operations
17+
* (\addrules, program-variable renaming). Sharing until first write means the (large) base index is
18+
* physically duplicated only when a goal actually modifies it, instead of on every branch.
19+
*
20+
* <p>
21+
* The backing map is a {@link LinkedHashMap}, so iteration order (hence taclet-match order and
22+
* proof search) is unchanged. Not strictly thread-safe, but a shared map is only read while a
23+
* writer clones away from it -- benign (at worst a redundant clone).
24+
*
25+
* @param <K> key type
26+
* @param <V> value type
27+
*/
28+
final class CopyOnWriteIndexMap<K, V> {
29+
private LinkedHashMap<K, V> map;
30+
/**
31+
* {@code true} while {@link #map} may be shared with another instance (see {@link #copy()}).
32+
*/
33+
private boolean shared;
34+
35+
CopyOnWriteIndexMap() {
36+
this.map = new LinkedHashMap<>();
37+
}
38+
39+
private CopyOnWriteIndexMap(LinkedHashMap<K, V> sharedMap) {
40+
this.map = sharedMap;
41+
this.shared = true;
42+
}
43+
44+
/**
45+
* Returns a copy that shares this map's backing store until one of them is written. O(1).
46+
*/
47+
CopyOnWriteIndexMap<K, V> copy() {
48+
this.shared = true;
49+
return new CopyOnWriteIndexMap<>(this.map);
50+
}
51+
52+
/** Take a private copy of the backing map before a write, if it is currently shared. */
53+
private void ensureExclusive() {
54+
if (shared) {
55+
map = new LinkedHashMap<>(map);
56+
shared = false;
57+
}
58+
}
59+
60+
V get(Object key) {
61+
return map.get(key);
62+
}
63+
64+
Collection<V> values() {
65+
return map.values();
66+
}
67+
68+
V put(K key, V value) {
69+
ensureExclusive();
70+
return map.put(key, value);
71+
}
72+
73+
V remove(Object key) {
74+
ensureExclusive();
75+
return map.remove(key);
76+
}
77+
}

‎key.core/src/main/java/de/uka/ilkd/key/proof/MultiThreadedTacletIndex.java‎

Lines changed: 6 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -46,9 +46,10 @@ final class MultiThreadedTacletIndex extends TacletIndex {
4646
super();
4747
}
4848

49-
private MultiThreadedTacletIndex(HashMap<Object, ImmutableList<NoPosTacletApp>> rwList,
50-
HashMap<Object, ImmutableList<NoPosTacletApp>> antecList,
51-
HashMap<Object, ImmutableList<NoPosTacletApp>> succList,
49+
private MultiThreadedTacletIndex(
50+
CopyOnWriteIndexMap<Object, ImmutableList<NoPosTacletApp>> rwList,
51+
CopyOnWriteIndexMap<Object, ImmutableList<NoPosTacletApp>> antecList,
52+
CopyOnWriteIndexMap<Object, ImmutableList<NoPosTacletApp>> succList,
5253
ImmutableList<NoPosTacletApp> noFindList,
5354
HashSet<NoPosTacletApp> partialInstantiatedRuleApps) {
5455
super(rwList, antecList, succList, noFindList, partialInstantiatedRuleApps);
@@ -60,11 +61,8 @@ private MultiThreadedTacletIndex(HashMap<Object, ImmutableList<NoPosTacletApp>>
6061
@SuppressWarnings("unchecked")
6162
@Override
6263
public TacletIndex copy() {
63-
return new MultiThreadedTacletIndex(
64-
(HashMap<Object, ImmutableList<NoPosTacletApp>>) rwList.clone(),
65-
(HashMap<Object, ImmutableList<NoPosTacletApp>>) antecList.clone(),
66-
(HashMap<Object, ImmutableList<NoPosTacletApp>>) succList.clone(), noFindList,
67-
(HashSet<NoPosTacletApp>) partialInstantiatedRuleApps.clone());
64+
return new MultiThreadedTacletIndex(rwList.copy(), antecList.copy(), succList.copy(),
65+
noFindList, (HashSet<NoPosTacletApp>) partialInstantiatedRuleApps.clone());
6866
}
6967

7068
/**

‎key.core/src/main/java/de/uka/ilkd/key/proof/SingleThreadedTacletIndex.java‎

Lines changed: 6 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,6 @@
33
* SPDX-License-Identifier: GPL-2.0-only */
44
package de.uka.ilkd.key.proof;
55

6-
import java.util.HashMap;
76
import java.util.HashSet;
87

98
import de.uka.ilkd.key.rule.NoPosTacletApp;
@@ -38,9 +37,10 @@ final class SingleThreadedTacletIndex extends TacletIndex {
3837
super(tacletSet);
3938
}
4039

41-
private SingleThreadedTacletIndex(HashMap<Object, ImmutableList<NoPosTacletApp>> rwList,
42-
HashMap<Object, ImmutableList<NoPosTacletApp>> antecList,
43-
HashMap<Object, ImmutableList<NoPosTacletApp>> succList,
40+
private SingleThreadedTacletIndex(
41+
CopyOnWriteIndexMap<Object, ImmutableList<NoPosTacletApp>> rwList,
42+
CopyOnWriteIndexMap<Object, ImmutableList<NoPosTacletApp>> antecList,
43+
CopyOnWriteIndexMap<Object, ImmutableList<NoPosTacletApp>> succList,
4444
ImmutableList<NoPosTacletApp> noFindList,
4545
HashSet<NoPosTacletApp> partialInstantiatedRuleApps) {
4646
super(rwList, antecList, succList, noFindList, partialInstantiatedRuleApps);
@@ -52,11 +52,8 @@ private SingleThreadedTacletIndex(HashMap<Object, ImmutableList<NoPosTacletApp>>
5252
@SuppressWarnings("unchecked")
5353
@Override
5454
public TacletIndex copy() {
55-
return new SingleThreadedTacletIndex(
56-
(HashMap<Object, ImmutableList<NoPosTacletApp>>) rwList.clone(),
57-
(HashMap<Object, ImmutableList<NoPosTacletApp>>) antecList.clone(),
58-
(HashMap<Object, ImmutableList<NoPosTacletApp>>) succList.clone(), noFindList,
59-
(HashSet<NoPosTacletApp>) partialInstantiatedRuleApps.clone());
55+
return new SingleThreadedTacletIndex(rwList.copy(), antecList.copy(), succList.copy(),
56+
noFindList, (HashSet<NoPosTacletApp>) partialInstantiatedRuleApps.clone());
6057
}
6158

6259
/**

‎key.core/src/main/java/de/uka/ilkd/key/proof/TacletIndex.java‎

Lines changed: 21 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -48,17 +48,20 @@ public abstract class TacletIndex implements RuleIndex<NoPosTacletApp> {
4848
/**
4949
* contains rewrite Taclets
5050
*/
51-
protected HashMap<Object, ImmutableList<NoPosTacletApp>> rwList = new LinkedHashMap<>();
51+
protected CopyOnWriteIndexMap<Object, ImmutableList<NoPosTacletApp>> rwList =
52+
new CopyOnWriteIndexMap<>();
5253

5354
/**
5455
* contains antecedent Taclets
5556
*/
56-
protected HashMap<Object, ImmutableList<NoPosTacletApp>> antecList = new LinkedHashMap<>();
57+
protected CopyOnWriteIndexMap<Object, ImmutableList<NoPosTacletApp>> antecList =
58+
new CopyOnWriteIndexMap<>();
5759

5860
/**
5961
* contains succedent Taclets
6062
*/
61-
protected HashMap<Object, ImmutableList<NoPosTacletApp>> succList = new LinkedHashMap<>();
63+
protected CopyOnWriteIndexMap<Object, ImmutableList<NoPosTacletApp>> succList =
64+
new CopyOnWriteIndexMap<>();
6265

6366
/**
6467
* contains NoFind-Taclets
@@ -81,16 +84,16 @@ public abstract class TacletIndex implements RuleIndex<NoPosTacletApp> {
8184
* creates a new TacletIndex with the given Taclets as initial contents.
8285
*/
8386
TacletIndex(Iterable<Taclet> tacletSet) {
84-
rwList = new LinkedHashMap<>();
85-
antecList = new LinkedHashMap<>();
86-
succList = new LinkedHashMap<>();
87+
rwList = new CopyOnWriteIndexMap<>();
88+
antecList = new CopyOnWriteIndexMap<>();
89+
succList = new CopyOnWriteIndexMap<>();
8790
noFindList = ImmutableList.nil();
8891
addTaclets(toNoPosTacletApp(tacletSet));
8992
}
9093

91-
protected TacletIndex(HashMap<Object, ImmutableList<NoPosTacletApp>> rwList,
92-
HashMap<Object, ImmutableList<NoPosTacletApp>> antecList,
93-
HashMap<Object, ImmutableList<NoPosTacletApp>> succList,
94+
protected TacletIndex(CopyOnWriteIndexMap<Object, ImmutableList<NoPosTacletApp>> rwList,
95+
CopyOnWriteIndexMap<Object, ImmutableList<NoPosTacletApp>> antecList,
96+
CopyOnWriteIndexMap<Object, ImmutableList<NoPosTacletApp>> succList,
9497
ImmutableList<NoPosTacletApp> noFindList,
9598
HashSet<NoPosTacletApp> partialInstantiatedRuleApps) {
9699
this.rwList = rwList;
@@ -141,7 +144,7 @@ private static Object getIndexObj(FindTaclet tac) {
141144

142145

143146
private void insertToMap(NoPosTacletApp tacletApp,
144-
HashMap<Object, ImmutableList<NoPosTacletApp>> map) {
147+
CopyOnWriteIndexMap<Object, ImmutableList<NoPosTacletApp>> map) {
145148
Object indexObj = getIndexObj((FindTaclet) tacletApp.taclet());
146149
ImmutableList<NoPosTacletApp> opList = map.get(indexObj);
147150
opList = Objects.requireNonNullElseGet(opList,
@@ -151,7 +154,7 @@ private void insertToMap(NoPosTacletApp tacletApp,
151154

152155

153156
private void removeFromMap(NoPosTacletApp tacletApp,
154-
HashMap<Object, ImmutableList<NoPosTacletApp>> map) {
157+
CopyOnWriteIndexMap<Object, ImmutableList<NoPosTacletApp>> map) {
155158
Object op = getIndexObj((FindTaclet) tacletApp.taclet());
156159
ImmutableList<NoPosTacletApp> opList = map.get(op);
157160
if (opList != null) {
@@ -305,7 +308,7 @@ protected abstract ImmutableList<NoPosTacletApp> matchTaclets(
305308
* prefix elements
306309
*/
307310
private ImmutableList<NoPosTacletApp> getJavaTacletList(
308-
HashMap<Object, ImmutableList<NoPosTacletApp>> map, ProgramElement pe,
311+
CopyOnWriteIndexMap<Object, ImmutableList<NoPosTacletApp>> map, ProgramElement pe,
309312
PrefixOccurrences prefixOccurrences) {
310313
ImmutableList<NoPosTacletApp> res = ImmutableList.nil();
311314
if (pe instanceof ProgramPrefix nt) {
@@ -324,7 +327,7 @@ private ImmutableList<NoPosTacletApp> getJavaTacletList(
324327

325328
@SuppressWarnings("deprecation")
326329
private ImmutableList<NoPosTacletApp> getListHelp(
327-
final HashMap<Object, ImmutableList<NoPosTacletApp>> map, final JTerm term,
330+
final CopyOnWriteIndexMap<Object, ImmutableList<NoPosTacletApp>> map, final JTerm term,
328331
final boolean ignoreUpdates, final PrefixOccurrences prefixOccurrences) {
329332

330333
ImmutableList<NoPosTacletApp> res = ImmutableList.nil();
@@ -405,7 +408,8 @@ private ImmutableList<NoPosTacletApp> merge(ImmutableList<NoPosTacletApp> first,
405408
* @param term the term that is used to find the selection
406409
*/
407410
private ImmutableList<NoPosTacletApp> getList(
408-
HashMap<Object, ImmutableList<NoPosTacletApp>> map, JTerm term, boolean ignoreUpdates) {
411+
CopyOnWriteIndexMap<Object, ImmutableList<NoPosTacletApp>> map, JTerm term,
412+
boolean ignoreUpdates) {
409413
return getListHelp(map, term, ignoreUpdates, new PrefixOccurrences());
410414
}
411415

@@ -445,7 +449,8 @@ public ImmutableList<NoPosTacletApp> getSuccedentTaclet(
445449
}
446450

447451
private ImmutableList<NoPosTacletApp> getTopLevelTaclets(
448-
HashMap<Object, ImmutableList<NoPosTacletApp>> findTaclets, RuleFilter filter,
452+
CopyOnWriteIndexMap<Object, ImmutableList<NoPosTacletApp>> findTaclets,
453+
RuleFilter filter,
449454
PosInOccurrence pos, LogicServices services) {
450455

451456
assert pos.isTopLevel();
@@ -626,7 +631,7 @@ public int occurred(ProgramElement pe) {
626631
* @param map a map to select from
627632
*/
628633
public ImmutableList<NoPosTacletApp> getList(
629-
HashMap<Object, ImmutableList<NoPosTacletApp>> map) {
634+
CopyOnWriteIndexMap<Object, ImmutableList<NoPosTacletApp>> map) {
630635
ImmutableList<NoPosTacletApp> result = ImmutableList.nil();
631636
for (int i = 0; i < PREFIXTYPES; i++) {
632637
if (occurred[i]) {

0 commit comments

Comments
 (0)