1module PartitionedRegression.Build.NativeHost
2
3import PartitionedRegression.NativeHost
4import PartitionedRegression.Build.ScalarEvaluation
5import Checkpoint.Envelope
6import Checkpoint.NativeEnvelope
7import Compiler.Planning.RegionFrame
8import Data.Bytes
9import Hardware.Nvidia.SM86.Command.WholeProgramPlan
10import Model.Word64
11import Platform.Linux.Nvidia.DeviceBinding
12import Platform.Linux.Nvidia.LinearStep
13import Platform.Linux.Nvidia.ProgramPlan
14import Platform.Linux.Nvidia.PlanHost
15import Platform.Linux.Nvidia.PlanHostRequest
16import Platform.RunPod.Nvidia.SM86
17import Realization.Nvidia.SM86.LinearStepSM86
18import Runtime.NativeFilePlan
19import Runtime.NativeLaunchRecipeLoad
20import Runtime.NativePhysicalEmbeddedArtifact
21import Runtime.NativePhysicalNativeELF
22import Runtime.NativePhysicalProgram
23import Runtime.NativePhysicalProgramComposer
24import Runtime.NativeRegionFrame
25import Runtime.RegionFrame
26import Runtime.SocketAddress
27import Std.Foundation
28import Std.Natural
29
30-- The numerical policy is shared by both roles and survives checkpoints.
31-- Parameters, sample-weighted combination and update use binary64. Each local
32-- sample rounds W to binary32, evaluates the checked SM86 gradient, then
33-- widens that value exactly. This is a declared mixed-precision learner,
34-- not a claim that arbitrary inputs equal the pure binary64 reference.
35def pgRun : Bytes =
36 b"partitioned-squared-error-native-v1"
37
38def pgSchema : Bytes =
39 b"f32-local-gradient-f64-update-with-u64-mass"
40
41def pgCheckpointContract =
42 (constructor
43 CheckpointEnvelopeContract
44 CheckpointEnvelopeContractValue
45 b"scalar-parameter-updates-batches-epoch/v1"
46 b"sample-mass-squared-error;rate=1/4;f32-gradient-f64-update"
47 b"fixed-repeated-batch:x=1,1,2;y=0"
48 b"initial-natural-weight=3"
49 (naturalMultiply 4 peerWordBytes)
50 (naturalMultiply 3 peerWordBytes)
51 1)
52
53def pgIdentity =
54 (lambda unrestricted name : Bytes .
55 (bytes-append
56 name
57 (phZeros (naturalSaturatingSubtract nativePhysicalEmbeddedIdentityLength (bytes-length name)))))
58
59def pgHostIdentity =
60 (pgIdentity b"partitioned-regression-sm86-host-v1")
61
62def pgProgramIdentity =
63 (pgIdentity b"partitioned-regression-sm86-program")
64
65def pgQMDIdentity =
66 (pgIdentity b"partitioned-regression-sm86-qmd")
67
68def pgPushIdentity =
69 (pgIdentity b"partitioned-regression-sm86-push")
70
71def pgRingIdentity =
72 (pgIdentity b"partitioned-regression-sm86-ring")
73
74def pgIdentities =
75 (lambda unrestricted kind : (family NativePhysicalEmbeddedComponentKind) .
76 (eliminate
77 NativePhysicalEmbeddedComponentKind
78 (lambda unrestricted current : (family NativePhysicalEmbeddedComponentKind) . Bytes)
79 kind
80 (branch NativePhysicalEmbeddedHostELF . pgHostIdentity)
81 (branch NativePhysicalEmbeddedProgramTable . pgProgramIdentity)
82 (branch NativePhysicalEmbeddedQMDTable . pgQMDIdentity)
83 (branch NativePhysicalEmbeddedPushbuffer . pgPushIdentity)
84 (branch NativePhysicalEmbeddedGPFIFO . pgRingIdentity)))
85
86def pgPlan =
87 regressionScalarPlan
88
89-- A gradient evaluation uploads the current parameter and one sample, issues
90-- the checked kernel, awaits its own retired fence, and consumes device
91-- readback. No host equation supplies the gradient. The program is the same
92-- for x=1 and x=2; samples are runtime state, not prerecorded output bytes.
93def pgGradient =
94 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
95 (lambda unrestricted entry : Nat .
96 (lambda unrestricted data : Nat .
97 (lambda unrestricted inputOffset : Nat .
98 (lambda unrestricted targetOffset : Nat .
99 (lambda unrestricted outputOffset : Nat .
100 (lambda unrestricted counter : Nat .
101 (lambda unrestricted scratch : Nat .
102 (lambda unrestricted weight : Nat .
103 (lambda unrestricted destination : Nat .
104 (lambda unrestricted sample : Nat .
105 (nlsEvaluateScalar
106 b"peer-arithmetic"
107 layout
108 entry
109 data
110 inputOffset
111 targetOffset
112 outputOffset
113 counter
114 scratch
115 (constructor
116 NvidiaLinearScalarInput
117 NvidiaLinearScalarBinary64
118 (frameNativeLoad weight))
119 (constructor NvidiaLinearScalarInput NvidiaLinearScalarNatural sample)
120 (constructor NvidiaLinearScalarInput NvidiaLinearScalarNatural 0)
121 (constructor NvidiaLinearScalarResult NvidiaLinearScalarGradient)
122 destination))))))))))))
123
124-- One participant holds x=1; the other holds x=1 and x=2. A second GPU
125-- issue computes the second contribution. Both gradients participate in the
126-- next shared parameter; a repeated issue counter is private to each channel.
127def pgContribution =
128 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
129 (lambda unrestricted entry : Nat .
130 (lambda unrestricted data : Nat .
131 (lambda unrestricted inputOffset : Nat .
132 (lambda unrestricted targetOffset : Nat .
133 (lambda unrestricted outputOffset : Nat .
134 (lambda unrestricted counter : Nat .
135 (lambda unrestricted scratch : Nat .
136 (lambda unrestricted second : Nat .
137 (lambda unrestricted worker : Nat .
138 (lambda unrestricted weight : Nat .
139 (lambda unrestricted destination : Nat .
140 (pgGradient
141 layout
142 entry
143 data
144 inputOffset
145 targetOffset
146 outputOffset
147 counter
148 scratch
149 weight
150 destination
151 1
152 (peerByRole
153 worker
154 peerEnd
155 (pgGradient
156 layout
157 entry
158 data
159 inputOffset
160 targetOffset
161 outputOffset
162 counter
163 scratch
164 weight
165 second
166 2
167 (peerBinary peerAdd destination destination second peerEnd))))))))))))))))
168
169-- Retain the final device record and both timestamped semaphore releases,
170-- followed by the completed issue count. This is a bounded raw artifact for
171-- the existing device-run evidence path, separate from the training wire
172-- format. It is created exclusively and never used as learning input.
173def pgReadback =
174 (nlsScalarReadback (peerArgument 5))
175
176-- A bound GPU session and authenticated recipe expansion. The peer protocol
177-- occupies slots 0..2 and state after phStateExtent; relocation reserves the
178-- NVIDIA result slots without moving either layout's state addresses.
179def pgPrelude =
180 (lambda unrestricted device : (family NvidiaDeviceBinding) .
181 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
182 (lambda unrestricted recipes : (family NvidiaPlanHostRecipeFills) .
183 (lambda unrestricted program : Bytes .
184 (lambda unrestricted qmd : Bytes .
185 (lambda unrestricted push : Bytes .
186 (lambda unrestricted ring : Bytes .
187 (nlsSessionPrelude
188 pgIdentities
189 b"partitioned-peer"
190 device
191 layout
192 recipes
193 program
194 qmd
195 push
196 ring
197 peerEnd))))))))
198
199-- argv: [previous checkpoint or unused], candidate, committed generation,
200-- containing directory, exclusive device-readback file. Socket address and
201-- exact card binding are admitted deployment inputs to compilation. Prediction
202-- uses the identical numerical checkpoint contract in a fresh process.
203def partitionedDeviceArtifact =
204 (lambda unrestricted profile : (family RunPodSM86TargetProfile) .
205 (lambda unrestricted device : (family NvidiaDeviceBinding) .
206 (lambda unrestricted worker : Nat .
207 (lambda unrestricted address : (family IPv4Address) .
208 (lambda unrestricted port : Nat .
209 (lambda unrestricted resume : Nat .
210 (lambda unrestricted steps : Nat .
211 (eliminate
212 NvidiaLinearStepPlan
213 (lambda unrestricted p : (family NvidiaLinearStepPlan) . Bytes)
214 (pgPlan profile)
215 (branch
216 NvidiaLinearStepPlanValue
217 layout
218 component
219 recipes
220 data
221 inputOffset
222 targetOffset
223 outputOffset
224 dataBytes
225 admitted
226 .
227 (nat-eliminate
228 (lambda unrestricted ok : Nat . Bytes)
229 b""
230 (lambda unrestricted previous : Nat .
231 (lambda unrestricted ignored : Bytes .
232 (peerLayoutsFor
233 pgRun
234 pgSchema
235 phStateExtent
236 (lambda unrestricted initial : (family RegionFrameLayout) .
237 (lambda unrestricted contribution : (family RegionFrameLayout) .
238 (lambda unrestricted updated : (family RegionFrameLayout) .
239 (lambda unrestricted acknowledged : (family RegionFrameLayout) .
240 (lambda unrestricted work : Nat .
241 (eliminate
242 StdResult
243 (lambda unrestricted r : (family StdResult (family NativeCheckpointFailure) (family NativeCheckpointLayout)) .
244 Bytes)
245 (planNativeCheckpoint
246 pgCheckpointContract
247 (frameAlign (peerEndpointEnd (peerWorkEnd work)))
248 peerWordBytes
249 (naturalMultiply 2 peerWordBytes)
250 1048576)
251 (branch StdFailure error . b"")
252 (branch
253 StdSuccess
254 checkpoint
255 .
256 (eliminate
257 StdResult
258 (lambda unrestricted r : (family StdResult (family SocketAddressFailure) Bytes) .
259 Bytes)
260 (linuxIPv4SocketAddress address port)
261 (branch StdFailure error . b"")
262 (branch
263 StdSuccess
264 socketAddress
265 .
266 (let unrestricted counter =
267 (frameAlign (nativeCheckpointEnd checkpoint))
268 in
269 (let unrestricted scratch =
270 (naturalAdd counter peerWordBytes)
271 in
272 (let unrestricted second =
273 (naturalAdd scratch peerWordBytes)
274 in
275 (let unrestricted extent =
276 (naturalAdd second peerWordBytes)
277 in
278 (let unrestricted destination =
279 (naturalSelect
280 worker
281 (framePayloadAt contribution)
282 (framePayloadAt updated))
283 in
284 (let unrestricted program =
285 (component
286 (constructor
287 NvidiaWholeProgramComponent
288 NvidiaWholeProgramProgramRecipe))
289 in
290 (let unrestricted qmd =
291 (component
292 (constructor
293 NvidiaWholeProgramComponent
294 NvidiaWholeProgramQMDRecipe))
295 in
296 (let unrestricted push =
297 (component
298 (constructor
299 NvidiaWholeProgramComponent
300 NvidiaWholeProgramPushbufferRecipe))
301 in
302 (let unrestricted ring =
303 (component
304 (constructor
305 NvidiaWholeProgramComponent
306 NvidiaWholeProgramGPFIFORecipe))
307 in
308 (let unrestricted entry =
309 (nvidiaPlanHostTableWord
310 (component
311 (constructor
312 NvidiaWholeProgramComponent
313 NvidiaWholeProgramGPFIFO))
314 0)
315 in
316 (nlsWithPrivateSlots
317 peerEndpointSlots
318 (pgPrelude device layout recipes program qmd push ring)
319 (lambda unrestricted prepare : (family NativePhysicalCommands) .
320 (nlsWithPrivateSlots
321 peerEndpointSlots
322 (pgContribution
323 layout
324 entry
325 data
326 inputOffset
327 targetOffset
328 outputOffset
329 counter
330 scratch
331 second
332 worker
333 (framePayloadAt initial)
334 destination)
335 (lambda unrestricted local : (family NativePhysicalCommands) .
336 (nlsWithPrivateSlots
337 peerEndpointSlots
338 (pgReadback
339 layout
340 data
341 outputOffset
342 counter
343 (phTelemetry
344 3
345 b"partitioned-peer:device-updates-retired"
346 (phRelease peerEnd)))
347 (lambda unrestricted finish : (family NativePhysicalCommands) .
348 (nlsEmbedHost
349 pgIdentities
350 (nativePhysicalGenerateNativeELFBytesDirect
351 (peerProgram
352 (naturalAdd peerEndpointSlots phSlots)
353 extent
354 (peerCheckpointStart
355 checkpoint
356 initial
357 resume
358 (peerStore
359 counter
360 (phImm 0)
361 (prSplice
362 prepare
363 (peerNativeSetup
364 worker
365 socketAddress
366 (peerWorkEnd work)
367 (peerImmediateTransmission
368 work
369 (peerUpdatesWith
370 (prSplice local)
371 (nativeLaunchRecipeSlotValue peerConnectionSlot)
372 worker
373 0
374 steps
375 (frameNativeLoad (peerCheckpointEpochAt checkpoint))
376 (frameNativeLoad (nativeCheckpointUpdatesAt checkpoint))
377 initial
378 contribution
379 updated
380 acknowledged
381 work
382 (prSplice
383 finish
384 (peerCheckpointFinish
385 checkpoint
386 initial
387 worker
388 steps
389 (nativeLaunchRecipeSlotValue peerConnectionSlot)))))))))))
390 program
391 qmd
392 push
393 ring)))))))))))))))))))))))))))))
394 (naturalAnd
395 admitted
396 (naturalAnd
397 (nvidiaDeviceBindingAdmitted device)
398 (naturalAnd
399 (naturalEqual (bytes-length (nvidiaDeviceBindingUUID device)) 16)
400 (naturalAnd
401 (naturalLessOrEqual worker 1)
402 (naturalAnd
403 (naturalLessOrEqual resume 1)
404 (naturalAnd
405 (naturalNonzero steps)
406 (naturalLessOrEqual steps regionFrameWordLimit)))))))))))))))))
407
408def partitionedDevicePredictionArtifact =
409 (checkpointPredictionArtifactFor pgCheckpointContract)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.