AlphaGitHub
Source/Reference

SM86.Scoreboard

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

437 lines42 declarations25.5 KiBSHA-256 e8d85751fb4f
Download exact fileView at revisionf5034773ad4bb52133

def · lines 248–259

sbReadBarrierOccupied

Full file
A read barrier is one outstanding token, even when successive stores read different registers. Reusing SB5 on Coppelius's four AdamW stores before waiting it left negative second moments in the first RTX 3090 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))))))))))

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.