Realization.Nvidia.SM86.ScaledGradientUpdateSM86

1module Realization.Nvidia.SM86.ScaledGradientUpdateSM86
2
3import Accelerator.SM86.Control
4import Accelerator.SM86.Instruction
5import Accelerator.SM86.Types
6
7-- Realizations of Learning.ScaledGradientUpdate's two independent operations.
8-- Every arithmetic instruction rounds separately to binary64, nearest-even.
9-- No contraction or conversion to binary32 is permitted. Values are supplied
10-- as register pairs by the enclosing kernel's layout; no model facts live here.
11--
12-- This fragment reserves SB0 (write) and SB1 (read). Entry waits retire prior
13-- work on both; each issue replaces both reservations. The continuation must
14-- wait on mask 3 before consuming a result or overwriting a source. A caller
15-- using other barriers must first retire them. The scoreboard checks the
16-- complete enclosing program, including the continuation.
17def scaledUpdate64Control =
18  (constructor
19    SM86Control
20    SM86ControlValue
21    (byte 15)
22    (constructor SM86YieldMode SM86Continue)
23    (constructor SM86Barrier SM86Barrier0)
24    (constructor SM86Barrier SM86Barrier1)
25    (byte 3)
26    (byte 0))
27
28def scaledUpdate64Next =
29  (lambda unrestricted operation : (family SM86Float64Operation) .
30    (lambda unrestricted destination : (family SM86RegisterPair) .
31      (lambda unrestricted left : (family SM86RegisterPair) .
32        (lambda unrestricted right : (family SM86RegisterPair) .
33          (lambda unrestricted tail : (family SM86Program) .
34            (constructor
35              SM86Program
36              SM86ProgramNext
37              (sm86Instruction
38                (constructor
39                  SM86InstructionBody
40                  SM86Float64Binary
41                  operation
42                  destination
43                  left
44                  right
45                  scaledUpdate64Control))
46              tail))))))
47
48-- Admitted pairs are even, so distinct bases imply disjoint word ranges.
49def scaledUpdate64Disjoint =
50  (lambda unrestricted left : (family SM86RegisterPair) .
51    (lambda unrestricted right : (family SM86RegisterPair) .
52      (nat-add
53        (nat-less-than (sm86RegisterPairIndex left) (sm86RegisterPairIndex right))
54        (nat-less-than (sm86RegisterPairIndex right) (sm86RegisterPairIndex left)))))
55
56def accumulateScaledGradient64Admitted =
57  (lambda unrestricted destination : (family SM86RegisterPair) .
58    (lambda unrestricted decay : (family SM86RegisterPair) .
59      (lambda unrestricted previous : (family SM86RegisterPair) .
60        (lambda unrestricted gradient : (family SM86RegisterPair) .
61          (nat-multiply
62            (sm86Float64RegistersAdmitted destination decay previous)
63            (nat-multiply
64              (sm86RegisterPairAdmitted gradient)
65              (scaledUpdate64Disjoint destination gradient)))))))
66
67def accumulateScaledGradient64SM86 =
68  (lambda unrestricted destination : (family SM86RegisterPair) .
69    (lambda unrestricted decay : (family SM86RegisterPair) .
70      (lambda unrestricted previous : (family SM86RegisterPair) .
71        (lambda unrestricted gradient : (family SM86RegisterPair) .
72          (lambda erased admitted : (equal Nat (accumulateScaledGradient64Admitted destination decay previous gradient) 1) .
73            (lambda unrestricted tail : (family SM86Program) .
74              (scaledUpdate64Next
75                (constructor SM86Float64Operation SM86Float64Multiply)
76                destination
77                decay
78                previous
79                (scaledUpdate64Next
80                  (constructor SM86Float64Operation SM86Float64Add)
81                  destination
82                  destination
83                  gradient
84                  tail))))))))
85
86def subtractScaledUpdate64Admitted =
87  (lambda unrestricted destination : (family SM86RegisterPair) .
88    (lambda unrestricted rate : (family SM86RegisterPair) .
89      (lambda unrestricted parameter : (family SM86RegisterPair) .
90        (lambda unrestricted update : (family SM86RegisterPair) .
91          (lambda unrestricted scratch : (family SM86RegisterPair) .
92            (nat-multiply
93              (sm86Float64RegistersAdmitted destination rate parameter)
94              (nat-multiply
95                (sm86Float64RegistersAdmitted scratch rate update)
96                (scaledUpdate64Disjoint scratch parameter))))))))
97
98def subtractScaledUpdate64SM86 =
99  (lambda unrestricted destination : (family SM86RegisterPair) .
100    (lambda unrestricted rate : (family SM86RegisterPair) .
101      (lambda unrestricted parameter : (family SM86RegisterPair) .
102        (lambda unrestricted update : (family SM86RegisterPair) .
103          (lambda unrestricted scratch : (family SM86RegisterPair) .
104            (lambda erased admitted : (equal Nat (subtractScaledUpdate64Admitted destination rate parameter update scratch) 1) .
105              (lambda unrestricted tail : (family SM86Program) .
106                (scaledUpdate64Next
107                  (constructor SM86Float64Operation SM86Float64Multiply)
108                  scratch
109                  rate
110                  update
111                  (scaledUpdate64Next
112                    (constructor SM86Float64Operation SM86Float64Subtract)
113                    destination
114                    parameter
115                    scratch
116                    tail)))))))))