1module Platform.Linux.Nvidia.DeviceBinding
2
3import Compiler.MachineX86Native
4import Compiler.MachineX86NativeAssembly
5import Std.Natural
6
7-- Deployment selection is distinct from target capability and memory layout.
8-- A Linux minor is not an RM device instance. The host derives the latter
9-- through CARD_INFO -> GPU_GET_ID_INFO_V2; it never probes allocation handles.
10-- UUID is empty only for an explicit node-only binding. Distributed deployments
11-- should pin the 16-byte binary UUID captured in their admitted inventory.
12family NvidiaDeviceBinding : Type 0
13constructor NvidiaDeviceBindingValue
14field unrestricted nvidiaDeviceMinor : Nat
15field unrestricted nvidiaDeviceExpectedUUID : Bytes
16
17end-family
18
19-- NVIDIA open-gpu-kernel-modules, tag 580.65.06:
20-- kernel-open/common/inc/nv-ioctl.h (nv_ioctl_card_info_t),
21-- kernel-open/common/inc/nv-chardev-numbers.h (regular minors 0..247),
22-- src/common/sdk/nvidia/inc/ctrl/ctrl0000/ctrl0000gpu.h (GET_ID_INFO_V2),
23-- src/common/sdk/nvidia/inc/ctrl/ctrl2080/ctrl2080gpu.h (binary SHA1 GID).
24-- https://github.com/NVIDIA/open-gpu-kernel-modules/tree/580.65.06
25-- This bounded host realization admits at most 32 inventory rows (the RM
26-- attached-ID bound). CARD_INFO itself refuses an undersized inventory, so
27-- a larger physical host fails rather than losing devices from the search.
28def nvidiaCardMinorMaximum : Nat =
29 247
30
31def nvidiaCardInfoMaximumRows : Nat =
32 32
33
34def nvidiaCardInfoValidOffset : Nat =
35 0
36
37def nvidiaCardInfoGPUIdOffset : Nat =
38 16
39
40def nvidiaCardInfoMinorOffset : Nat =
41 56
42
43def nvidiaCardInfoRowBytes : Nat =
44 72
45
46def nvidiaCardInfoBytes : Nat =
47 (naturalMultiply nvidiaCardInfoMaximumRows nvidiaCardInfoRowBytes)
48
49def nvidiaCardInfoIoctl : Nat =
50 (naturalAdd 0xC00046C8 (naturalMultiply nvidiaCardInfoBytes 65536))
51
52def nvidiaDeviceInfoCommand : Nat =
53 0x205
54
55def nvidiaDeviceInfoBytes : Nat =
56 32
57
58def nvidiaDeviceInfoInstanceOffset : Nat =
59 8
60
61def nvidiaDeviceInfoSubdeviceOffset : Nat =
62 12
63
64def nvidiaDeviceUUIDBytes : Nat =
65 16
66
67def nvidiaDeviceBindingMinor =
68 (lambda unrestricted binding : (family NvidiaDeviceBinding) .
69 (eliminate
70 NvidiaDeviceBinding
71 (lambda unrestricted value : (family NvidiaDeviceBinding) . Nat)
72 binding
73 (branch NvidiaDeviceBindingValue minor uuid . minor)))
74
75def nvidiaDeviceBindingUUID =
76 (lambda unrestricted binding : (family NvidiaDeviceBinding) .
77 (eliminate
78 NvidiaDeviceBinding
79 (lambda unrestricted value : (family NvidiaDeviceBinding) . Bytes)
80 binding
81 (branch NvidiaDeviceBindingValue minor uuid . uuid)))
82
83def nvidiaDeviceBindingAdmitted =
84 (lambda unrestricted binding : (family NvidiaDeviceBinding) .
85 (eliminate
86 NvidiaDeviceBinding
87 (lambda unrestricted value : (family NvidiaDeviceBinding) . Nat)
88 binding
89 (branch
90 NvidiaDeviceBindingValue
91 minor
92 uuid
93 .
94 (naturalAnd
95 (naturalLessOrEqual minor nvidiaCardMinorMaximum)
96 (naturalOr
97 (naturalIsZero (bytes-length uuid))
98 (naturalEqual (bytes-length uuid) nvidiaDeviceUUIDBytes))))))
99
100def nvidiaDeviceBindingPath =
101 (lambda unrestricted binding : (family NvidiaDeviceBinding) .
102 (bytes-append
103 b"/dev/nvidia"
104 (bytes-append (naturalDecimalBytesWithin 3 (nvidiaDeviceBindingMinor binding)) b"\x00")))
105
106-- Compatibility entry points now mean exactly card 0, never the last card
107-- opened or the first RM allocation that happened to succeed. Sparse pods
108-- use the explicit binding entry points with their actual Linux minor.
109def nvidiaDeviceZero : (family NvidiaDeviceBinding) =
110 (constructor NvidiaDeviceBinding NvidiaDeviceBindingValue 0 b"")
111
112-- SysV RDI: destination u32, RSI: admitted row arena, RDX: row count,
113-- RCX: minor. Return 0 only for exactly one valid matching row. Failure
114-- returns 1 without modifying destination; no reads occur for bad bounds.
115-- Rows from the kernel have valid 0/1; other values are malformed. Scan the
116-- entire admitted inventory so a duplicate cannot select an arbitrary GPU.
117-- Only caller-saved registers are used; this is independent of RM syscalls.
118def nvidiaCardInfoGPUIdAssembly : (family X86NativeAssembly) =
119 (constructor
120 X86NativeAssembly
121 X86NativeAssemblyEmit
122 (constructor
123 X86NativeInstruction
124 X86NativeCompareImmediate64
125 (constructor X86NativeRegister64 X86NativeRDX)
126 (x86NativeImmediate32FromNatural 0))
127 (constructor
128 X86NativeAssembly
129 X86NativeAssemblyJumpCondition
130 (constructor X86NativeCondition X86NativeConditionZero)
131 b"invalid"
132 (constructor
133 X86NativeAssembly
134 X86NativeAssemblyEmit
135 (constructor
136 X86NativeInstruction
137 X86NativeCompareImmediate64
138 (constructor X86NativeRegister64 X86NativeRDX)
139 (x86NativeImmediate32FromNatural nvidiaCardInfoMaximumRows))
140 (constructor
141 X86NativeAssembly
142 X86NativeAssemblyJumpCondition
143 (constructor X86NativeCondition X86NativeConditionAbove)
144 b"invalid"
145 (constructor
146 X86NativeAssembly
147 X86NativeAssemblyEmit
148 (constructor
149 X86NativeInstruction
150 X86NativeCompareImmediate64
151 (constructor X86NativeRegister64 X86NativeRCX)
152 (x86NativeImmediate32FromNatural nvidiaCardMinorMaximum))
153 (constructor
154 X86NativeAssembly
155 X86NativeAssemblyJumpCondition
156 (constructor X86NativeCondition X86NativeConditionAbove)
157 b"invalid"
158 (constructor
159 X86NativeAssembly
160 X86NativeAssemblyEmit
161 (constructor
162 X86NativeInstruction
163 X86NativeClear32
164 (constructor X86NativeRegister64 X86NativeR8))
165 (constructor
166 X86NativeAssembly
167 X86NativeAssemblyLabel
168 b"row"
169 (constructor
170 X86NativeAssembly
171 X86NativeAssemblyEmit
172 (constructor
173 X86NativeInstruction
174 X86NativeLoadMemory8ZeroExtend64
175 (constructor X86NativeRegister64 X86NativeRAX)
176 (constructor X86NativeRegister64 X86NativeRSI)
177 (x86NativeDisplacement32FromNatural nvidiaCardInfoValidOffset))
178 (constructor
179 X86NativeAssembly
180 X86NativeAssemblyEmit
181 (constructor
182 X86NativeInstruction
183 X86NativeCompareImmediate64
184 (constructor X86NativeRegister64 X86NativeRAX)
185 (x86NativeImmediate32FromNatural 0))
186 (constructor
187 X86NativeAssembly
188 X86NativeAssemblyJumpCondition
189 (constructor X86NativeCondition X86NativeConditionZero)
190 b"next"
191 (constructor
192 X86NativeAssembly
193 X86NativeAssemblyEmit
194 (constructor
195 X86NativeInstruction
196 X86NativeCompareImmediate64
197 (constructor X86NativeRegister64 X86NativeRAX)
198 (x86NativeImmediate32FromNatural 1))
199 (constructor
200 X86NativeAssembly
201 X86NativeAssemblyJumpCondition
202 (constructor X86NativeCondition X86NativeConditionNotZero)
203 b"invalid"
204 (constructor
205 X86NativeAssembly
206 X86NativeAssemblyEmit
207 (constructor
208 X86NativeInstruction
209 X86NativeLoadMemory32ZeroExtend64
210 (constructor X86NativeRegister64 X86NativeRAX)
211 (constructor X86NativeRegister64 X86NativeRSI)
212 (x86NativeDisplacement32FromNatural nvidiaCardInfoMinorOffset))
213 (constructor
214 X86NativeAssembly
215 X86NativeAssemblyEmit
216 (constructor
217 X86NativeInstruction
218 X86NativeCompareRegister64
219 (constructor X86NativeRegister64 X86NativeRCX)
220 (constructor X86NativeRegister64 X86NativeRAX))
221 (constructor
222 X86NativeAssembly
223 X86NativeAssemblyJumpCondition
224 (constructor X86NativeCondition X86NativeConditionNotZero)
225 b"next"
226 (constructor
227 X86NativeAssembly
228 X86NativeAssemblyEmit
229 (constructor
230 X86NativeInstruction
231 X86NativeCompareImmediate64
232 (constructor X86NativeRegister64 X86NativeR8)
233 (x86NativeImmediate32FromNatural 0))
234 (constructor
235 X86NativeAssembly
236 X86NativeAssemblyJumpCondition
237 (constructor X86NativeCondition X86NativeConditionNotZero)
238 b"invalid"
239 (constructor
240 X86NativeAssembly
241 X86NativeAssemblyEmit
242 (constructor
243 X86NativeInstruction
244 X86NativeAddImmediate64
245 (constructor X86NativeRegister64 X86NativeR8)
246 (x86NativeImmediate32FromNatural 1))
247 (constructor
248 X86NativeAssembly
249 X86NativeAssemblyEmit
250 (constructor
251 X86NativeInstruction
252 X86NativeLoadMemory32ZeroExtend64
253 (constructor X86NativeRegister64 X86NativeR9)
254 (constructor X86NativeRegister64 X86NativeRSI)
255 (x86NativeDisplacement32FromNatural
256 nvidiaCardInfoGPUIdOffset))
257 (constructor
258 X86NativeAssembly
259 X86NativeAssemblyLabel
260 b"next"
261 (constructor
262 X86NativeAssembly
263 X86NativeAssemblyEmit
264 (constructor
265 X86NativeInstruction
266 X86NativeAddImmediate64
267 (constructor X86NativeRegister64 X86NativeRSI)
268 (x86NativeImmediate32FromNatural nvidiaCardInfoRowBytes))
269 (constructor
270 X86NativeAssembly
271 X86NativeAssemblyEmit
272 (constructor
273 X86NativeInstruction
274 X86NativeAddImmediate64
275 (constructor X86NativeRegister64 X86NativeRDX)
276 (x86NativeImmediate32FromNatural 4294967295))
277 (constructor
278 X86NativeAssembly
279 X86NativeAssemblyEmit
280 (constructor
281 X86NativeInstruction
282 X86NativeCompareImmediate64
283 (constructor X86NativeRegister64 X86NativeRDX)
284 (x86NativeImmediate32FromNatural 0))
285 (constructor
286 X86NativeAssembly
287 X86NativeAssemblyJumpCondition
288 (constructor X86NativeCondition X86NativeConditionNotZero)
289 b"row"
290 (constructor
291 X86NativeAssembly
292 X86NativeAssemblyEmit
293 (constructor
294 X86NativeInstruction
295 X86NativeCompareImmediate64
296 (constructor X86NativeRegister64 X86NativeR8)
297 (x86NativeImmediate32FromNatural 1))
298 (constructor
299 X86NativeAssembly
300 X86NativeAssemblyJumpCondition
301 (constructor X86NativeCondition X86NativeConditionNotZero)
302 b"invalid"
303 (constructor
304 X86NativeAssembly
305 X86NativeAssemblyEmit
306 (constructor
307 X86NativeInstruction
308 X86NativeStoreMemory32
309 (constructor X86NativeRegister64 X86NativeRDI)
310 (x86NativeDisplacement32FromNatural 0)
311 (constructor X86NativeRegister64 X86NativeR9))
312 (constructor
313 X86NativeAssembly
314 X86NativeAssemblyEmit
315 (constructor
316 X86NativeInstruction
317 X86NativeClear32
318 (constructor X86NativeRegister64 X86NativeRAX))
319 (constructor
320 X86NativeAssembly
321 X86NativeAssemblyEmit
322 (constructor X86NativeInstruction X86NativeReturn)
323 (constructor
324 X86NativeAssembly
325 X86NativeAssemblyLabel
326 b"invalid"
327 (constructor
328 X86NativeAssembly
329 X86NativeAssemblyEmit
330 (constructor
331 X86NativeInstruction
332 X86NativeMoveImmediate32
333 (constructor X86NativeRegister64 X86NativeRAX)
334 (x86NativeImmediate32FromNatural 1))
335 (constructor
336 X86NativeAssembly
337 X86NativeAssemblyEmit
338 (constructor X86NativeInstruction X86NativeReturn)
339 (constructor X86NativeAssembly X86NativeAssemblyEnd))))))))))))))))))))))))))))))))))
340
341def nvidiaCardInfoGPUIdCode : Bytes =
342 (compiler-native-encode (family X86NativeAssembly) nvidiaCardInfoGPUIdAssembly)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.