1module Platform.Linux.Nvidia.PlanHost
2
3import Data.Bytes
4import Model.Config
5import Model.Parameter
6import Model.Word32
7import Model.Word64
8import Compiler.MachineX86Native
9import Compiler.MachineX86NativeAssembly
10import Runtime.ArenaCertificate
11import Runtime.NativeLaunchRecipeLoad
12import Runtime.NativeTelemetry
13import Runtime.NativeTelemetrySeal
14import Runtime.NativePhysicalProgram
15import Runtime.NativePhysicalNativeELF
16import Runtime.NativePhysicalTrainingRoutine
17import Std.Natural
18
19-- The host the compiler derives from a whole-program plan: the compute-channel
20-- protocol the SM86 launch ladder proved on the RTX 3070 and the RTX 3090
21-- (rungs D..Q, Coppelius S5, the checked linear step), as typed command
22-- builders parameterised by the plan's placement. Every address, extent and
23-- handle is a parameter or derived from one; the protocol is stated once,
24-- here, for every plan.
25--
26-- Two lifecycles, selected by the layout:
27-- direct-RM every buffer is system memory; its GPU range is a fixed RM
28-- virtual reservation and a DMA map; the channel has 0x400
29-- entries and its own USERD buffer.
30-- UVM RM's VA space is duplicated into the UVM driver; buffers are
31-- external ranges mapped through it; video-memory buffers are
32-- allowed and are not host-mapped; the GPFIFO is one contiguous
33-- video allocation whose last page is USERD; the channel is
34-- registered with UVM and scheduled last. This is the
35-- lifecycle the Coppelius training executables run.
36--
37-- In order: open the card and the control node; root, device, subdevice,
38-- UVM: the DMA selector, the VA space, UVM: initialise the driver, register
39-- the GPU and the VA space, reserve the external range; the fixed buffers
40-- GPFIFO, pushbuffer, semaphores, program, QMD, direct-RM: USERD, and every
41-- data buffer; the error notifier; channel group, context share, channel,
42-- compute and usermode objects; direct-RM: bind, schedule, token, doorbell;
43-- UVM: doorbell, preemption, token, register the channel, schedule. Then
44-- the uploads, gpPut, the doorbell, a FenceWait on the plan's semaphore, the
45-- readbacks to stdout, exit 0. Every driver status is pre-set to a sentinel
46-- and recorded after the call; under NvidiaPlanHostStrict (the executables)
47-- each is asserted zero too, so a host without a card stops at its first
48-- device call with a command failure; under NvidiaPlanHostProbe (the
49-- channel probe) none after the root's is, and the host prints the status
50-- area. The root client is freed before exit.
51--
52-- Measured on the RTX 3090, driver 580.126.09, 2026-09-22, the checked
53-- linear step: UVM lifecycle 11/11 runs; two submissions per host, one
54-- semaphore slot each: 6/6, both slots released with timestamps. The
55-- direct-RM channel allocation used to fail NV_ERR_INSUFFICIENT_RESOURCES
56-- 0x1e intermittently, in streaks, at a rate that drifted with the host
57-- machine's other tenants (3/10 .. 17/60). Root-caused 2026-09-23 with the
58-- channel probe, one placement at a time interleaved with the baseline:
59-- the cause is USERD as a separate SYSTEM-memory allocation. Not the
60-- channel flags, the bind, the schedule, the root free, the work, the
61-- GPFIFO's memory or the error notifier's (each within noise of the
62-- baseline); USERD in video memory 0/60 against 17/60, and the step with
63-- USERD in video memory 60/60 records bit-identical against 6/60 failures
64-- of the old host interleaved. The Ampere direct-RM profile therefore admits
65-- a layout only with a video-memory USERD (nvidiaPlanHostLayoutAdmitted);
66-- the UVM lifecycle's USERD is the last page of its video GPFIFO already.
67
68-- System memory is one physically contiguous allocation; paged system
69-- memory is not (NVOS32 PHYSICALITY NONCONTIGUOUS), which is what a buffer
70-- too large for contiguous pages needs -- the GB10's arena, which has no
71-- video memory to live in. The GPU reaches either through its page tables.
72family NvidiaPlanHostMemory : Type 0
73constructor NvidiaPlanHostSystemMemory
74constructor NvidiaPlanHostVideoMemory
75-- Noncontiguous physical pages, still host-cached and GPU virtually contiguous.
76constructor NvidiaPlanHostPagedSystemMemory
77-- Noncontiguous system memory the GPU caches in its L2, in 64 KiB pages,
78-- never mapped into the process: the allocation cudaMalloc makes on the GB10
79-- (read off the driver's RM calls, 2026-09-26: NV01_MEMORY_SYSTEM, attr
80-- PAGE_SIZE_BIG | LOCATION_PCI | PHYSICALITY_NONCONTIGUOUS, attr2
81-- GPU_CACHEABLE_YES | ZBC_PREFER_NO_ZBC, flags IGNORE_BANK_PLACEMENT |
82-- MEMORY_HANDLE_PROVIDED | MAP_NOT_REQUIRED, PTE kind 6, 64 KiB aligned).
83-- Paged system memory is not L2-cached by the GPU: an L2-resident copy runs
84-- at 190 GB/s there against 880 GB/s here.
85constructor NvidiaPlanHostGPUCachedSystemMemory
86end-family
87
88-- host 0 = not mapped into the process
89family NvidiaPlanHostBuffer : Type 0
90constructor NvidiaPlanHostBufferValue
91field unrestricted nvidiaPlanHostBufferIdentity : Bytes
92field unrestricted nvidiaPlanHostBufferGPU : Nat
93field unrestricted nvidiaPlanHostBufferHost : Nat
94field unrestricted nvidiaPlanHostBufferExtent : Nat
95field unrestricted nvidiaPlanHostBufferMemory : (family NvidiaPlanHostMemory)
96end-family
97
98family NvidiaPlanHostBuffers : Type 0
99constructor NvidiaPlanHostBuffersEnd
100constructor NvidiaPlanHostBuffersNext
101field unrestricted nvidiaPlanHostBuffersHead : (family NvidiaPlanHostBuffer)
102recursive unrestricted nvidiaPlanHostBuffersTail
103end-family
104
105family NvidiaPlanHostABI : Type 0
106constructor NvidiaPlanHostABIValue
107field unrestricted nvidiaPlanHostMapDMAIoctl : Nat
108field unrestricted nvidiaPlanHostNVOS46Size : Nat
109field unrestricted nvidiaPlanHostNVOS46DMAOffset : Nat
110field unrestricted nvidiaPlanHostNVOS46Status : Nat
111field unrestricted nvidiaPlanHostChannelClass : Nat
112field unrestricted nvidiaPlanHostComputeClass : Nat
113field unrestricted nvidiaPlanHostUsermodeClass : Nat
114field unrestricted nvidiaPlanHostEngineType : Nat
115-- the first four bytes of the driver version the ABI was built for,
116-- little-endian ("580." is 0x2E303835): the host asks the driver for its
117-- version before any card call and refuses another branch by name
118field unrestricted nvidiaPlanHostDriverBranch : Nat
119-- the bytes of NVA06C_CTRL_GPFIFO_SCHEDULE_PARAMS: 2 on the 570 branch
120-- (bEnable, bSkipSubmit), 3 from 580 (bSkipEnable added); the wrong size is
121-- NV_ERR_INVALID_ARGUMENT (0x1f), measured on an RTX A6000, 570.195.03
122field unrestricted nvidiaPlanHostScheduleParamsSize : Nat
123-- Required location of a separately allocated direct-RM USERD buffer.
124-- Discrete Ampere needs video memory; the measured integrated GB10 path
125-- uses system memory. This is target policy, not a runtime retry choice.
126field unrestricted nvidiaPlanHostDirectUSERDMemory : (family NvidiaPlanHostMemory)
127field unrestricted nvidiaPlanHostDirectChannelFlags : Nat
128-- Direct-RM cache snooping is target policy. The GB10 bring-up's host-cached
129-- system buffers use 0x8010; the qualified Ampere path keeps 0x8000. See
130-- Memory.ABI.memoryABIDMAMappingFlags. A CPU publication barrier alone does
131-- not make a non-snooping GPU mapping coherent with cached CPU writes.
132field unrestricted nvidiaPlanHostDirectDMAFlags : Nat
133end-family
134
135-- one upload: bytes, or the contents of a file at run time
136family NvidiaPlanHostFills : Type 0
137constructor NvidiaPlanHostFillsEnd
138constructor NvidiaPlanHostFillBytes
139field unrestricted nvidiaPlanHostFillHost : Nat
140field unrestricted nvidiaPlanHostFillPayload : Bytes
141recursive unrestricted nvidiaPlanHostFillsTail
142constructor NvidiaPlanHostFillFile
143field unrestricted nvidiaPlanHostFillFileHost : Nat
144field unrestricted nvidiaPlanHostFillFilePath : Bytes
145field unrestricted nvidiaPlanHostFillFileExtent : Nat
146recursive unrestricted nvidiaPlanHostFillFileTail
147end-family
148
149-- one readback: a host range written to stdout after completion
150family NvidiaPlanHostReads : Type 0
151constructor NvidiaPlanHostReadsEnd
152constructor NvidiaPlanHostReadsNext
153field unrestricted nvidiaPlanHostReadHost : Nat
154field unrestricted nvidiaPlanHostReadExtent : Nat
155recursive unrestricted nvidiaPlanHostReadsTail
156end-family
157
158family NvidiaPlanHostLifecycle : Type 0
159constructor NvidiaPlanHostDirectRM
160constructor NvidiaPlanHostUVM
161field unrestricted nvidiaPlanHostExternalRangeBase : Nat
162field unrestricted nvidiaPlanHostExternalRangeExtent : Nat
163end-family
164
165-- How the host treats a driver status. Strict: every one is asserted zero
166-- (the executables). Probe: every one after the root client's is recorded
167-- and none asserted, so a host on a card reports which call refused instead
168-- of stopping at it (the channel probe). The card-name and driver-branch
169-- assertions hold in both: a probe against the wrong card, or a driver
170-- whose ABI the host was not built for, stops.
171family NvidiaPlanHostMode : Type 0
172constructor NvidiaPlanHostStrict
173constructor NvidiaPlanHostProbe
174end-family
175
176family NvidiaPlanHostLayout : Type 0
177constructor NvidiaPlanHostLayoutValue
178field unrestricted nvidiaPlanHostGPFIFO : (family NvidiaPlanHostBuffer)
179field unrestricted nvidiaPlanHostPushbuffer : (family NvidiaPlanHostBuffer)
180field unrestricted nvidiaPlanHostSemaphores : (family NvidiaPlanHostBuffer)
181field unrestricted nvidiaPlanHostProgram : (family NvidiaPlanHostBuffer)
182field unrestricted nvidiaPlanHostQMD : (family NvidiaPlanHostBuffer)
183field unrestricted nvidiaPlanHostUSERD : (family NvidiaPlanHostBuffer)
184field unrestricted nvidiaPlanHostData : (family NvidiaPlanHostBuffers)
185field unrestricted nvidiaPlanHostABI : (family NvidiaPlanHostABI)
186field unrestricted nvidiaPlanHostLifecycle : (family NvidiaPlanHostLifecycle)
187field unrestricted nvidiaPlanHostExpectedName : Bytes
188-- the host address the error notifier page is mapped at, 0 = not mapped
189field unrestricted nvidiaPlanHostErrorHost : Nat
190end-family
191
192-- The 570 branch: the 56-byte NVOS46 (the layout the retired 575 ABI of
193-- the RTX 3070 fixtures used) and the 2-byte schedule parameters. The 575
194-- branch is no longer offered for any sm_86 card on RunPod (2026-09-24:
195-- 570.195, 580.65 .. 580.178, 595.91), so its ABI could not be qualified
196-- again and was retired; this one is qualified on an RTX A6000, 570.195.03.
197def nvidiaPlanHostAmpere570 : (family NvidiaPlanHostABI) =
198 (constructor NvidiaPlanHostABI NvidiaPlanHostABIValue 0xC0384657 56 40 48 0xC56F 0xC7C0 0xC561 0 0x2E303735 2
199 (constructor NvidiaPlanHostMemory NvidiaPlanHostVideoMemory) 0x01000000 0x8000)
200
201def nvidiaPlanHostAmpere580 : (family NvidiaPlanHostABI) =
202 (constructor NvidiaPlanHostABI NvidiaPlanHostABIValue 0xC0404657 64 48 56 0xC56F 0xC7C0 0xC561 0 0x2E303835 3
203 (constructor NvidiaPlanHostMemory NvidiaPlanHostVideoMemory) 0x01000000 0x8000)
204
205-- The DGX Spark's GB10 (compute 12.1) on the 580 branch: the 580 DMA-map ABI
206-- above with the classes this GPU's class list offers and the ladder
207-- allocated (tools/dgx/rung_tsg.py, rung_execute.py): BLACKWELL_CHANNEL_GPFIFO_A
208-- 0xC96F, BLACKWELL_COMPUTE_B 0xCEC0, HOPPER_USERMODE_A 0xC661.
209def nvidiaPlanHostBlackwell580 : (family NvidiaPlanHostABI) =
210 (constructor NvidiaPlanHostABI NvidiaPlanHostABIValue 0xC0404657 64 48 56 0xC96F 0xCEC0 0xC661 0 0x2E303835 3
211 -- USERD in system memory (the GB10's channel buffers, Coppelius.Build.
212 -- NativeHost), the channel flags every UVM plan allocates with, and the
213 -- direct-RM DMA flags, which a UVM plan never reads
214 (constructor NvidiaPlanHostMemory NvidiaPlanHostSystemMemory) 0x01000000 0x8000)
215
216-- A layout built for another driver ABI: every buffer, the lifecycle and
217-- the expected card unchanged, only the ABI (the DMA-map parameters, the
218-- classes, the driver branch it demands) replaced.
219def nvidiaPlanHostWithABI =
220 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
221 (lambda unrestricted abi : (family NvidiaPlanHostABI) .
222 (eliminate NvidiaPlanHostLayout (lambda unrestricted current : (family NvidiaPlanHostLayout) . (family NvidiaPlanHostLayout)) layout
223 (branch NvidiaPlanHostLayoutValue gpfifo push sem program qmd userd data previous lifecycle expectedName errorHost .
224 (constructor NvidiaPlanHostLayout NvidiaPlanHostLayoutValue gpfifo push sem program qmd userd data abi lifecycle expectedName errorHost)))))
225
226-- ---- operands and commands ----
227def phWord = (lambda unrestricted value : Nat . (modelWord64FromNaturalTruncated value))
228def phImm = nativeLaunchRecipeImmediate
229def phSlot = nativeLaunchRecipeSlotValue
230def phStore = nativeLaunchRecipeStore
231def phDiscard : (family NativePhysicalResultBinding) = (constructor NativePhysicalResultBinding NativePhysicalDiscardResult)
232def phState = (lambda unrestricted offset : Nat . (constructor NativePhysicalOperand NativePhysicalStateAddress (phWord offset)))
233def phLoad = (lambda unrestricted offset : Nat . (constructor NativePhysicalOperand NativePhysicalStateLoad64 (phWord offset)))
234def phPayload : (family NativePhysicalOperand) = (constructor NativePhysicalOperand NativePhysicalPayloadAddress modelWord64Zero)
235
236def phArgs =
237 (lambda unrestricted a0 : (family NativePhysicalOperand) .
238 (lambda unrestricted a1 : (family NativePhysicalOperand) .
239 (lambda unrestricted a2 : (family NativePhysicalOperand) .
240 (lambda unrestricted a3 : (family NativePhysicalOperand) .
241 (lambda unrestricted a4 : (family NativePhysicalOperand) .
242 (lambda unrestricted a5 : (family NativePhysicalOperand) .
243 (constructor NativePhysicalArguments NativePhysicalArgumentsValue a0 a1 a2 a3 a4 a5)))))))
244
245def phArgs3 =
246 (lambda unrestricted a0 : (family NativePhysicalOperand) .
247 (lambda unrestricted a1 : (family NativePhysicalOperand) .
248 (lambda unrestricted a2 : (family NativePhysicalOperand) .
249 (phArgs a0 a1 a2 (phImm 0) (phImm 0) (phImm 0)))))
250
251def phIdentity : Bytes = b"nvidia-plan-host"
252
253def phNext =
254 (lambda unrestricted operation : (family NativePhysicalOperation) .
255 (lambda unrestricted tail : (family NativePhysicalCommands) .
256 (nativeLaunchRecipeCommand operation phIdentity tail)))
257
258def phCall =
259 (lambda unrestricted number : Nat .
260 (lambda unrestricted argv : (family NativePhysicalArguments) .
261 (lambda unrestricted payload : Bytes .
262 (lambda unrestricted result : (family NativePhysicalResultBinding) .
263 (lambda unrestricted tail : (family NativePhysicalCommands) .
264 (phNext (constructor NativePhysicalOperation NativePhysicalSystemCall (phImm number) argv payload result) tail))))))
265
266def phCopy =
267 (lambda unrestricted offset : Nat .
268 (lambda unrestricted payload : Bytes .
269 (lambda unrestricted tail : (family NativePhysicalCommands) .
270 (phNext (constructor NativePhysicalOperation NativePhysicalCopyPayloadToState (phWord offset) (phWord (bytes-length payload)) payload) tail))))
271
272-- Linux x86-64
273def phSysRead : Nat = 0
274def phSysWrite : Nat = 1
275def phSysClose : Nat = 3
276def phSysMmap : Nat = 9
277def phSysIoctl : Nat = 16
278def phSysDup2 : Nat = 33
279def phSysExitGroup : Nat = 231
280def phSysOpenat : Nat = 257
281def phSysPipe2 : Nat = 293
282def phAtFdCwd : Nat = 18446744073709551516
283def phOpenFlags : Nat = 0x80002
284def phMapAnonymousFixed : Nat = 0x32
285def phMapSharedFixed : Nat = 0x11
286def phNoDescriptor : Nat = 18446744073709551615
287
288-- RM and UVM escapes
289def phRMAlloc : Nat = 0xC020462B
290def phRMControl : Nat = 0xC020462A
291def phRMMapMemory : Nat = 0xC038464E
292def phRMFree : Nat = 0xC0104629
293def phRegisterFD : Nat = 0xC00446C9
294def phWaitOpen : Nat = 0xC00846DA
295def phUVMInitialize : Nat = 0x30000001
296def phUVMMMInitialize : Nat = 75
297def phUVMRegisterGPU : Nat = 37
298def phUVMRegisterGPUVASpace : Nat = 25
299def phUVMRegisterChannel : Nat = 27
300def phUVMCreateExternalRange : Nat = 73
301def phUVMMapExternalAllocation : Nat = 33
302def phUVMChannelRangeBase : Nat = 0xA00000000
303def phUVMChannelRangeExtent : Nat = 0x4000000
304
305-- result slots and fixed descriptors
306def phSlotControl : Nat = 0
307def phSlotGPU : Nat = 1
308def phSlotMap : Nat = 2
309def phSlotFile : Nat = 3
310-- slots 4..13 belong to the request host (PlanHostRequest), 14 and 15 to
311-- the native telemetry. Transfers own the next slot and never overwrite a
312-- request file descriptor or a mapping result while checking short I/O.
313def phSlotTransfer : Nat = 16
314def phSlots : Nat = (succ phSlotTransfer)
315def phFdControl : Nat = 100
316def phFdCard : Nat = 101
317def phFdMap : Nat = 102
318def phFdUVM : Nat = 103
319def phFdUVMMemoryMap : Nat = 104
320
321-- RM handles, caller-chosen for children
322def phHDevice : Nat = 0xDEAD0080
323def phHSubdevice : Nat = 0xDEAD2080
324def phHVASpace : Nat = 0xDEAD90F1
325def phHError : Nat = 0xDEAD0E44
326def phHGroup : Nat = 0xDEADA06C
327def phHContext : Nat = 0xDEAD9067
328def phHDMA : Nat = 0xDEAD0070
329def phHMemory = (lambda unrestricted index : Nat . (naturalAdd 0xB0000000 index))
330def phHVirtual = (lambda unrestricted index : Nat . (naturalAdd 0xB1000000 index))
331def phHClass = (lambda unrestricted class : Nat . (naturalAdd 0xDEAD0000 class))
332
333-- state layout, 16 KiB: RM call blocks, then a 16-byte status record per
334-- buffer, then 256 bytes of call blocks per buffer (at most 24 buffers, to
335-- 10240); the request host's areas follow (PlanHostRequest)
336def phStateExtent : Nat = 16384
337def phBufferBlocksEnd : Nat = 10240
338def phRoot : Nat = 0
339def phDev : Nat = 64
340def phSub : Nat = 128
341def phVAS : Nat = 192
342def phErrMap : Nat = 256
343def phErr : Nat = 2048
344def phGroup : Nat = 2112
345def phCtx : Nat = 2176
346def phChan : Nat = 2240
347def phComp : Nat = 2304
348def phUser : Nat = 2368
349def phBind : Nat = 2432
350def phSched : Nat = 2496
351def phTok : Nat = 2560
352def phDoorMap : Nat = 2624
353def phWait : Nat = 2688
354def phPipe : Nat = 2752
355def phScratch : Nat = 2816
356def phName : Nat = 2880
357def phPreempt : Nat = 3008
358def phFree : Nat = 3040
359def phDMAObject : Nat = 3072
360def phUVMControl : Nat = 3136
361def phBufferState = (lambda unrestricted index : Nat . (naturalAdd 4096 (naturalMultiply index 256)))
362def phBufferStatus = (lambda unrestricted index : Nat . (naturalAdd 3200 (naturalMultiply index 16)))
363def phBuffersMaximum : Nat = 24
364
365-- the fixed anonymous parameter page, 64 KiB
366def phParams : Nat = 0x50000000
367def phDevP : Nat = 0x50000000
368def phSubP : Nat = 0x50000100
369def phVASP : Nat = 0x50000200
370def phErrP : Nat = 0x50001100
371def phGroupP : Nat = 0x50001200
372def phCtxP : Nat = 0x50001300
373def phChanP : Nat = 0x50001400
374def phBindP : Nat = 0x50001600
375def phSchedP : Nat = 0x50001700
376def phTokP : Nat = 0x50001800
377def phRegFdP : Nat = 0x50001980
378def phPreemptP : Nat = 0x50001A00
379def phNameP : Nat = 0x50001B00
380def phMemP = (lambda unrestricted index : Nat . (naturalAdd 0x50002000 (naturalMultiply index 0x200)))
381def phVirtP = (lambda unrestricted index : Nat . (naturalAdd 0x50002100 (naturalMultiply index 0x200)))
382def phDMAObjectP : Nat = 0x50007F00
383def phUVMGidP : Nat = 0x50008000
384def phUVMInitP : Nat = 0x50008200
385def phUVMMMP : Nat = 0x50008300
386def phUVMRegisterGPUP : Nat = 0x50008400
387def phUVMRegisterVASpaceP : Nat = 0x50008500
388def phUVMRegisterChannelP : Nat = 0x50008600
389def phUVMCreateRangeP : Nat = 0x50008700
390def phUVMMapAllocationP : Nat = 0x50009000
391def phDoorHost : Nat = 0x60800000
392def phStatusSentinel : Nat = 0xFFFFFFFF
393
394-- ---- little-endian blocks ----
395def phZeros =
396 (lambda unrestricted count : Nat .
397 (nat-eliminate
398 (lambda unrestricted current : Nat . Bytes)
399 b""
400 (lambda unrestricted predecessor : Nat .
401 (lambda unrestricted induction : Bytes . (bytes-cons (byte 0) induction)))
402 count))
403
404def phDrop = dataBytesDropValidated
405
406def phTake = dataBytesTakeValidated
407
408def phW32 = (lambda unrestricted value : Nat . (dataBytesWord32LE (modelWord32FromNaturalTruncated value)))
409def phW64 = (lambda unrestricted value : Nat . (dataBytesWord64LE (phWord value)))
410
411def phSet =
412 (lambda unrestricted block : Bytes .
413 (lambda unrestricted offset : Nat .
414 (lambda unrestricted field : Bytes .
415 (bytes-append (phTake offset block) (bytes-append field (phDrop (naturalAdd offset (bytes-length field)) block))))))
416
417def phSet32 = (lambda unrestricted block : Bytes . (lambda unrestricted offset : Nat . (lambda unrestricted value : Nat . (phSet block offset (phW32 value)))))
418def phSet64 = (lambda unrestricted block : Bytes . (lambda unrestricted offset : Nat . (lambda unrestricted value : Nat . (phSet block offset (phW64 value)))))
419
420-- ---- the pipe memcpy ----
421def phCopyStateToState =
422 (lambda unrestricted destination : Nat .
423 (lambda unrestricted source : Nat .
424 (lambda unrestricted count : Nat .
425 (lambda unrestricted tail : (family NativePhysicalCommands) .
426 (phCall phSysWrite (phArgs3 (phLoad (naturalAdd phPipe 4)) (phState source) (phImm count)) b"" phDiscard
427 (phCall phSysRead (phArgs3 (phLoad phPipe) (phState destination) (phImm count)) b"" phDiscard tail))))))
428
429-- A pipe is not an unbounded staging buffer. A single-threaded write/read
430-- pair deadlocks when its write exceeds capacity (the matrix qualification
431-- stopped in write(901120), after filling 65536 bytes). Drain every bounded
432-- chunk before writing another. Linux PIPE_BUF is 4096 on both target ABIs;
433-- the empty pipe admits that atomic extent even when capacity is one page.
434-- Short/error returns fail by name, including interruption; no partial copy
435-- is reported as a successful upload. Result slot ownership is explicit.
436def phPipeChunkBytes : Nat = 4096
437def phPipeChunkCount = (lambda unrestricted count : Nat .
438 (naturalAdd (naturalDivideUnchecked count phPipeChunkBytes)
439 (naturalNonzero (naturalModuloUnchecked count phPipeChunkBytes))))
440def phPipeChunk = (lambda unrestricted source : (family NativePhysicalOperand) .
441 (lambda unrestricted destination : (family NativePhysicalOperand) .
442 (lambda unrestricted count : Nat . (lambda unrestricted payload : Bytes .
443 (lambda unrestricted tail : (family NativePhysicalCommands) .
444 (phCall phSysWrite (phArgs3 (phLoad (naturalAdd phPipe 4)) source (phImm count)) payload (phStore phSlotTransfer)
445 (nativeLaunchRecipeAssertEqual (phSlot phSlotTransfer) (phImm count) b"pipe-copy-write"
446 (phCall phSysRead (phArgs3 (phLoad phPipe) destination (phImm count)) b"" (phStore phSlotTransfer)
447 (nativeLaunchRecipeAssertEqual (phSlot phSlotTransfer) (phImm count) b"pipe-copy-read" tail)))))))))
448def phFill = (lambda unrestricted address : Nat . (lambda unrestricted payload : Bytes .
449 (lambda unrestricted tail : (family NativePhysicalCommands) .
450 (app (nat-eliminate
451 (lambda unrestricted remaining : Nat .
452 (pi unrestricted at : Nat . (pi unrestricted bytes : Bytes . (family NativePhysicalCommands))))
453 (lambda unrestricted at : Nat . (lambda unrestricted bytes : Bytes . tail))
454 (lambda unrestricted predecessor : Nat .
455 (lambda unrestricted induction : (pi unrestricted at : Nat . (pi unrestricted bytes : Bytes . (family NativePhysicalCommands))) .
456 (lambda unrestricted at : Nat . (lambda unrestricted bytes : Bytes .
457 (let unrestricted count = (naturalMinimum phPipeChunkBytes (bytes-length bytes)) in
458 (phPipeChunk phPayload (phImm at) count (dataBytesTakeValidated count bytes)
459 (induction (naturalAdd at count) (dataBytesDropValidated count bytes))))))))
460 (phPipeChunkCount (bytes-length payload))) address payload))))
461-- Address-based copies share the same transfer/check mechanism. Their
462-- ranges must be disjoint as before; this is not an overlapping memmove.
463def phPipeRanges = (lambda unrestricted source : (pi unrestricted offset : Nat . (family NativePhysicalOperand)) .
464 (lambda unrestricted destination : (pi unrestricted offset : Nat . (family NativePhysicalOperand)) .
465 (lambda unrestricted count : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) .
466 (let unrestricted chunks = (phPipeChunkCount count) in
467 (nat-eliminate (lambda unrestricted i : Nat . (family NativePhysicalCommands)) tail
468 (lambda unrestricted index : Nat . (lambda unrestricted rest : (family NativePhysicalCommands) .
469 (let unrestricted offset = (naturalMultiply (naturalSaturatingSubtract chunks (succ index)) phPipeChunkBytes) in
470 (phPipeChunk (source offset) (destination offset)
471 (naturalMinimum phPipeChunkBytes (naturalSaturatingSubtract count offset)) b"" rest)))) chunks))))))
472def phCopyMappedToState = (lambda unrestricted address : Nat . (lambda unrestricted destination : Nat .
473 (phPipeRanges (lambda unrestricted offset : Nat . (phImm (naturalAdd address offset)))
474 (lambda unrestricted offset : Nat . (phState (naturalAdd destination offset))))))
475def phCopyStateToMapped = (lambda unrestricted source : Nat . (lambda unrestricted address : Nat .
476 (phPipeRanges (lambda unrestricted offset : Nat . (phState (naturalAdd source offset)))
477 (lambda unrestricted offset : Nat . (phImm (naturalAdd address offset))))))
478def phCopyMappedToMapped = (lambda unrestricted source : Nat . (lambda unrestricted destination : Nat .
479 (phPipeRanges (lambda unrestricted offset : Nat . (phImm (naturalAdd source offset)))
480 (lambda unrestricted offset : Nat . (phImm (naturalAdd destination offset))))))
481
482-- the pipe the memcpys above go through; every entry point creates it first
483def phPipeCreate =
484 (lambda unrestricted tail : (family NativePhysicalCommands) .
485 (phCall phSysPipe2 (phArgs3 (phState phPipe) (phImm 0) (phImm 0)) b"" phDiscard tail))
486
487-- Read the declared prefix into a mapped buffer. Short reads (including
488-- interruption), missing files and I/O errors fail before later uploads or
489-- submissions; an unread suffix is allowed by this fill's prefix contract.
490-- Keep the descriptor in phScratch while phSlotFile carries read/close
491-- results. Both are owned temporaries across this straight-line fragment;
492-- no caller's request or telemetry slot is borrowed. Closing also prevents
493-- a multi-tensor import from exhausting the process's file descriptors.
494-- Bytes has an explicit extent; openat requires a terminating zero. An
495-- eight-byte path otherwise runs into the next payload in the host image.
496-- Caller-supplied trailing zeros remain harmless; never rely on pool padding.
497def phReadFile =
498 (lambda unrestricted path : Bytes .
499 (lambda unrestricted address : Nat .
500 (lambda unrestricted count : Nat .
501 (lambda unrestricted tail : (family NativePhysicalCommands) .
502 (phCall phSysOpenat (phArgs3 (phImm phAtFdCwd) phPayload (phImm 0)) (bytes-append path b"\x00") (phStore phSlotFile)
503 (phNext (constructor NativePhysicalOperation NativePhysicalStoreWord64 (phState phScratch) (phSlot phSlotFile))
504 (phCall phSysRead (phArgs3 (phSlot phSlotFile) (phImm address) (phImm count)) b"" (phStore phSlotFile)
505 (nativeLaunchRecipeAssertEqual (phSlot phSlotFile) (phImm count) b"input-file-read"
506 (phCall phSysClose (phArgs3 (phLoad phScratch) (phImm 0) (phImm 0)) b"" (phStore phSlotFile)
507 (nativeLaunchRecipeAssertEqual (phSlot phSlotFile) (phImm 0) b"input-file-close" tail))))))))))
508
509def phRangeBase =
510 (lambda unrestricted lifecycle : (family NvidiaPlanHostLifecycle) .
511 (eliminate NvidiaPlanHostLifecycle (lambda unrestricted current : (family NvidiaPlanHostLifecycle) . Nat) lifecycle
512 (branch NvidiaPlanHostDirectRM . 0)
513 (branch NvidiaPlanHostUVM base extent . base)))
514
515def phRangeExtent =
516 (lambda unrestricted lifecycle : (family NvidiaPlanHostLifecycle) .
517 (eliminate NvidiaPlanHostLifecycle (lambda unrestricted current : (family NvidiaPlanHostLifecycle) . Nat) lifecycle
518 (branch NvidiaPlanHostDirectRM . 0)
519 (branch NvidiaPlanHostUVM base extent . extent)))
520
521-- 1 when the buffer lies inside the lifecycle's pre-created external range,
522-- the video arena: such a buffer is mapped into the range, not given one
523def phInsideRange =
524 (lambda unrestricted lifecycle : (family NvidiaPlanHostLifecycle) .
525 (lambda unrestricted gpu : Nat .
526 (lambda unrestricted extent : Nat .
527 (naturalAnd (naturalNonzero (phRangeExtent lifecycle))
528 (naturalAnd (naturalLessOrEqual (phRangeBase lifecycle) gpu)
529 (naturalLessOrEqual (naturalAdd gpu extent) (naturalAdd (phRangeBase lifecycle) (phRangeExtent lifecycle))))))))
530
531def phWhen =
532 (lambda unrestricted flag : Nat .
533 (lambda unrestricted commands : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
534 (lambda unrestricted tail : (family NativePhysicalCommands) .
535 (nat-eliminate
536 (lambda unrestricted current : Nat . (family NativePhysicalCommands))
537 tail
538 (lambda unrestricted predecessor : Nat .
539 (lambda unrestricted ignored : (family NativePhysicalCommands) . (commands tail)))
540 flag))))
541
542-- ---- fail closed ----
543def phAssertStateZero32 =
544 (lambda unrestricted identity : Bytes .
545 (lambda unrestricted offset : Nat .
546 (lambda unrestricted tail : (family NativePhysicalCommands) .
547 (phCopy phScratch (phZeros 8)
548 (phCopyStateToState phScratch offset 4
549 (nativeLaunchRecipeAssertEqual (phLoad phScratch) (phImm 0) identity tail))))))
550
551def phAssertMappedZero32 =
552 (lambda unrestricted identity : Bytes .
553 (lambda unrestricted address : Nat .
554 (lambda unrestricted tail : (family NativePhysicalCommands) .
555 (phCopy phScratch (phZeros 8)
556 (phCopyMappedToState address phScratch 4
557 (nativeLaunchRecipeAssertEqual (phLoad phScratch) (phImm 0) identity tail))))))
558
559-- the same, unless tolerated
560def phCheckStateZero32 =
561 (lambda unrestricted identity : Bytes .
562 (lambda unrestricted tolerate : Nat .
563 (lambda unrestricted offset : Nat .
564 (lambda unrestricted tail : (family NativePhysicalCommands) .
565 (phWhen (naturalIsZero tolerate) (phAssertStateZero32 identity offset) tail)))))
566
567def phCheckMappedZero32 =
568 (lambda unrestricted identity : Bytes .
569 (lambda unrestricted tolerate : Nat .
570 (lambda unrestricted address : Nat .
571 (lambda unrestricted tail : (family NativePhysicalCommands) .
572 (phWhen (naturalIsZero tolerate) (phAssertMappedZero32 identity address) tail)))))
573
574-- ---- RM alloc / control, each asserted ----
575def phAlloc =
576 (lambda unrestricted identity : Bytes .
577 (lambda unrestricted tolerate : Nat .
578 (lambda unrestricted block : Nat .
579 (lambda unrestricted parent : Nat .
580 (lambda unrestricted class : Nat .
581 (lambda unrestricted paramsAddress : Nat .
582 (lambda unrestricted paramsSize : Nat .
583 (lambda unrestricted handle : Nat .
584 (lambda unrestricted statusOffset : Nat .
585 (lambda unrestricted tail : (family NativePhysicalCommands) .
586 (phCopy block (phSet32 (phSet32 (phSet32 (phSet32 (phSet32 (phSet32 (phZeros 32) 4 parent) 8 handle) 12 class) 16 paramsAddress) 24 paramsSize) 28 phStatusSentinel)
587 (phCopyStateToState block (naturalAdd phRoot 8) 4
588 (phCall phSysIoctl (phArgs3 (phSlot phSlotControl) (phImm phRMAlloc) (phState block)) b"" phDiscard
589 (phCopyStateToState statusOffset (naturalAdd block 28) 4
590 (phCheckStateZero32 identity tolerate (naturalAdd block 28) tail)))))))))))))))
591
592def phControl =
593 (lambda unrestricted identity : Bytes .
594 (lambda unrestricted tolerate : Nat .
595 (lambda unrestricted statusOffset : Nat .
596 (lambda unrestricted block : Nat .
597 (lambda unrestricted object : Nat .
598 (lambda unrestricted command : Nat .
599 (lambda unrestricted paramsAddress : Nat .
600 (lambda unrestricted paramsSize : Nat .
601 (lambda unrestricted tail : (family NativePhysicalCommands) .
602 (phCopy block (phSet32 (phSet32 (phSet32 (phSet32 (phSet32 (phZeros 32) 4 object) 8 command) 16 paramsAddress) 24 paramsSize) 28 phStatusSentinel)
603 (phCopyStateToState block (naturalAdd phRoot 8) 4
604 (phCall phSysIoctl (phArgs3 (phSlot phSlotControl) (phImm phRMControl) (phState block)) b"" phDiscard
605 (phCopyStateToState statusOffset (naturalAdd block 28) 4
606 (phCheckStateZero32 identity tolerate (naturalAdd block 28) tail))))))))))))))
607
608-- a UVM ioctl whose status word lives in its parameter block: the word is
609-- recorded in the UVM status record, one 4-byte slot per call, and asserted
610-- zero unless the call is one the proven hosts tolerate a non-zero from
611def phUVMStatusRecord : Nat = 3584
612def phUVMStatusSlot = (lambda unrestricted slot : Nat . (naturalAdd phUVMStatusRecord (naturalMultiply slot 4)))
613def phUVMStatusRecordExtent : Nat = 512
614 -- RM status record slots after the UVM slots
615def phRMStatusSlot = (lambda unrestricted slot : Nat . (naturalAdd 4000 (naturalMultiply slot 4)))
616
617-- the `tolerate` an RM alloc or control takes under a mode
618def phTolerate =
619 (lambda unrestricted mode : (family NvidiaPlanHostMode) .
620 (eliminate NvidiaPlanHostMode (lambda unrestricted current : (family NvidiaPlanHostMode) . Nat) mode
621 (branch NvidiaPlanHostStrict . 0)
622 (branch NvidiaPlanHostProbe . 1)))
623
624def phUVMCall =
625 (lambda unrestricted identity : Bytes .
626 (lambda unrestricted slot : Nat .
627 (lambda unrestricted tolerate : Nat .
628 (lambda unrestricted descriptor : Nat .
629 (lambda unrestricted request : Nat .
630 (lambda unrestricted paramsAddress : Nat .
631 (lambda unrestricted statusOffset : Nat .
632 (lambda unrestricted tail : (family NativePhysicalCommands) .
633 (phCall phSysIoctl (phArgs3 (phImm descriptor) (phImm request) (phImm paramsAddress)) b"" phDiscard
634 (phCopyMappedToState (naturalAdd paramsAddress statusOffset) (phUVMStatusSlot slot) 4
635 (phCheckMappedZero32 identity tolerate (naturalAdd paramsAddress statusOffset) tail)))))))))))
636
637-- the same, right after the UVM device was opened onto `descriptor`: the
638-- dup2 that placed it returned `descriptor` (it returns a negative errno
639-- when the open failed), or -- unless `openTolerate` -- the host stops with
640-- `uvm-open`, not at the ioctl that finds no device behind the descriptor.
641-- Measured on RunPod, 2026-09-24: a container whose /dev/nvidia-uvm exists
642-- but opens with EIO used to stop at `uvm-initialize`.
643def phUVMCallAfterOpen =
644 (lambda unrestricted openTolerate : Nat .
645 (lambda unrestricted identity : Bytes .
646 (lambda unrestricted slot : Nat .
647 (lambda unrestricted tolerate : Nat .
648 (lambda unrestricted descriptor : Nat .
649 (lambda unrestricted request : Nat .
650 (lambda unrestricted paramsAddress : Nat .
651 (lambda unrestricted statusOffset : Nat .
652 (lambda unrestricted tail : (family NativePhysicalCommands) .
653 (phWhen (naturalIsZero openTolerate)
654 (nativeLaunchRecipeAssertEqual (phSlot phSlotMap) (phImm descriptor) b"uvm-open")
655 (phUVMCall identity slot tolerate descriptor request paramsAddress statusOffset tail)))))))))))
656
657-- ---- buffers ----
658-- Preserve the layout's semantic buffer name at the RM allocation boundary.
659-- A generic allocation error hides which resource the driver refused.
660def phBufferIdentity =
661 (lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
662 (eliminate NvidiaPlanHostBuffer (lambda unrestricted current : (family NvidiaPlanHostBuffer) . Bytes) buffer
663 (branch NvidiaPlanHostBufferValue identity gpu host extent memory . identity)))
664def phBufferGPU =
665 (lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
666 (eliminate NvidiaPlanHostBuffer (lambda unrestricted current : (family NvidiaPlanHostBuffer) . Nat) buffer
667 (branch NvidiaPlanHostBufferValue identity gpu host extent memory . gpu)))
668def phBufferHost =
669 (lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
670 (eliminate NvidiaPlanHostBuffer (lambda unrestricted current : (family NvidiaPlanHostBuffer) . Nat) buffer
671 (branch NvidiaPlanHostBufferValue identity gpu host extent memory . host)))
672def phBufferExtent =
673 (lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
674 (eliminate NvidiaPlanHostBuffer (lambda unrestricted current : (family NvidiaPlanHostBuffer) . Nat) buffer
675 (branch NvidiaPlanHostBufferValue identity gpu host extent memory . extent)))
676def phBufferIsVideo =
677 (lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
678 (eliminate NvidiaPlanHostBuffer (lambda unrestricted current : (family NvidiaPlanHostBuffer) . Nat) buffer
679 (branch NvidiaPlanHostBufferValue identity gpu host extent memory .
680 (eliminate NvidiaPlanHostMemory (lambda unrestricted current : (family NvidiaPlanHostMemory) . Nat) memory
681 (branch NvidiaPlanHostSystemMemory . 0)
682 (branch NvidiaPlanHostVideoMemory . 1)
683 (branch NvidiaPlanHostPagedSystemMemory . 0)
684 (branch NvidiaPlanHostGPUCachedSystemMemory . 0)))))
685
686def phBufferIsPaged =
687 (lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
688 (eliminate NvidiaPlanHostBuffer (lambda unrestricted current : (family NvidiaPlanHostBuffer) . Nat) buffer
689 (branch NvidiaPlanHostBufferValue identity gpu host extent memory .
690 (eliminate NvidiaPlanHostMemory (lambda unrestricted current : (family NvidiaPlanHostMemory) . Nat) memory
691 (branch NvidiaPlanHostSystemMemory . 0)
692 (branch NvidiaPlanHostVideoMemory . 0)
693 (branch NvidiaPlanHostPagedSystemMemory . 1)
694 (branch NvidiaPlanHostGPUCachedSystemMemory . 0)))))
695
696def phBufferIsGPUCached =
697 (lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
698 (eliminate NvidiaPlanHostBuffer (lambda unrestricted current : (family NvidiaPlanHostBuffer) . Nat) buffer
699 (branch NvidiaPlanHostBufferValue identity gpu host extent memory .
700 (eliminate NvidiaPlanHostMemory (lambda unrestricted current : (family NvidiaPlanHostMemory) . Nat) memory
701 (branch NvidiaPlanHostSystemMemory . 0)
702 (branch NvidiaPlanHostVideoMemory . 0)
703 (branch NvidiaPlanHostPagedSystemMemory . 0)
704 (branch NvidiaPlanHostGPUCachedSystemMemory . 1)))))
705
706def phABI =
707 (lambda unrestricted abi : (family NvidiaPlanHostABI) .
708 (lambda unrestricted which : Nat .
709 (eliminate NvidiaPlanHostABI (lambda unrestricted current : (family NvidiaPlanHostABI) . Nat) abi
710 (branch NvidiaPlanHostABIValue mapDMA size dmaOffset status channel compute usermode engine driverBranch scheduleSize userdMemory channelFlags directDMAFlags .
711 (naturalSelect (naturalEqual which 0) mapDMA
712 (naturalSelect (naturalEqual which 1) size
713 (naturalSelect (naturalEqual which 2) dmaOffset
714 (naturalSelect (naturalEqual which 3) status
715 (naturalSelect (naturalEqual which 4) channel
716 (naturalSelect (naturalEqual which 5) compute
717 (naturalSelect (naturalEqual which 6) usermode (naturalSelect (naturalEqual which 7) engine (naturalSelect (naturalEqual which 8) driverBranch
718 (naturalSelect (naturalEqual which 9) scheduleSize channelFlags))))))))))))))
719
720def phUSERDRequiresVideo =
721 (lambda unrestricted abi : (family NvidiaPlanHostABI) .
722 (eliminate NvidiaPlanHostABI (lambda unrestricted current : (family NvidiaPlanHostABI) . Nat) abi
723 (branch NvidiaPlanHostABIValue mapDMA size dmaOffset status channel compute usermode engine driverBranch scheduleSize userdMemory channelFlags directDMAFlags .
724 (eliminate NvidiaPlanHostMemory (lambda unrestricted memory : (family NvidiaPlanHostMemory) . Nat) userdMemory
725 (branch NvidiaPlanHostSystemMemory . 0)
726 (branch NvidiaPlanHostVideoMemory . 1)
727 (branch NvidiaPlanHostPagedSystemMemory . 0)
728 (branch NvidiaPlanHostGPUCachedSystemMemory . 0)))))
729
730def phIsUVM =
731 (lambda unrestricted lifecycle : (family NvidiaPlanHostLifecycle) .
732 (eliminate NvidiaPlanHostLifecycle (lambda unrestricted current : (family NvidiaPlanHostLifecycle) . Nat) lifecycle
733 (branch NvidiaPlanHostDirectRM . 0)
734 (branch NvidiaPlanHostUVM base extent . 1)))
735
736-- a buffer extent for a table: the table's bytes rounded up to a unit
737def nvidiaPlanHostRoundUp =
738 (lambda unrestricted value : Nat .
739 (lambda unrestricted unit : Nat .
740 (naturalMultiply (naturalDivideUnchecked (naturalAdd value (naturalSaturatingSubtract unit 1)) unit) unit)))
741
742-- Where the host may write: the host-mapped buffers of a layout (host 0 =
743-- not mapped), the error notifier's page among them. A range is admitted
744-- when mapped buffers cover it end to end -- adjacent mappings may carry
745-- one table across their seam (Coppelius's QMD primary and overflow).
746def nvidiaPlanHostErrorPageBytes : Nat = 0x1000
747
748def phMapped =
749 (lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
750 (lambda unrestricted rest : (family NvidiaPlanHostBuffers) .
751 (constructor NvidiaPlanHostBuffers NvidiaPlanHostBuffersNext buffer rest)))
752
753def phLayoutMappings =
754 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
755 (eliminate NvidiaPlanHostLayout (lambda unrestricted current : (family NvidiaPlanHostLayout) . (family NvidiaPlanHostBuffers)) layout
756 (branch NvidiaPlanHostLayoutValue gpfifo push sem program qmd userd data abi lifecycle expectedName errorHost .
757 (phMapped gpfifo (phMapped push (phMapped sem (phMapped program (phMapped qmd (phMapped userd
758 (phMapped (constructor NvidiaPlanHostBuffer NvidiaPlanHostBufferValue b"error-notifier" 0 errorHost nvidiaPlanHostErrorPageBytes
759 (constructor NvidiaPlanHostMemory NvidiaPlanHostSystemMemory))
760 data))))))))))
761
762def phMappingCount =
763 (lambda unrestricted buffers : (family NvidiaPlanHostBuffers) .
764 (eliminate NvidiaPlanHostBuffers (lambda unrestricted current : (family NvidiaPlanHostBuffers) . Nat) buffers
765 (branch NvidiaPlanHostBuffersEnd . 0)
766 (branch NvidiaPlanHostBuffersNext head rest induction . (succ induction))))
767
768-- the end of the first host-mapped buffer holding the byte at `host`, 0 when none does
769def phMappingEndAt =
770 (lambda unrestricted buffers : (family NvidiaPlanHostBuffers) .
771 (lambda unrestricted host : Nat .
772 (eliminate NvidiaPlanHostBuffers (lambda unrestricted current : (family NvidiaPlanHostBuffers) . Nat) buffers
773 (branch NvidiaPlanHostBuffersEnd . 0)
774 (branch NvidiaPlanHostBuffersNext head rest induction .
775 (naturalSelect
776 (naturalAnd (naturalNonzero (phBufferHost head))
777 (naturalAnd (naturalLessOrEqual (phBufferHost head) host)
778 (naturalLess host (naturalAdd (phBufferHost head) (phBufferExtent head)))))
779 (naturalAdd (phBufferHost head) (phBufferExtent head))
780 induction)))))
781
782-- 1 when the buffers cover [host, host + extent): step from mapping to
783-- mapping, at most once per mapping (the fuel)
784def phCovers =
785 (lambda unrestricted buffers : (family NvidiaPlanHostBuffers) .
786 (lambda unrestricted fuel : Nat .
787 (nat-eliminate
788 (lambda unrestricted current : Nat . (pi unrestricted host : Nat . (pi unrestricted extent : Nat . Nat)))
789 (lambda unrestricted host : Nat . (lambda unrestricted extent : Nat . (naturalEqual extent 0)))
790 (lambda unrestricted predecessor : Nat .
791 (lambda unrestricted induction : (pi unrestricted host : Nat . (pi unrestricted extent : Nat . Nat)) .
792 (lambda unrestricted host : Nat .
793 (lambda unrestricted extent : Nat .
794 (let unrestricted end = (phMappingEndAt buffers host)
795 in (naturalSelect (naturalEqual extent 0) 1
796 (naturalSelect (naturalEqual end 0) 0
797 (induction end (naturalSaturatingSubtract (naturalAdd host extent) end)))))))))
798 fuel)))
799
800def nvidiaPlanHostContains =
801 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
802 (lambda unrestricted host : Nat .
803 (lambda unrestricted extent : Nat .
804 (let unrestricted mappings = (phLayoutMappings layout)
805 in (phCovers mappings (phMappingCount mappings) host extent)))))
806
807-- a GPU-cached buffer is CPU-uncached (MAP_NOT_REQUIRED): no host address
808def phGPUCachedUnmapped =
809 (lambda unrestricted buffers : (family NvidiaPlanHostBuffers) .
810 (eliminate NvidiaPlanHostBuffers (lambda unrestricted current : (family NvidiaPlanHostBuffers) . Nat) buffers
811 (branch NvidiaPlanHostBuffersEnd . 1)
812 (branch NvidiaPlanHostBuffersNext head rest induction .
813 (naturalAnd induction (naturalSelect (phBufferIsGPUCached head) (naturalIsZero (phBufferHost head)) 1)))))
814
815-- Admission, 1 when the host will be derived: under direct-RM the USERD
816-- buffer has the target ABI's location (Ampere requires video memory;
817-- the integrated GB10 profile requires system memory). Under
818-- UVM the USERD entry is the alias of the GPFIFO's last page and is not
819-- allocated, so there is nothing to admit. A pairing gates its artifact
820-- on this and the checker decides it.
821def nvidiaPlanHostLayoutAdmitted =
822 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
823 (eliminate NvidiaPlanHostLayout (lambda unrestricted current : (family NvidiaPlanHostLayout) . Nat) layout
824 (branch NvidiaPlanHostLayoutValue gpfifo push sem program qmd userd data abi lifecycle expectedName errorHost .
825 (naturalAnd (phGPUCachedUnmapped (phLayoutMappings layout))
826 (naturalSelect (phIsUVM lifecycle) 1
827 (naturalEqual (phBufferIsVideo userd) (phUSERDRequiresVideo abi)))))))
828
829
830-- ---- the layout's placement certificate ----
831-- Every buffer of a layout is a resident of two arenas: the card's virtual
832-- address space (49 bits on Ampere) at its GPU address, and the process's
833-- (47 bits of user space) at its host address when it is mapped there. In
834-- each, Runtime.ArenaCertificate decides every resident page-aligned,
835-- non-empty, inside, and disjoint from every other -- PlanHost's own fixed
836-- mappings (the parameter page, the doorbell) and, under UVM, the channel's
837-- range among them. The one sanctioned alias, the UVM USERD entry (the
838-- GPFIFO buffer's last page, never allocated), is not a resident: it must
839-- lie inside the GPFIFO buffer in both spaces.
840def nvidiaPlanHostPageBytes : Nat = 0x1000
841def phGPUSpaceBytes : Nat = 0x2_0000_0000_0000
842def phHostSpaceBytes : Nat = 0x8000_0000_0000
843
844def phResident =
845 (lambda unrestricted identity : Bytes .
846 (lambda unrestricted offset : Nat .
847 (lambda unrestricted extent : Nat .
848 (lambda unrestricted rest : (family ArenaResidents) .
849 (constructor ArenaResidents ArenaResidentsNext
850 (constructor ArenaResident ArenaResidentValue identity offset extent nvidiaPlanHostPageBytes)
851 rest)))))
852
853-- a buffer at its GPU address
854def phGPUResident =
855 (lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
856 (lambda unrestricted rest : (family ArenaResidents) .
857 (eliminate NvidiaPlanHostBuffer (lambda unrestricted current : (family NvidiaPlanHostBuffer) . (family ArenaResidents)) buffer
858 (branch NvidiaPlanHostBufferValue identity gpu host extent memory . (phResident identity gpu extent rest)))))
859
860-- a buffer at its host address, when it is mapped (host 0 = not mapped)
861def phHostResident =
862 (lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
863 (lambda unrestricted rest : (family ArenaResidents) .
864 (eliminate NvidiaPlanHostBuffer (lambda unrestricted current : (family NvidiaPlanHostBuffer) . (family ArenaResidents)) buffer
865 (branch NvidiaPlanHostBufferValue identity gpu host extent memory .
866 (nat-eliminate (lambda unrestricted current : Nat . (family ArenaResidents))
867 rest
868 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family ArenaResidents) .
869 (phResident identity host extent rest)))
870 (naturalNonzero host))))))
871
872def phEachResident =
873 (lambda unrestricted place : (pi unrestricted buffer : (family NvidiaPlanHostBuffer) . (pi unrestricted rest : (family ArenaResidents) . (family ArenaResidents))) .
874 (lambda unrestricted buffers : (family NvidiaPlanHostBuffers) .
875 (lambda unrestricted rest : (family ArenaResidents) .
876 (eliminate NvidiaPlanHostBuffers (lambda unrestricted current : (family NvidiaPlanHostBuffers) . (family ArenaResidents)) buffers
877 (branch NvidiaPlanHostBuffersEnd . rest)
878 (branch NvidiaPlanHostBuffersNext head tail induction . (place head induction))))))
879
880-- the layout's buffers, the USERD entry only when it is allocated (direct-RM)
881def phAllocatedBuffers =
882 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
883 (eliminate NvidiaPlanHostLayout (lambda unrestricted current : (family NvidiaPlanHostLayout) . (family NvidiaPlanHostBuffers)) layout
884 (branch NvidiaPlanHostLayoutValue gpfifo push sem program qmd userd data abi lifecycle expectedName errorHost .
885 (phMapped gpfifo (phMapped push (phMapped sem (phMapped program (phMapped qmd
886 (nat-eliminate (lambda unrestricted current : Nat . (family NvidiaPlanHostBuffers))
887 (phMapped userd data)
888 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family NvidiaPlanHostBuffers) . data))
889 (phIsUVM lifecycle))))))))))
890
891def phGPUResidents =
892 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
893 (phEachResident phGPUResident (phAllocatedBuffers layout)
894 (eliminate NvidiaPlanHostLayout (lambda unrestricted current : (family NvidiaPlanHostLayout) . (family ArenaResidents)) layout
895 (branch NvidiaPlanHostLayoutValue gpfifo push sem program qmd userd data abi lifecycle expectedName errorHost .
896 (eliminate NvidiaPlanHostLifecycle (lambda unrestricted current : (family NvidiaPlanHostLifecycle) . (family ArenaResidents)) lifecycle
897 (branch NvidiaPlanHostDirectRM . (constructor ArenaResidents ArenaResidentsEnd))
898 (branch NvidiaPlanHostUVM base extent .
899 (phResident b"uvm-channel-range" phUVMChannelRangeBase phUVMChannelRangeExtent (constructor ArenaResidents ArenaResidentsEnd))))))))
900
901-- `extras`: the mappings a host adds of its own (the request host's recipe
902-- staging area)
903def phHostResidents =
904 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
905 (lambda unrestricted extras : (family ArenaResidents) .
906 (phEachResident phHostResident (phAllocatedBuffers layout)
907 (phResident b"parameters" phParams 0x10000
908 (phResident b"doorbell" phDoorHost 0x10000
909 (eliminate NvidiaPlanHostLayout (lambda unrestricted current : (family NvidiaPlanHostLayout) . (family ArenaResidents)) layout
910 (branch NvidiaPlanHostLayoutValue gpfifo push sem program qmd userd data abi lifecycle expectedName errorHost .
911 (nat-eliminate (lambda unrestricted current : Nat . (family ArenaResidents))
912 extras
913 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family ArenaResidents) .
914 (phResident b"error-notifier" errorHost nvidiaPlanHostErrorPageBytes extras)))
915 (naturalNonzero errorHost)))))))))
916
917-- [inner, inner + innerExtent) inside [outer, outer + outerExtent)
918def phInside =
919 (lambda unrestricted inner : Nat . (lambda unrestricted innerExtent : Nat .
920 (lambda unrestricted outer : Nat . (lambda unrestricted outerExtent : Nat .
921 (naturalAnd (naturalLessOrEqual outer inner)
922 (naturalLessOrEqual (naturalAdd inner innerExtent) (naturalAdd outer outerExtent)))))))
923
924-- under UVM, the USERD entry inside the GPFIFO buffer in both spaces
925def phUSERDAliasInside =
926 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
927 (eliminate NvidiaPlanHostLayout (lambda unrestricted current : (family NvidiaPlanHostLayout) . Nat) layout
928 (branch NvidiaPlanHostLayoutValue gpfifo push sem program qmd userd data abi lifecycle expectedName errorHost .
929 (naturalSelect (phIsUVM lifecycle)
930 (eliminate NvidiaPlanHostBuffer (lambda unrestricted current : (family NvidiaPlanHostBuffer) . Nat) userd
931 (branch NvidiaPlanHostBufferValue aliasIdentity aliasGPU aliasHost aliasExtent aliasMemory .
932 (eliminate NvidiaPlanHostBuffer (lambda unrestricted current : (family NvidiaPlanHostBuffer) . Nat) gpfifo
933 (branch NvidiaPlanHostBufferValue identity gpu host extent memory .
934 (naturalAnd (phInside aliasGPU aliasExtent gpu extent) (phInside aliasHost aliasExtent host extent))))))
935 1))))
936
937-- 1 when the layout's placement is certified in both spaces
938def nvidiaPlanHostLayoutCertified =
939 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
940 (lambda unrestricted extras : (family ArenaResidents) .
941 (naturalAnd (arenaCertificate phGPUSpaceBytes (phGPUResidents layout))
942 (naturalAnd (arenaCertificate phHostSpaceBytes (phHostResidents layout extras))
943 (phUSERDAliasInside layout)))))
944
945-- Every upload lands inside a host-mapped buffer of the layout: bytes, or a
946-- file's declared extent. The subagent's RTX 3070 sweep (2026-09-23) found
947-- program tables up to 7936 bytes built into a 4096-byte program buffer and
948-- copied past it at run time -- the kernel never ran; now the build refuses.
949def nvidiaPlanHostFillsAdmitted =
950 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
951 (lambda unrestricted fills : (family NvidiaPlanHostFills) .
952 (eliminate NvidiaPlanHostFills (lambda unrestricted current : (family NvidiaPlanHostFills) . Nat) fills
953 (branch NvidiaPlanHostFillsEnd . 1)
954 (branch NvidiaPlanHostFillBytes host payload rest induction .
955 (naturalAnd (nvidiaPlanHostContains layout host (bytes-length payload)) induction))
956 (branch NvidiaPlanHostFillFile host path extent rest induction .
957 (naturalAnd (nvidiaPlanHostContains layout host extent) induction)))))
958
959-- what a plan-derived host needs admitted before it is built
960def nvidiaPlanHostAdmitted =
961 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
962 (lambda unrestricted fills : (family NvidiaPlanHostFills) .
963 (naturalAnd (nvidiaPlanHostLayoutAdmitted layout)
964 (naturalAnd (nvidiaPlanHostLayoutCertified layout (constructor ArenaResidents ArenaResidentsEnd))
965 (nvidiaPlanHostFillsAdmitted layout fills)))))
966
967-- system memory: host-cached, contiguous or noncontiguous as declared. video memory: the local-user
968-- object, write-combined, contiguous, page-aligned.
969-- system memory's attributes: PCI, cached, and contiguous (0x32000000) or,
970-- paged, non-contiguous (0x2A000000)
971def phGPUCachedPageBytes : Nat = 0x10000
972
973-- NV_MEMORY_ALLOCATION_PARAMS for a buffer: owner, flags (8), attr (24),
974-- attr2 (28), format (32), size (64), alignment (72), limit (88)
975def phGPUCachedMemoryParams =
976 (lambda unrestricted extent : Nat .
977 (phSet64 (phSet64 (phSet64 (phSet32 (phSet32 (phSet32 (phSet32 (phSet32 (phZeros 128)
978 0 0x636c6161) 8 0x0000C001) 24 0x0B000000) 28 0x00000005) 32 0x00000006)
979 64 extent) 72 phGPUCachedPageBytes) 88 (naturalSaturatingSubtract extent 1)))
980
981
982def phMemoryParams =
983 (lambda unrestricted video : Nat .
984 (lambda unrestricted paged : Nat .
985 (lambda unrestricted cached : Nat .
986 (lambda unrestricted inside : Nat .
987 (lambda unrestricted extent : Nat .
988 (nat-eliminate
989 (lambda unrestricted current : Nat . Bytes)
990 (nat-eliminate
991 (lambda unrestricted current : Nat . Bytes)
992 (phSet64 (phSet32 (phSet32 (phZeros 128) 0 0x636c6161) 24 (naturalSelect paged 0x2A000000 0x32000000)) 64 extent)
993 (lambda unrestricted predecessor : Nat .
994 (lambda unrestricted ignored : Bytes . (phGPUCachedMemoryParams extent)))
995 cached)
996 (lambda unrestricted predecessor : Nat .
997 (lambda unrestricted ignored : Bytes .
998 (phSet64 (phSet64 (phSet32 (phSet32 (phSet32 (phZeros 128) 0 0x48454C49) 8 0x00008000) 24 (naturalSelect inside 0x58000000 0x50000000)) 64 extent) 72 0x1000)))
999 video))))))
1000
1001def phMemoryClass =
1002 (lambda unrestricted video : Nat . (naturalSelect video 0x40 0x3E))
1003
1004-- the host mapping of one buffer through a fresh control descriptor, or for
1005-- video memory through a fresh card descriptor
1006def phOpenCardsInto =
1007 (lambda unrestricted descriptor : Nat .
1008 (lambda unrestricted path : Bytes .
1009 (lambda unrestricted tail : (family NativePhysicalCommands) .
1010 (phCall phSysOpenat (phArgs3 (phImm phAtFdCwd) phPayload (phImm phOpenFlags)) path (phStore phSlotMap)
1011 (phCall phSysIoctl (phArgs3 (phSlot phSlotMap) (phImm phWaitOpen) (phState phWait)) b"" phDiscard
1012 (phCall phSysDup2 (phArgs3 (phSlot phSlotMap) (phImm descriptor) (phImm 0)) b"" phDiscard tail))))))
1013
1014def phMappingDescriptor =
1015 (lambda unrestricted video : Nat .
1016 (lambda unrestricted tail : (family NativePhysicalCommands) .
1017 (nat-eliminate
1018 (lambda unrestricted current : Nat . (family NativePhysicalCommands))
1019 (phCall phSysOpenat (phArgs3 (phImm phAtFdCwd) phPayload (phImm phOpenFlags)) b"/dev/nvidiactl\x00" (phStore phSlotMap)
1020 (phCall phSysDup2 (phArgs3 (phSlot phSlotMap) (phImm phFdMap) (phImm 0)) b"" phDiscard tail))
1021 (lambda unrestricted predecessor : Nat .
1022 (lambda unrestricted ignored : (family NativePhysicalCommands) .
1023 (phOpenCardsInto phFdMap b"/dev/nvidia0\x00" (phOpenCardsInto phFdMap b"/dev/nvidia1\x00"
1024 (phOpenCardsInto phFdMap b"/dev/nvidia2\x00" (phOpenCardsInto phFdMap b"/dev/nvidia3\x00"
1025 (phOpenCardsInto phFdMap b"/dev/nvidia4\x00" (phOpenCardsInto phFdMap b"/dev/nvidia5\x00"
1026 (phOpenCardsInto phFdMap b"/dev/nvidia6\x00" (phOpenCardsInto phFdMap b"/dev/nvidia7\x00" tail))))))))))
1027 video)))
1028
1029-- the host mapping of one RM memory object: the NVOS33 map through the
1030-- fresh descriptor, its status recorded, then mmap at the host address
1031def phMapMemory =
1032 (lambda unrestricted identity : Bytes .
1033 (lambda unrestricted mode : (family NvidiaPlanHostMode) .
1034 (lambda unrestricted block : Nat .
1035 (lambda unrestricted hMemory : Nat .
1036 (lambda unrestricted video : Nat .
1037 (lambda unrestricted extent : Nat .
1038 (lambda unrestricted host : Nat .
1039 (lambda unrestricted statusOffset : Nat .
1040 (lambda unrestricted tail : (family NativePhysicalCommands) .
1041 (let unrestricted flags = (naturalSelect video 0x01010000 0x03008000)
1042 in
1043 (phMappingDescriptor video
1044 (phCall phSysIoctl (phArgs3 (phImm phFdMap) (phImm phRegisterFD) (phImm phRegFdP)) b"" phDiscard
1045 (phCopy block (phSet32 (phSet32 (phSet32 (phSet64 (phSet32 (phSet32 (phZeros 56) 4 phHDevice) 8 hMemory) 24 extent) 40 phStatusSentinel) 44 flags) 48 phFdMap)
1046 (phCopyStateToState block (naturalAdd phRoot 8) 4
1047 (phCall phSysIoctl (phArgs3 (phImm phFdControl) (phImm phRMMapMemory) (phState block)) b"" phDiscard
1048 (phCopyStateToState statusOffset (naturalAdd block 40) 4
1049 (phCheckStateZero32 identity (phTolerate mode) (naturalAdd block 40)
1050 (phCall phSysMmap (phArgs (phImm host) (phImm extent) (phImm 3) (phImm phMapSharedFixed) (phImm phFdMap) (phImm 0)) b"" phDiscard
1051 tail))))))))))))))))))
1052
1053def phHostMap =
1054 (lambda unrestricted mode : (family NvidiaPlanHostMode) .
1055 (lambda unrestricted index : Nat .
1056 (lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
1057 (lambda unrestricted tail : (family NativePhysicalCommands) .
1058 (phMapMemory b"host-map" mode (naturalAdd (phBufferState index) 128) (phHMemory index) (phBufferIsVideo buffer)
1059 (phBufferExtent buffer) (phBufferHost buffer) (naturalAdd (phBufferStatus index) 12) tail)))))
1060
1061def phDirectDMAFlags =
1062 (lambda unrestricted abi : (family NvidiaPlanHostABI) .
1063 (eliminate NvidiaPlanHostABI (lambda unrestricted current : (family NvidiaPlanHostABI) . Nat) abi
1064 (branch NvidiaPlanHostABIValue mapDMA size dmaOffset status channel compute usermode engine driverBranch scheduleSize userdMemory channelFlags directDMAFlags . directDMAFlags)))
1065
1066-- direct-RM: a fixed virtual reservation and the DMA map to it
1067def phDirectRange =
1068 (lambda unrestricted abi : (family NvidiaPlanHostABI) .
1069 (lambda unrestricted mode : (family NvidiaPlanHostMode) .
1070 (lambda unrestricted index : Nat .
1071 (lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
1072 (lambda unrestricted tail : (family NativePhysicalCommands) .
1073 (let unrestricted st = (phBufferState index)
1074 in (let unrestricted gpu = (phBufferGPU buffer)
1075 in (let unrestricted extent = (phBufferExtent buffer)
1076 in
1077 (phFill (phVirtP index) (phSet32 (phSet64 (phSet64 (phZeros 24) 0 gpu) 8 (naturalSaturatingSubtract (naturalAdd gpu extent) 1)) 16 phHVASpace)
1078 (phAlloc b"alloc:virtual" (phTolerate mode) (naturalAdd st 32) phHDevice 0x70 (phVirtP index) 24 (phHVirtual index) (naturalAdd (phBufferStatus index) 4)
1079 (phCopy (naturalAdd st 64) (phSet32 (phSet64 (phSet64 (phSet32 (phSet32 (phSet32 (phSet32 (phZeros (phABI abi 1)) 4 phHDevice) 8 (phHVirtual index)) 12 (phHMemory index)) 32 (phDirectDMAFlags abi)) 24 extent) (phABI abi 2) gpu) (phABI abi 3) phStatusSentinel)
1080 (phCopyStateToState (naturalAdd st 64) (naturalAdd phRoot 8) 4
1081 (phCall phSysIoctl (phArgs3 (phSlot phSlotControl) (phImm (phABI abi 0)) (phState (naturalAdd st 64))) b"" phDiscard
1082 (phCopyStateToState (naturalAdd (phBufferStatus index) 8) (naturalAdd st (naturalAdd 64 (phABI abi 3))) 4
1083 (phCheckStateZero32 b"dma-map" (phTolerate mode) (naturalAdd st (naturalAdd 64 (phABI abi 3))) tail)))))))))))))))
1084
1085-- NVOS46 flags of the UVM path's DMA map: DMA_OFFSET_FIXED, CACHE_SNOOP,
1086-- and 4 KiB pages; a GPU-cached buffer takes the allocation's own (64 KiB)
1087-- page size instead
1088def phUVMDMAFlags : Nat = 0x8110
1089def phUVMDMAFlagsDefaultPages : Nat = 0x8010
1090
1091-- UVM: an external range at the plan's address, the DMA map through the
1092-- device DMA selector, and the mapping registered with UVM
1093def phUVMRange =
1094 (lambda unrestricted abi : (family NvidiaPlanHostABI) .
1095 (lambda unrestricted mode : (family NvidiaPlanHostMode) .
1096 (lambda unrestricted inside : Nat .
1097 (lambda unrestricted index : Nat .
1098 (lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
1099 (lambda unrestricted tail : (family NativePhysicalCommands) .
1100 (let unrestricted st = (phBufferState index)
1101 in (let unrestricted gpu = (phBufferGPU buffer)
1102 in (let unrestricted extent = (phBufferExtent buffer)
1103 in (let unrestricted tolerate = (phTolerate mode)
1104 in
1105 (phWhen (naturalIsZero inside)
1106 (lambda unrestricted rest : (family NativePhysicalCommands) .
1107 (phFill phUVMCreateRangeP (phSet32 (phSet64 (phSet64 (phZeros 24) 0 gpu) 8 extent) 16 phStatusSentinel)
1108 (phUVMCall b"uvm-buffer-range" (naturalAdd 8 (naturalMultiply 2 index)) tolerate phFdUVM phUVMCreateExternalRange phUVMCreateRangeP 16 rest)))
1109 (phCopy (naturalAdd st 64) (phSet32 (phSet64 (phSet64 (phSet32 (phSet32 (phSet32 (phSet32 (phZeros (phABI abi 1)) 4 phHDevice) 8 phHDMA) 12 (phHMemory index)) 32 (naturalSelect (phBufferIsGPUCached buffer) phUVMDMAFlagsDefaultPages phUVMDMAFlags)) 24 extent) (phABI abi 2) gpu) (phABI abi 3) phStatusSentinel)
1110 (phCopyStateToState (naturalAdd st 64) (naturalAdd phRoot 8) 4
1111 (phCall phSysIoctl (phArgs3 (phSlot phSlotControl) (phImm (phABI abi 0)) (phState (naturalAdd st 64))) b"" phDiscard
1112 (phCopyStateToState (naturalAdd (phBufferStatus index) 8) (naturalAdd st (naturalAdd 64 (phABI abi 3))) 4
1113 (phCheckStateZero32 b"dma-map-uvm" tolerate (naturalAdd st (naturalAdd 64 (phABI abi 3)))
1114 (phFill phUVMMapAllocationP (phSet32 (phSet32 (phSet32 (phSet64 (phSet32 (phSet64 (phSet64 (phZeros 9264) 0 gpu) 8 extent) 40 1) 9240 1) 9248 phFdControl) 9256 (phHMemory index)) 9260 phStatusSentinel)
1115 (phCopyMappedToMapped (naturalAdd phUVMGidP 12) (naturalAdd phUVMMapAllocationP 24) 16
1116 (phCopyStateToMapped (naturalAdd phRoot 8) (naturalAdd phUVMMapAllocationP 9252) 4
1117 (phUVMCall b"uvm-buffer-map" (naturalAdd 9 (naturalMultiply 2 index)) tolerate phFdUVM phUVMMapExternalAllocation phUVMMapAllocationP 9260 tail))))))))))))))))))))
1118
1119-- One buffer: allocate, place, map.
1120def phBuffer =
1121 (lambda unrestricted abi : (family NvidiaPlanHostABI) .
1122 (lambda unrestricted mode : (family NvidiaPlanHostMode) .
1123 (lambda unrestricted lifecycle : (family NvidiaPlanHostLifecycle) .
1124 (lambda unrestricted index : Nat .
1125 (lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
1126 (lambda unrestricted tail : (family NativePhysicalCommands) .
1127 (let unrestricted video = (phBufferIsVideo buffer)
1128 in (let unrestricted uvm = (phIsUVM lifecycle)
1129 in (let unrestricted inside = (phInsideRange lifecycle (phBufferGPU buffer) (phBufferExtent buffer))
1130 in
1131 (phFill (phMemP index) (phMemoryParams video (phBufferIsPaged buffer) (phBufferIsGPUCached buffer) inside (phBufferExtent buffer))
1132 (phAlloc (bytes-append b"alloc:" (phBufferIdentity buffer)) (phTolerate mode) (phBufferState index) phHDevice (phMemoryClass video) (phMemP index) 128 (phHMemory index) (phBufferStatus index)
1133 (phWhen (naturalIsZero uvm) (phDirectRange abi mode index buffer)
1134 (phWhen uvm (phUVMRange abi mode inside index buffer)
1135 (phWhen (naturalNonzero (phBufferHost buffer)) (phHostMap mode index buffer)
1136 tail))))))))))))))
1137
1138def phDataBuffers =
1139 (lambda unrestricted abi : (family NvidiaPlanHostABI) .
1140 (lambda unrestricted mode : (family NvidiaPlanHostMode) .
1141 (lambda unrestricted lifecycle : (family NvidiaPlanHostLifecycle) .
1142 (lambda unrestricted first : Nat .
1143 (lambda unrestricted buffers : (family NvidiaPlanHostBuffers) .
1144 (lambda unrestricted tail : (family NativePhysicalCommands) .
1145 (app
1146 (eliminate NvidiaPlanHostBuffers
1147 (lambda unrestricted current : (family NvidiaPlanHostBuffers) . (pi unrestricted index : Nat . (family NativePhysicalCommands)))
1148 buffers
1149 (branch NvidiaPlanHostBuffersEnd . (lambda unrestricted index : Nat . tail))
1150 (branch NvidiaPlanHostBuffersNext head rest induction .
1151 (lambda unrestricted index : Nat . (phBuffer abi mode lifecycle index head (induction (succ index))))))
1152 first)))))))
1153
1154-- ---- device discovery ----
1155def phOpenCard =
1156 (lambda unrestricted path : Bytes .
1157 (lambda unrestricted tail : (family NativePhysicalCommands) .
1158 (phCall phSysOpenat (phArgs3 (phImm phAtFdCwd) phPayload (phImm phOpenFlags)) path (phStore phSlotGPU)
1159 (phCall phSysIoctl (phArgs3 (phSlot phSlotGPU) (phImm phWaitOpen) (phState phWait)) b"" phDiscard
1160 (phCall phSysDup2 (phArgs3 (phSlot phSlotGPU) (phImm phFdCard) (phImm 0)) b"" phDiscard tail)))))
1161
1162def phDeviceProbe =
1163 (lambda unrestricted index : Nat .
1164 (lambda unrestricted tail : (family NativePhysicalCommands) .
1165 (phFill phDevP (phSet32 (phZeros 56) 0 index)
1166 (phCall phSysIoctl (phArgs3 (phSlot phSlotControl) (phImm phRMAlloc) (phState phDev)) b"" phDiscard tail))))
1167
1168-- NV2080_CTRL_CMD_GPU_GET_NAME_STRING: the 64 ASCII bytes the card reports
1169-- must equal the name the plan was paired with
1170def phNameWord =
1171 (lambda unrestricted expected : Bytes .
1172 (lambda unrestricted offset : Nat .
1173 (lambda unrestricted tail : (family NativePhysicalCommands) .
1174 (phCopyMappedToState (naturalAdd (naturalAdd phNameP 4) offset) phScratch 8
1175 (phCopy (naturalAdd phScratch 8) (phTake 8 (phDrop offset expected))
1176 (nativeLaunchRecipeAssertEqual (phLoad phScratch) (phLoad (naturalAdd phScratch 8)) phIdentity tail))))))
1177
1178def phExpectName =
1179 (lambda unrestricted mode : (family NvidiaPlanHostMode) .
1180 (lambda unrestricted expected : Bytes .
1181 (lambda unrestricted tail : (family NativePhysicalCommands) .
1182 (phFill phNameP (phZeros 132)
1183 (phControl b"control:phName" (phTolerate mode) (phRMStatusSlot 11) phName phHSubdevice 0x20800110 phNameP 132
1184 (phNameWord expected 0 (phNameWord expected 8 (phNameWord expected 16 (phNameWord expected 24
1185 (phNameWord expected 32 (phNameWord expected 40 (phNameWord expected 48 (phNameWord expected 56 tail)))))))))))))
1186
1187-- ---- the UVM driver ----
1188def phUVMPrepare =
1189 (lambda unrestricted mode : (family NvidiaPlanHostMode) .
1190 (lambda unrestricted base : Nat .
1191 (lambda unrestricted extent : Nat .
1192 (lambda unrestricted tail : (family NativePhysicalCommands) .
1193 (phFill phUVMGidP (phSet32 (phSet32 (phZeros 268) 4 2) 8 16)
1194 (phControl b"control:phUVMControl" (phTolerate mode) (phRMStatusSlot 12) phUVMControl phHSubdevice 0x2080014A phUVMGidP 268
1195 (phCall phSysOpenat (phArgs3 (phImm phAtFdCwd) phPayload (phImm phOpenFlags)) b"/dev/nvidia-uvm\x00" (phStore phSlotMap)
1196 (phCall phSysDup2 (phArgs3 (phSlot phSlotMap) (phImm phFdUVM) (phImm 0)) b"" (phStore phSlotMap)
1197 (phFill phUVMInitP (phSet32 (phZeros 16) 8 phStatusSentinel)
1198 (phUVMCallAfterOpen (phTolerate mode) b"uvm-initialize" 1 (phTolerate mode) phFdUVM phUVMInitialize phUVMInitP 8
1199 (phCall phSysOpenat (phArgs3 (phImm phAtFdCwd) phPayload (phImm phOpenFlags)) b"/dev/nvidia-uvm\x00" (phStore phSlotMap)
1200 (phCall phSysDup2 (phArgs3 (phSlot phSlotMap) (phImm phFdUVMMemoryMap) (phImm 0)) b"" (phStore phSlotMap)
1201 (phFill phUVMMMP (phSet32 (phSet32 (phZeros 8) 0 phFdUVM) 4 phStatusSentinel)
1202 (phUVMCallAfterOpen (phTolerate mode) b"uvm-mm-initialize" 2 1 phFdUVMMemoryMap phUVMMMInitialize phUVMMMP 4
1203 (phFill phUVMRegisterGPUP (phSet32 (phSet32 (phZeros 40) 24 phStatusSentinel) 36 phStatusSentinel)
1204 (phCopyMappedToMapped (naturalAdd phUVMGidP 12) phUVMRegisterGPUP 16
1205 (phUVMCall b"uvm-register-gpu" 3 (phTolerate mode) phFdUVM phUVMRegisterGPU phUVMRegisterGPUP 36
1206 (phFill phUVMRegisterVASpaceP (phSet32 (phSet32 (phSet32 (phZeros 32) 16 phFdControl) 24 phHVASpace) 28 phStatusSentinel)
1207 (phCopyMappedToMapped (naturalAdd phUVMGidP 12) phUVMRegisterVASpaceP 16
1208 (phCopyStateToMapped (naturalAdd phRoot 8) (naturalAdd phUVMRegisterVASpaceP 20) 4
1209 (phUVMCall b"uvm-register-vaspace" 4 (phTolerate mode) phFdUVM phUVMRegisterGPUVASpace phUVMRegisterVASpaceP 28
1210 (phWhen (naturalNonzero extent)
1211 (lambda unrestricted rest : (family NativePhysicalCommands) .
1212 (phFill phUVMCreateRangeP (phSet32 (phSet64 (phSet64 (phZeros 24) 0 base) 8 extent) 16 phStatusSentinel)
1213 (phUVMCall b"uvm-external-range" 6 (phTolerate mode) phFdUVM phUVMCreateExternalRange phUVMCreateRangeP 16 rest)))
1214 tail))))))))))))))))))))))
1215
1216def phUVMRegisterChannelCommands =
1217 (lambda unrestricted abi : (family NvidiaPlanHostABI) .
1218 (lambda unrestricted mode : (family NvidiaPlanHostMode) .
1219 (lambda unrestricted tail : (family NativePhysicalCommands) .
1220 (phFill phUVMRegisterChannelP (phSet32 (phSet64 (phSet64 (phSet32 (phSet32 (phZeros 56) 16 phFdControl) 24 (phHClass (phABI abi 4))) 32 phUVMChannelRangeBase) 40 phUVMChannelRangeExtent) 48 phStatusSentinel)
1221 (phCopyMappedToMapped (naturalAdd phUVMGidP 12) phUVMRegisterChannelP 16
1222 (phCopyStateToMapped (naturalAdd phRoot 8) (naturalAdd phUVMRegisterChannelP 20) 4
1223 (phUVMCall b"uvm-register-channel" 5 (phTolerate mode) phFdUVM phUVMRegisterChannel phUVMRegisterChannelP 48 tail)))))))
1224
1225-- ---- publishing a submission ----
1226-- gpPut into USERD, SFENCE, the work-submit token into the doorbell: the
1227-- training runtime's publication routine (x86: mov [rdi], esi; sfence;
1228-- mov [rdx], ecx), run on this thread, so the doorbell cannot reach the card
1229-- ahead of gpPut through a write-combining buffer. The token is loaded
1230-- from the parameter page into the scratch word first.
1231--
1232-- Measured on an RTX 3090, driver 580.178.04, 2026-09-24. Before, gpPut
1233-- went through the pipe copy and the doorbell after it, unordered: 7 hangs
1234-- in 250 warp-sum runs, and in every one the semaphores were untouched (the
1235-- device never began the pushbuffer), USERD's GP_PUT 1 and GP_GET 0 (the
1236-- channel never fetched the entry) -- the doorbell had arrived before
1237-- gpPut. A membarrier between the two (a locked-instruction barrier, which
1238-- need not drain write-combining buffers) did not help: 11 hangs in 300
1239-- against 6 unfenced. This routine: 0 hangs in 300 against 13 unfenced,
1240-- interleaved on the same card.
1241def phPublishCode : Bytes =
1242 (eliminate X86NativeAssemblyResult (lambda unrestricted current : (family X86NativeAssemblyResult) . Bytes)
1243 nativePhysicalTrainingGeneratePublish32Routine
1244 (branch X86NativeAssemblyEncoded code . code)
1245 (branch X86NativeAssemblyEncodeDuplicateLabel name . b"")
1246 (branch X86NativeAssemblyEncodeOffsetOverflow . b"")
1247 (branch X86NativeAssemblyMissingLabel name . b"")
1248 (branch X86NativeAssemblyDisplacementOutOfRange name . b""))
1249
1250def phLoadToken =
1251 (lambda unrestricted tail : (family NativePhysicalCommands) .
1252 (phCopy phScratch (phZeros 8)
1253 (phCopyMappedToState phTokP phScratch 4 tail)))
1254
1255def phPublishOperand =
1256 (lambda unrestricted userdGPPut : Nat .
1257 (lambda unrestricted gpPut : (family NativePhysicalOperand) .
1258 (lambda unrestricted tail : (family NativePhysicalCommands) .
1259 (phNext (constructor NativePhysicalOperation NativePhysicalMachineRoutine phPublishCode
1260 (phArgs (phImm userdGPPut) gpPut (phImm (naturalAdd phDoorHost 0x90)) (phLoad phScratch) (phImm 0) (phImm 0))
1261 phDiscard)
1262 tail))))
1263
1264def phPublish =
1265 (lambda unrestricted userdGPPut : Nat . (lambda unrestricted gpPut : Nat . (phPublishOperand userdGPPut (phImm gpPut))))
1266
1267-- ---- the doorbell ----
1268def phDoorbell =
1269 (lambda unrestricted abi : (family NvidiaPlanHostABI) .
1270 (lambda unrestricted mode : (family NvidiaPlanHostMode) .
1271 (lambda unrestricted tail : (family NativePhysicalCommands) .
1272 (phCall phSysIoctl (phArgs3 (phImm phFdCard) (phImm phRegisterFD) (phImm phRegFdP)) b"" phDiscard
1273 (phCopy phDoorMap (phSet32 (phSet32 (phSet32 (phSet64 (phSet32 (phSet32 (phZeros 56) 4 phHSubdevice) 8 (phHClass (phABI abi 6))) 24 0x10000) 40 phStatusSentinel) 44 0) 48 phFdCard)
1274 (phCopyStateToState phDoorMap (naturalAdd phRoot 8) 4
1275 (phCall phSysIoctl (phArgs3 (phImm phFdControl) (phImm phRMMapMemory) (phState phDoorMap)) b"" phDiscard
1276 (phCopyStateToState (phRMStatusSlot 18) (naturalAdd phDoorMap 40) 4
1277 (phCheckStateZero32 b"doorbell-map" (phTolerate mode) (naturalAdd phDoorMap 40)
1278 (phCall phSysMmap (phArgs (phImm phDoorHost) (phImm 0x10000) (phImm 3) (phImm phMapSharedFixed) (phImm phFdCard) (phImm 0)) b"" phDiscard tail))))))))))
1279
1280def phToken =
1281 (lambda unrestricted abi : (family NvidiaPlanHostABI) .
1282 (lambda unrestricted mode : (family NvidiaPlanHostMode) .
1283 (lambda unrestricted tail : (family NativePhysicalCommands) .
1284 (phFill phTokP (phZeros 4)
1285 (phControl b"control:phTok" (phTolerate mode) (phRMStatusSlot 15) phTok (phHClass (phABI abi 4)) 0xc36f0108 phTokP 4 tail)))))
1286
1287def phSchedule =
1288 (lambda unrestricted abi : (family NvidiaPlanHostABI) .
1289 (lambda unrestricted mode : (family NvidiaPlanHostMode) .
1290 (lambda unrestricted tail : (family NativePhysicalCommands) .
1291 (phFill phSchedP (phTake (phABI abi 9) (bytes 1 0 0))
1292 (phControl b"control:phSched" (phTolerate mode) (phRMStatusSlot 14) phSched phHGroup 0xa06c0101 phSchedP (phABI abi 9) tail)))))
1293
1294def phVASpaceParams =
1295 (lambda unrestricted uvm : Nat .
1296 (nat-eliminate
1297 (lambda unrestricted current : Nat . Bytes)
1298 (phZeros 48)
1299 (lambda unrestricted predecessor : Nat .
1300 (lambda unrestricted ignored : Bytes . (phSet64 (phSet64 (phSet32 (phZeros 48) 4 0x48) 8 0x1FFFFFB000000) 40 0x1000)))
1301 uvm))
1302
1303def phUVMLifecycle =
1304 (lambda unrestricted mode : (family NvidiaPlanHostMode) .
1305 (lambda unrestricted lifecycle : (family NvidiaPlanHostLifecycle) .
1306 (lambda unrestricted tail : (family NativePhysicalCommands) .
1307 (eliminate NvidiaPlanHostLifecycle
1308 (lambda unrestricted current : (family NvidiaPlanHostLifecycle) . (family NativePhysicalCommands))
1309 lifecycle
1310 (branch NvidiaPlanHostDirectRM . tail)
1311 (branch NvidiaPlanHostUVM base extent . (phUVMPrepare mode base extent tail))))))
1312
1313def phDMASelector =
1314 (lambda unrestricted mode : (family NvidiaPlanHostMode) .
1315 (lambda unrestricted tail : (family NativePhysicalCommands) .
1316 (phFill phDMAObjectP (phSet64 (phZeros 24) 8 0x1FFFFFFFFFFFF)
1317 (phAlloc b"alloc:phDMAObject" (phTolerate mode) phDMAObject phHDevice 0x70 phDMAObjectP 24 phHDMA (phRMStatusSlot 2) tail))))
1318
1319def phDirectActivate =
1320 (lambda unrestricted abi : (family NvidiaPlanHostABI) .
1321 (lambda unrestricted mode : (family NvidiaPlanHostMode) .
1322 (lambda unrestricted tail : (family NativePhysicalCommands) .
1323 (phFill phBindP (phW32 1)
1324 (phControl b"control:phBind" (phTolerate mode) (phRMStatusSlot 13) phBind (phHClass (phABI abi 4)) 0xa06f0104 phBindP 4
1325 (phSchedule abi mode (phToken abi mode (phDoorbell abi mode tail))))))))
1326
1327def phUVMActivate =
1328 (lambda unrestricted abi : (family NvidiaPlanHostABI) .
1329 (lambda unrestricted mode : (family NvidiaPlanHostMode) .
1330 (lambda unrestricted tail : (family NativePhysicalCommands) .
1331 (phDoorbell abi mode
1332 (phFill phPreemptP (phSet32 (phSet32 (phSet32 (phSet32 (phZeros 32) 0 1) 4 phHGroup) 8 0) 12 2)
1333 (phControl b"control:phPreempt" (phTolerate mode) (phRMStatusSlot 16) phPreempt phHSubdevice 0x20801210 phPreemptP 32
1334 (phToken abi mode (phUVMRegisterChannelCommands abi mode (phSchedule abi mode tail)))))))))
1335
1336-- the UVM lifecycle's GPFIFO: 0x8000 entries of 8 bytes in the video GPFIFO
1337-- buffer, USERD the page after them
1338def nvidiaPlanHostUVMGPFIFOEntries : Nat = 0x8000
1339def nvidiaPlanHostUVMGPFIFOBytes : Nat = (naturalMultiply nvidiaPlanHostUVMGPFIFOEntries 8)
1340
1341-- Where a plan maps its buffers in the process: from the origin, each
1342-- after the previous at the alignment, in extents of the mapping unit.
1343-- The host side of the arena certificate decides that they are disjoint
1344-- and clear of the host's own mappings.
1345def nvidiaPlanHostMappingOrigin : Nat = 0x6000_0000
1346def nvidiaPlanHostMappingAlignment : Nat = 0x0200_0000
1347def nvidiaPlanHostMappingUnit : Nat = 0x10000
1348
1349-- the USERD page mapped after the GPFIFO entries, and the words of it the
1350-- host reads: GP_GET and GP_PUT (Accelerator.SM86.USERD's layout, slot 0)
1351def nvidiaPlanHostUSERDBytes : Nat = nvidiaPlanHostPageBytes
1352def nvidiaPlanHostUSERDGPGetOffset : Nat = 0x88
1353def nvidiaPlanHostUSERDGPPutOffset : Nat = 0x8c
1354def nvidiaPlanHostDirectGPFIFOEntries : Nat = 0x400
1355
1356def phChannelParams =
1357 (lambda unrestricted abi : (family NvidiaPlanHostABI) .
1358 (lambda unrestricted direct : Nat .
1359 (lambda unrestricted gpfifoGPU : Nat .
1360 (phSet32 (phSet64 (phSet32 (phSet32 (phSet32 (phSet32 (phSet64 (phSet32 (phSet32 (phZeros 368) 0 phHError) 4 (phHMemory 0)) 8 gpfifoGPU) 16 (naturalSelect direct nvidiaPlanHostDirectGPFIFOEntries nvidiaPlanHostUVMGPFIFOEntries)) 20 (naturalSelect direct (phABI abi 10) 0)) 24 phHContext) 32 (naturalSelect direct (phHMemory 5) (phHMemory 0))) 64 (naturalSelect direct 0 nvidiaPlanHostUVMGPFIFOBytes)) 128 (phABI abi 7)))))
1361
1362-- ---- the driver's branch ----
1363-- NV_ESC_CHECK_VERSION_STR (0xD2, 72 bytes: cmd, reply, 64 version bytes)
1364-- with cmd '2', query: the driver writes its own version string. Its first
1365-- four bytes must be the branch the host's ABI was built for, or the host
1366-- stops, naming `driver-branch`, before any card call -- a 580-ABI host on a
1367-- 575 driver used to run until its DMA map failed (exit 120 at `dma-map`),
1368-- and on a 570 driver it faulted. Measured on the RTX 3090, 2026-09-24:
1369-- driver 580.178.04 answers `580.178.04`, reply 1. A driver that does not
1370-- answer leaves the bytes zero and is refused the same way.
1371def phCheckVersionIoctl : Nat = 0xC04846D2
1372def phVersion : Nat = 1024
1373
1374def phRootAndDriverBranch =
1375 (lambda unrestricted abi : (family NvidiaPlanHostABI) .
1376 (lambda unrestricted offset : Nat .
1377 (lambda unrestricted tail : (family NativePhysicalCommands) .
1378 (phAssertStateZero32 b"root" offset
1379 (phCopy phVersion (phSet32 (phZeros 72) 0 0x32)
1380 (phCall phSysIoctl (phArgs3 (phSlot phSlotControl) (phImm phCheckVersionIoctl) (phState phVersion)) b"" phDiscard
1381 (phCopy phScratch (phZeros 8)
1382 (phCopyStateToState phScratch (naturalAdd phVersion 8) 4
1383 (nativeLaunchRecipeAssertEqual (phLoad phScratch) (phImm (phABI abi 8)) b"driver-branch" tail)))))))))
1384
1385-- ---- the prelude: a working compute channel ----
1386def phPrelude =
1387 (lambda unrestricted mode : (family NvidiaPlanHostMode) .
1388 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
1389 (lambda unrestricted tail : (family NativePhysicalCommands) .
1390 (eliminate NvidiaPlanHostLayout
1391 (lambda unrestricted current : (family NvidiaPlanHostLayout) . (family NativePhysicalCommands))
1392 layout
1393 (branch NvidiaPlanHostLayoutValue gpfifo push sem program qmd userd data abi lifecycle expectedName errorHost .
1394 (let unrestricted uvm = (phIsUVM lifecycle)
1395 in (let unrestricted direct = (naturalIsZero uvm)
1396 in (let unrestricted channelClass = (phHClass (phABI abi 4))
1397 in (let unrestricted tolerate = (phTolerate mode)
1398 in
1399 (phOpenCard b"/dev/nvidia0\x00" (phOpenCard b"/dev/nvidia1\x00" (phOpenCard b"/dev/nvidia2\x00" (phOpenCard b"/dev/nvidia3\x00"
1400 (phOpenCard b"/dev/nvidia4\x00" (phOpenCard b"/dev/nvidia5\x00" (phOpenCard b"/dev/nvidia6\x00" (phOpenCard b"/dev/nvidia7\x00"
1401 (phCall phSysOpenat (phArgs3 (phImm phAtFdCwd) phPayload (phImm phOpenFlags)) b"/dev/nvidiactl\x00" (phStore phSlotControl)
1402 (phCall phSysDup2 (phArgs3 (phSlot phSlotControl) (phImm phFdControl) (phImm 0)) b"" phDiscard
1403 (phCopy phRoot (phSet32 (phZeros 32) 28 phStatusSentinel)
1404 (phCall phSysIoctl (phArgs3 (phSlot phSlotControl) (phImm phRMAlloc) (phState phRoot)) b"" phDiscard
1405 (phCopyStateToState (phRMStatusSlot 0) (naturalAdd phRoot 28) 4
1406 (phRootAndDriverBranch abi (naturalAdd phRoot 28)
1407 (phCall phSysMmap (phArgs (phImm phParams) (phImm 0x10000) (phImm 3) (phImm phMapAnonymousFixed) (phImm phNoDescriptor) (phImm 0)) b"" phDiscard
1408 (phFill phRegFdP (phW32 phFdControl)
1409 (phCopy phDev (phSet32 (phSet32 (phSet32 (phSet32 (phZeros 32) 8 phHDevice) 12 0x80) 16 phDevP) 24 56)
1410 (phCopyStateToState phDev (naturalAdd phRoot 8) 4
1411 (phCopyStateToState (naturalAdd phDev 4) (naturalAdd phRoot 8) 4
1412 (phDeviceProbe 0 (phDeviceProbe 1 (phDeviceProbe 2 (phDeviceProbe 3
1413 (phDeviceProbe 4 (phDeviceProbe 5 (phDeviceProbe 6 (phDeviceProbe 7
1414 (phFill phSubP (phZeros 4)
1415 (phAlloc b"alloc:phSub" tolerate phSub phHDevice 0x2080 phSubP 4 phHSubdevice (phRMStatusSlot 1)
1416 (phWhen (naturalNonzero (bytes-length expectedName)) (phExpectName mode expectedName)
1417 (phWhen uvm (phDMASelector mode)
1418 (phFill phVASP (phVASpaceParams uvm)
1419 (phAlloc b"alloc:phVAS" tolerate phVAS phHDevice 0x90f1 phVASP 48 phHVASpace (phRMStatusSlot 3)
1420 (phUVMLifecycle mode lifecycle
1421 (phBuffer abi mode lifecycle 0 gpfifo (phBuffer abi mode lifecycle 1 push (phBuffer abi mode lifecycle 2 sem (phBuffer abi mode lifecycle 3 program (phBuffer abi mode lifecycle 4 qmd
1422 (phWhen direct (phBuffer abi mode lifecycle 5 userd)
1423 (phDataBuffers abi mode lifecycle 6 data
1424 (phFill phErrP (phMemoryParams 0 0 0 0 0x1000)
1425 (phAlloc b"alloc:phErr" tolerate phErr phHDevice 0x3E phErrP 128 phHError (phRMStatusSlot 4)
1426 (phWhen (naturalNonzero errorHost) (phMapMemory b"error-map" mode phErrMap phHError 0 0x1000 errorHost (phRMStatusSlot 7))
1427 (phFill phGroupP (phSet32 (phSet32 (phZeros 20) 8 (naturalSelect direct phHVASpace 0)) 12 1)
1428 (phAlloc b"alloc:phGroup" tolerate phGroup phHDevice 0xa06c phGroupP 20 phHGroup (phRMStatusSlot 5)
1429 (phFill phCtxP (phSet32 (phSet32 (phZeros 12) 0 phHVASpace) 4 uvm)
1430 (phAlloc b"alloc:phCtx" tolerate phCtx phHGroup 0x9067 phCtxP 12 phHContext (phRMStatusSlot 6)
1431 (phFill phChanP (phChannelParams abi direct (phBufferGPU gpfifo))
1432 (phAlloc b"alloc:phChan" tolerate phChan phHGroup (phABI abi 4) phChanP 368 channelClass (phRMStatusSlot 8)
1433 (phAlloc b"alloc:phComp" tolerate phComp channelClass (phABI abi 5) 0 0 (phHClass (phABI abi 5)) (phRMStatusSlot 9)
1434 (phAlloc b"alloc:phUser" tolerate phUser phHSubdevice (phABI abi 6) 0 0 (phHClass (phABI abi 6)) (phRMStatusSlot 10)
1435 (phWhen direct (phDirectActivate abi mode)
1436 (phWhen uvm (phUVMActivate abi mode)
1437 tail)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
1438
1439-- ---- uploads, submission, completion, readback ----
1440def phFills =
1441 (lambda unrestricted fills : (family NvidiaPlanHostFills) .
1442 (lambda unrestricted tail : (family NativePhysicalCommands) .
1443 (eliminate NvidiaPlanHostFills
1444 (lambda unrestricted current : (family NvidiaPlanHostFills) . (family NativePhysicalCommands))
1445 fills
1446 (branch NvidiaPlanHostFillsEnd . tail)
1447 (branch NvidiaPlanHostFillBytes host payload rest induction . (phFill host payload induction))
1448 (branch NvidiaPlanHostFillFile host path extent rest induction . (phReadFile path host extent induction)))))
1449
1450def phReads =
1451 (lambda unrestricted reads : (family NvidiaPlanHostReads) .
1452 (lambda unrestricted tail : (family NativePhysicalCommands) .
1453 (eliminate NvidiaPlanHostReads
1454 (lambda unrestricted current : (family NvidiaPlanHostReads) . (family NativePhysicalCommands))
1455 reads
1456 (branch NvidiaPlanHostReadsEnd . tail)
1457 (branch NvidiaPlanHostReadsNext host extent rest induction .
1458 (phCall phSysWrite (phArgs3 (phImm 1) (phImm host) (phImm extent)) b"" phDiscard induction)))))
1459
1460def nvidiaPlanHostFenceValue : Nat = 65261
1461def nvidiaPlanHostFenceInterval : Nat = 1000000
1462def nvidiaPlanHostFenceMaximumPolls : Nat = 600000
1463
1464def phUSERDHost =
1465 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
1466 (eliminate NvidiaPlanHostLayout (lambda unrestricted current : (family NvidiaPlanHostLayout) . Nat) layout
1467 (branch NvidiaPlanHostLayoutValue gpfifo push sem program qmd userd data abi lifecycle expectedName errorHost .
1468 (phBufferHost userd))))
1469
1470-- Release everything before exit: freeing the root client tears the whole
1471-- object hierarchy down synchronously. Left to the driver's asynchronous
1472-- reclaim at process exit, back-to-back hosts on the RTX 3090 hit
1473-- NV_ERR_INSUFFICIENT_RESOURCES on the channel allocation about a third of
1474-- the time, in streaks; v3 of this host, which did not free, did too.
1475def phRelease =
1476 (lambda unrestricted tail : (family NativePhysicalCommands) .
1477 (phCopy phFree (phSet32 (phZeros 16) 12 phStatusSentinel)
1478 (phCopyStateToState phFree (naturalAdd phRoot 8) 4
1479 (phCopyStateToState (naturalAdd phFree 4) (naturalAdd phRoot 8) 4
1480 (phCopyStateToState (naturalAdd phFree 8) (naturalAdd phRoot 8) 4
1481 (phCall phSysIoctl (phArgs3 (phImm phFdControl) (phImm phRMFree) (phState phFree)) b"" phDiscard
1482 (phCopyStateToState (phRMStatusSlot 17) (naturalAdd phFree 12) 4
1483 (phAssertStateZero32 b"rm-free-root" (naturalAdd phFree 12) tail))))))))
1484
1485-- The whole host, Strict: `submissions` is gpPut, the number of GPFIFO
1486-- entries the plan's tables carry; `fenceHost` the host address of the
1487-- semaphore slot the last submission releases; `statusHost`, when not 0, a
1488-- mapped address the UVM status record is copied to before the readbacks.
1489-- ---- native telemetry (docs/observability PRD item 9) ----
1490-- At each phase boundary the host appends an ALPHATEL record to
1491-- `alpha-host.alphatel` in its working directory: the body is
1492-- Runtime.NativeTelemetry's own encoding, made at build time (domain 1,
1493-- event 1 "reached", the boundary's ordinal as phase and sequence, status
1494-- 0, its name as payload), with the monotonic nanoseconds left zero; at
1495-- run time the host reads CLOCK_MONOTONIC and Runtime.NativeTelemetrySeal
1496-- writes the reading into the body, digests it and writes the record. A
1497-- record exists only if the host got there, so the last one names how far
1498-- a failed run came. The write is asserted whole (`telemetry-write`): a
1499-- host that cannot record says so and stops, rather than running unobserved.
1500-- Its pages: a fixed anonymous mapping of its own, taken before any device
1501-- call, so a host with no card still records its beginning.
1502def phTelemetryPage : Nat = 0x5E000000
1503def phTelemetryPadded : Nat = 0x5E000000
1504def phTelemetryRecord : Nat = 0x5E000400
1505def phTelemetryClock : Nat = 0x5E000800
1506def phTelemetryWork : Nat = 0x5E000C00
1507def phSlotTelemetry : Nat = 14
1508def phSlotTelemetryWritten : Nat = 15
1509def phTelemetryPath : Bytes = b"alpha-host.alphatel\x00"
1510def phSysClockGettime : Nat = 228
1511def phClockMonotonic : Nat = 1
1512-- O_WRONLY | O_CREAT | O_APPEND, mode 0600
1513def phTelemetryOpenFlags : Nat = 1089
1514def phTelemetryMode : Nat = 384
1515
1516def phTelemetryIdentity : Bytes = (bytes-append phIdentity (phZeros (naturalSaturatingSubtract nativeTelemetryDigestBytes (bytes-length phIdentity))))
1517def phTelemetryZero : (family ModelWord64) = (phWord 0)
1518
1519-- the body Runtime.NativeTelemetry encodes for boundary `ordinal`, its
1520-- clock reading zero: no error code, the name as payload
1521def phTelemetryBody =
1522 (lambda unrestricted ordinal : Nat . (lambda unrestricted name : Bytes .
1523 (nativeTelemetryRecordBody (phWord ordinal) phTelemetryZero (byte 1) (byte 1) (nat-to-byte ordinal) (byte 0)
1524 (constructor NativeTelemetryCounters NativeTelemetryCountersValue
1525 phTelemetryZero phTelemetryZero phTelemetryZero phTelemetryZero phTelemetryZero phTelemetryZero phTelemetryZero phTelemetryZero)
1526 phTelemetryIdentity b"" name phTelemetryZero (phWord (bytes-length name)))))
1527
1528-- the body with SHA-256's padding: 0x80, zeros to 56 mod 64, the bit length
1529-- (big-endian; a body is far below 8 KiB)
1530def phTelemetryPadding =
1531 (lambda unrestricted length : Nat .
1532 (bytes-cons (byte 128)
1533 (bytes-append (phZeros (naturalModuloUnchecked (naturalSaturatingSubtract (naturalAdd 55 512) length) 64))
1534 (bytes-append (phZeros 6)
1535 (bytes-cons (nat-to-byte (naturalDivideUnchecked (naturalMultiply 8 length) 256))
1536 (bytes-cons (nat-to-byte (naturalModuloUnchecked (naturalMultiply 8 length) 256)) b""))))))
1537
1538-- map the telemetry page and put the magic in the record buffer
1539def phTelemetryOpen =
1540 (lambda unrestricted tail : (family NativePhysicalCommands) .
1541 (phCall phSysMmap (phArgs (phImm phTelemetryPage) (phImm 0x1000) (phImm 3) (phImm phMapAnonymousFixed) (phImm phNoDescriptor) (phImm 0)) b"" phDiscard
1542 (phFill phTelemetryRecord b"ALPHATEL" tail)))
1543
1544-- boundary `ordinal`, named: seal and append its record
1545def phTelemetry =
1546 (lambda unrestricted ordinal : Nat . (lambda unrestricted name : Bytes . (lambda unrestricted tail : (family NativePhysicalCommands) .
1547 (let unrestricted body = (phTelemetryBody ordinal name)
1548 in (let unrestricted length = (bytes-length body)
1549 in (let unrestricted padded = (bytes-append body (phTelemetryPadding length))
1550 in (phFill phTelemetryPadded padded
1551 (phCall phSysClockGettime (phArgs3 (phImm phClockMonotonic) (phImm phTelemetryClock) (phImm 0)) b"" phDiscard
1552 (phNext (constructor NativePhysicalOperation NativePhysicalMachineRoutine nativeTelemetrySealRoutine
1553 (phArgs (phImm phTelemetryPadded) (phImm (naturalDivideUnchecked (bytes-length padded) 64)) (phImm phTelemetryRecord)
1554 (phImm length) (phImm phTelemetryClock) (phImm phTelemetryWork))
1555 phDiscard)
1556 (phCall phSysOpenat (phArgs (phImm phAtFdCwd) phPayload (phImm phTelemetryOpenFlags) (phImm phTelemetryMode) (phImm 0) (phImm 0)) phTelemetryPath (phStore phSlotTelemetry)
1557 (phCall phSysWrite (phArgs3 (phSlot phSlotTelemetry) (phImm phTelemetryRecord) (phImm (naturalAdd 72 length))) b"" (phStore phSlotTelemetryWritten)
1558 (nativeLaunchRecipeAssertEqual (phSlot phSlotTelemetryWritten) (phImm (naturalAdd 72 length)) b"telemetry-write"
1559 (phCall phSysClose (phArgs3 (phSlot phSlotTelemetry) (phImm 0) (phImm 0)) b"" phDiscard tail)))))))))))))
1560
1561-- Preparation has two ordered phases: envelope validation before any card
1562-- call, and expansion after the buffers exist. Keeping these continuations
1563-- here gives recipe-backed probes the same telemetry and submit/wait path
1564-- as the ordinary host, without copying its RM command stream.
1565def nvidiaPlanHostPreparedCommands =
1566 (lambda unrestricted before : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
1567 (lambda unrestricted mapped : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
1568 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
1569 (lambda unrestricted fills : (family NvidiaPlanHostFills) .
1570 (lambda unrestricted submissions : Nat .
1571 (lambda unrestricted fenceHost : Nat .
1572 (lambda unrestricted statusHost : Nat .
1573 (lambda unrestricted reads : (family NvidiaPlanHostReads) .
1574 (phPipeCreate
1575 (phTelemetryOpen (phTelemetry 0 b"plan-host:begin"
1576 (before (phPrelude (constructor NvidiaPlanHostMode NvidiaPlanHostStrict) layout
1577 (phTelemetry 1 b"plan-host:channel-ready"
1578 (mapped (phFills fills
1579 (phTelemetry 2 b"plan-host:uploaded"
1580 (phLoadToken
1581 (phPublish (naturalAdd (phUSERDHost layout) nvidiaPlanHostUSERDGPPutOffset) submissions
1582 (phTelemetry 3 b"plan-host:submitted"
1583 (phNext (constructor NativePhysicalOperation NativePhysicalFenceWait (phImm fenceHost) (phImm nvidiaPlanHostFenceValue) (phWord nvidiaPlanHostFenceMaximumPolls) (phWord nvidiaPlanHostFenceInterval))
1584 (phTelemetry 4 b"plan-host:completed"
1585 (phWhen (naturalNonzero statusHost) (phCopyStateToMapped phUVMStatusRecord statusHost phUVMStatusRecordExtent)
1586 (phReads reads
1587 (phTelemetry 5 b"plan-host:read-back"
1588 (phCall phSysExitGroup (phArgs3 (phImm 0) (phImm 0) (phImm 0)) b"" phDiscard
1589 (phNext (constructor NativePhysicalOperation NativePhysicalHaltSuccess)
1590 (constructor NativePhysicalCommands NativePhysicalCommandsEnd))))))))))))))))))))))))))))
1591
1592def phNoPreparation =
1593 (lambda unrestricted tail : (family NativePhysicalCommands) . tail)
1594
1595def nvidiaPlanHostCommands =
1596 (nvidiaPlanHostPreparedCommands phNoPreparation phNoPreparation)
1597
1598-- The channel probe, Probe mode: the prelude alone, every status after the
1599-- root client's recorded and none asserted, then to stdout the status area
1600-- -- the 16-byte record per buffer, the UVM slots, the RM slots -- from the
1601-- state and the channel allocation's parameter block as the driver left it
1602-- (its `cid` word at 132 is the hardware channel identifier), then the root
1603-- freed. With a card it prints both and exits 0 whether or not the channel
1604-- came up; which call refused is read off the area.
1605def phProbeRecord : Nat = (phBufferStatus 0)
1606def phProbeRecordExtent : Nat = (naturalSaturatingSubtract (phBufferState 0) (phBufferStatus 0))
1607def phChannelParamsExtent : Nat = 368
1608
1609def nvidiaPlanHostProbeCommands =
1610 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
1611 (phPipeCreate
1612 (phPrelude (constructor NvidiaPlanHostMode NvidiaPlanHostProbe) layout
1613 (phCall phSysWrite (phArgs3 (phImm 1) (phState phProbeRecord) (phImm phProbeRecordExtent)) b"" phDiscard
1614 (phCall phSysWrite (phArgs3 (phImm 1) (phImm phChanP) (phImm phChannelParamsExtent)) b"" phDiscard
1615 (phRelease
1616 (phCall phSysExitGroup (phArgs3 (phImm 0) (phImm 0) (phImm 0)) b"" phDiscard
1617 (phNext (constructor NativePhysicalOperation NativePhysicalHaltSuccess)
1618 (constructor NativePhysicalCommands NativePhysicalCommandsEnd)))))))))
1619
1620def phCommandCount =
1621 (lambda unrestricted commands : (family NativePhysicalCommands) .
1622 (eliminate NativePhysicalCommands
1623 (lambda unrestricted current : (family NativePhysicalCommands) . Nat)
1624 commands
1625 (branch NativePhysicalCommandsEnd . zero)
1626 (branch NativePhysicalCommandsNext head tail induction . (succ induction))))
1627
1628-- The number of assertions a command list carries: what a mode decides.
1629def phOperationIsAssert =
1630 (lambda unrestricted operation : (family NativePhysicalOperation) .
1631 (eliminate NativePhysicalOperation
1632 (lambda unrestricted current : (family NativePhysicalOperation) . Nat)
1633 operation
1634 (branch NativePhysicalSystemCall number argv payload result . 0)
1635 (branch NativePhysicalCopyPayloadToState destination extent payload . 0)
1636 (branch NativePhysicalMachineRoutine code argv result . 0)
1637 (branch NativePhysicalFencePoll address expected polls . 0)
1638 (branch NativePhysicalTelemetryAppend path record . 0)
1639 (branch NativePhysicalAssertEqual left right error . 1)
1640 (branch NativePhysicalAssertOneOf observed first second error . 1)
1641 (branch NativePhysicalHaltSuccess . 0)
1642 (branch NativePhysicalRepeatBegin count . 0)
1643 (branch NativePhysicalRepeatEnd . 0)
1644 (branch NativePhysicalStoreWord64 destination value . 0)
1645 (branch NativePhysicalFenceWait address expected polls interval . 0)
1646 (branch NativePhysicalRepeatBeginCounted count . 0)
1647 (branch NativePhysicalAddWord64 destination left right . 0)
1648 (branch NativePhysicalFloat64 operation destination left right . 0)))
1649
1650def phCommandIsAssert =
1651 (lambda unrestricted command : (family NativePhysicalCommand) .
1652 (eliminate NativePhysicalCommand
1653 (lambda unrestricted current : (family NativePhysicalCommand) . Nat)
1654 command
1655 (branch NativePhysicalCommandValue operation identity . (phOperationIsAssert operation))))
1656
1657def nvidiaPlanHostAssertionCount =
1658 (lambda unrestricted commands : (family NativePhysicalCommands) .
1659 (eliminate NativePhysicalCommands
1660 (lambda unrestricted current : (family NativePhysicalCommands) . Nat)
1661 commands
1662 (branch NativePhysicalCommandsEnd . zero)
1663 (branch NativePhysicalCommandsNext head tail induction . (naturalAdd (phCommandIsAssert head) induction))))
1664
1665-- the prelude alone under a mode, for the assertion contracts
1666def nvidiaPlanHostPreludeCommands =
1667 (lambda unrestricted mode : (family NvidiaPlanHostMode) .
1668 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
1669 (phPrelude mode layout (constructor NativePhysicalCommands NativePhysicalCommandsEnd))))
1670
1671def nvidiaPlanHostProgram =
1672 (lambda unrestricted identity : Bytes .
1673 (lambda unrestricted commands : (family NativePhysicalCommands) .
1674 (constructor NativePhysicalProgram NativePhysicalProgramValue (phWord phStateExtent) (phWord phSlots) commands (phCommandCount commands) identity zero)))
1675
1676def nvidiaPlanHostELF =
1677 (lambda unrestricted identity : Bytes .
1678 (lambda unrestricted commands : (family NativePhysicalCommands) .
1679 (nativePhysicalGenerateNativeELFBytesDirect (nvidiaPlanHostProgram identity commands))))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.