module Platform.Linux.Nvidia.DeviceBinding import Compiler.MachineX86Native import Compiler.MachineX86NativeAssembly import Std.Natural -- Deployment selection is distinct from target capability and memory layout. -- A Linux minor is not an RM device instance. The host derives the latter -- through CARD_INFO -> GPU_GET_ID_INFO_V2; it never probes allocation handles. -- UUID is empty only for an explicit node-only binding. Distributed deployments -- should pin the 16-byte binary UUID captured in their admitted inventory. family NvidiaDeviceBinding : Type 0 constructor NvidiaDeviceBindingValue field unrestricted nvidiaDeviceMinor : Nat field unrestricted nvidiaDeviceExpectedUUID : Bytes end-family -- NVIDIA open-gpu-kernel-modules, tag 580.65.06: -- kernel-open/common/inc/nv-ioctl.h (nv_ioctl_card_info_t), -- kernel-open/common/inc/nv-chardev-numbers.h (regular minors 0..247), -- src/common/sdk/nvidia/inc/ctrl/ctrl0000/ctrl0000gpu.h (GET_ID_INFO_V2), -- src/common/sdk/nvidia/inc/ctrl/ctrl2080/ctrl2080gpu.h (binary SHA1 GID). -- https://github.com/NVIDIA/open-gpu-kernel-modules/tree/580.65.06 -- This bounded host realization admits at most 32 inventory rows (the RM -- attached-ID bound). CARD_INFO itself refuses an undersized inventory, so -- a larger physical host fails rather than losing devices from the search. def nvidiaCardMinorMaximum : Nat = 247 def nvidiaCardInfoMaximumRows : Nat = 32 def nvidiaCardInfoValidOffset : Nat = 0 def nvidiaCardInfoGPUIdOffset : Nat = 16 def nvidiaCardInfoMinorOffset : Nat = 56 def nvidiaCardInfoRowBytes : Nat = 72 def nvidiaCardInfoBytes : Nat = (naturalMultiply nvidiaCardInfoMaximumRows nvidiaCardInfoRowBytes) def nvidiaCardInfoIoctl : Nat = (naturalAdd 0xC00046C8 (naturalMultiply nvidiaCardInfoBytes 65536)) def nvidiaDeviceInfoCommand : Nat = 0x205 def nvidiaDeviceInfoBytes : Nat = 32 def nvidiaDeviceInfoInstanceOffset : Nat = 8 def nvidiaDeviceInfoSubdeviceOffset : Nat = 12 def nvidiaDeviceUUIDBytes : Nat = 16 def nvidiaDeviceBindingMinor = (lambda unrestricted binding : (family NvidiaDeviceBinding) . (eliminate NvidiaDeviceBinding (lambda unrestricted value : (family NvidiaDeviceBinding) . Nat) binding (branch NvidiaDeviceBindingValue minor uuid . minor))) def nvidiaDeviceBindingUUID = (lambda unrestricted binding : (family NvidiaDeviceBinding) . (eliminate NvidiaDeviceBinding (lambda unrestricted value : (family NvidiaDeviceBinding) . Bytes) binding (branch NvidiaDeviceBindingValue minor uuid . uuid))) def nvidiaDeviceBindingAdmitted = (lambda unrestricted binding : (family NvidiaDeviceBinding) . (eliminate NvidiaDeviceBinding (lambda unrestricted value : (family NvidiaDeviceBinding) . Nat) binding (branch NvidiaDeviceBindingValue minor uuid . (naturalAnd (naturalLessOrEqual minor nvidiaCardMinorMaximum) (naturalOr (naturalIsZero (bytes-length uuid)) (naturalEqual (bytes-length uuid) nvidiaDeviceUUIDBytes)))))) def nvidiaDeviceBindingPath = (lambda unrestricted binding : (family NvidiaDeviceBinding) . (bytes-append b"/dev/nvidia" (bytes-append (naturalDecimalBytesWithin 3 (nvidiaDeviceBindingMinor binding)) b"\x00"))) -- Compatibility entry points now mean exactly card 0, never the last card -- opened or the first RM allocation that happened to succeed. Sparse pods -- use the explicit binding entry points with their actual Linux minor. def nvidiaDeviceZero : (family NvidiaDeviceBinding) = (constructor NvidiaDeviceBinding NvidiaDeviceBindingValue 0 b"") -- SysV RDI: destination u32, RSI: admitted row arena, RDX: row count, -- RCX: minor. Return 0 only for exactly one valid matching row. Failure -- returns 1 without modifying destination; no reads occur for bad bounds. -- Rows from the kernel have valid 0/1; other values are malformed. Scan the -- entire admitted inventory so a duplicate cannot select an arbitrary GPU. -- Only caller-saved registers are used; this is independent of RM syscalls. def nvidiaCardInfoGPUIdAssembly : (family X86NativeAssembly) = (constructor X86NativeAssembly X86NativeAssemblyEmit (constructor X86NativeInstruction X86NativeCompareImmediate64 (constructor X86NativeRegister64 X86NativeRDX) (x86NativeImmediate32FromNatural 0)) (constructor X86NativeAssembly X86NativeAssemblyJumpCondition (constructor X86NativeCondition X86NativeConditionZero) b"invalid" (constructor X86NativeAssembly X86NativeAssemblyEmit (constructor X86NativeInstruction X86NativeCompareImmediate64 (constructor X86NativeRegister64 X86NativeRDX) (x86NativeImmediate32FromNatural nvidiaCardInfoMaximumRows)) (constructor X86NativeAssembly X86NativeAssemblyJumpCondition (constructor X86NativeCondition X86NativeConditionAbove) b"invalid" (constructor X86NativeAssembly X86NativeAssemblyEmit (constructor X86NativeInstruction X86NativeCompareImmediate64 (constructor X86NativeRegister64 X86NativeRCX) (x86NativeImmediate32FromNatural nvidiaCardMinorMaximum)) (constructor X86NativeAssembly X86NativeAssemblyJumpCondition (constructor X86NativeCondition X86NativeConditionAbove) b"invalid" (constructor X86NativeAssembly X86NativeAssemblyEmit (constructor X86NativeInstruction X86NativeClear32 (constructor X86NativeRegister64 X86NativeR8)) (constructor X86NativeAssembly X86NativeAssemblyLabel b"row" (constructor X86NativeAssembly X86NativeAssemblyEmit (constructor X86NativeInstruction X86NativeLoadMemory8ZeroExtend64 (constructor X86NativeRegister64 X86NativeRAX) (constructor X86NativeRegister64 X86NativeRSI) (x86NativeDisplacement32FromNatural nvidiaCardInfoValidOffset)) (constructor X86NativeAssembly X86NativeAssemblyEmit (constructor X86NativeInstruction X86NativeCompareImmediate64 (constructor X86NativeRegister64 X86NativeRAX) (x86NativeImmediate32FromNatural 0)) (constructor X86NativeAssembly X86NativeAssemblyJumpCondition (constructor X86NativeCondition X86NativeConditionZero) b"next" (constructor X86NativeAssembly X86NativeAssemblyEmit (constructor X86NativeInstruction X86NativeCompareImmediate64 (constructor X86NativeRegister64 X86NativeRAX) (x86NativeImmediate32FromNatural 1)) (constructor X86NativeAssembly X86NativeAssemblyJumpCondition (constructor X86NativeCondition X86NativeConditionNotZero) b"invalid" (constructor X86NativeAssembly X86NativeAssemblyEmit (constructor X86NativeInstruction X86NativeLoadMemory32ZeroExtend64 (constructor X86NativeRegister64 X86NativeRAX) (constructor X86NativeRegister64 X86NativeRSI) (x86NativeDisplacement32FromNatural nvidiaCardInfoMinorOffset)) (constructor X86NativeAssembly X86NativeAssemblyEmit (constructor X86NativeInstruction X86NativeCompareRegister64 (constructor X86NativeRegister64 X86NativeRCX) (constructor X86NativeRegister64 X86NativeRAX)) (constructor X86NativeAssembly X86NativeAssemblyJumpCondition (constructor X86NativeCondition X86NativeConditionNotZero) b"next" (constructor X86NativeAssembly X86NativeAssemblyEmit (constructor X86NativeInstruction X86NativeCompareImmediate64 (constructor X86NativeRegister64 X86NativeR8) (x86NativeImmediate32FromNatural 0)) (constructor X86NativeAssembly X86NativeAssemblyJumpCondition (constructor X86NativeCondition X86NativeConditionNotZero) b"invalid" (constructor X86NativeAssembly X86NativeAssemblyEmit (constructor X86NativeInstruction X86NativeAddImmediate64 (constructor X86NativeRegister64 X86NativeR8) (x86NativeImmediate32FromNatural 1)) (constructor X86NativeAssembly X86NativeAssemblyEmit (constructor X86NativeInstruction X86NativeLoadMemory32ZeroExtend64 (constructor X86NativeRegister64 X86NativeR9) (constructor X86NativeRegister64 X86NativeRSI) (x86NativeDisplacement32FromNatural nvidiaCardInfoGPUIdOffset)) (constructor X86NativeAssembly X86NativeAssemblyLabel b"next" (constructor X86NativeAssembly X86NativeAssemblyEmit (constructor X86NativeInstruction X86NativeAddImmediate64 (constructor X86NativeRegister64 X86NativeRSI) (x86NativeImmediate32FromNatural nvidiaCardInfoRowBytes)) (constructor X86NativeAssembly X86NativeAssemblyEmit (constructor X86NativeInstruction X86NativeAddImmediate64 (constructor X86NativeRegister64 X86NativeRDX) (x86NativeImmediate32FromNatural 4294967295)) (constructor X86NativeAssembly X86NativeAssemblyEmit (constructor X86NativeInstruction X86NativeCompareImmediate64 (constructor X86NativeRegister64 X86NativeRDX) (x86NativeImmediate32FromNatural 0)) (constructor X86NativeAssembly X86NativeAssemblyJumpCondition (constructor X86NativeCondition X86NativeConditionNotZero) b"row" (constructor X86NativeAssembly X86NativeAssemblyEmit (constructor X86NativeInstruction X86NativeCompareImmediate64 (constructor X86NativeRegister64 X86NativeR8) (x86NativeImmediate32FromNatural 1)) (constructor X86NativeAssembly X86NativeAssemblyJumpCondition (constructor X86NativeCondition X86NativeConditionNotZero) b"invalid" (constructor X86NativeAssembly X86NativeAssemblyEmit (constructor X86NativeInstruction X86NativeStoreMemory32 (constructor X86NativeRegister64 X86NativeRDI) (x86NativeDisplacement32FromNatural 0) (constructor X86NativeRegister64 X86NativeR9)) (constructor X86NativeAssembly X86NativeAssemblyEmit (constructor X86NativeInstruction X86NativeClear32 (constructor X86NativeRegister64 X86NativeRAX)) (constructor X86NativeAssembly X86NativeAssemblyEmit (constructor X86NativeInstruction X86NativeReturn) (constructor X86NativeAssembly X86NativeAssemblyLabel b"invalid" (constructor X86NativeAssembly X86NativeAssemblyEmit (constructor X86NativeInstruction X86NativeMoveImmediate32 (constructor X86NativeRegister64 X86NativeRAX) (x86NativeImmediate32FromNatural 1)) (constructor X86NativeAssembly X86NativeAssemblyEmit (constructor X86NativeInstruction X86NativeReturn) (constructor X86NativeAssembly X86NativeAssemblyEnd)))))))))))))))))))))))))))))))))) def nvidiaCardInfoGPUIdCode : Bytes = (compiler-native-encode (family X86NativeAssembly) nvidiaCardInfoGPUIdAssembly)