1module Platform.Linux.Nvidia.ProgramPlan
2
3import Accelerator.SM86.Instruction
4import Accelerator.SM86.InstructionEncoding
5import Accelerator.SM86.Types
6import Compiler.Planning.VA
7import Hardware.Nvidia.SM86.Command.WholeProgramPlan
8import Model.Config
9import Model.Parameter
10import Model.Word64
11import Platform.Linux.Nvidia.PlanHost
12import Platform.Linux.Nvidia.DeviceBinding
13import Platform.Linux.Nvidia.PlanHostRequest
14import Platform.Linux.Nvidia.ResourcePlan
15import Runtime.NativePhysicalMemory
16import Runtime.NativeResourcePlan
17import Execution.ResourceGraph
18import Std.Foundation
19import Std.List
20import Runtime.ArenaCertificate
21import Runtime.NativePhysicalEmbeddedArtifact
22import Runtime.NativePhysicalProgram
23import Runtime.NativeFloatPlan
24import Runtime.NativeFilePlan
25import Data.Bytes
26import Runtime.NativeLaunchRecipeLoad
27import Runtime.NativePhysicalProgramComposer
28import Std.Natural
29
30-- One shared native session plan for target-owned programs. Model-specific
31-- parameter/data layouts supply typed regions and launch declarations; this
32-- owner derives backing, placement, tables, recipes and admission. The data
33-- backing is explicit, so persistent learner state can use video memory.
34-- Current code-region admission is SM86. A new architecture must provide its
35-- own established extent/placement semantics, not reuse a guessed capacity.
36family NvidiaProgramPlan : Type 0
37constructor NvidiaProgramPlanValue
38field unrestricted nvidiaProgramLayout : (family NvidiaPlanHostLayout)
39field unrestricted nvidiaProgramComponents : (pi unrestricted component : (family NvidiaWholeProgramComponent) . Bytes)
40field unrestricted nvidiaProgramRecipes : (family NvidiaPlanHostRecipeFills)
41field unrestricted nvidiaProgramDataHost : Nat
42field unrestricted nvidiaProgramDataGPU : Nat
43field unrestricted nvidiaProgramDataBytes : Nat
44field unrestricted nvidiaProgramAdmitted : Nat
45
46end-family
47
48-- Append a relocated device fragment only after successful admission. Result
49-- slots are private to the device session; state addresses already come from
50-- the caller's combined layout. A failed relocation produces no executable.
51def nlsWithPrivateSlots =
52 (lambda unrestricted slotsBefore : Nat .
53 (lambda unrestricted commands : (family NativePhysicalCommands) .
54 (lambda unrestricted emit : (pi unrestricted relocated : (family NativePhysicalCommands) . Bytes) .
55 (eliminate
56 NativePhysicalProgramComposeCommandsResult
57 (lambda unrestricted r : (family NativePhysicalProgramComposeCommandsResult) . Bytes)
58 (nativePhysicalProgramComposeRelocateCommands
59 commands
60 (phWord 0)
61 (phWord slotsBefore)
62 (phWord 0))
63 (branch
64 NativePhysicalProgramComposeCommandsRelocated
65 relocated
66 count
67 operations
68 operands
69 checks
70 .
71 (emit relocated))
72 (branch
73 NativePhysicalProgramComposeCommandsRejected
74 error
75 count
76 operations
77 operands
78 checks
79 .
80 b"")))))
81
82def nlsExtent =
83 (lambda unrestricted bytes : Nat . (nvidiaPlanHostRoundUp bytes nvidiaPlanHostMappingUnit))
84
85def nlsAfter =
86 (lambda unrestricted base : Nat .
87 (lambda unrestricted bytes : Nat . (vaPlaceAfter base bytes nvidiaPlanHostMappingAlignment)))
88
89def nlsBuffer =
90 (lambda unrestricted name : Bytes .
91 (lambda unrestricted gpu : Nat .
92 (lambda unrestricted host : Nat .
93 (lambda unrestricted bytes : Nat .
94 (lambda unrestricted memory : (family NvidiaPlanHostMemory) .
95 (constructor
96 NvidiaPlanHostBuffer
97 NvidiaPlanHostBufferValue
98 name
99 gpu
100 host
101 (nlsExtent bytes)
102 memory))))))
103
104def nlsRecipe =
105 (lambda unrestricted host : Nat .
106 (lambda unrestricted extent : Nat .
107 (lambda unrestricted kind : (family NativePhysicalEmbeddedComponentKind) .
108 (lambda unrestricted tail : (family NvidiaPlanHostRecipeFills) .
109 (constructor
110 NvidiaPlanHostRecipeFills
111 NvidiaPlanHostRecipeFillsNext
112 host
113 extent
114 kind
115 tail)))))
116
117def nlsHostExtras =
118 (phResident
119 b"recipe-staging"
120 nvidiaPlanHostStaging
121 nvidiaPlanHostStagingExtent
122 (constructor ArenaResidents ArenaResidentsEnd))
123
124-- This anonymous mapping is created by nlsSessionPrelude below. Its timestamp
125-- and recipe views share one allocation; account for it once alongside the
126-- target session and the actual interpreter program before emitting bytes.
127def nlsResourceContext =
128 (lambda unrestricted context : (family NvidiaResourceContext) .
129 (stdResultBind
130 (family NativePhysicalMemoryFailure)
131 (family ResourceLease)
132 (family NvidiaResourceContext)
133 (nvidiaResourceHostLease context b"/control/recipe-staging" nvidiaPlanHostStagingExtent)
134 (lambda unrestricted lease : (family ResourceLease) .
135 (constructor
136 StdResult
137 StdSuccess
138 (family NativePhysicalMemoryFailure)
139 (family NvidiaResourceContext)
140 (nvidiaResourceWithNative
141 context
142 (nativeResourceContextAddLeases
143 (nvidiaResourceNative context)
144 (constructor
145 StdList
146 StdListCons
147 (family ResourceLease)
148 lease
149 (constructor StdList StdListEmpty (family ResourceLease)))))))))
150
151def nlsGenerateResourceELF =
152 (lambda unrestricted context : (family NvidiaResourceContext) .
153 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
154 (lambda unrestricted program : (family NativePhysicalProgram) .
155 (eliminate
156 StdResult
157 (lambda unrestricted result : (family StdResult (family NativePhysicalMemoryFailure) (family NvidiaResourceContext)) .
158 Bytes)
159 (nlsResourceContext context)
160 (branch StdFailure reason . b"")
161 (branch
162 StdSuccess
163 withStaging
164 .
165 (nvidiaPlanHostGenerateResourceELF withStaging layout program))))))
166
167-- Session setup owns the native driver, executable verification and recipe
168-- expansion. Identities belong to the compiled composition; the device path
169-- never learns the caller's model, learner, endpoint or checkpoint layout.
170def nlsSessionPrelude =
171 (lambda unrestricted identity : (pi unrestricted kind : (family NativePhysicalEmbeddedComponentKind) . Bytes) .
172 (lambda unrestricted label : Bytes .
173 (lambda unrestricted device : (family NvidiaDeviceBinding) .
174 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
175 (lambda unrestricted recipes : (family NvidiaPlanHostRecipeFills) .
176 (lambda unrestricted program : Bytes .
177 (lambda unrestricted qmd : Bytes .
178 (lambda unrestricted push : Bytes .
179 (lambda unrestricted ring : Bytes .
180 (lambda unrestricted tail : (family NativePhysicalCommands) .
181 (prFenceRegister
182 (phPipeCreate
183 (phTelemetryOpen
184 (phTelemetry
185 1
186 (bytes-append label b":begin")
187 (prEnvelope
188 (identity
189 (constructor
190 NativePhysicalEmbeddedComponentKind
191 NativePhysicalEmbeddedHostELF))
192 (identity
193 (constructor
194 NativePhysicalEmbeddedComponentKind
195 NativePhysicalEmbeddedProgramTable))
196 (identity
197 (constructor
198 NativePhysicalEmbeddedComponentKind
199 NativePhysicalEmbeddedQMDTable))
200 (identity
201 (constructor
202 NativePhysicalEmbeddedComponentKind
203 NativePhysicalEmbeddedPushbuffer))
204 (identity
205 (constructor
206 NativePhysicalEmbeddedComponentKind
207 NativePhysicalEmbeddedGPFIFO))
208 (bytes-length program)
209 (bytes-length qmd)
210 (bytes-length push)
211 (bytes-length ring)
212 (phPreludeOn
213 device
214 (constructor NvidiaPlanHostMode NvidiaPlanHostStrict)
215 layout
216 (nativeLaunchRecipeStagingCommands
217 nvidiaPlanHostStaging
218 nvidiaPlanHostStagingExtent
219 prSlotStatus
220 phIdentity
221 (prRecipeFills
222 recipes
223 (phTelemetry 2 (bytes-append label b":channel-ready") tail)))))))))))))))))))
224
225-- The compiler's typed envelope builder places and seals the five reachable
226-- components. Neither the caller nor this plan joins executable bytes itself.
227-- The schedule owns each ring entry and its semaphore ordinal. The caller
228-- selects an admitted ordinal and owns one initialized fresh-channel counter;
229-- prReissueCounted serializes retirement before any successor touches memory.
230def nvidiaProgramIssue =
231 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
232 (lambda unrestricted component : (pi unrestricted kind : (family NvidiaWholeProgramComponent) . Bytes) .
233 (lambda unrestricted counter : Nat .
234 (lambda unrestricted ordinal : Nat .
235 (prReissueCounted
236 layout
237 counter
238 ordinal
239 (nvidiaPlanHostTableWord
240 (component (constructor NvidiaWholeProgramComponent NvidiaWholeProgramGPFIFO))
241 ordinal))))))
242
243def nlsEmbedHost =
244 (lambda unrestricted identity : (pi unrestricted kind : (family NativePhysicalEmbeddedComponentKind) . Bytes) .
245 (lambda unrestricted host : Bytes .
246 (lambda unrestricted program : Bytes .
247 (lambda unrestricted qmd : Bytes .
248 (lambda unrestricted push : Bytes .
249 (lambda unrestricted ring : Bytes .
250 (nativePhysicalEmbeddedBuildResultBytes
251 (nativePhysicalEmbeddedBuild
252 (nativePhysicalEmbeddedPayloadInMemory
253 (identity
254 (constructor
255 NativePhysicalEmbeddedComponentKind
256 NativePhysicalEmbeddedHostELF))
257 host)
258 (nativePhysicalEmbeddedPayloadInMemory
259 (identity
260 (constructor
261 NativePhysicalEmbeddedComponentKind
262 NativePhysicalEmbeddedProgramTable))
263 program)
264 (nativePhysicalEmbeddedPayloadInMemory
265 (identity
266 (constructor
267 NativePhysicalEmbeddedComponentKind
268 NativePhysicalEmbeddedQMDTable))
269 qmd)
270 (nativePhysicalEmbeddedPayloadInMemory
271 (identity
272 (constructor
273 NativePhysicalEmbeddedComponentKind
274 NativePhysicalEmbeddedPushbuffer))
275 push)
276 (nativePhysicalEmbeddedPayloadInMemory
277 (identity
278 (constructor NativePhysicalEmbeddedComponentKind NativePhysicalEmbeddedGPFIFO))
279 ring)))))))))
280
281-- Placement is derived before the launch parameters are specialized. Program
282-- capacity, QMDs, semaphores and pushbuffer size come from that same schedule.
283-- The initial ring recipe must fit the channel's admitted entry count. A
284-- runtime may reissue an entry after retirement; a larger static schedule
285-- instead needs a different channel plan, not an oversized startup recipe.
286def nvidiaProgramSubmissionsAdmitted =
287 (lambda unrestricted submissions : (family NvidiaSubmissionSchedule) .
288 (let unrestricted count =
289 (nvidiaSubmissionScheduleCount submissions)
290 in
291 (naturalAnd
292 (naturalNonzero count)
293 (naturalLessOrEqual count nvidiaPlanHostDirectGPFIFOEntries))))
294
295def nvidiaProgramPlan =
296 (lambda unrestricted regions : (family NvidiaDeviceRegions) .
297 (lambda unrestricted launchesAt : (pi unrestricted programGPU : Nat . (pi unrestricted dataGPU : Nat . (family NvidiaLaunchSchedule))) .
298 (lambda unrestricted submissions : (family NvidiaSubmissionSchedule) .
299 (lambda unrestricted dataBytes : Nat .
300 (lambda unrestricted dataMemory : (family NvidiaPlanHostMemory) .
301 (lambda unrestricted architecture : (family ModelWord32) .
302 (lambda unrestricted computeClass : (family ModelWord32) .
303 (lambda unrestricted spaVersion : (family ModelWord32) .
304 (lambda unrestricted qmdSlotBytes : Nat .
305 (lambda unrestricted product : Bytes .
306 (lambda unrestricted abi : (family NvidiaPlanHostABI) .
307 (lambda unrestricted availableVideo : Nat .
308 (let unrestricted dataGPU =
309 (nlsAfter phUVMChannelRangeBase phUVMChannelRangeExtent)
310 in
311 (let unrestricted dataHost =
312 (nlsAfter phDoorHost nvidiaPlanHostMappingUnit)
313 in
314 (let unrestricted programGPU =
315 (nlsAfter dataGPU (nlsExtent dataBytes))
316 in
317 (let unrestricted programHost =
318 (nlsAfter dataHost (nlsExtent dataBytes))
319 in
320 (let unrestricted launches =
321 (launchesAt programGPU dataGPU)
322 in
323 (let unrestricted launchCount =
324 (nvidiaLaunchScheduleCount launches)
325 in
326 (let unrestricted submissionCount =
327 (nvidiaSubmissionScheduleCount submissions)
328 in
329 (let unrestricted referenceCount =
330 (nvidiaSubmissionScheduleReferenceCount submissions)
331 in
332 (let unrestricted programBytes =
333 (nvidiaSM86ProgramCapacity regions launches)
334 in
335 (let unrestricted qmdBytes =
336 (naturalMultiply qmdSlotBytes launchCount)
337 in
338 (let unrestricted pushBytes =
339 (nvidiaSubmissionScheduleEncodedBytes submissions)
340 in
341 (let unrestricted semBytes =
342 (nvidiaSubmissionSemaphoreExtent
343 submissions
344 prSemaphoreStride
345 launchCount)
346 in
347 (let unrestricted ringBytes =
348 (naturalMultiply nvidiaPlanHostDirectGPFIFOEntries 8)
349 in
350 (let unrestricted qmdGPU =
351 (nlsAfter programGPU (nlsExtent programBytes))
352 in
353 (let unrestricted qmdHost =
354 (nlsAfter programHost (nlsExtent programBytes))
355 in
356 (let unrestricted pushGPU =
357 (nlsAfter qmdGPU (nlsExtent qmdBytes))
358 in
359 (let unrestricted pushHost =
360 (nlsAfter qmdHost (nlsExtent qmdBytes))
361 in
362 (let unrestricted semGPU =
363 (nlsAfter pushGPU (nlsExtent pushBytes))
364 in
365 (let unrestricted semHost =
366 (nlsAfter pushHost (nlsExtent pushBytes))
367 in
368 (let unrestricted ringGPU =
369 (nlsAfter semGPU (nlsExtent semBytes))
370 in
371 (let unrestricted ringHost =
372 (nlsAfter semHost (nlsExtent semBytes))
373 in
374 (let unrestricted userdHost =
375 (nlsAfter ringHost (nlsExtent ringBytes))
376 in
377 (let unrestricted userdGPU =
378 (nlsAfter ringGPU (nlsExtent ringBytes))
379 in
380 (let unrestricted errorHost =
381 (nlsAfter userdHost nvidiaPlanHostUSERDBytes)
382 in
383 (let unrestricted system =
384 (constructor
385 NvidiaPlanHostMemory
386 NvidiaPlanHostSystemMemory)
387 in
388 (let unrestricted video =
389 (constructor NvidiaPlanHostMemory NvidiaPlanHostVideoMemory)
390 in
391 (let unrestricted layout =
392 (constructor
393 NvidiaPlanHostLayout
394 NvidiaPlanHostLayoutValue
395 (nlsBuffer b"gpfifo" ringGPU ringHost ringBytes system)
396 (nlsBuffer b"push" pushGPU pushHost pushBytes system)
397 (nlsBuffer b"semaphores" semGPU semHost semBytes system)
398 (nlsBuffer
399 b"program"
400 programGPU
401 programHost
402 programBytes
403 system)
404 (nlsBuffer b"qmd" qmdGPU qmdHost qmdBytes system)
405 (constructor
406 NvidiaPlanHostBuffer
407 NvidiaPlanHostBufferValue
408 b"userd"
409 userdGPU
410 userdHost
411 nvidiaPlanHostUSERDBytes
412 video)
413 (constructor
414 NvidiaPlanHostBuffers
415 NvidiaPlanHostBuffersNext
416 (nlsBuffer b"data" dataGPU dataHost dataBytes dataMemory)
417 (constructor NvidiaPlanHostBuffers NvidiaPlanHostBuffersEnd))
418 abi
419 (constructor NvidiaPlanHostLifecycle NvidiaPlanHostDirectRM nvidiaPlanHostDirectGPFIFOEntries)
420 product
421 errorHost)
422 in
423 (let unrestricted component =
424 (lambda unrestricted selected : (family NvidiaWholeProgramComponent) .
425 (compiler-native-encode
426 (family NvidiaWholeProgramPlan)
427 (constructor
428 NvidiaWholeProgramPlan
429 NvidiaWholeProgramPlanValue
430 selected
431 architecture
432 computeClass
433 spaVersion
434 (phWord programGPU)
435 (phWord qmdGPU)
436 (phWord pushGPU)
437 (phWord semGPU)
438 nvidiaCodeRegionAlignment
439 programBytes
440 regions
441 launches
442 launchCount
443 qmdBytes
444 submissions
445 submissionCount
446 referenceCount)))
447 in
448 (let unrestricted recipes =
449 (nlsRecipe
450 programHost
451 programBytes
452 (constructor
453 NativePhysicalEmbeddedComponentKind
454 NativePhysicalEmbeddedProgramTable)
455 (nlsRecipe
456 qmdHost
457 qmdBytes
458 (constructor
459 NativePhysicalEmbeddedComponentKind
460 NativePhysicalEmbeddedQMDTable)
461 (nlsRecipe
462 pushHost
463 pushBytes
464 (constructor
465 NativePhysicalEmbeddedComponentKind
466 NativePhysicalEmbeddedPushbuffer)
467 (nlsRecipe
468 ringHost
469 -- The allocation holds the cyclic ring; the recipe
470 -- contains only this schedule's initial entries.
471 -- The loader requires its exact expanded extent.
472 (naturalMultiply submissionCount 8)
473 (constructor
474 NativePhysicalEmbeddedComponentKind
475 NativePhysicalEmbeddedGPFIFO)
476 (constructor
477 NvidiaPlanHostRecipeFills
478 NvidiaPlanHostRecipeFillsEnd)))))
479 in
480 (let unrestricted admitted =
481 (naturalAnd
482 (nvidiaSM86RegionsAdmitted regions)
483 (naturalAnd
484 (naturalNonzero launchCount)
485 (naturalAnd
486 (nvidiaProgramSubmissionsAdmitted submissions)
487 (naturalAnd
488 (nvidiaPlanHostLayoutAdmitted layout)
489 (naturalAnd
490 (nvidiaPlanHostLayoutCertified layout nlsHostExtras)
491 (naturalAnd
492 (prRecipesAdmitted layout recipes)
493 (naturalAnd
494 (naturalLessOrEqual
495 (nvidiaPlanHostVideoAllocationBytes layout)
496 availableVideo)
497 (naturalAnd
498 (naturalLessOrEqual
499 (bytes-length
500 (component
501 (constructor
502 NvidiaWholeProgramComponent
503 NvidiaWholeProgramProgram)))
504 programBytes)
505 (naturalAnd
506 (naturalEqual
507 (bytes-length
508 (component
509 (constructor
510 NvidiaWholeProgramComponent
511 NvidiaWholeProgramQMD)))
512 qmdBytes)
513 (naturalEqual
514 (bytes-length
515 (component
516 (constructor
517 NvidiaWholeProgramComponent
518 NvidiaWholeProgramPushbuffer)))
519 pushBytes))))))))))
520 in
521 (constructor
522 NvidiaProgramPlan
523 NvidiaProgramPlanValue
524 layout
525 component
526 recipes
527 dataHost
528 dataGPU
529 dataBytes
530 admitted)))))))))))))))))))))))))))))))))))))))))))
531
532-- Select every compiler-derived recipe once before embedding its closure.
533def nlsWithProgramRecipes =
534 (lambda unrestricted component : (pi unrestricted selected : (family NvidiaWholeProgramComponent) . Bytes) .
535 (lambda unrestricted emit : (pi unrestricted program : Bytes . (pi unrestricted qmd : Bytes . (pi unrestricted push : Bytes . (pi unrestricted ring : Bytes . Bytes)))) .
536 (emit
537 (component (constructor NvidiaWholeProgramComponent NvidiaWholeProgramProgramRecipe))
538 (component (constructor NvidiaWholeProgramComponent NvidiaWholeProgramQMDRecipe))
539 (component (constructor NvidiaWholeProgramComponent NvidiaWholeProgramPushbufferRecipe))
540 (component (constructor NvidiaWholeProgramComponent NvidiaWholeProgramGPFIFORecipe)))))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.