Accelerator.SM86.Capability

1module Accelerator.SM86.Capability
2
3import Model.Parameter
4import Model.Word64
5import Std.Natural
6
7-- Capability admission is deliberately independent of marketing product names.
8-- A caller supplies measured device/runtime facts; a system supplies the exact
9-- minimums it needs.  Product name, UUID, PCI identity and driver version belong
10-- in the physical receipt that accompanies these facts, not in admission.
11family SM86DeviceCapabilities : Type 0
12constructor SM86DeviceCapabilitiesValue
13field unrestricted sm86CapabilityComputeMajor : Nat
14field unrestricted sm86CapabilityComputeMinor : Nat
15field unrestricted sm86CapabilityTotalVideoMemoryBytes : (family ModelWord64)
16field unrestricted sm86CapabilityAvailableVideoMemoryBytes : (family ModelWord64)
17field unrestricted sm86CapabilityMappedAddressEnd : (family ModelWord64)
18field unrestricted sm86CapabilityMaximumGridX : Nat
19field unrestricted sm86CapabilityUVMSupported : Nat
20field unrestricted sm86CapabilityResourceManagerSupported : Nat
21field unrestricted sm86CapabilityQMDSupported : Nat
22field unrestricted sm86CapabilityPushbufferSupported : Nat
23field unrestricted sm86CapabilityGPFIFOSupported : Nat
24field unrestricted sm86CapabilityDeviceTimestampsSupported : Nat
25field unrestricted sm86CapabilityHostFallbacks : Nat
26
27end-family
28
29family SM86CapabilityRequirements : Type 0
30constructor SM86CapabilityRequirementsValue
31field unrestricted sm86RequirementComputeMajor : Nat
32field unrestricted sm86RequirementComputeMinor : Nat
33field unrestricted sm86RequirementAvailableVideoMemoryBytes : (family ModelWord64)
34field unrestricted sm86RequirementMappedAddressEnd : (family ModelWord64)
35field unrestricted sm86RequirementMaximumGridX : Nat
36field unrestricted sm86RequirementUVM : Nat
37field unrestricted sm86RequirementResourceManager : Nat
38field unrestricted sm86RequirementQMD : Nat
39field unrestricted sm86RequirementPushbuffer : Nat
40field unrestricted sm86RequirementGPFIFO : Nat
41field unrestricted sm86RequirementDeviceTimestamps : Nat
42field unrestricted sm86RequirementNoHostFallback : Nat
43
44end-family
45
46family SM86CapabilityChecks : Type 0
47constructor SM86CapabilityChecksValue
48field unrestricted sm86CapabilityArchitectureAccepted : Nat
49field unrestricted sm86CapabilityMemoryAccepted : Nat
50field unrestricted sm86CapabilityAddressExtentAccepted : Nat
51field unrestricted sm86CapabilityGridAccepted : Nat
52field unrestricted sm86CapabilityUVMAccepted : Nat
53field unrestricted sm86CapabilityResourceManagerAccepted : Nat
54field unrestricted sm86CapabilityQMDAccepted : Nat
55field unrestricted sm86CapabilityPushbufferAccepted : Nat
56field unrestricted sm86CapabilityGPFIFOAccepted : Nat
57field unrestricted sm86CapabilityDeviceTimestampsAccepted : Nat
58field unrestricted sm86CapabilityNoHostFallbackAccepted : Nat
59
60end-family
61
62family SM86CapabilityAdmission : Type 0
63constructor SM86CapabilityAccepted
64field unrestricted sm86CapabilityAcceptedChecks : (family SM86CapabilityChecks)
65constructor SM86CapabilityRejected
66field unrestricted sm86CapabilityRejectedChecks : (family SM86CapabilityChecks)
67
68end-family
69
70def sm86CapabilityOne : Nat =
71  (succ zero)
72
73-- Static shared memory needs no per-kernel opt-in QMD setting on SM86. A
74-- planner that wants more must establish and encode the dynamic allocation.
75def sm86StaticSharedBytesPerBlock : Nat = (naturalMultiply 48 1024)
76
77def sm86CapabilityFlagAccepted =
78  (lambda unrestricted value : Nat . (naturalEqual value sm86CapabilityOne))
79
80def sm86CapabilityWord64AtLeast =
81  (lambda unrestricted observed : (family ModelWord64) .
82    (lambda unrestricted required : (family ModelWord64) .
83      (naturalIsZero (modelWord64LessThan observed required))))
84
85def sm86CapabilityChecks =
86  (lambda unrestricted requirements : (family SM86CapabilityRequirements) .
87    (lambda unrestricted observed : (family SM86DeviceCapabilities) .
88      (eliminate
89        SM86CapabilityRequirements
90        (lambda unrestricted current : (family SM86CapabilityRequirements) .
91          (family SM86CapabilityChecks))
92        requirements
93        (branch
94          SM86CapabilityRequirementsValue
95          requiredMajor
96          requiredMinor
97          requiredMemory
98          requiredAddressEnd
99          requiredGridX
100          requiredUVM
101          requiredRM
102          requiredQMD
103          requiredPushbuffer
104          requiredGPFIFO
105          requiredTimestamps
106          requiredNoFallback
107          .
108          (eliminate
109            SM86DeviceCapabilities
110            (lambda unrestricted current : (family SM86DeviceCapabilities) .
111              (family SM86CapabilityChecks))
112            observed
113            (branch
114              SM86DeviceCapabilitiesValue
115              observedMajor
116              observedMinor
117              observedTotalMemory
118              observedAvailableMemory
119              observedAddressEnd
120              observedGridX
121              observedUVM
122              observedRM
123              observedQMD
124              observedPushbuffer
125              observedGPFIFO
126              observedTimestamps
127              observedFallbacks
128              .
129              (constructor
130                SM86CapabilityChecks
131                SM86CapabilityChecksValue
132                (naturalAnd
133                  (naturalEqual observedMajor requiredMajor)
134                  (naturalEqual observedMinor requiredMinor))
135                (sm86CapabilityWord64AtLeast observedAvailableMemory requiredMemory)
136                (sm86CapabilityWord64AtLeast observedAddressEnd requiredAddressEnd)
137                (naturalLessOrEqual requiredGridX observedGridX)
138                (naturalEqual (sm86CapabilityFlagAccepted observedUVM) requiredUVM)
139                (naturalEqual (sm86CapabilityFlagAccepted observedRM) requiredRM)
140                (naturalEqual (sm86CapabilityFlagAccepted observedQMD) requiredQMD)
141                (naturalEqual (sm86CapabilityFlagAccepted observedPushbuffer) requiredPushbuffer)
142                (naturalEqual (sm86CapabilityFlagAccepted observedGPFIFO) requiredGPFIFO)
143                (naturalEqual (sm86CapabilityFlagAccepted observedTimestamps) requiredTimestamps)
144                (naturalEqual (naturalIsZero observedFallbacks) requiredNoFallback))))))))
145
146def sm86CapabilityChecksAccepted =
147  (lambda unrestricted checks : (family SM86CapabilityChecks) .
148    (eliminate
149      SM86CapabilityChecks
150      (lambda unrestricted current : (family SM86CapabilityChecks) . Nat)
151      checks
152      (branch
153        SM86CapabilityChecksValue
154        architecture
155        memory
156        addressExtent
157        grid
158        uvm
159        resourceManager
160        qmd
161        pushbuffer
162        gpfifo
163        timestamps
164        noFallback
165        .
166        (naturalAnd
167          architecture
168          (naturalAnd
169            memory
170            (naturalAnd
171              addressExtent
172              (naturalAnd
173                grid
174                (naturalAnd
175                  uvm
176                  (naturalAnd
177                    resourceManager
178                    (naturalAnd
179                      qmd
180                      (naturalAnd pushbuffer (naturalAnd gpfifo (naturalAnd timestamps noFallback)))))))))))))
181
182def sm86CapabilityAdmit =
183  (lambda unrestricted requirements : (family SM86CapabilityRequirements) .
184    (lambda unrestricted observed : (family SM86DeviceCapabilities) .
185      (app
186        (lambda unrestricted checks : (family SM86CapabilityChecks) .
187          (nat-eliminate
188            (lambda unrestricted accepted : Nat . (family SM86CapabilityAdmission))
189            (constructor SM86CapabilityAdmission SM86CapabilityRejected checks)
190            (lambda unrestricted predecessor : Nat .
191              (lambda unrestricted induction : (family SM86CapabilityAdmission) .
192                (constructor SM86CapabilityAdmission SM86CapabilityAccepted checks)))
193            (sm86CapabilityChecksAccepted checks)))
194        (sm86CapabilityChecks requirements observed))))
195
196def sm86CapabilityAdmissionAccepted =
197  (lambda unrestricted admission : (family SM86CapabilityAdmission) .
198    (eliminate
199      SM86CapabilityAdmission
200      (lambda unrestricted current : (family SM86CapabilityAdmission) . Nat)
201      admission
202      (branch SM86CapabilityAccepted checks . sm86CapabilityOne)
203      (branch SM86CapabilityRejected checks . zero)))