`drained` nonzero: the last instruction also waits until every
fixed-latency result in flight is ready, so whatever the program is placed
before (a piece of a larger program, a loop's back edge) reads nothing
early
231def sm86CompactStallsWith =
232 (lambda unrestricted drained : Nat .
233 (lambda unrestricted program : (family SM86Program) .
234 (app (app
235 (eliminate CompactionAnnotated
236 (lambda unrestricted current : (family CompactionAnnotated) .
237 (pi unrestricted now : Nat . (pi unrestricted pending : (family CompactionPending) . (family SM86Program))))
238 (sm86AnnotateProgram program)
239 (branch CompactionAnnotatedEnd .
240 (lambda unrestricted now : Nat . (lambda unrestricted pending : (family CompactionPending) .
241 (constructor SM86Program SM86ProgramEnd))))
242 (branch CompactionAnnotatedNext instruction needs issue setKeys latency minimum tail induction .
243 (lambda unrestricted now : Nat . (lambda unrestricted pending : (family CompactionPending) .
244 (let unrestricted issued =
245 (scIssue issue (naturalAdd now latency)
246 (scIssue setKeys (naturalAdd now sm86BarrierSetCycles) pending))
247 in (let unrestricted need =
248 (eliminate CompactionAnnotated
249 (lambda unrestricted current : (family CompactionAnnotated) . Nat)
250 tail
251 (branch CompactionAnnotatedEnd . (naturalSelect drained (scLatest issued) zero))
252 (branch CompactionAnnotatedNext followingInstruction followingNeeds followingIssue followingSetKeys followingLatency followingMinimum followingTail followingInduction .
253 (scReadyOf issued followingNeeds)))
254 in (let unrestricted stall = (scMax minimum
255 (naturalSelect (naturalLess (naturalAdd now 1) need) (naturalSaturatingSubtract need now) 1))
256 in (let unrestricted clamped = (naturalSelect (naturalLess 15 stall) 15 stall)
257 in (constructor SM86Program SM86ProgramNext (scWithStall instruction clamped)
258 (induction (naturalAdd now clamped) (scPrune issued (naturalAdd now clamped))))))))))))
259 0) (constructor CompactionPending CompactionPendingEnd))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.