Source/Reference

SM86.Scoreboard

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

437 lines42 declarations25.5 KiBSHA-256 e8d85751fb4f

def · lines 150–164

sbMasksLookup

Full file
1 when the register is pending on any barrier: seven indexed reads, one 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))))))))

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.