retry.bend

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