Platform.RunPod.Nvidia.SM86

1module Platform.RunPod.Nvidia.SM86
2
3import Accelerator.SM86.Capability
4import Model.Config
5import Model.Parameter
6import Model.Word32
7import Model.Word64
8import Platform.Linux.Nvidia.Compatibility
9import Platform.Linux.Nvidia.Memory.ABI
10import Std.List
11import Std.Natural
12import Std.Word
13
14-- A concrete target profile is stricter than generic SM86 capability
15-- admission.  It binds an artifact to one exact provider-visible product while
16-- leaving model and learner packages unaware of any card name.
17family RunPodSM86TargetProfile : Type 0
18constructor RunPodSM86TargetProfileValue
19field unrestricted runPodSM86TargetIdentityValue : Bytes
20field unrestricted runPodSM86ProductIdentityValue : Bytes
21field unrestricted runPodSM86ComputeMajorValue : Nat
22field unrestricted runPodSM86ComputeMinorValue : Nat
23field unrestricted runPodSM86TotalVideoMemoryValue : (family ModelWord64)
24
25end-family
26
27def runPodRTX3070TargetIdentity : Bytes =
28  b"runpod-nvidia-geforce-rtx3070-sm86"
29
30def runPodRTX3070ProductIdentity : Bytes =
31  b"NVIDIA GeForce RTX 3070"
32
33def runPodRTX3070TotalVideoMemory : StdU64 =
34  0x0000_0002_0000_0000
35
36def runPodRTX3070TargetProfile : (family RunPodSM86TargetProfile) =
37  (record
38    RunPodSM86TargetProfile
39    (runPodSM86TargetIdentityValue = runPodRTX3070TargetIdentity)
40    (runPodSM86ProductIdentityValue = runPodRTX3070ProductIdentity)
41    (runPodSM86ComputeMajorValue = 8)
42    (runPodSM86ComputeMinorValue = 6)
43    (runPodSM86TotalVideoMemoryValue = runPodRTX3070TotalVideoMemory))
44
45def runPodRTX3090TargetIdentity : Bytes =
46  b"runpod-nvidia-geforce-rtx3090-sm86"
47
48def runPodRTX3090ProductIdentity : Bytes =
49  b"NVIDIA GeForce RTX 3090"
50
51def runPodRTX3090TotalVideoMemory : StdU64 =
52  0x0000_0006_0000_0000
53
54def runPodRTX3090TargetProfile : (family RunPodSM86TargetProfile) =
55  (record
56    RunPodSM86TargetProfile
57    (runPodSM86TargetIdentityValue = runPodRTX3090TargetIdentity)
58    (runPodSM86ProductIdentityValue = runPodRTX3090ProductIdentity)
59    (runPodSM86ComputeMajorValue = 8)
60    (runPodSM86ComputeMinorValue = 6)
61    (runPodSM86TotalVideoMemoryValue = runPodRTX3090TotalVideoMemory))
62
63-- Ampere command-stream facts belong to the exact target package.  Systems
64-- consume these values when late realization derives QMDs and pushbuffers;
65-- they never branch on a card name or copy driver constants.
66def runPodSM86QMDArchitecture : (family ModelWord32) =
67  (constructor ModelWord32 ModelWord32Value (byte 134) (byte 0) (byte 0) (byte 0))
68
69-- Ampere QMD v0.3 occupies one 256-byte SEND_PCAS slot. This is a target
70-- command-format fact, separate from the number of launches a system emits.
71def runPodSM86QMDSlotBytes : Nat = 256
72
73def runPodSM86ComputeClass : (family ModelWord32) =
74  (constructor ModelWord32 ModelWord32Value (byte 192) (byte 199) (byte 0) (byte 0))
75
76def runPodSM86SPAVersion : (family ModelWord32) =
77  (constructor ModelWord32 ModelWord32Value (byte 6) (byte 8) (byte 0) (byte 0))
78
79def runPodSM86TargetIdentity =
80  (lambda unrestricted profile : (family RunPodSM86TargetProfile) .
81    (eliminate
82      RunPodSM86TargetProfile
83      (lambda unrestricted current : (family RunPodSM86TargetProfile) . Bytes)
84      profile
85      (branch
86        RunPodSM86TargetProfileValue
87        targetIdentity
88        productIdentity
89        computeMajor
90        computeMinor
91        totalVideoMemory
92        .
93        targetIdentity)))
94
95def runPodSM86TotalVideoMemory =
96  (lambda unrestricted profile : (family RunPodSM86TargetProfile) .
97    (eliminate
98      RunPodSM86TargetProfile
99      (lambda unrestricted current : (family RunPodSM86TargetProfile) . (family ModelWord64))
100      profile
101      (branch
102        RunPodSM86TargetProfileValue
103        targetIdentity
104        productIdentity
105        computeMajor
106        computeMinor
107        totalVideoMemory
108        .
109        totalVideoMemory)))
110
111def runPodSM86ProductIdentity =
112  (lambda unrestricted profile : (family RunPodSM86TargetProfile) .
113    (eliminate
114      RunPodSM86TargetProfile
115      (lambda unrestricted current : (family RunPodSM86TargetProfile) . Bytes)
116      profile
117      (branch
118        RunPodSM86TargetProfileValue
119        targetIdentity
120        productIdentity
121        computeMajor
122        computeMinor
123        totalVideoMemory
124        .
125        productIdentity)))
126
127-- NV2080_CTRL_CMD_GPU_GET_NAME_STRING uses one fixed 64-byte ASCII field.
128-- The concrete product identity remains readable source text and only the ABI
129-- projection adds its required trailing NUL bytes.
130def runPodSM86ProductIdentityPadded =
131  (lambda unrestricted profile : (family RunPodSM86TargetProfile) .
132    (bytes-append
133      (runPodSM86ProductIdentity profile)
134      (memoryABIZeroBytes
135        (naturalSaturatingSubtract 64 (bytes-length (runPodSM86ProductIdentity profile))))))
136
137-- Product matching is a pre-submission guard.  The system-specific generic
138-- SM86 admission remains a second, independent check for memory, addresses,
139-- grid, RM/UVM, command formats, timestamps and absence of fallback.
140def runPodSM86TargetMatches =
141  (lambda unrestricted profile : (family RunPodSM86TargetProfile) .
142    (lambda unrestricted observedProductIdentity : Bytes .
143      (lambda unrestricted observed : (family SM86DeviceCapabilities) .
144        (eliminate
145          RunPodSM86TargetProfile
146          (lambda unrestricted current : (family RunPodSM86TargetProfile) . Nat)
147          profile
148          (branch
149            RunPodSM86TargetProfileValue
150            targetIdentity
151            requiredProductIdentity
152            requiredMajor
153            requiredMinor
154            requiredTotalVideoMemory
155            .
156            (eliminate
157              SM86DeviceCapabilities
158              (lambda unrestricted current : (family SM86DeviceCapabilities) . Nat)
159              observed
160              (branch
161                SM86DeviceCapabilitiesValue
162                observedMajor
163                observedMinor
164                observedTotalVideoMemory
165                observedAvailableVideoMemory
166                observedMappedAddressEnd
167                observedMaximumGridX
168                observedUVM
169                observedResourceManager
170                observedQMD
171                observedPushbuffer
172                observedGPFIFO
173                observedTimestamps
174                observedFallbacks
175                .
176                (naturalAnd
177                  (bytes-equal observedProductIdentity requiredProductIdentity)
178                  (naturalAnd
179                    (naturalEqual observedMajor requiredMajor)
180                    (naturalAnd
181                      (naturalEqual observedMinor requiredMinor)
182                      (modelWord64Equal observedTotalVideoMemory requiredTotalVideoMemory)))))))))))
183
184-- ---- what the cards supply (Platform.Linux.Nvidia.Compatibility) ----
185-- The architecture's, with its source; the rest as the qualified runs on
186-- the card recorded them (`record`: the run's evidence).
187def runPodSM86Architectural = (lambda unrestricted source : Bytes . (constructor NvidiaEvidence NvidiaEvidenceArchitectural source))
188
189def runPodSM86Supplies =
190  (lambda unrestricted profile : (family RunPodSM86TargetProfile) .
191    (lambda unrestricted record : Bytes .
192      (let unrestricted measured = (constructor NvidiaEvidence NvidiaEvidenceMeasured record) in
193      (eliminate RunPodSM86TargetProfile (lambda unrestricted current : (family RunPodSM86TargetProfile) . (family StdList (family NvidiaSupply))) profile
194        (branch RunPodSM86TargetProfileValue target product major minor memory .
195          (nvidiaSupply b"instruction-set" (naturalAdd (naturalMultiply 10 major) minor)
196            (runPodSM86Architectural b"NVIDIA Ampere GA10x: compute capability 8.6 (CUDA C++ Programming Guide, compute capabilities)")
197          (nvidiaSupply b"compute-class" (modelWord32ToNatural runPodSM86ComputeClass)
198            (runPodSM86Architectural b"AMPERE_COMPUTE_B (open-gpu-kernel-modules, clc7c0.h)")
199          (nvidiaSupply b"registers-per-thread" 255
200            (runPodSM86Architectural b"SM86: an 8-bit register operand, R255 the zero register (Accelerator.SM86.Types)")
201          (nvidiaSupply b"threads-per-block" 1024
202            (runPodSM86Architectural b"compute capability 8.6: at most 1024 threads per block")
203          (nvidiaSupply b"shared-bytes-per-block" 49152
204            (runPodSM86Architectural b"compute capability 8.6: 48 KiB of static shared memory per block")
205          (nvidiaSupply b"driver-branch" (nvidiaCompatibilityTextWord b"580.") measured
206          (nvidiaSupply b"unified-memory" 1 measured
207          (nvidiaSupply b"video-memory-bytes" (modelWord64Natural memory) measured
208            nvidiaNoSupplies)))))))))))))
209
210def runPodRTX3070Record : Bytes = b"tests/observability/import/envelope-rtx3070/README.md"
211def runPodRTX3090Record : Bytes = b"tests/observability/import/bob-rtx3090/README.md"
212
213def runPodRTX3070Supplies : (family StdList (family NvidiaSupply)) = (runPodSM86Supplies runPodRTX3070TargetProfile runPodRTX3070Record)
214def runPodRTX3090Supplies : (family StdList (family NvidiaSupply)) = (runPodSM86Supplies runPodRTX3090TargetProfile runPodRTX3090Record)