retry.bend
bend-kit-retry@0.2.0.0 · 254 lines · 0 definitions
1# Retry policy: a shared attempt budget, an operation deadline, bounded backoff, and a circuit breaker.
2# All times are ms on one monotonic clock. The caller reads the clock; these defs are pure.
3import Base
4
5# left: attempts the whole operation may still start, the first one included. Nested layers share one Budget.
6# deadline: no attempt starts at or after this time. None: no deadline.
7type Budget is Data:
8 Budget{left: Nat, deadline: Maybe<&2, Nat>}
9
10type Deny is Data:
11 DenyLate{}
12 DenySpent{}
13 DenyOpen{}
14
15type Gate is Data:
16 GateGo{}
17 GateNo{why: Deny}
18
19# threshold: failures in a row, each inside window ms of the newest, that open the circuit. cooldown: ms it stays open.
20# probes: attempts allowed at once while half-open.
21type Circuit is Data:
22 Circuit{threshold: Nat, window: Nat, cooldown: Nat, probes: Nat}
23
24# Closed: the failures since the last success that are still inside the window, newest first.
25# Open: no attempt before until. Half: probes in flight.
26type State is Data:
27 CircuitClosed{fails: List<&2, Nat>}
28 CircuitOpen{until: Nat}
29 CircuitHalf{busy: Nat}
30
31type Breaker is Data:
32 BreakerOff{}
33 BreakerOn{circuit: Circuit, state: State}
34
35# Settled: a success. Failed: a failure that another try would repeat. Unsafe: a transient failure of a
36# request that must not repeat. Transient: another try can help; after is the server's wait in ms.
37type Outcome is Data:
38 Settled{}
39 Failed{}
40 Unsafe{}
41 Transient{after: Maybe<&2, Nat>}
42
43# attempts: tries in one layer, the first one included. base: the first backoff in ms. cap: the longest wait in ms.
44# deadline: ms from the start of the operation to its deadline. None: no deadline.
45type Policy is Data:
46 Policy{attempts: Nat, base: Nat, cap: U32, deadline: Maybe<&2, Nat>}
47
48type Plan is Data:
49 PlanStop{}
50 PlanWait{ms: Nat}
51
52# ---- budget
53
54def Budget.new(+attempts: Nat, +now: Nat, ms: Maybe<&2, Nat>) -> Budget:
55 match ms:
56 case None{}:
57 Budget{attempts, None{}}
58 case Some{m}:
59 Budget{attempts, Some{Nat.add(now, m)}}
60
61def Budget.late(+now: Nat, d: Maybe<&2, Nat>) -> Bool:
62 match d:
63 case None{}:
64 False{}
65 case Some{t}:
66 Nat.is_le(t, now)
67
68# ---- circuit
69
70# The failure times still inside the window: now < t + window. Newest first, so the first old time ends the list.
71def prune(+now: Nat, +window: Nat, fs: List<&2, Nat>) -> List<&2, Nat>:
72 match fs:
73 case Nil{}:
74 Nil{}
75 case Con{+t, rest}:
76 Bool.pick(List<&2, Nat>, Nat.is_lt(now, Nat.add(t, window)), Con{t, prune(now, window, rest)}, Nil{})
77
78def Circuit.probes(c: Circuit) -> Nat:
79 Circuit{t, w, cd, p} = c
80 p
81
82def Circuit.cooldown(c: Circuit) -> Nat:
83 Circuit{t, w, cd, p} = c
84 cd
85
86def half.admit(go: Bool, +k: Nat) -> State & Bool:
87 match go:
88 case True{}:
89 (CircuitHalf{1n+k}, True{})
90 case False{}:
91 (CircuitHalf{k}, False{})
92
93def open.admit(early: Bool, +p: Nat, +u: Nat) -> State & Bool:
94 match early:
95 case True{}:
96 (CircuitOpen{u}, False{})
97 case False{}:
98 half.admit(Nat.is_lt(0n, p), 0n)
99
100# Closed admits. Open admits nothing before until; at or after until it turns half-open and admits a probe.
101# Half-open admits while fewer than probes are in flight.
102def State.admit(+c: Circuit, s: State, +now: Nat) -> State & Bool:
103 match s:
104 case CircuitClosed{fs}:
105 (CircuitClosed{fs}, True{})
106 case CircuitOpen{+u}:
107 open.admit(Nat.is_lt(now, u), Circuit.probes(c), u)
108 case CircuitHalf{+k}:
109 half.admit(Nat.is_lt(k, Circuit.probes(c)), k)
110
111def closed.trip(under: Bool, fs: List<&2, Nat>, +until: Nat) -> State:
112 match under:
113 case True{}:
114 CircuitClosed{fs}
115 case False{}:
116 CircuitOpen{until}
117
118def closed.fail(+c: Circuit, fs: List<&2, Nat>, +now: Nat) -> State:
119 Circuit{+t, +w, +cd, p} = c
120 +kept = {Con{now, prune(now, w, fs)} : List<&2, Nat>}
121 closed.trip(Nat.is_lt(List.length(&2, Nat, kept), t), kept, Nat.add(now, cd))
122
123# A closed success clears the failures. A closed failure opens the circuit when the window then holds threshold
124# failures. A half-open success closes it; a half-open failure opens it again for cooldown. An attempt that ends
125# while open changes nothing.
126def State.done(+c: Circuit, s: State, +now: Nat, failed: Bool) -> State:
127 match s:
128 case CircuitClosed{fs}:
129 match failed:
130 case False{}:
131 CircuitClosed{Nil{}}
132 case True{}:
133 closed.fail(c, fs, now)
134 case CircuitOpen{u}:
135 CircuitOpen{u}
136 case CircuitHalf{k}:
137 match failed:
138 case False{}:
139 CircuitClosed{Nil{}}
140 case True{}:
141 CircuitOpen{Nat.add(now, Circuit.cooldown(c))}
142
143def Breaker.new(c: Circuit) -> Breaker:
144 BreakerOn{c, CircuitClosed{Nil{}}}
145
146def Breaker.on(+c: Circuit, x: State & Bool) -> Breaker & Bool:
147 (s, ok) = x
148 (BreakerOn{c, s}, ok)
149
150def Breaker.admit(br: Breaker, +now: Nat) -> Breaker & Bool:
151 match br:
152 case BreakerOff{}:
153 (BreakerOff{}, True{})
154 case BreakerOn{+c, s}:
155 Breaker.on(c, State.admit(c, s, now))
156
157def Breaker.done(br: Breaker, +now: Nat, failed: Bool) -> Breaker:
158 match br:
159 case BreakerOff{}:
160 BreakerOff{}
161 case BreakerOn{+c, s}:
162 BreakerOn{c, State.done(c, s, now, failed)}
163
164# ---- admission
165
166def admit.ok(ok: Bool, br: Breaker, +p: Nat, d: Maybe<&2, Nat>) -> Breaker & Budget & Gate:
167 match ok:
168 case True{}:
169 (br, Budget{p, d}, GateGo{})
170 case False{}:
171 (br, Budget{1n+p, d}, GateNo{DenyOpen{}})
172
173def admit.breaker(x: Breaker & Bool, +p: Nat, d: Maybe<&2, Nat>) -> Breaker & Budget & Gate:
174 (br, ok) = x
175 admit.ok(ok, br, p, d)
176
177def admit.late(late: Bool, br: Breaker, left: Nat, d: Maybe<&2, Nat>, +now: Nat) -> Breaker & Budget & Gate:
178 match late:
179 case True{}:
180 (br, Budget{left, d}, GateNo{DenyLate{}})
181 case False{}:
182 match left:
183 case 0n:
184 (br, Budget{0n, d}, GateNo{DenySpent{}})
185 case 1n+p:
186 admit.breaker(Breaker.admit(br, now), p, d)
187
188# Ask to start one attempt at now. The deadline is checked first, then the budget, then the breaker.
189# Only GateGo takes one attempt from the budget.
190def admit(br: Breaker, b: Budget, +now: Nat) -> Breaker & Budget & Gate:
191 Budget{left, +d} = b
192 admit.late(Budget.late(now, d), br, left, d, now)
193
194# ---- backoff
195
196# min(cap, base * 2^n), doubled one step at a time, so no step passes cap.
197def delay(n: Nat, +base: Nat, +cap: Nat) -> Nat:
198 match n:
199 case 0n:
200 Nat.min(base, cap)
201 case 1n+p:
202 +d = delay(p, base, cap)
203 Nat.min(Nat.add(d, d), cap)
204
205# Equal jitter: d / 2, plus r mod (d / 2 + 1). The wait is in [d / 2, d] for every r.
206def jitter(+d: Nat, +r: Nat) -> Nat:
207 +h = Nat.div(d, 2n)
208 Nat.add(h, Nat.mod(r, 1n+h))
209
210# The wait before retry n (0 first): the server's wait when it gave one, else the jittered backoff. At most cap.
211def wait(after: Maybe<&2, Nat>, p: Policy, +n: Nat, +r: Nat) -> Nat:
212 match after:
213 case None{}:
214 Policy{a, +base, +cap, d} = p
215 jitter(delay(n, base, U32.to_nat(cap)), r)
216 case Some{+ms}:
217 Policy{a, base, +cap, d} = p
218 Nat.min(ms, U32.to_nat(cap))
219
220def plan.left(left: Nat, +w: Nat, d: Maybe<&2, Nat>, +now: Nat) -> Plan:
221 match left:
222 case 0n:
223 PlanStop{}
224 case 1n+k:
225 Bool.pick(Plan, Budget.late(Nat.add(now, w), d), PlanStop{}, PlanWait{w})
226
227def plan.at(+w: Nat, b: Budget, +now: Nat) -> Plan:
228 Budget{left, d} = b
229 plan.left(left, w, d, now)
230
231# After an attempt ends at now: stop, or wait ms and then ask admit again. Settled, Failed, and Unsafe always stop.
232# A transient outcome stops when the budget is spent or the wait would reach the deadline.
233def plan(o: Outcome, p: Policy, b: Budget, +n: Nat, +now: Nat, +r: Nat) -> Plan:
234 match o:
235 case Settled{}:
236 PlanStop{}
237 case Failed{}:
238 PlanStop{}
239 case Unsafe{}:
240 PlanStop{}
241 case Transient{after}:
242 plan.at(wait(after, p, n, r), b, now)
243
244# Failed, Unsafe, and Transient count as failures for the breaker.
245def failed(o: Outcome) -> Bool:
246 match o:
247 case Settled{}:
248 False{}
249 case Failed{}:
250 True{}
251 case Unsafe{}:
252 True{}
253 case Transient{after}:
254 True{}