Source/Reference

SM86.Scoreboard

reference/target-models/checked/SM86/Scoreboard.alpha

437 lines42 declarations25.5 KiBSHA-256 e8d85751fb4f

def · lines 368–378

flLate

Full file
---- fixed latency: the second machine-level pass ---- The barrier pass above orders variable-latency results. This one orders fixed-latency results by the stall counts: the program issues one instruction, then waits its stall (at least one cycle) before the next; a register or predicate a fixed-latency form writes may be read, or written again, sm86FixedLatency cycles after that form issued (Accelerator.SM86.Operands -- an ASSUMED table, held to silicon). Barrier waits only lengthen the time between issues, so counting the stalls alone is the tighter bound. A barrier an instruction sets is a key too, set sm86BarrierSetCycles after issue and read by every wait on it. An instruction's own stall is at least its sm86MinimumStall (a BAR.SYNC's 6). 0 for a clean program, else the ordinal (from 1) of the first instruction that touches a result -- or waits on a barrier -- before it is ready, or stalls less than its minimum. 1 when some key is still in flight at cycle `now`. The comparisons are the primitive's own, each a 0/1 flag eliminated where it is made: the scan stops at the first entry in flight (the rest is evaluated only when this one is not), the value the helper form (naturalOr of naturalAnd of 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)))))))))))

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.