src/containers/lru.bend
bend-collections-laws-containers@1.0.0.0 · 881 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/src/math/u64.bend as W
3import bend-collections-laws-containers@1.0.0.0/src/math/hash.bend as HS
4import bend-collections-laws-containers@1.0.0.0/src/containers/hash_table.bend as H
5
6# LRU cache, performance layout (experiment). Same observable semantics as
7# src/lru/fast.bend and benchmarks/native/lru.c: capacity eviction of the
8# oldest entry, lifetimes, five 64-bit metrics, touch-on-get, no-touch peek
9# and contains, expired entries dropped (as removals) when a read finds them.
10#
11# Layout, chosen for Bend 2's native backend:
12# - every record field is a register word, so the state is kept NARROW:
13# F{cap, n, head, tail, free, m, tab, ks, ents, lk} is ten words;
14# - cold scalars and the counters live in one packed Array<U32> `m`;
15# - `tab` is the hash map's bucket table (src/containers/hash_table.bend):
16# (check word, link) pairs, linear probing over a power-of-two size, load
17# <= 1/2, backward-shift delete; probing, placement, growth and deletion
18# are the hash map's own functions, so their proofs are shared;
19# - per slot: key `ks`, entry `ents`, and (prev, next, check word, timed,
20# deadline lo, deadline hi) in `lk` (8 words).
21# Links are slot + 1; 0 = none. Nothing here is ever shared with `+` unless it
22# is an unboxed word: sharing a boxed value makes the runtime reference-count
23# every node of its type program-wide.
24
25# ---- m: meta words ----
26# 0 fresh 1 size 2 depth 3 ttl 4 life lo 5 life hi 6 tmask 7 tbits
27# 16 + 2c, 17 + 2c: counter c (0 inserts, 1 evictions, 2 removals, 3 hits, 4 misses)
28
29def pick(b: Bool, +x: U32, +y: U32) -> U32:
30 match b:
31 case True{}:
32 x
33 case False{}:
34 y
35
36def pidx(+s: U32) -> U32:
37 U32.shl(U32.shl(U32.shl(s)))
38
39def nidx(+s: U32) -> U32:
40 U32.inc(pidx(s))
41
42# ---- the cache ----
43
44# An entry about to be stored: its value, whether it is timed, its deadline.
45type Ent<a, -V: Kind(a)> is Kind(a):
46 E{v: V, t: U32, lo: U32, hi: U32}
47
48# An entry array of `depth` vacant cells (Array.new needs Data values).
49def vac(a, -V: Kind(a), d: Nat) -> Array<Maybe<a, V>>:
50 match d:
51 case 0n:
52 ALeaf{None{}}
53 case 1n+ +p:
54 ANode{vac(a, V, p), vac(a, V, p)}
55
56type LRU<a, -V: Kind(a)> is Type:
57 F{cap: U32, n: U32, head: U32, tail: U32, free: U32, m: Array<U32>, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>}
58
59# ---- keys: hashing and equality (short keys stay out of recursion) ----
60
61def bump_hi_go(+i: U32, r: Array<U32> & U32) -> Array<U32>:
62 (k, +h) = r
63 Array.set(U32, k, i, U32.inc(h))
64
65type Made<a, -V: Kind(a)> is Type:
66 Made{f: LRU<a, V>}
67 Rejected{reason: String}
68
69def meta0() -> Array<U32>:
70 Array.set(U32, Array.set(U32, Array.set(U32, Array.new(U32, 5n, 0), 1, 1), 6, 1), 7, 1)
71
72def init(a, -V: Kind(a), +cap: U32) -> LRU<a, V>:
73 F{cap, 0, 0, 0, 0, meta0(), Array.new(U32, 2n, 0), Array.new(String, 0n, ""), ALeaf{None{}}, Array.new(U32, 3n, 0)}
74
75def capacity(a, -V: Kind(a), f: LRU<a, V>) -> LRU<a, V> & U32:
76 F{+cap, n, head, tail, free, m, tab, ks, ents, lk} = f
77 (F{cap, n, head, tail, free, m, tab, ks, ents, lk}, cap)
78
79def new_checked(a, -V: Kind(a), +cap: U32, zero: Bool, reserved: Bool) -> Made<a, V>:
80 match zero reserved:
81 case True{} r:
82 Rejected{"capacity must be positive"}
83 case False{} True{}:
84 Rejected{"size must not be 0XFFFFFFFF"}
85 case False{} False{}:
86 Made{init(a, V, cap)}
87
88def new(a, -V: Kind(a), +cap: U32) -> Made<a, V>:
89 new_checked(a, V, cap, U32.is_eq(cap, 0), U32.is_eq(cap, 4294967295))
90
91# ---- add ----
92
93def grow_tab_b(tab: Array<U32>, +mask: U32, r: Array<U32> & U32) -> Array<U32> & Array<U32>:
94 (m2, +bits) = r
95 +nmask = U32.inc(U32.shl(mask))
96 (Array.set(U32, Array.set(U32, m2, 6, nmask), 7, U32.inc(bits)),
97 H.mv_fin(H.mv_go(U32.to_nat(U32.inc(mask)), 0, nmask, H.MV{tab, Array.new(U32, U32.to_nat(U32.add(bits, 2)), 0)})))
98
99def grow_tab(m: Array<U32>, tab: Array<U32>, +mask: U32, over: Bool) -> Array<U32> & Array<U32>:
100 match over:
101 case False{}:
102 (m, tab)
103 case True{}:
104 grow_tab_b(tab, mask, Array.get(U32, m, 7))
105
106def room_fin(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, r: Array<U32> & Array<U32>) -> LRU<a, V>:
107 (m, tab) = r
108 F{cap, n, head, tail, free, m, tab, ks, ents, lk}
109
110def room_m(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, r: Array<U32> & U32) -> LRU<a, V>:
111 (m, +mask) = r
112 room_fin(a, V, cap, n, head, tail, free, ks, ents, lk, grow_tab(m, tab, mask, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(mask))))
113
114# Keep the table load <= 1/2 for one more entry.
115def room(a, -V: Kind(a), f: LRU<a, V>) -> LRU<a, V>:
116 F{+cap, +n, +head, +tail, +free, m, tab, ks, ents, lk} = f
117 room_m(a, V, cap, n, head, tail, free, tab, ks, ents, lk, Array.get(U32, m, 6))
118
119def ent_dl(a, -V: Kind(a), v: V, d: W.U64) -> Ent<a, V>:
120 W.U64{lo, hi} = d
121 E{v, 1, lo, hi}
122
123def life_hi(a, -V: Kind(a), v: V, now: W.U64, +lo: U32, r: Array<U32> & U32) -> Array<U32> & Ent<a, V>:
124 (m, +hi) = r
125 (m, ent_dl(a, V, v, W.add(now, W.U64{lo, hi})))
126
127def life_lo(a, -V: Kind(a), v: V, now: W.U64, r: Array<U32> & U32) -> Array<U32> & Ent<a, V>:
128 (m, +lo) = r
129 life_hi(a, V, v, now, lo, Array.get(U32, m, 5))
130
131def ent_if(a, -V: Kind(a), v: V, now: W.U64, m: Array<U32>, on: Bool) -> Array<U32> & Ent<a, V>:
132 match on:
133 case False{}:
134 (m, E{v, 0, 0, 0})
135 case True{}:
136 life_lo(a, V, v, now, Array.get(U32, m, 4))
137
138def ent_ttl(a, -V: Kind(a), v: V, now: W.U64, r: Array<U32> & U32) -> Array<U32> & Ent<a, V>:
139 (m, +t) = r
140 ent_if(a, V, v, now, m, U32.is_ne(t, 0))
141
142# The entry to store: immortal without a lifetime, else due at now + lifetime.
143def entry_of(a, -V: Kind(a), m: Array<U32>, v: V, now: W.U64) -> Array<U32> & Ent<a, V>:
144 ent_ttl(a, V, v, now, Array.get(U32, m, 3))
145
146def set_if(a: Array<U32>, +i: U32, +x: U32, skip: Bool) -> Array<U32>:
147 match skip:
148 case True{}:
149 a
150 case False{}:
151 Array.set(U32, a, i, x)
152
153# ---- recency links ----
154
155def ul_fin(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, +p: U32, r: Array<U32> & U32) -> LRU<a, V>:
156 (lk, +q) = r
157 F{cap, n, pick(U32.is_eq(p, 0), q, head), pick(U32.is_eq(q, 0), p, tail), free, m, tab, ks, ents,
158 set_if(set_if(lk, pidx(H.slot(q)), p, U32.is_eq(q, 0)), nidx(H.slot(p)), q, U32.is_eq(p, 0))}
159
160def ul_p(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, +s: U32, r: Array<U32> & U32) -> LRU<a, V>:
161 (lk, +p) = r
162 ul_fin(a, V, cap, n, head, tail, free, m, tab, ks, ents, p, Array.get(U32, lk, nidx(s)))
163
164# Detach slot s from the recency list.
165def unlink(a, -V: Kind(a), f: LRU<a, V>, +s: U32) -> LRU<a, V>:
166 F{+cap, +n, +head, +tail, +free, m, tab, ks, ents, lk} = f
167 ul_p(a, V, cap, n, head, tail, free, m, tab, ks, ents, s, Array.get(U32, lk, pidx(s)))
168
169# Attach slot s as the newest.
170def link_tail(a, -V: Kind(a), f: LRU<a, V>, +s: U32) -> LRU<a, V>:
171 F{cap, n, head, +tail, free, m, tab, ks, ents, lk} = f
172 F{cap, n, pick(U32.is_eq(tail, 0), H.link(s), head), H.link(s), free, m, tab, ks, ents,
173 set_if(Array.set(U32, Array.set(U32, lk, pidx(s), tail), nidx(s), 0), nidx(H.slot(tail)), H.link(s), U32.is_eq(tail, 0))}
174
175def touch_go(a, -V: Kind(a), f: LRU<a, V>, +s: U32, newest: Bool) -> LRU<a, V>:
176 match newest:
177 case True{}:
178 f
179 case False{}:
180 link_tail(a, V, unlink(a, V, f, s), s)
181
182def touch(a, -V: Kind(a), f: LRU<a, V>, +s: U32) -> LRU<a, V>:
183 F{cap, n, head, +tail, free, m, tab, ks, ents, lk} = f
184 touch_go(a, V, F{cap, n, head, tail, free, m, tab, ks, ents, lk}, s, U32.is_eq(H.link(s), tail))
185
186def bump_hi(k: Array<U32>, +c: U32, zero: Bool) -> Array<U32>:
187 match zero:
188 case False{}:
189 k
190 case True{}:
191 bump_hi_go(U32.add(17, U32.shl(c)), Array.get(U32, k, U32.add(17, U32.shl(c))))
192
193def bump_lo(+c: U32, r: Array<U32> & U32) -> Array<U32>:
194 (k, +l) = r
195 +l2 = U32.inc(l)
196 bump_hi(Array.set(U32, k, U32.add(16, U32.shl(c)), l2), c, U32.is_eq(l2, 0))
197
198def bump(+c: U32, k: Array<U32>) -> Array<U32>:
199 bump_lo(c, Array.get(U32, k, U32.add(16, U32.shl(c))))
200
201def tidx(+s: U32) -> U32:
202 U32.add(pidx(s), 3)
203
204def dlo_idx(+s: U32) -> U32:
205 U32.add(pidx(s), 4)
206
207def dhi_idx(+s: U32) -> U32:
208 U32.add(pidx(s), 5)
209
210# Present key: new entry in place, touched, counted as an insertion.
211def put_ent(a, -V: Kind(a), ents: Array<Maybe<a, V>>, lk: Array<U32>, +s: U32, e: Ent<a, V>) -> Array<Maybe<a, V>> & Array<U32>:
212 E{v, +t, +lo, +hi} = e
213 (Array.set(Maybe<a, V>, ents, s, Some{v}), Array.set(U32, Array.set(U32, Array.set(U32, lk, tidx(s), t), dlo_idx(s), lo), dhi_idx(s), hi))
214
215def repl_fin(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, tab: Array<U32>, ks: Array<String>, +s: U32, r: Array<Maybe<a, V>> & Array<U32>) -> LRU<a, V>:
216 (ents, lk) = r
217 touch(a, V, F{cap, n, head, tail, free, bump(0, m), tab, ks, ents, lk}, s)
218
219# Present key: new entry in place, touched, counted as an insertion.
220def replace(a, -V: Kind(a), f: LRU<a, V>, +s: U32, e: Ent<a, V>) -> LRU<a, V>:
221 F{+cap, +n, +head, +tail, +free, m, tab, ks, ents, lk} = f
222 repl_fin(a, V, cap, n, head, tail, free, m, tab, ks, s, put_ent(a, V, ents, lk, s, e))
223
224
225
226# ---- dropping a live slot ----
227
228def drop_e(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, tab: Array<U32>, ks: Array<String>, lk: Array<U32>, +s: U32, +c: U32, r: Array<Maybe<a, V>> & Maybe<a, V>) -> LRU<a, V> & Maybe<a, V>:
229 (ents, old) = r
230 (F{cap, U32.sub(n, 1), head, tail, H.link(s), bump(c, m), tab, ks, ents, Array.set(U32, lk, nidx(s), free)}, old)
231
232# Unlink live slot s, free it and count it (c = 1 eviction, 2 removal); the
233# table is updated by the caller.
234def drop_core(a, -V: Kind(a), f: LRU<a, V>, +s: U32, +c: U32) -> LRU<a, V> & Maybe<a, V>:
235 F{+cap, +n, +head, +tail, +free, m, tab, ks, ents, lk} = f
236 drop_e(a, V, cap, n, head, tail, free, m, tab, ks, lk, s, c, Array.swap(Maybe<a, V>, ents, s, None{}))
237
238def drop_slot(a, -V: Kind(a), f: LRU<a, V>, +s: U32, +c: U32) -> LRU<a, V> & Maybe<a, V>:
239 drop_core(a, V, unlink(a, V, f, s), s, c)
240
241type DStep is Type:
242 DHit{tab: Array<U32>}
243 DNext{tab: Array<U32>}
244
245def ds_if(tab: Array<U32>, e: Bool) -> DStep:
246 match e:
247 case True{}:
248 DHit{tab}
249 case False{}:
250 DNext{tab}
251
252def ds_l(+l: U32, r: Array<U32> & U32) -> DStep:
253 (tab, +x) = r
254 ds_if(tab, U32.is_eq(x, l))
255
256def dstep(tab: Array<U32>, +i: U32, +l: U32) -> DStep:
257 ds_l(l, Array.get(U32, tab, U32.inc(U32.shl(i))))
258
259def dfind(fuel: Nat, s: DStep, +mask: U32, +l: U32, +i: U32) -> Array<U32>:
260 match fuel s:
261 case 0n DHit{tab}:
262 tab
263 case 0n DNext{tab}:
264 tab
265 case 1n+p DHit{tab}:
266 H.del_at(tab, mask, i)
267 case 1n+p DNext{tab}:
268 +j = H.bnext(i, mask)
269 dfind(p, dstep(tab, j, l), mask, l, j)
270
271# Delete the bucket holding link l (its check word is w): no key comparison.
272def del_link(tab: Array<U32>, +mask: U32, +w: U32, +l: U32) -> Array<U32>:
273 dfind(U32.to_nat(U32.inc(mask)), dstep(tab, HS.bucket(w, mask), l), mask, l, HS.bucket(w, mask))
274
275def dl_h(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, +s: U32, +c: U32, +mask: U32, m: Array<U32>, r: Array<U32> & U32) -> LRU<a, V> & Maybe<a, V>:
276 (lk, +h) = r
277 drop_slot(a, V, F{cap, n, head, tail, free, m, del_link(tab, mask, h, H.link(s)), ks, ents, lk}, s, c)
278
279def hidx(+s: U32) -> U32:
280 U32.add(pidx(s), 2)
281
282def dl_m(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, +s: U32, +c: U32, r: Array<U32> & U32) -> LRU<a, V> & Maybe<a, V>:
283 (m, +mask) = r
284 dl_h(a, V, cap, n, head, tail, free, tab, ks, ents, s, c, mask, m, Array.get(U32, lk, hidx(s)))
285
286# Drop slot s and its bucket (found by its stored hash and link).
287def remove_slot(a, -V: Kind(a), f: LRU<a, V>, +s: U32, +c: U32) -> LRU<a, V> & Maybe<a, V>:
288 F{+cap, +n, +head, +tail, +free, m, tab, ks, ents, lk} = f
289 dl_m(a, V, cap, n, head, tail, free, tab, ks, ents, lk, s, c, Array.get(U32, m, 6))
290
291def drop_v(a, -V: Kind(a), r: LRU<a, V> & Maybe<a, V>) -> LRU<a, V>:
292 (f, v) = r
293 f
294
295def evict_oldest(a, -V: Kind(a), f: LRU<a, V>) -> LRU<a, V>:
296 F{cap, n, +head, tail, free, m, tab, ks, ents, lk} = f
297 drop_v(a, V, remove_slot(a, V, F{cap, n, head, tail, free, m, tab, ks, ents, lk}, H.slot(head), 1))
298
299def ps_fin(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, tab: Array<U32>, ks: Array<String>, +s: U32, +h: U32, r: Array<Maybe<a, V>> & Array<U32>) -> LRU<a, V>:
300 (ents, lk) = r
301 link_tail(a, V, F{cap, U32.inc(n), head, tail, free, bump(0, m), tab, ks, ents, Array.set(U32, lk, hidx(s), h)}, s)
302
303def put_slot(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, +s: U32, key: String, +h: U32, e: Ent<a, V>) -> LRU<a, V>:
304 ps_fin(a, V, cap, n, head, tail, free, m, tab, Array.set(String, ks, s, key), s, h, put_ent(a, V, ents, lk, s, e))
305
306def grow_sz(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, key: String, +h: U32, e: Ent<a, V>, +fresh: U32, +size: U32, r: Array<U32> & U32) -> LRU<a, V>:
307 (m, +depth) = r
308 +d = U32.to_nat(depth)
309 put_slot(a, V, cap, n, head, tail, free,
310 Array.set(U32, Array.set(U32, Array.set(U32, m, 0, U32.inc(fresh)), 1, U32.shl(size)), 2, U32.inc(depth)), tab,
311 ANode{ks, Array.new(String, d, "")}, ANode{ents, vac(a, V, d)}, ANode{lk, Array.new(U32, Nat.add(d, 3n), 0)},
312 fresh, key, h, e)
313
314def fresh_room(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, key: String, +h: U32, e: Ent<a, V>, +fresh: U32, +size: U32, room: Bool) -> LRU<a, V>:
315 match room:
316 case True{}:
317 put_slot(a, V, cap, n, head, tail, free, Array.set(U32, m, 0, U32.inc(fresh)), tab, ks, ents, lk, fresh, key, h, e)
318 case False{}:
319 grow_sz(a, V, cap, n, head, tail, free, tab, ks, ents, lk, key, h, e, fresh, size, Array.get(U32, m, 2))
320
321def fresh_sz(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, key: String, +h: U32, e: Ent<a, V>, +fresh: U32, r: Array<U32> & U32) -> LRU<a, V>:
322 (m, +size) = r
323 fresh_room(a, V, cap, n, head, tail, free, m, tab, ks, ents, lk, key, h, e, fresh, size, U32.is_lt(fresh, size))
324
325def fresh_f(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, key: String, +h: U32, e: Ent<a, V>, r: Array<U32> & U32) -> LRU<a, V>:
326 (m, +fresh) = r
327 fresh_sz(a, V, cap, n, head, tail, free, tab, ks, ents, lk, key, h, e, fresh, Array.get(U32, m, 1))
328
329def free_next(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +s: U32, m: Array<U32>, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, key: String, +h: U32, e: Ent<a, V>, r: Array<U32> & U32) -> LRU<a, V>:
330 (lk, +nf) = r
331 put_slot(a, V, cap, n, head, tail, nf, m, tab, ks, ents, lk, s, key, h, e)
332
333def alloc_pick(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, key: String, +h: U32, e: Ent<a, V>, none: Bool) -> LRU<a, V>:
334 match none:
335 case True{}:
336 fresh_f(a, V, cap, n, head, tail, free, tab, ks, ents, lk, key, h, e, Array.get(U32, m, 0))
337 case False{}:
338 free_next(a, V, cap, n, head, tail, H.slot(free), m, tab, ks, ents, key, h, e, Array.get(U32, lk, nidx(H.slot(free))))
339
340# Store a new key (its bucket already written) in a free or fresh slot.
341def insert_slot(a, -V: Kind(a), f: LRU<a, V>, key: String, +h: U32, e: Ent<a, V>) -> LRU<a, V>:
342 F{+cap, +n, +head, +tail, +free, m, tab, ks, ents, lk} = f
343 alloc_pick(a, V, cap, n, head, tail, free, m, tab, ks, ents, lk, key, h, e, U32.is_eq(free, 0))
344
345# The slot insert_slot will take: the free-list head, else the next fresh one.
346def next_slot_m(+free: U32, r: Array<U32> & U32) -> Array<U32> & U32:
347 (m, +fresh) = r
348 (m, pick(U32.is_eq(free, 0), fresh, H.slot(free)))
349
350def set_bucket_m(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, +at: U32, +h: U32, r: Array<U32> & U32) -> LRU<a, V>:
351 (m, +s) = r
352 F{cap, n, head, tail, free, m, H.put_bucket(tab, at, h, H.link(s)), ks, ents, lk}
353
354
355def ins_m(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, +h: U32, +mask: U32, r: Array<U32> & U32) -> LRU<a, V>:
356 (m, +s) = r
357 F{cap, n, head, tail, free, m, H.ins_raw(tab, mask, h, H.link(s)), ks, ents, lk}
358
359def ins_mask(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, +h: U32, r: Array<U32> & U32) -> LRU<a, V>:
360 (m, +mask) = r
361 ins_m(a, V, cap, n, head, tail, free, tab, ks, ents, lk, h, mask, next_slot_m(free, Array.get(U32, m, 0)))
362
363# Full: evict the oldest first (which may shift buckets), then re-probe for
364# an empty bucket; the key is known absent.
365def miss_full(a, -V: Kind(a), f: LRU<a, V>, key: String, +h: U32, e: Ent<a, V>) -> LRU<a, V>:
366 F{+cap, +n, +head, +tail, +free, m, tab, ks, ents, lk} = f
367 insert_slot(a, V, ins_mask(a, V, cap, n, head, tail, free, tab, ks, ents, lk, h, Array.get(U32, m, 6)), key, h, e)
368
369# Not full: the probe's empty bucket takes the key.
370def mr_size(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, key: String, +at: U32, +h: U32, e: Ent<a, V>, +fresh: U32, r: Array<U32> & U32) -> LRU<a, V>:
371 (m, +size) = r
372 fresh_room(a, V, cap, n, head, tail, 0, m, H.put_bucket(tab, at, h, H.link(fresh)), ks, ents, lk, key, h, e, fresh, size, U32.is_lt(fresh, size))
373
374def mr_fresh(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, key: String, +at: U32, +h: U32, e: Ent<a, V>, r: Array<U32> & U32) -> LRU<a, V>:
375 (m, +fresh) = r
376 mr_size(a, V, cap, n, head, tail, tab, ks, ents, lk, key, at, h, e, fresh, Array.get(U32, m, 1))
377
378def mr_pick(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, key: String, +at: U32, +h: U32, e: Ent<a, V>, none: Bool) -> LRU<a, V>:
379 match none:
380 case True{}:
381 mr_fresh(a, V, cap, n, head, tail, tab, ks, ents, lk, key, at, h, e, Array.get(U32, m, 0))
382 case False{}:
383 free_next(a, V, cap, n, head, tail, H.slot(free), m, H.put_bucket(tab, at, h, free), ks, ents, key, h, e, Array.get(U32, lk, nidx(H.slot(free))))
384
385# Not full: the probe's empty bucket takes the key; the slot is chosen once.
386def miss_room(a, -V: Kind(a), f: LRU<a, V>, key: String, +at: U32, +h: U32, e: Ent<a, V>) -> LRU<a, V>:
387 F{+cap, +n, +head, +tail, +free, m, tab, ks, ents, lk} = f
388 mr_pick(a, V, cap, n, head, tail, free, m, tab, ks, ents, lk, key, at, h, e, U32.is_eq(free, 0))
389
390def add_miss(a, -V: Kind(a), f: LRU<a, V>, key: String, +at: U32, +h: U32, e: Ent<a, V>, full: Bool) -> LRU<a, V> & Bool:
391 match full:
392 case False{}:
393 (miss_room(a, V, f, key, at, h, e), False{})
394 case True{}:
395 (miss_full(a, V, evict_oldest(a, V, f), key, h, e), True{})
396
397def add_full(a, -V: Kind(a), f: LRU<a, V>, key: String, +at: U32, +h: U32, e: Ent<a, V>) -> LRU<a, V> & Bool:
398 F{+cap, +n, head, tail, free, m, tab, ks, ents, lk} = f
399 add_miss(a, V, F{cap, n, head, tail, free, m, tab, ks, ents, lk}, key, at, h, e, U32.is_le(cap, n))
400
401def add_pick(a, -V: Kind(a), f: LRU<a, V>, key: String, +at: U32, +h: U32, +l: U32, e: Ent<a, V>, absent: Bool) -> LRU<a, V> & Bool:
402 match absent:
403 case False{}:
404 (replace(a, V, f, H.slot(l), e), False{})
405 case True{}:
406 add_full(a, V, f, key, at, h, e)
407
408def add_e(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, key: String, +at: U32, +h: U32, +l: U32, r: Array<U32> & Ent<a, V>) -> LRU<a, V> & Bool:
409 (m, e) = r
410 add_pick(a, V, F{cap, n, head, tail, free, m, tab, ks, ents, lk}, key, at, h, l, e, U32.is_eq(l, 0))
411
412def add_fd(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, ents: Array<Maybe<a, V>>, lk: Array<U32>, v: V, now: W.U64, +h: U32, fd: H.Found) -> LRU<a, V> & Bool:
413 H.FD{tab, ks, key, +at, +l} = fd
414 add_e(a, V, cap, n, head, tail, free, tab, ks, ents, lk, key, at, h, l, entry_of(a, V, m, v, now))
415
416def add_found(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, ents: Array<Maybe<a, V>>, lk: Array<U32>, v: V, now: W.U64, r: H.Found & U32) -> LRU<a, V> & Bool:
417 (fd, +h) = r
418 add_fd(a, V, cap, n, head, tail, free, m, ents, lk, v, now, h, fd)
419
420def add_m(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, key: String, v: V, now: W.U64, r: Array<U32> & U32) -> LRU<a, V> & Bool:
421 (m, +mask) = r
422 add_found(a, V, cap, n, head, tail, free, m, ents, lk, v, now, H.probe(tab, ks, mask, key))
423
424def add_go(a, -V: Kind(a), f: LRU<a, V>, key: String, v: V, now: W.U64) -> LRU<a, V> & Bool:
425 F{+cap, +n, +head, +tail, +free, m, tab, ks, ents, lk} = f
426 add_m(a, V, cap, n, head, tail, free, tab, ks, ents, lk, key, v, now, Array.get(U32, m, 6))
427
428def add_long(a, -V: Kind(a), f: LRU<a, V>, key: String, v: V, now: W.U64) -> LRU<a, V> & Bool:
429 add_go(a, V, room(a, V, f), key, v, now)
430
431# Insert or replace key; the Bool reports whether an entry was evicted.
432def add(a, -V: Kind(a), f: LRU<a, V>, key: String, v: V, now: W.U64) -> LRU<a, V> & Bool:
433 add_long(a, V, f, key, v, now)
434
435def fbump(a, -V: Kind(a), +c: U32, f: LRU<a, V>) -> LRU<a, V>:
436 F{cap, n, head, tail, free, m, tab, ks, ents, lk} = f
437 F{cap, n, head, tail, free, bump(c, m), tab, ks, ents, lk}
438
439def expired_choose(deadline: W.U64, now: W.U64, immortal: Bool) -> Bool:
440 match immortal:
441 case True{}:
442 False{}
443 case False{}:
444 W.le_signed(deadline, now)
445
446# A deadline of zero never expires; otherwise deadline <= now (signed).
447def expired(+deadline: W.U64, now: W.U64) -> Bool:
448 expired_choose(deadline, now, W.is_zero(deadline))
449
450# Whether slot s holds an expired entry (from its timing words in lk).
451def gone_hi(+lo: U32, now: W.U64, r: Array<U32> & U32) -> Array<U32> & Bool:
452 (lk, +hi) = r
453 (lk, expired(W.U64{lo, hi}, now))
454
455def gone_lo(+s: U32, now: W.U64, r: Array<U32> & U32) -> Array<U32> & Bool:
456 (lk, +lo) = r
457 gone_hi(lo, now, Array.get(U32, lk, dhi_idx(s)))
458
459def gone_t(+s: U32, now: W.U64, lk: Array<U32>, timed: Bool) -> Array<U32> & Bool:
460 match timed:
461 case False{}:
462 (lk, False{})
463 case True{}:
464 gone_lo(s, now, Array.get(U32, lk, dlo_idx(s)))
465
466def gone_r(+s: U32, now: W.U64, r: Array<U32> & U32) -> Array<U32> & Bool:
467 (lk, +t) = r
468 gone_t(s, now, lk, U32.is_ne(t, 0))
469
470def gone(lk: Array<U32>, +s: U32, now: W.U64) -> Array<U32> & Bool:
471 gone_r(s, now, Array.get(U32, lk, tidx(s)))
472
473# ---- reads ----
474
475def miss_if(a, -V: Kind(a), f: LRU<a, V>, +tracked: Bool) -> LRU<a, V>:
476 match tracked:
477 case True{}:
478 fbump(a, V, 4, f)
479 case False{}:
480 f
481
482def rd_live(a, -V: Kind(a), f: LRU<a, V>, +s: U32, +tracked: Bool, v: V) -> LRU<a, V> & Maybe<a, V>:
483 match tracked:
484 case True{}:
485 (touch(a, V, fbump(a, V, 3, f), s), Some{v})
486 case False{}:
487 (f, Some{v})
488
489def rd_gone(a, -V: Kind(a), +tracked: Bool, r: LRU<a, V> & Maybe<a, V>) -> LRU<a, V> & Maybe<a, V>:
490 (f, v) = r
491 (miss_if(a, V, f, tracked), None{})
492
493def rd_exp_m(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, +s: U32, +at: U32, +tracked: Bool, r: Array<U32> & U32) -> LRU<a, V> & Maybe<a, V>:
494 (m, +mask) = r
495 rd_gone(a, V, tracked, drop_slot(a, V, F{cap, n, head, tail, free, m, H.del_at(tab, mask, at), ks, ents, lk}, s, 2))
496
497# The expired entry found at bucket `at`: dropped as a removal, read as a miss.
498def rd_expire(a, -V: Kind(a), f: LRU<a, V>, +s: U32, +at: U32, +tracked: Bool) -> LRU<a, V> & Maybe<a, V>:
499 F{+cap, +n, +head, +tail, +free, m, tab, ks, ents, lk} = f
500 rd_exp_m(a, V, cap, n, head, tail, free, tab, ks, ents, lk, s, at, tracked, Array.get(U32, m, 6))
501
502
503
504def rd_val(-V: Data, f: LRU<&2, V>, +s: U32, +tracked: Bool, m: Maybe<&2, V>) -> LRU<&2, V> & Maybe<&2, V>:
505 match m:
506 case None{}:
507 (miss_if(&2, V, f, tracked), None{})
508 case Some{v}:
509 rd_live(&2, V, f, s, tracked, v)
510
511def rd_v(-V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, tab: Array<U32>, ks: Array<String>, lk: Array<U32>, +s: U32, +tracked: Bool, r: Array<Maybe<&2, V>> & Maybe<&2, V>) -> LRU<&2, V> & Maybe<&2, V>:
512 (ents, e) = r
513 rd_val(V, F{cap, n, head, tail, free, m, tab, ks, ents, lk}, s, tracked, e)
514
515def rd_live_f(-V: Data, f: LRU<&2, V>, +s: U32, +tracked: Bool) -> LRU<&2, V> & Maybe<&2, V>:
516 F{+cap, +n, +head, +tail, +free, m, tab, ks, ents, lk} = f
517 rd_v(V, cap, n, head, tail, free, m, tab, ks, lk, s, tracked, Array.get(Maybe<&2, V>, ents, s))
518
519def rd_gone_pick(-V: Data, f: LRU<&2, V>, +s: U32, +at: U32, +tracked: Bool, g: Bool) -> LRU<&2, V> & Maybe<&2, V>:
520 match g:
521 case False{}:
522 rd_live_f(V, f, s, tracked)
523 case True{}:
524 rd_expire(&2, V, f, s, at, tracked)
525
526def rd_g(-V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<&2, V>>, +s: U32, +at: U32, +tracked: Bool, r: Array<U32> & Bool) -> LRU<&2, V> & Maybe<&2, V>:
527 (lk, g) = r
528 rd_gone_pick(V, F{cap, n, head, tail, free, m, tab, ks, ents, lk}, s, at, tracked, g)
529
530def rd_hit(-V: Data, f: LRU<&2, V>, +s: U32, +at: U32, now: W.U64, +tracked: Bool) -> LRU<&2, V> & Maybe<&2, V>:
531 F{+cap, +n, +head, +tail, +free, m, tab, ks, ents, lk} = f
532 rd_g(V, cap, n, head, tail, free, m, tab, ks, ents, s, at, tracked, gone(lk, s, now))
533
534def rd_pick(-V: Data, f: LRU<&2, V>, +at: U32, +l: U32, now: W.U64, +tracked: Bool, absent: Bool) -> LRU<&2, V> & Maybe<&2, V>:
535 match absent:
536 case True{}:
537 (miss_if(&2, V, f, tracked), None{})
538 case False{}:
539 rd_hit(V, f, H.slot(l), at, now, tracked)
540
541def rd_fd(-V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, ents: Array<Maybe<&2, V>>, lk: Array<U32>, now: W.U64, +tracked: Bool, fd: H.Found) -> LRU<&2, V> & Maybe<&2, V>:
542 H.FD{tab, ks, key, +at, +l} = fd
543 rd_pick(V, F{cap, n, head, tail, free, m, tab, ks, ents, lk}, at, l, now, tracked, U32.is_eq(l, 0))
544
545def rd_found(-V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, ents: Array<Maybe<&2, V>>, lk: Array<U32>, now: W.U64, +tracked: Bool, r: H.Found & U32) -> LRU<&2, V> & Maybe<&2, V>:
546 (fd, w) = r
547 rd_fd(V, cap, n, head, tail, free, m, ents, lk, now, tracked, fd)
548
549def rd_m(-V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<&2, V>>, lk: Array<U32>, key: String, now: W.U64, +tracked: Bool, r: Array<U32> & U32) -> LRU<&2, V> & Maybe<&2, V>:
550 (m, +mask) = r
551 rd_found(V, cap, n, head, tail, free, m, ents, lk, now, tracked, H.probe(tab, ks, mask, key))
552
553def read_long(-V: Data, f: LRU<&2, V>, key: String, now: W.U64, +tracked: Bool) -> LRU<&2, V> & Maybe<&2, V>:
554 F{+cap, +n, +head, +tail, +free, m, tab, ks, ents, lk} = f
555 rd_m(V, cap, n, head, tail, free, tab, ks, ents, lk, key, now, tracked, Array.get(U32, m, 6))
556
557def read(-V: Data, f: LRU<&2, V>, key: String, now: W.U64, +tracked: Bool) -> LRU<&2, V> & Maybe<&2, V>:
558 read_long(V, f, key, now, tracked)
559
560def get(-V: Data, f: LRU<&2, V>, key: String, now: W.U64) -> LRU<&2, V> & Maybe<&2, V>:
561 read(V, f, key, now, True{})
562
563def len(a, -V: Kind(a), f: LRU<a, V>) -> LRU<a, V> & U32:
564 F{cap, +n, head, tail, free, m, tab, ks, ents, lk} = f
565 (F{cap, n, head, tail, free, m, tab, ks, ents, lk}, n)
566
567# A copy of the meta words: counter c is at 16 + 2c (low) and 17 + 2c (high).
568def cnt_fin(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, r: Array<U32> & Array<U32>) -> LRU<a, V> & Array<U32>:
569 (m, copy) = r
570 (F{cap, n, head, tail, free, m, tab, ks, ents, lk}, copy)
571
572def counters(a, -V: Kind(a), f: LRU<a, V>) -> LRU<a, V> & Array<U32>:
573 F{cap, n, head, tail, free, m, tab, ks, ents, lk} = f
574 cnt_fin(a, V, cap, n, head, tail, free, tab, ks, ents, lk, Array.clone(U32, m))
575
576def set_life(m: Array<U32>, s: W.U64, +on: U32) -> Array<U32>:
577 W.U64{+lo, +hi} = s
578 Array.set(U32, Array.set(U32, Array.set(U32, m, 3, on), 4, lo), 5, hi)
579
580# Lifetime in nanoseconds; zero means entries never expire. It is kept in
581# milliseconds, so a deadline is one limb addition.
582def set_lifetime_packed(a, -V: Kind(a), f: LRU<a, V>, +ns: W.U64) -> LRU<a, V>:
583 F{cap, n, head, tail, free, m, tab, ks, ents, lk} = f
584 F{cap, n, head, tail, free, set_life(m, W.div_small_signed(ns, 1000000), W.carry(Bool.not(W.is_zero(ns)))), tab, ks, ents, lk}
585
586def peek(-V: Data, f: LRU<&2, V>, key: String, now: W.U64) -> LRU<&2, V> & Maybe<&2, V>:
587 read(V, f, key, now, False{})
588
589
590
591def ct_expire(a, -V: Kind(a), r: LRU<a, V> & Maybe<a, V>) -> LRU<a, V> & Bool:
592 (f, v) = r
593 (f, False{})
594
595def ct_pick(a, -V: Kind(a), f: LRU<a, V>, +s: U32, +at: U32, g: Bool) -> LRU<a, V> & Bool:
596 match g:
597 case False{}:
598 (f, True{})
599 case True{}:
600 ct_expire(a, V, rd_expire(a, V, f, s, at, False{}))
601
602def ct_g(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, +s: U32, +at: U32, r: Array<U32> & Bool) -> LRU<a, V> & Bool:
603 (lk, g) = r
604 ct_pick(a, V, F{cap, n, head, tail, free, m, tab, ks, ents, lk}, s, at, g)
605
606def ct_hit(a, -V: Kind(a), f: LRU<a, V>, +s: U32, +at: U32, now: W.U64) -> LRU<a, V> & Bool:
607 F{+cap, +n, +head, +tail, +free, m, tab, ks, ents, lk} = f
608 ct_g(a, V, cap, n, head, tail, free, m, tab, ks, ents, s, at, gone(lk, s, now))
609
610def ct_found_pick(a, -V: Kind(a), f: LRU<a, V>, +at: U32, +l: U32, now: W.U64, absent: Bool) -> LRU<a, V> & Bool:
611 match absent:
612 case True{}:
613 (f, False{})
614 case False{}:
615 ct_hit(a, V, f, H.slot(l), at, now)
616
617def ct_fd(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, ents: Array<Maybe<a, V>>, lk: Array<U32>, now: W.U64, fd: H.Found) -> LRU<a, V> & Bool:
618 H.FD{tab, ks, key, +at, +l} = fd
619 ct_found_pick(a, V, F{cap, n, head, tail, free, m, tab, ks, ents, lk}, at, l, now, U32.is_eq(l, 0))
620
621def ct_found(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, ents: Array<Maybe<a, V>>, lk: Array<U32>, now: W.U64, r: H.Found & U32) -> LRU<a, V> & Bool:
622 (fd, w) = r
623 ct_fd(a, V, cap, n, head, tail, free, m, ents, lk, now, fd)
624
625def ct_m(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, key: String, now: W.U64, r: Array<U32> & U32) -> LRU<a, V> & Bool:
626 (m, +mask) = r
627 ct_found(a, V, cap, n, head, tail, free, m, ents, lk, now, H.probe(tab, ks, mask, key))
628
629def ct_long(a, -V: Kind(a), f: LRU<a, V>, key: String, now: W.U64) -> LRU<a, V> & Bool:
630 F{+cap, +n, +head, +tail, +free, m, tab, ks, ents, lk} = f
631 ct_m(a, V, cap, n, head, tail, free, tab, ks, ents, lk, key, now, Array.get(U32, m, 6))
632
633def contains(a, -V: Kind(a), f: LRU<a, V>, key: String, now: W.U64) -> LRU<a, V> & Bool:
634 ct_long(a, V, f, key, now)
635
636def rm_hit(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, +at: U32, +l: U32, r: Array<U32> & U32) -> LRU<a, V> & Maybe<a, V>:
637 (m, +mask) = r
638 drop_slot(a, V, F{cap, n, head, tail, free, m, H.del_at(tab, mask, at), ks, ents, lk}, H.slot(l), 2)
639
640def rm_go(a, -V: Kind(a), f: LRU<a, V>, +at: U32, +l: U32) -> LRU<a, V> & Maybe<a, V>:
641 F{+cap, +n, +head, +tail, +free, m, tab, ks, ents, lk} = f
642 rm_hit(a, V, cap, n, head, tail, free, tab, ks, ents, lk, at, l, Array.get(U32, m, 6))
643
644def rm_pick(a, -V: Kind(a), f: LRU<a, V>, +at: U32, +l: U32, absent: Bool) -> LRU<a, V> & Maybe<a, V>:
645 match absent:
646 case True{}:
647 (f, None{})
648 case False{}:
649 rm_go(a, V, f, at, l)
650
651def rm_pick2(a, -V: Kind(a), f: LRU<a, V>, +at: U32, +l: U32, absent: Bool) -> LRU<a, V> & Maybe<a, V>:
652 rm_pick(a, V, f, at, l, absent)
653
654def rm_fd(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, ents: Array<Maybe<a, V>>, lk: Array<U32>, fd: H.Found) -> LRU<a, V> & Maybe<a, V>:
655 H.FD{tab, ks, key, +at, +l} = fd
656 rm_pick2(a, V, F{cap, n, head, tail, free, m, tab, ks, ents, lk}, at, l, U32.is_eq(l, 0))
657
658def rm_found(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, ents: Array<Maybe<a, V>>, lk: Array<U32>, r: H.Found & U32) -> LRU<a, V> & Maybe<a, V>:
659 (fd, w) = r
660 rm_fd(a, V, cap, n, head, tail, free, m, ents, lk, fd)
661
662def rm_m(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, key: String, r: Array<U32> & U32) -> LRU<a, V> & Maybe<a, V>:
663 (m, +mask) = r
664 rm_found(a, V, cap, n, head, tail, free, m, ents, lk, H.probe(tab, ks, mask, key))
665
666# Fused one-character remove: the probe loop finishes the operation itself,
667# so no continuation is pushed around it.
668def qrm(a, -V: Kind(a), fuel: Nat, s: H.QStep, +mask: U32, +w: U32, +i: U32, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>) -> LRU<a, V> & Maybe<a, V>:
669 match fuel s:
670 case 0n H.QEnd{tab}:
671 (F{cap, n, head, tail, free, m, tab, ks, ents, lk}, None{})
672 case 0n H.QHit{tab, +l}:
673 drop_slot(a, V, F{cap, n, head, tail, free, m, H.del_at(tab, mask, i), ks, ents, lk}, H.slot(l), 2)
674 case 0n H.QNext{tab}:
675 (F{cap, n, head, tail, free, m, tab, ks, ents, lk}, None{})
676 case 1n+p H.QEnd{tab}:
677 (F{cap, n, head, tail, free, m, tab, ks, ents, lk}, None{})
678 case 1n+p H.QHit{tab, +l}:
679 drop_slot(a, V, F{cap, n, head, tail, free, m, H.del_at(tab, mask, i), ks, ents, lk}, H.slot(l), 2)
680 case 1n+p H.QNext{tab}:
681 +j = H.bnext(i, mask)
682 qrm(a, V, p, H.qstep(tab, j, w), mask, w, j, cap, n, head, tail, free, m, ks, ents, lk)
683
684def rm_q2(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, +w: U32, r: Array<U32> & U32) -> LRU<a, V> & Maybe<a, V>:
685 (m, +mask) = r
686 qrm(a, V, U32.to_nat(U32.inc(mask)), H.qstep(tab, HS.bucket(w, mask), w), mask, w, HS.bucket(w, mask), cap, n, head, tail, free, m, ks, ents, lk)
687
688def rm_q(a, -V: Kind(a), f: LRU<a, V>, +w: U32) -> LRU<a, V> & Maybe<a, V>:
689 F{+cap, +n, +head, +tail, +free, m, tab, ks, ents, lk} = f
690 rm_q2(a, V, cap, n, head, tail, free, tab, ks, ents, lk, w, Array.get(U32, m, 6))
691
692def remove_long(a, -V: Kind(a), f: LRU<a, V>, key: String) -> LRU<a, V> & Maybe<a, V>:
693 F{+cap, +n, +head, +tail, +free, m, tab, ks, ents, lk} = f
694 rm_m(a, V, cap, n, head, tail, free, tab, ks, ents, lk, key, Array.get(U32, m, 6))
695
696def rm_short(a, -V: Kind(a), f: LRU<a, V>, +c: U32, ok: Bool) -> LRU<a, V> & Maybe<a, V>:
697 match ok:
698 case True{}:
699 rm_q(a, V, f, H.short_word(c))
700 case False{}:
701 remove_long(a, V, f, SCon{Chr{c}, SNil{}})
702
703def rm_c(a, -V: Kind(a), f: LRU<a, V>, +c: U32, t: String) -> LRU<a, V> & Maybe<a, V>:
704 match t:
705 case SNil{}:
706 rm_short(a, V, f, c, U32.is_lt(c, H.tag()))
707 case SCon{d, t2}:
708 remove_long(a, V, f, SCon{Chr{c}, SCon{d, t2}})
709
710def remove(a, -V: Kind(a), f: LRU<a, V>, key: String) -> LRU<a, V> & Maybe<a, V>:
711 match key:
712 case SNil{}:
713 remove_long(a, V, f, SNil{})
714 case SCon{Chr{+c}, t}:
715 rm_c(a, V, f, c, t)
716
717# ---- purge / resize ----
718
719def zero_ctrs(m: Array<U32>) -> Array<U32>:
720 Array.set(U32, Array.set(U32, Array.set(U32, Array.set(U32, Array.set(U32,
721 Array.set(U32, Array.set(U32, Array.set(U32, Array.set(U32, Array.set(U32,
722 Array.set(U32, m, 0, 0), 16, 0), 17, 0), 18, 0), 19, 0), 20, 0), 21, 0), 22, 0), 23, 0), 24, 0), 25, 0)
723
724def purge_b(a, -V: Kind(a), +cap: U32, +n: U32, ks: Array<String>, ents: Array<Maybe<a, V>>, lk: Array<U32>, r: Array<U32> & U32) -> LRU<a, V> & U32:
725 (m2, +bits) = r
726 (F{cap, 0, 0, 0, 0, zero_ctrs(m2), Array.new(U32, U32.to_nat(U32.inc(bits)), 0), ks, ents, lk}, n)
727
728# Every entry and the metrics are cleared; the table keeps its size.
729def purge(a, -V: Kind(a), f: LRU<a, V>) -> LRU<a, V> & U32:
730 F{+cap, +n, head, tail, free, m, tab, ks, ents, lk} = f
731 purge_b(a, V, cap, n, ks, ents, lk, Array.get(U32, m, 7))
732
733type Rz<a, -V: Kind(a)> is Type:
734 RzMore{f: LRU<a, V>}
735 RzDone{f: LRU<a, V>}
736
737def rz_pick(a, -V: Kind(a), f: LRU<a, V>, over: Bool) -> Rz<a, V>:
738 match over:
739 case True{}:
740 RzMore{f}
741 case False{}:
742 RzDone{f}
743
744def rz_check(a, -V: Kind(a), f: LRU<a, V>) -> Rz<a, V>:
745 F{+cap, +n, head, tail, free, m, tab, ks, ents, lk} = f
746 rz_pick(a, V, F{cap, n, head, tail, free, m, tab, ks, ents, lk}, U32.is_lt(cap, n))
747
748def rz_go(a, -V: Kind(a), fuel: Nat, s: Rz<a, V>, +ev: U32) -> LRU<a, V> & Result<&2, &2, String, U32>:
749 match fuel s:
750 case 0n RzMore{f}:
751 (f, Done{ev})
752 case 0n RzDone{f}:
753 (f, Done{ev})
754 case 1n+p RzMore{f}:
755 rz_go(a, V, p, rz_check(a, V, evict_oldest(a, V, f)), U32.inc(ev))
756 case 1n+p RzDone{f}:
757 (f, Done{ev})
758
759def set_cap(a, -V: Kind(a), f: LRU<a, V>, +cap: U32) -> LRU<a, V>:
760 F{c0, +n, head, tail, free, m, tab, ks, ents, lk} = f
761 F{cap, n, head, tail, free, m, tab, ks, ents, lk}
762
763def rz_start(a, -V: Kind(a), f: LRU<a, V>) -> LRU<a, V> & Result<&2, &2, String, U32>:
764 F{cap, +n, head, tail, free, m, tab, ks, ents, lk} = f
765 rz_go(a, V, U32.to_nat(n), rz_check(a, V, F{cap, n, head, tail, free, m, tab, ks, ents, lk}), 0)
766
767def resize_go(a, -V: Kind(a), f: LRU<a, V>, +cap: U32, zero: Bool) -> LRU<a, V> & Result<&2, &2, String, U32>:
768 match zero:
769 case True{}:
770 (f, Fail{"capacity must be positive"})
771 case False{}:
772 rz_start(a, V, set_cap(a, V, f, cap))
773
774# Set a positive capacity, evicting the oldest entries until the cache fits;
775# reports how many were evicted. Capacity 0 fails and changes nothing.
776def resize(a, -V: Kind(a), f: LRU<a, V>, +cap: U32) -> LRU<a, V> & Result<&2, &2, String, U32>:
777 resize_go(a, V, f, cap, U32.is_eq(cap, 0))
778
779# ---- keys ----
780
781type Kx<a, -V: Kind(a)> is Type:
782 KMore{f: LRU<a, V>}
783 KDone{f: LRU<a, V>}
784
785def kx_pick(a, -V: Kind(a), f: LRU<a, V>, gone: Bool) -> Kx<a, V>:
786 match gone:
787 case True{}:
788 KMore{f}
789 case False{}:
790 KDone{f}
791
792
793
794def kx_g(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, tab: Array<U32>, ks: Array<String>, ents: Array<Maybe<a, V>>, r: Array<U32> & Bool) -> Kx<a, V>:
795 (lk, g) = r
796 kx_pick(a, V, F{cap, n, head, tail, free, m, tab, ks, ents, lk}, g)
797
798def kx_head(a, -V: Kind(a), f: LRU<a, V>, +now: W.U64) -> Kx<a, V>:
799 F{+cap, +n, +head, +tail, +free, m, tab, ks, ents, lk} = f
800 kx_g(a, V, cap, n, head, tail, free, m, tab, ks, ents, gone(lk, H.slot(head), now))
801
802def kx_if(a, -V: Kind(a), f: LRU<a, V>, +now: W.U64, empty: Bool) -> Kx<a, V>:
803 match empty:
804 case True{}:
805 KDone{f}
806 case False{}:
807 kx_head(a, V, f, now)
808
809def kx_check(a, -V: Kind(a), f: LRU<a, V>, +now: W.U64) -> Kx<a, V>:
810 F{cap, n, +head, tail, free, m, tab, ks, ents, lk} = f
811 kx_if(a, V, F{cap, n, head, tail, free, m, tab, ks, ents, lk}, now, U32.is_eq(head, 0))
812
813def drop_head(a, -V: Kind(a), f: LRU<a, V>) -> LRU<a, V>:
814 F{cap, n, +head, tail, free, m, tab, ks, ents, lk} = f
815 drop_v(a, V, remove_slot(a, V, F{cap, n, head, tail, free, m, tab, ks, ents, lk}, H.slot(head), 2))
816
817def kx_go(a, -V: Kind(a), fuel: Nat, +now: W.U64, s: Kx<a, V>) -> LRU<a, V>:
818 match fuel s:
819 case 0n KMore{f}:
820 f
821 case 0n KDone{f}:
822 f
823 case 1n+p KMore{f}:
824 kx_go(a, V, p, now, kx_check(a, V, drop_head(a, V, f), now))
825 case 1n+p KDone{f}:
826 f
827
828type Walk is Type:
829 WK{ks: Array<String>, lk: Array<U32>, acc: List<&2, String>, at: U32}
830
831def wk_p(ks: Array<String>, acc: List<&2, String>, r: Array<U32> & U32) -> Walk:
832 (lk, +p) = r
833 WK{ks, lk, acc, p}
834
835def wk_c(ks: Array<String>, lk: Array<U32>, acc: List<&2, String>, +at: U32, kk: String & String) -> Walk:
836 (k1, k2) = kk
837 wk_p(Array.set(String, ks, H.slot(at), k1), Con{k2, acc}, Array.get(U32, lk, pidx(H.slot(at))))
838
839def wk_k(lk: Array<U32>, acc: List<&2, String>, +at: U32, r: Array<String> & String) -> Walk:
840 (ks, k) = r
841 wk_c(ks, lk, acc, at, H.str_copy(k))
842
843def wk_word(ks: Array<String>, acc: List<&2, String>, +at: U32, +kw: U32, lk: Array<U32>, short: Bool) -> Walk:
844 match short:
845 case True{}:
846 wk_p(ks, Con{SCon{Chr{U32.and(kw, 2147483647)}, SNil{}}, acc}, Array.get(U32, lk, pidx(H.slot(at))))
847 case False{}:
848 wk_k(lk, acc, at, Array.swap(String, ks, H.slot(at), SNil{}))
849
850def wk_w(ks: Array<String>, acc: List<&2, String>, +at: U32, r: Array<U32> & U32) -> Walk:
851 (lk, +kw) = r
852 wk_word(ks, acc, at, kw, lk, H.is_short(kw))
853
854# A one-character key is stored only as its tagged word.
855def wk_step(w: Walk) -> Walk:
856 WK{ks, lk, acc, +at} = w
857 wk_w(ks, acc, at, Array.get(U32, lk, hidx(H.slot(at))))
858
859def wk_loop(fuel: Nat, w: Walk) -> Walk:
860 match fuel:
861 case 0n:
862 w
863 case 1n+p:
864 wk_loop(p, wk_step(w))
865
866def keys_fin(a, -V: Kind(a), +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, m: Array<U32>, tab: Array<U32>, ents: Array<Maybe<a, V>>, w: Walk) -> LRU<a, V> & List<&2, String>:
867 WK{ks, lk, acc, at} = w
868 (F{cap, n, head, tail, free, m, tab, ks, ents, lk}, acc)
869
870def keys_list(a, -V: Kind(a), f: LRU<a, V>) -> LRU<a, V> & List<&2, String>:
871 F{+cap, +n, +head, +tail, +free, m, tab, ks, ents, lk} = f
872 keys_fin(a, V, cap, n, head, tail, free, m, tab, ents, wk_loop(U32.to_nat(n), WK{ks, lk, Nil{}, tail}))
873
874def keys_n(a, -V: Kind(a), +now: W.U64, f: LRU<a, V>) -> LRU<a, V>:
875 F{cap, +n, head, tail, free, m, tab, ks, ents, lk} = f
876 kx_go(a, V, U32.to_nat(n), now, kx_check(a, V, F{cap, n, head, tail, free, m, tab, ks, ents, lk}, now))
877
878# The keys oldest first, after the oldest EXPIRED prefix is removed (each a
879# removal), stopping at the first immortal or live oldest entry.
880def keys(a, -V: Kind(a), f: LRU<a, V>, +now: W.U64) -> LRU<a, V> & List<&2, String>:
881 keys_list(a, V, keys_n(a, V, now, f))