one register issued on one barrier: that barrier's mask gains the bit.
The case is a 0/1 elimination returning the mask unchanged or written,
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))))))))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.