1module SM86.Scoreboard
2
3import Accelerator.SM86.Control
4import Accelerator.SM86.Instruction
5import Accelerator.SM86.Operands
6import Accelerator.SM86.Types
7import Data.Bytes
8import Std.List
9import Std.Natural
10
11-- The scoreboard pass: the machine-level check the functional model cannot
12-- make. SM86.MachineModel gives every instruction its result at once; the
13-- silicon does not. A variable-latency instruction (S2R, a global load,
14-- shuffles, shared-memory and tensor-core forms) delivers its destination
15-- later, and the only thing that orders a consumer after it is the control
16-- word: the producer names a write barrier (SB0..SB5) and the consumer's
17-- wait mask names that barrier. A consumer without the wait reads whatever
18-- the register held before -- on the RTX 3090 (2026-09-22) the first linear
19-- step realization read zeros for W, x and t and wrote a record of zeros,
20-- while the functional model had accepted it.
21--
22-- This pass walks the program in order as one straight-line issue stream
23-- (predication does not change issue), keeping the registers whose value is
24-- still in flight and the barrier each waits on. An instruction first
25-- retires every pending register whose barrier is in its wait mask, then any
26-- register it reads or writes that is still pending is a hazard, then its
27-- own variable-latency destinations become pending on its write barrier -- or
28-- on a barrier no mask can name, when it declares none, so every later use
29-- is a hazard. The result is 0 for a clean program, else the ordinal (from
30-- 1) of the first hazardous instruction. Fixed-latency forms are ordered
31-- by their stall counts, which this pass does not model.
32
33family ScoreboardPending : Type 0
34constructor ScoreboardPendingEnd
35constructor ScoreboardPendingNext
36field unrestricted scoreboardPendingRegister : Nat
37field unrestricted scoreboardPendingBarrier : Nat
38recursive unrestricted scoreboardPendingTail
39end-family
40-- Pending as seven byte masks, not a scanned list. The old pending list
41-- grew with every unretired variable-latency write -- barriers a step never
42-- waits on, and barrier 8 (scoreboardNever) which no mask can name -- and
43-- every instruction scanned the whole accumulation per register it touched:
44-- quadratic in the program length (268 s for the wait-stripped 1,259
45-- instruction mutant, 8.4 s clean). One mask per barrier (1..6 and 8)
46-- holds a 1 at each pending register, so membership is seven indexed reads,
47-- issue is one indexed write per written register, and retire swaps in the
48-- shared empty for every barrier the wait mask names: bounded work per
49-- instruction, near-linear overall.
50-- Equivalence (exact, on every program): the old list's multiplicity is
51-- unobservable -- every query is membership by register and every removal
52-- is a bulk delete by barrier, and the masks track exactly the set of live
53-- (register, barrier) pairs through both. RZ (255) is never inserted
54-- (sm86RegisterRun names nothing from it) and stays guarded at lookup.
55family ScoreboardMasks : Type 0
56constructor ScoreboardMasksValue
57field unrestricted scoreboardMasksBarrier1 : Bytes
58field unrestricted scoreboardMasksBarrier2 : Bytes
59field unrestricted scoreboardMasksBarrier3 : Bytes
60field unrestricted scoreboardMasksBarrier4 : Bytes
61field unrestricted scoreboardMasksBarrier5 : Bytes
62field unrestricted scoreboardMasksBarrier6 : Bytes
63field unrestricted scoreboardMasksNever : Bytes
64end-family
65
66-- The result of one instruction: the hazard flag and the pending set after issue.
67family ScoreboardStep : Type 0
68constructor ScoreboardStepValue
69field unrestricted scoreboardStepHazard : Nat
70field unrestricted scoreboardStepPending : (family ScoreboardMasks)
71field unrestricted scoreboardStepReadPending : (family ScoreboardMasks)
72end-family
73
74def scoreboardNever : Nat = 8
75
76
77-- What an instruction reads and writes is Accelerator.SM86.Operands'
78-- one-elimination summary (sm86OpSummaryOfBody, shared with the register
79-- demand: pairs for 64-bit operands, quads for the tensor core's A, C and
80-- D -- until 2026-09-23 this pass listed those as pairs and could miss a
81-- hazard on the upper half); the latency class rides in the same summary.
82
83
84def sbControlOfBody = sm86BodyControlOf
85
86
87-- the write barrier as 1..6 (SB0..SB5), 0 for none
88def scoreboardWriteBarrierOf =
89 (lambda unrestricted control : (family SM86Control) .
90 (eliminate SM86Control
91 (lambda unrestricted current : (family SM86Control) . Nat)
92 control
93 (branch SM86ControlValue stall yield write read wait reuse .
94 (eliminate SM86Barrier
95 (lambda unrestricted current : (family SM86Barrier) . Nat)
96 write
97 (branch SM86Barrier0 . 1)
98 (branch SM86Barrier1 . 2)
99 (branch SM86Barrier2 . 3)
100 (branch SM86Barrier3 . 4)
101 (branch SM86Barrier4 . 5)
102 (branch SM86Barrier5 . 6)
103 (branch SM86Barrier6 . 7)
104 (branch SM86BarrierNone . 0)))))
105
106-- Read barriers retire late source reads. A write barrier retires the
107-- destination but does not protect an LDG address on Ampere: this was
108-- isolated on the RTX 3090 in c28712e8.
109def scoreboardReadBarrierOf =
110 (lambda unrestricted control : (family SM86Control) .
111 (eliminate SM86Control
112 (lambda unrestricted current : (family SM86Control) . Nat) control
113 (branch SM86ControlValue stall yield write read wait reuse .
114 (eliminate SM86Barrier
115 (lambda unrestricted current : (family SM86Barrier) . Nat) read
116 (branch SM86Barrier0 . 1) (branch SM86Barrier1 . 2)
117 (branch SM86Barrier2 . 3) (branch SM86Barrier3 . 4)
118 (branch SM86Barrier4 . 5) (branch SM86Barrier5 . 6)
119 (branch SM86Barrier6 . 7) (branch SM86BarrierNone . 0)))))
120
121def scoreboardWaitMaskOf =
122 (lambda unrestricted control : (family SM86Control) .
123 (eliminate SM86Control
124 (lambda unrestricted current : (family SM86Control) . Nat)
125 control
126 (branch SM86ControlValue stall yield write read wait reuse . (byte-to-nat wait))))
127
128-- bit (barrier - 1) of the mask, for barrier 1..6; never for 0 or 8
129def scoreboardMaskNames =
130 (lambda unrestricted mask : Nat .
131 (lambda unrestricted barrier : Nat .
132 (nat-eliminate
133 (lambda unrestricted current : Nat . Nat)
134 zero
135 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Nat .
136 (naturalAnd (naturalLess predecessor 7)
137 (nat-modulo (nat-divide mask (naturalPowerOfTwo predecessor)) 2))))
138 barrier)))
139
140-- (an empty wait mask retires nothing: the pending masks are kept as they
141-- are, not walked and rebuilt -- most instructions wait on no barrier)
142def sbBytesEmpty : Bytes = (dataBytesRepeatByte (byte 0) 256)
143
144def sbMasksEmpty : (family ScoreboardMasks) =
145 (constructor ScoreboardMasks ScoreboardMasksValue
146 sbBytesEmpty sbBytesEmpty sbBytesEmpty sbBytesEmpty sbBytesEmpty sbBytesEmpty sbBytesEmpty)
147
148-- 1 when the register is pending on any barrier: seven indexed reads, one
149-- machine operation each, no walk
150def sbMasksLookup =
151 (lambda unrestricted pending : (family ScoreboardMasks) .
152 (lambda unrestricted register : Nat .
153 (eliminate ScoreboardMasks
154 (lambda unrestricted current : (family ScoreboardMasks) . Nat)
155 pending
156 (branch ScoreboardMasksValue b1 b2 b3 b4 b5 b6 bn .
157 (nat-less-than zero
158 (nat-add
159 (nat-add
160 (nat-add (bytes-index-nonzero b1 register) (bytes-index-nonzero b2 register))
161 (nat-add (bytes-index-nonzero b3 register) (bytes-index-nonzero b4 register)))
162 (nat-add
163 (nat-add (bytes-index-nonzero b5 register) (bytes-index-nonzero b6 register))
164 (bytes-index-nonzero bn register))))))))
165
166-- RZ is never pending
167def sbMasksAnyPending =
168 (lambda unrestricted pending : (family ScoreboardMasks) .
169 (lambda unrestricted registers : (family StdList Nat) .
170 (eliminate StdList
171 (lambda unrestricted current : (family StdList Nat) . Nat)
172 registers
173 (branch StdListEmpty . zero)
174 (branch StdListCons register tail induction .
175 (nat-eliminate (lambda unrestricted current : Nat . Nat)
176 induction
177 (lambda unrestricted flagPredecessor : Nat . (lambda unrestricted flagRest : Nat .
178 (nat-eliminate (lambda unrestricted current : Nat . Nat)
179 induction
180 (lambda unrestricted flagPredecessor : Nat . (lambda unrestricted flagRest : Nat . (succ zero)))
181 (sbMasksLookup pending register))))
182 (nat-add (nat-less-than register 255) (nat-less-than 255 register)))))))
183
184-- one register issued on one barrier: that barrier's mask gains the bit.
185-- The case is a 0/1 elimination returning the mask unchanged or written,
186-- so only the named mask is ever rebuilt.
187def sbMasksIssueOne =
188 (lambda unrestricted pending : (family ScoreboardMasks) .
189 (lambda unrestricted register : Nat .
190 (lambda unrestricted barrier : Nat .
191 (eliminate ScoreboardMasks
192 (lambda unrestricted current : (family ScoreboardMasks) . (family ScoreboardMasks))
193 pending
194 (branch ScoreboardMasksValue b1 b2 b3 b4 b5 b6 bn .
195 (constructor ScoreboardMasks ScoreboardMasksValue
196 (nat-eliminate (lambda unrestricted current : Nat . Bytes) b1 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Bytes . (bytes-set-index b1 register))) (naturalEqual barrier 1))
197 (nat-eliminate (lambda unrestricted current : Nat . Bytes) b2 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Bytes . (bytes-set-index b2 register))) (naturalEqual barrier 2))
198 (nat-eliminate (lambda unrestricted current : Nat . Bytes) b3 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Bytes . (bytes-set-index b3 register))) (naturalEqual barrier 3))
199 (nat-eliminate (lambda unrestricted current : Nat . Bytes) b4 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Bytes . (bytes-set-index b4 register))) (naturalEqual barrier 4))
200 (nat-eliminate (lambda unrestricted current : Nat . Bytes) b5 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Bytes . (bytes-set-index b5 register))) (naturalEqual barrier 5))
201 (nat-eliminate (lambda unrestricted current : Nat . Bytes) b6 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Bytes . (bytes-set-index b6 register))) (naturalEqual barrier 6))
202 (nat-eliminate (lambda unrestricted current : Nat . Bytes) bn (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Bytes . (bytes-set-index bn register))) (naturalEqual barrier 8))))))))
203
204def sbMasksIssue =
205 (lambda unrestricted barrier : Nat .
206 (lambda unrestricted registers : (family StdList Nat) .
207 (lambda unrestricted pending : (family ScoreboardMasks) .
208 (eliminate StdList
209 (lambda unrestricted current : (family StdList Nat) . (family ScoreboardMasks))
210 registers
211 (branch StdListEmpty . pending)
212 (branch StdListCons register tail induction .
213 (sbMasksIssueOne induction register barrier))))))
214
215-- retire every barrier the wait mask names by swapping in the shared empty;
216-- barrier 8 is never named, so the never mask passes through
217def sbMasksRetire =
218 (lambda unrestricted mask : Nat .
219 (lambda unrestricted pending : (family ScoreboardMasks) .
220 (nat-eliminate
221 (lambda unrestricted current : Nat . (family ScoreboardMasks))
222 pending
223 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : (family ScoreboardMasks) .
224 (eliminate ScoreboardMasks
225 (lambda unrestricted current : (family ScoreboardMasks) . (family ScoreboardMasks))
226 pending
227 (branch ScoreboardMasksValue b1 b2 b3 b4 b5 b6 bn .
228 (constructor ScoreboardMasks ScoreboardMasksValue
229 (nat-eliminate (lambda unrestricted current : Nat . Bytes) b1 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Bytes . sbBytesEmpty)) (scoreboardMaskNames mask 1))
230 (nat-eliminate (lambda unrestricted current : Nat . Bytes) b2 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Bytes . sbBytesEmpty)) (scoreboardMaskNames mask 2))
231 (nat-eliminate (lambda unrestricted current : Nat . Bytes) b3 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Bytes . sbBytesEmpty)) (scoreboardMaskNames mask 3))
232 (nat-eliminate (lambda unrestricted current : Nat . Bytes) b4 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Bytes . sbBytesEmpty)) (scoreboardMaskNames mask 4))
233 (nat-eliminate (lambda unrestricted current : Nat . Bytes) b5 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Bytes . sbBytesEmpty)) (scoreboardMaskNames mask 5))
234 (nat-eliminate (lambda unrestricted current : Nat . Bytes) b6 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Bytes . sbBytesEmpty)) (scoreboardMaskNames mask 6))
235 bn)))))
236 (naturalNonzero mask))))
237
238def sbRegistersNonempty =
239 (lambda unrestricted registers : (family StdList Nat) .
240 (eliminate StdList (lambda unrestricted current : (family StdList Nat) . Nat) registers
241 (branch StdListEmpty . 0)
242 (branch StdListCons register tail induction . 1)))
243
244-- A read barrier is one outstanding token, even when successive stores
245-- read different registers. Reusing SB5 on Coppelius's four AdamW stores
246-- before waiting it left negative second moments in the first RTX 3090
247-- checkpoint (2026-09-27); waiting before each reuse removed them.
248def sbReadBarrierOccupied =
249 (lambda unrestricted pending : (family ScoreboardMasks) .
250 (lambda unrestricted barrier : Nat .
251 (eliminate ScoreboardMasks
252 (lambda unrestricted current : (family ScoreboardMasks) . Nat) pending
253 (branch ScoreboardMasksValue b1 b2 b3 b4 b5 b6 bn .
254 (naturalSelect (naturalEqual barrier 1) (naturalIsZero (bytes-equal b1 sbBytesEmpty))
255 (naturalSelect (naturalEqual barrier 2) (naturalIsZero (bytes-equal b2 sbBytesEmpty))
256 (naturalSelect (naturalEqual barrier 3) (naturalIsZero (bytes-equal b3 sbBytesEmpty))
257 (naturalSelect (naturalEqual barrier 4) (naturalIsZero (bytes-equal b4 sbBytesEmpty))
258 (naturalSelect (naturalEqual barrier 5) (naturalIsZero (bytes-equal b5 sbBytesEmpty))
259 (naturalSelect (naturalEqual barrier 6) (naturalIsZero (bytes-equal b6 sbBytesEmpty)) 0))))))))))
260
261def scoreboardStep =
262 (lambda unrestricted pending : (family ScoreboardMasks) .
263 (lambda unrestricted pendingReads : (family ScoreboardMasks) .
264 (lambda unrestricted summary : (family SM86OpSummary) .
265 (eliminate SM86OpSummary
266 (lambda unrestricted current : (family SM86OpSummary) . (family ScoreboardStep))
267 summary
268 (branch SM86OpSummaryValue reads writes predicateWrites waitKeys setKeys stall latency variable minimum control .
269 (let unrestricted retired = (sbMasksRetire (scoreboardWaitMaskOf control) pending)
270 in (let unrestricted readsRetired = (sbMasksRetire (scoreboardWaitMaskOf control) pendingReads)
271 in (let unrestricted hazard =
272 (naturalOr
273 (naturalOr (sbMasksAnyPending retired reads) (sbMasksAnyPending retired writes))
274 (naturalOr (sbMasksAnyPending readsRetired writes)
275 (naturalAnd (sbRegistersNonempty reads)
276 (sbReadBarrierOccupied readsRetired (scoreboardReadBarrierOf control)))))
277 in (let unrestricted declared = (scoreboardWriteBarrierOf control)
278 in (let unrestricted declaredRead = (scoreboardReadBarrierOf control)
279 in (let unrestricted barrier =
280 (nat-eliminate
281 (lambda unrestricted current : Nat . Nat)
282 (nat-eliminate
283 (lambda unrestricted current : Nat . Nat)
284 zero
285 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Nat . scoreboardNever))
286 variable)
287 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Nat . declared))
288 declared)
289 in
290 (constructor ScoreboardStep ScoreboardStepValue
291 hazard
292 (nat-eliminate
293 (lambda unrestricted current : Nat . (family ScoreboardMasks))
294 retired
295 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : (family ScoreboardMasks) .
296 (sbMasksIssue barrier writes retired)))
297 barrier)
298 (nat-eliminate
299 (lambda unrestricted current : Nat . (family ScoreboardMasks))
300 readsRetired
301 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : (family ScoreboardMasks) .
302 (sbMasksIssue
303 (naturalSelect (naturalIsZero declaredRead) scoreboardNever declaredRead)
304 reads readsRetired)))
305 (naturalAnd (naturalOr variable (naturalNonzero declaredRead))
306 (sbRegistersNonempty reads)))))))))))))))
307
308def scoreboardBodyOf =
309 (lambda unrestricted instruction : (family SM86Instruction) .
310 (eliminate SM86Instruction
311 (lambda unrestricted current : (family SM86Instruction) . (family SM86InstructionBody))
312 instruction
313 (branch SM86InstructionValue guard body . body)))
314
315-- 0 when clean, else the ordinal (from 1) of the first hazardous instruction.
316def sm86Scoreboard =
317 (lambda unrestricted program : (family SM86Program) .
318 (app
319 (app
320 (app
321 (eliminate SM86Program
322 (lambda unrestricted current : (family SM86Program) .
323 (pi unrestricted ordinal : Nat .
324 (pi unrestricted pending : (family ScoreboardMasks) .
325 (pi unrestricted pendingReads : (family ScoreboardMasks) . Nat))))
326 program
327 (branch SM86ProgramEnd .
328 (lambda unrestricted ordinal : Nat .
329 (lambda unrestricted pending : (family ScoreboardMasks) .
330 (lambda unrestricted pendingReads : (family ScoreboardMasks) . zero))))
331 (branch SM86ProgramNext instruction tail induction .
332 (lambda unrestricted ordinal : Nat .
333 (lambda unrestricted pending : (family ScoreboardMasks) .
334 (lambda unrestricted pendingReads : (family ScoreboardMasks) .
335 (eliminate ScoreboardStep
336 (lambda unrestricted current : (family ScoreboardStep) . Nat)
337 (scoreboardStep pending pendingReads (sm86OpSummaryOfBody (scoreboardBodyOf instruction)))
338 (branch ScoreboardStepValue hazard next nextReads .
339 (nat-eliminate
340 (lambda unrestricted current : Nat . Nat)
341 (induction (succ ordinal) next nextReads)
342 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Nat . ordinal))
343 hazard))))))))
344 1)
345 sbMasksEmpty)
346 sbMasksEmpty))
347
348-- ---- fixed latency: the second machine-level pass ----
349-- The barrier pass above orders variable-latency results. This one orders
350-- fixed-latency results by the stall counts: the program issues one
351-- instruction, then waits its stall (at least one cycle) before the next;
352-- a register or predicate a fixed-latency form writes may be read, or
353-- written again, sm86FixedLatency cycles after that form issued
354-- (Accelerator.SM86.Operands -- an ASSUMED table, held to silicon). Barrier
355-- waits only lengthen the time between issues, so counting the stalls alone
356-- is the tighter bound. A barrier an instruction sets is a key too, set
357-- sm86BarrierSetCycles after issue and read by every wait on it. An
358-- instruction's own stall is at least its sm86MinimumStall (a BAR.SYNC's
359-- 6). 0 for a clean program, else the ordinal (from 1) of the first
360-- instruction that touches a result -- or waits on a barrier -- before it is
361-- ready, or stalls less than its minimum.
362
363-- 1 when some key is still in flight at cycle `now`. The comparisons are
364-- the primitive's own, each a 0/1 flag eliminated where it is made: the scan
365-- stops at the first entry in flight (the rest is evaluated only when this
366-- one is not), the value the helper form (naturalOr of naturalAnd of
367-- naturalEqual and naturalLess over the whole list) gives
368def flLate =
369 (lambda unrestricted pending : (family ScoreboardPending) .
370 (lambda unrestricted keys : (family StdList Nat) .
371 (lambda unrestricted now : Nat .
372 (eliminate StdList (lambda unrestricted current : (family StdList Nat) . Nat) keys
373 (branch StdListEmpty . zero)
374 (branch StdListCons key rest induction .
375 (nat-eliminate (lambda unrestricted current : Nat . Nat) induction (lambda unrestricted flagPredecessor : Nat . (lambda unrestricted flagRest : Nat . (succ zero))) (eliminate ScoreboardPending (lambda unrestricted current : (family ScoreboardPending) . Nat) pending
376 (branch ScoreboardPendingEnd . zero)
377 (branch ScoreboardPendingNext bound ready tail inner .
378 (nat-eliminate (lambda unrestricted current : Nat . Nat) inner (lambda unrestricted flagPredecessor : Nat . (lambda unrestricted flagRest : Nat . (nat-eliminate (lambda unrestricted current : Nat . Nat) inner (lambda unrestricted flagPredecessor : Nat . (lambda unrestricted flagRest : Nat . (succ zero))) (nat-less-than now ready)))) (nat-eliminate (lambda unrestricted current : Nat . Nat) (nat-eliminate (lambda unrestricted current : Nat . Nat) (succ zero) (lambda unrestricted flagPredecessor : Nat . (lambda unrestricted flagRest : Nat . zero)) (nat-less-than key bound)) (lambda unrestricted flagPredecessor : Nat . (lambda unrestricted flagRest : Nat . zero)) (nat-less-than bound key)))))))))))
379
380-- the entries still in flight at cycle `now`
381def flPrune =
382 (lambda unrestricted pending : (family ScoreboardPending) .
383 (lambda unrestricted now : Nat .
384 (eliminate ScoreboardPending (lambda unrestricted current : (family ScoreboardPending) . (family ScoreboardPending)) pending
385 (branch ScoreboardPendingEnd . (constructor ScoreboardPending ScoreboardPendingEnd))
386 (branch ScoreboardPendingNext bound ready tail induction .
387 (nat-eliminate
388 (lambda unrestricted current : Nat . (family ScoreboardPending))
389 induction
390 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : (family ScoreboardPending) .
391 (constructor ScoreboardPending ScoreboardPendingNext bound ready induction)))
392 (naturalLess now ready))))))
393
394-- the keys written, ready at `ready`
395def flIssue =
396 (lambda unrestricted keys : (family StdList Nat) .
397 (lambda unrestricted ready : Nat .
398 (lambda unrestricted pending : (family ScoreboardPending) .
399 (eliminate StdList (lambda unrestricted current : (family StdList Nat) . (family ScoreboardPending)) keys
400 (branch StdListEmpty . pending)
401 (branch StdListCons key rest induction .
402 (constructor ScoreboardPending ScoreboardPendingNext key ready induction))))))
403
404def sm86FixedLatencyHazard =
405 (lambda unrestricted program : (family SM86Program) .
406 (app (app (app
407 (eliminate SM86Program
408 (lambda unrestricted current : (family SM86Program) .
409 (pi unrestricted ordinal : Nat . (pi unrestricted now : Nat . (pi unrestricted pending : (family ScoreboardPending) . Nat))))
410 program
411 (branch SM86ProgramEnd .
412 (lambda unrestricted ordinal : Nat . (lambda unrestricted now : Nat . (lambda unrestricted pending : (family ScoreboardPending) . zero))))
413 (branch SM86ProgramNext instruction tail induction .
414 (lambda unrestricted ordinal : Nat . (lambda unrestricted now : Nat . (lambda unrestricted pending : (family ScoreboardPending) .
415 (eliminate SM86OpSummary
416 (lambda unrestricted current : (family SM86OpSummary) . Nat)
417 (sm86OpSummaryOfBody (sm86InstructionBodyOf instruction))
418 (branch SM86OpSummaryValue readsBody writesBody predicateWrites waitKeys setKeys stall latency variable minimum control .
419 (let unrestricted reads =
420 (stdListAppend Nat readsBody (stdListAppend Nat (sm86GuardKeys instruction) waitKeys))
421 in (let unrestricted writes = (stdListAppend Nat writesBody predicateWrites)
422 in (let unrestricted issued =
423 (flIssue setKeys (naturalAdd now sm86BarrierSetCycles) (flPrune pending now))
424 in (nat-eliminate
425 (lambda unrestricted current : Nat . Nat)
426 (induction (succ ordinal)
427 (naturalAdd now (naturalSelect (naturalNonzero stall) stall 1))
428 (nat-eliminate
429 (lambda unrestricted current : Nat . (family ScoreboardPending))
430 issued
431 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : (family ScoreboardPending) .
432 (flIssue writes (naturalAdd now latency) issued)))
433 latency))
434 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Nat . ordinal))
435 (naturalOr (naturalLess (naturalSelect (naturalNonzero stall) stall 1) minimum)
436 (naturalOr (flLate pending reads now) (flLate pending writes now))))))))))))))
437 1) 0) (constructor ScoreboardPending ScoreboardPendingEnd)))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.