1module Runtime.NativeDataParallel
2
3import Learning.DataParallel
4import Learning.Numerics
5import Learning.Transition
6import Std.Numeric.Profile
7import Component.Pointwise
8import Runtime.OrderedCombine
9import Compiler.Planning.OrderedCombine
10import Runtime.Protocol
11import Compiler.Planning.Protocol
12import Runtime.NativeProtocol
13import Runtime.NativeCombine
14import Runtime.RegionTransfer
15import Runtime.RegionFrame
16import Compiler.Planning.RegionFrame
17import Runtime.NativeRegionFrame
18import Runtime.NativePeerEndpoint
19import Runtime.NativeFloatPlan
20import Runtime.NativeMemoryPlan
21import Runtime.NativeLaunchRecipeLoad
22import Runtime.NativePhysicalProgram
23import Runtime.NativePhysicalProgramComposer
24import Runtime.NativePointwisePlan
25import Runtime.NativeHostTarget
26import Runtime.NativeResourcePlan
27import Runtime.NativeSocketPlan
28import Runtime.NativeIndependentState
29import Runtime.NativeWordArithmetic
30import Runtime.ArenaCertificate
31import Checkpoint.Envelope
32import Checkpoint.NativeEnvelope
33import Checkpoint.NativeRegions
34import Checkpoint.NativePeerPublication
35import Checkpoint.RegionManifest
36import Representation.Partition
37import Data.Bytes
38import Data.SHA256Digest
39import Model.Word64
40import Std.Foundation
41import Std.List
42import Std.Natural
43import Std.Word
44
45-- The native host realization of a data-parallel learner
46-- (Learning.DataParallel) over owners 0..n-1 on a star centred on owner 0 or
47-- on a bounded-fan-out hierarchy (Runtime.NativeDataParallelTree).
48--
49-- One update is one round of a global protocol:
50-- every owner: sum its own samples' contributions in sample order into a
51-- (numerator, mass) value, starting from +0;
52-- ordered combine: on a star the left-deep sum (((v0 + v1) + v2) + ...)
53-- at owner 0; on a hierarchy each node's own value followed by its
54-- children's subtree values, left-deep at the node; replicated to every
55-- owner (Runtime.NativeCombine), elementwise binary64 addition of
56-- numerators and of masses;
57-- every owner: mean = numerator / mass, then the update program on
58-- (parameters, mean, rate); version and input cursor advance.
59-- Every owner computes the same bits, so the parameters stay replicated
60-- without a separate broadcast. The evaluation order is the combine tree;
61-- its numerical contract and digest are part of the frame identities, so a
62-- peer compiled for another order refuses before any result.
63--
64-- Persistence: the parameters are one logical region held (replicated) by
65-- every owner; owner 0 publishes it as one shard and every owner's whole
66-- replicated state must equal owner 0's before anything is published. Restore
67-- reads that shard into every owner's parameters. Samples are immutable
68-- program inputs and are not checkpointed. This module owns everything
69-- except the publication itself; the star's publication is below and the
70-- hierarchy's in Runtime.NativeDataParallelTree.
71family DataParallelRoundOperation : Type 0
72constructor DataParallelContribute
73constructor DataParallelCombine
74field unrestricted dataParallelCombineOperation : (family OrderedCombineOperation (family RegionTransferIdentity))
75constructor DataParallelUpdate
76
77end-family
78
79-- How the owners exchange: a star centred on owner 0, or a bounded-fan-out
80-- hierarchy (Representation.ParticipantTree). The topology fixes the
81-- combine tree, hence the floating-point order, so it is part of the
82-- numerical contract.
83family DataParallelTopology : Type 0
84constructor DataParallelStar
85constructor DataParallelHierarchy
86field unrestricted dataParallelFanout : Nat
87
88end-family
89
90-- Where one owner's combine storage and owner state live; the publication's
91-- storage lies between them.
92family NativeDataParallelLayout : Type 0
93constructor NativeDataParallelLayoutOf
94field unrestricted dataParallelPlacement : (family NativeCombinePlacement)
95field unrestricted dataParallelStateAt : Nat
96-- the learner's identity digest, computed once per artifact: every frame
97-- and anchor identity of the owner names it
98field unrestricted dataParallelDigest : Bytes
99
100end-family
101
102-- The star publication's frames and checkpoint plan.
103family NativeDataParallelStarLayout : Type 0
104constructor NativeDataParallelStarLayoutOf
105field unrestricted dataParallelCaptureFrame : (family RegionFrameLayout)
106field unrestricted dataParallelCommittedFrame : (family RegionFrameLayout)
107field unrestricted dataParallelCheckpoint : (family NativeRegionCheckpoint)
108
109end-family
110
111def dpPlacement =
112 (lambda unrestricted layout : (family NativeDataParallelLayout) .
113 (eliminate
114 NativeDataParallelLayout
115 (lambda unrestricted current : (family NativeDataParallelLayout) .
116 (family NativeCombinePlacement))
117 layout
118 (branch NativeDataParallelLayoutOf placement stateAt digest . placement)))
119
120def dpStateAt =
121 (lambda unrestricted layout : (family NativeDataParallelLayout) .
122 (eliminate
123 NativeDataParallelLayout
124 (lambda unrestricted current : (family NativeDataParallelLayout) . Nat)
125 layout
126 (branch NativeDataParallelLayoutOf placement stateAt digest . stateAt)))
127
128def dpDigest =
129 (lambda unrestricted layout : (family NativeDataParallelLayout) .
130 (eliminate
131 NativeDataParallelLayout
132 (lambda unrestricted current : (family NativeDataParallelLayout) . Bytes)
133 layout
134 (branch NativeDataParallelLayoutOf placement stateAt digest . digest)))
135
136def dpCapture =
137 (lambda unrestricted star : (family NativeDataParallelStarLayout) .
138 (eliminate
139 NativeDataParallelStarLayout
140 (lambda unrestricted current : (family NativeDataParallelStarLayout) .
141 (family RegionFrameLayout))
142 star
143 (branch NativeDataParallelStarLayoutOf capture committed checkpoint . capture)))
144
145def dpCommitted =
146 (lambda unrestricted star : (family NativeDataParallelStarLayout) .
147 (eliminate
148 NativeDataParallelStarLayout
149 (lambda unrestricted current : (family NativeDataParallelStarLayout) .
150 (family RegionFrameLayout))
151 star
152 (branch NativeDataParallelStarLayoutOf capture committed checkpoint . committed)))
153
154def dpCheckpoint =
155 (lambda unrestricted star : (family NativeDataParallelStarLayout) .
156 (eliminate
157 NativeDataParallelStarLayout
158 (lambda unrestricted current : (family NativeDataParallelStarLayout) .
159 (family NativeRegionCheckpoint))
160 star
161 (branch NativeDataParallelStarLayoutOf capture committed checkpoint . checkpoint)))
162
163def dpWord : Nat =
164 nativePointwiseWordBytes
165
166def dpEnd =
167 (constructor NativePhysicalCommands NativePhysicalCommandsEnd)
168
169def dpHalt =
170 (nativeLaunchRecipeCommand
171 (constructor NativePhysicalOperation NativePhysicalHaltSuccess)
172 b"data-parallel-done"
173 dpEnd)
174
175-- ---- shapes ----
176def dpK =
177 (lambda unrestricted c : Nat .
178 (lambda unrestricted u : Nat .
179 (lambda unrestricted system : (family DataParallelSystem c u) .
180 (dataParallelParameters c u system))))
181
182def dpS =
183 (lambda unrestricted c : Nat .
184 (lambda unrestricted u : Nat .
185 (lambda unrestricted system : (family DataParallelSystem c u) .
186 (dataParallelWidth c u system))))
187
188def dpOwners =
189 (lambda unrestricted c : Nat .
190 (lambda unrestricted u : Nat .
191 (lambda unrestricted system : (family DataParallelSystem c u) .
192 (dataParallelOwners c u system))))
193
194-- A combined value: k numerator words followed by the mass word.
195def dpValueBytes =
196 (lambda unrestricted c : Nat .
197 (lambda unrestricted u : Nat .
198 (lambda unrestricted system : (family DataParallelSystem c u) .
199 (naturalMultiply dpWord (succ (dpK c u system))))))
200
201def dpParameterBytes =
202 (lambda unrestricted c : Nat .
203 (lambda unrestricted u : Nat .
204 (lambda unrestricted system : (family DataParallelSystem c u) .
205 (naturalMultiply dpWord (dpK c u system)))))
206
207-- m, the optimizer state's words; they follow the parameters in the owner
208-- state, so the replicated bytes are one interval: parameters, then state.
209def dpM =
210 (lambda unrestricted c : Nat .
211 (lambda unrestricted u : Nat .
212 (lambda unrestricted system : (family DataParallelSystem c u) .
213 (dataParallelStateCount c u system))))
214
215def dpOptimizerBytes =
216 (lambda unrestricted c : Nat .
217 (lambda unrestricted u : Nat .
218 (lambda unrestricted system : (family DataParallelSystem c u) .
219 (naturalMultiply dpWord (dpM c u system)))))
220
221def dpReplicatedBytes =
222 (lambda unrestricted c : Nat .
223 (lambda unrestricted u : Nat .
224 (lambda unrestricted system : (family DataParallelSystem c u) .
225 (naturalAdd (dpParameterBytes c u system) (dpOptimizerBytes c u system)))))
226
227def dpStateBytes =
228 (lambda unrestricted c : Nat .
229 (lambda unrestricted u : Nat .
230 (lambda unrestricted system : (family DataParallelSystem c u) .
231 (naturalAdd nativeRegionCaptureBytes (dpReplicatedBytes c u system)))))
232
233-- ---- numerical contract and identities ----
234def dpIdentityDigest =
235 (lambda unrestricted c : Nat .
236 (lambda unrestricted u : Nat .
237 (lambda unrestricted system : (family DataParallelSystem c u) .
238 (sha256RawDigestOrEmpty (dataParallelIdentity c u system)))))
239
240-- Elementwise binary64 numerator and mass addition in the combine tree's
241-- order; the tree digest itself enters every transfer identity.
242def dpRelation =
243 (lambda unrestricted topology : (family DataParallelTopology) .
244 (lambda unrestricted owners : Nat .
245 (eliminate
246 DataParallelTopology
247 (lambda unrestricted current : (family DataParallelTopology) . Bytes)
248 topology
249 (branch
250 DataParallelStar
251 .
252 (bytes-append b"data-parallel-left-chain-sum;mass-add;owners=" (regionFrameWord owners)))
253 (branch
254 DataParallelHierarchy
255 fanout
256 .
257 (bytes-append
258 b"data-parallel-hierarchy-sum;mass-add;owners="
259 (bytes-append
260 (regionFrameWord owners)
261 (bytes-append b";fanout=" (regionFrameWord fanout))))))))
262
263def dpContract =
264 (lambda unrestricted topology : (family DataParallelTopology) .
265 (lambda unrestricted owners : Nat .
266 (constructor
267 NumericalContract
268 NumericalContractOf
269 nativeFiniteFloat64Profile
270 (constructor
271 StdList
272 StdListCons
273 (family StdNumericOperation)
274 stdOpAdd
275 (constructor
276 StdList
277 StdListCons
278 (family StdNumericOperation)
279 stdOpAdd
280 (constructor StdList StdListEmpty (family StdNumericOperation))))
281 (constructor NumericalRelation NumericalExactOrder (dpRelation topology owners)))))
282
283def dpBaseAnchor =
284 (lambda unrestricted c : Nat .
285 (lambda unrestricted u : Nat .
286 (lambda unrestricted system : (family DataParallelSystem c u) .
287 (lambda unrestricted digest : Bytes .
288 (constructor
289 RegionTransferIdentity
290 RegionTransferIdentityOf
291 b"data-parallel"
292 digest
293 b"numerator-mass"
294 b"binary64-vector-and-mass"
295 (constructor LearningRound LearningRoundOf 1 0)
296 0
297 0
298 0
299 (constructor LogicalInterval LogicalIntervalOf 0 (dpOwners c u system)))))))
300
301def dpMembers =
302 (lambda unrestricted owners : Nat .
303 (constructor CombineCoverage CombineOrderedMembers (stdListNaturalsBelow owners)))
304
305def dpAnchor =
306 (lambda unrestricted c : Nat .
307 (lambda unrestricted u : Nat .
308 (lambda unrestricted system : (family DataParallelSystem c u) .
309 (lambda unrestricted digest : Bytes .
310 (lambda unrestricted topology : (family DataParallelTopology) .
311 (combineCoverageAnchor
312 (dpMembers (dpOwners c u system))
313 (combineNumericalAnchor
314 (dpContract topology (dpOwners c u system))
315 (dpBaseAnchor c u system digest))))))))
316
317def dpTree =
318 (lambda unrestricted topology : (family DataParallelTopology) .
319 (lambda unrestricted owners : Nat .
320 (eliminate
321 DataParallelTopology
322 (lambda unrestricted current : (family DataParallelTopology) . (family OrderedCombineTree))
323 topology
324 (branch DataParallelStar . (nativeCombineChain 0 owners))
325 (branch DataParallelHierarchy fanout . (nativeCombineHierarchy fanout owners)))))
326
327-- Capture and release frames of the publication star, one per edge.
328def dpPublicationIdentity =
329 (lambda unrestricted c : Nat .
330 (lambda unrestricted u : Nat .
331 (lambda unrestricted system : (family DataParallelSystem c u) .
332 (lambda unrestricted digest : Bytes .
333 (lambda unrestricted operation : Nat .
334 (lambda unrestricted sender : Nat .
335 (lambda unrestricted receiver : Nat .
336 (constructor
337 RegionTransferIdentity
338 RegionTransferIdentityOf
339 digest
340 b"data-parallel-publication-v1"
341 b"parameters"
342 b"finite-f64-rne-separate"
343 (constructor LearningRound LearningRoundOf 1 0)
344 operation
345 sender
346 receiver
347 (constructor LogicalInterval LogicalIntervalOf 0 (dpReplicatedBytes c u system))))))))))
348
349def dpCaptureFor =
350 (lambda unrestricted c : Nat .
351 (lambda unrestricted u : Nat .
352 (lambda unrestricted system : (family DataParallelSystem c u) .
353 (lambda unrestricted digest : Bytes .
354 (lambda unrestricted layout : (family NativeDataParallelStarLayout) .
355 (lambda unrestricted owner : Nat .
356 (niFrameAt
357 (dpPublicationIdentity c u system digest 0 owner 0)
358 (dpStateBytes c u system)
359 (dpCapture layout))))))))
360
361def dpCommittedFor =
362 (lambda unrestricted c : Nat .
363 (lambda unrestricted u : Nat .
364 (lambda unrestricted system : (family DataParallelSystem c u) .
365 (lambda unrestricted digest : Bytes .
366 (lambda unrestricted layout : (family NativeDataParallelStarLayout) .
367 (lambda unrestricted owner : Nat .
368 (niFrameAt
369 (dpPublicationIdentity c u system digest 1 0 owner)
370 dpWord
371 (dpCommitted layout))))))))
372
373def dpContext =
374 (lambda unrestricted c : Nat .
375 (lambda unrestricted u : Nat .
376 (lambda unrestricted system : (family DataParallelSystem c u) .
377 (lambda unrestricted digest : Bytes .
378 (constructor
379 CheckpointEnvelopeContract
380 CheckpointEnvelopeContractValue
381 (bytes-append
382 b"data-parallel-replicated-f64-finite-rne-separate-v1;"
383 (bytes-append
384 (numericalExactContractDigest
385 (dpContract
386 (constructor DataParallelTopology DataParallelStar)
387 (dpOwners c u system)))
388 digest))
389 b"typed-sample-contributions;ordered-combine;typed-update"
390 b"immutable-partitioned-samples;one-pass-per-update"
391 b"declared-initial-parameters;no-randomness"
392 1
393 1
394 1)))))
395
396def dpRegions =
397 (lambda unrestricted c : Nat .
398 (lambda unrestricted u : Nat .
399 (lambda unrestricted system : (family DataParallelSystem c u) .
400 (constructor
401 StdList
402 StdListCons
403 (family CheckpointLogicalRegion)
404 (constructor
405 CheckpointLogicalRegion
406 CheckpointLogicalRegionOf
407 b"parameters"
408 b"f64-le"
409 (dpParameterBytes c u system))
410 (nat-eliminate
411 (lambda unrestricted words : Nat . (family StdList (family CheckpointLogicalRegion)))
412 (constructor StdList StdListEmpty (family CheckpointLogicalRegion))
413 (lambda unrestricted previous : Nat .
414 (lambda unrestricted ignored : (family StdList (family CheckpointLogicalRegion)) .
415 (constructor
416 StdList
417 StdListCons
418 (family CheckpointLogicalRegion)
419 (constructor
420 CheckpointLogicalRegion
421 CheckpointLogicalRegionOf
422 b"optimizer-state"
423 b"f64-le"
424 (dpOptimizerBytes c u system))
425 (constructor StdList StdListEmpty (family CheckpointLogicalRegion)))))
426 (dpM c u system))))))
427
428def dpPartitions =
429 (lambda unrestricted c : Nat .
430 (lambda unrestricted u : Nat .
431 (lambda unrestricted system : (family DataParallelSystem c u) .
432 (constructor
433 StdList
434 StdListCons
435 (family CheckpointRegionPartition)
436 (constructor
437 CheckpointRegionPartition
438 CheckpointRegionPartitionOf
439 0
440 (constructor
441 StdList
442 StdListCons
443 (family LogicalInterval)
444 (constructor LogicalInterval LogicalIntervalOf 0 (dpParameterBytes c u system))
445 (constructor StdList StdListEmpty (family LogicalInterval))))
446 (nat-eliminate
447 (lambda unrestricted words : Nat . (family StdList (family CheckpointRegionPartition)))
448 (constructor StdList StdListEmpty (family CheckpointRegionPartition))
449 (lambda unrestricted previous : Nat .
450 (lambda unrestricted ignored : (family StdList (family CheckpointRegionPartition)) .
451 (constructor
452 StdList
453 StdListCons
454 (family CheckpointRegionPartition)
455 (constructor
456 CheckpointRegionPartition
457 CheckpointRegionPartitionOf
458 1
459 (constructor
460 StdList
461 StdListCons
462 (family LogicalInterval)
463 (constructor
464 LogicalInterval
465 LogicalIntervalOf
466 0
467 (dpOptimizerBytes c u system))
468 (constructor StdList StdListEmpty (family LogicalInterval))))
469 (constructor StdList StdListEmpty (family CheckpointRegionPartition)))))
470 (dpM c u system))))))
471
472-- Where a shard's bytes lie in an owner's state: past the capture prefix,
473-- parameters (region 0) then optimizer state (region 1).
474def dpShardOffset =
475 (lambda unrestricted c : Nat .
476 (lambda unrestricted u : Nat .
477 (lambda unrestricted system : (family DataParallelSystem c u) .
478 (lambda unrestricted shard : (family NativeRegionShard) .
479 (naturalAdd
480 nativeRegionCaptureBytes
481 (naturalAdd
482 (naturalMultiply (nativeRegionOrdinal shard) (dpParameterBytes c u system))
483 (intervalBegin (nativeRegionInterval shard))))))))
484
485-- The replicated regions' shard count: parameters, and optimizer state when
486-- the learner has any.
487def dpShardCount =
488 (lambda unrestricted c : Nat .
489 (lambda unrestricted u : Nat .
490 (lambda unrestricted system : (family DataParallelSystem c u) .
491 (naturalAdd 1 (naturalNonzero (dpM c u system))))))
492
493-- argv with h shards: 1 previous manifest, 2..h+1 previous shards (parameters,
494-- then optimizer state), then each shard's candidate and committed file, the
495-- candidate and committed manifest and the directory (with one shard: 3/4
496-- shard, 5/6 manifest, 7 directory).
497def dpPaths =
498 (lambda unrestricted c : Nat .
499 (lambda unrestricted u : Nat .
500 (lambda unrestricted system : (family DataParallelSystem c u) .
501 (constructor NativeRegionPaths NativeRegionPathsOf 1 (dpShardCount c u system)))))
502
503-- ---- layout ----
504def dpLeafAt =
505 (lambda unrestricted layout : (family NativeDataParallelLayout) .
506 (nativeCombineRegionEnd (dpPlacement layout)))
507
508def dpParametersAt =
509 (lambda unrestricted layout : (family NativeDataParallelLayout) .
510 (naturalAdd (dpStateAt layout) nativeRegionCaptureBytes))
511
512def dpContributionAt =
513 (lambda unrestricted c : Nat .
514 (lambda unrestricted u : Nat .
515 (lambda unrestricted system : (family DataParallelSystem c u) .
516 (lambda unrestricted layout : (family NativeDataParallelLayout) .
517 (naturalAdd (dpParametersAt layout) (dpReplicatedBytes c u system))))))
518
519def dpContributionEnd =
520 (lambda unrestricted c : Nat .
521 (lambda unrestricted u : Nat .
522 (lambda unrestricted system : (family DataParallelSystem c u) .
523 (lambda unrestricted layout : (family NativeDataParallelLayout) .
524 (nativePointwiseExtent
525 c
526 (dataParallelContributionProgram c u system)
527 (dpContributionAt c u system layout))))))
528
529def dpUpdateAt =
530 (lambda unrestricted c : Nat .
531 (lambda unrestricted u : Nat .
532 (lambda unrestricted system : (family DataParallelSystem c u) .
533 (lambda unrestricted layout : (family NativeDataParallelLayout) .
534 (dpContributionEnd c u system layout)))))
535
536def dpUpdateEnd =
537 (lambda unrestricted c : Nat .
538 (lambda unrestricted u : Nat .
539 (lambda unrestricted system : (family DataParallelSystem c u) .
540 (lambda unrestricted layout : (family NativeDataParallelLayout) .
541 (nativePointwiseExtent
542 u
543 (dataParallelUpdateProgram c u system)
544 (dpUpdateAt c u system layout))))))
545
546-- The binary64 constant 1, the mass of one sample.
547def dpOneAt =
548 (lambda unrestricted c : Nat .
549 (lambda unrestricted u : Nat .
550 (lambda unrestricted system : (family DataParallelSystem c u) .
551 (lambda unrestricted layout : (family NativeDataParallelLayout) .
552 (dpUpdateEnd c u system layout)))))
553
554def dpSamplesAt =
555 (lambda unrestricted c : Nat .
556 (lambda unrestricted u : Nat .
557 (lambda unrestricted system : (family DataParallelSystem c u) .
558 (lambda unrestricted layout : (family NativeDataParallelLayout) .
559 (naturalAdd (dpOneAt c u system layout) dpWord)))))
560
561def dpSampleBytes =
562 (lambda unrestricted c : Nat .
563 (lambda unrestricted u : Nat .
564 (lambda unrestricted system : (family DataParallelSystem c u) .
565 (naturalMultiply dpWord (dpS c u system)))))
566
567def dpEndpointAt =
568 (lambda unrestricted c : Nat .
569 (lambda unrestricted u : Nat .
570 (lambda unrestricted system : (family DataParallelSystem c u) .
571 (lambda unrestricted layout : (family NativeDataParallelLayout) .
572 (lambda unrestricted owner : Nat .
573 (naturalAdd
574 (dpSamplesAt c u system layout)
575 (naturalMultiply
576 (dpSampleBytes c u system)
577 (stdListLength (family StdList StdU64) (dataParallelSamplesOf c u system owner)))))))))
578
579-- This role's combine placement under `topology`, from address 0.
580def dpPlacementFor =
581 (lambda unrestricted c : Nat .
582 (lambda unrestricted u : Nat .
583 (lambda unrestricted system : (family DataParallelSystem c u) .
584 (lambda unrestricted digest : Bytes .
585 (lambda unrestricted topology : (family DataParallelTopology) .
586 (lambda unrestricted role : Nat .
587 (constructor
588 NativeCombinePlacement
589 NativeCombinePlacementOf
590 (nativeCombineContextFor
591 (dpAnchor c u system digest topology)
592 role
593 (dpTree topology (dpOwners c u system)))
594 0
595 (dpValueBytes c u system))))))))
596
597-- Where a publication's storage may begin: after the combine region and this
598-- owner's leaf value.
599def dpPublicationBase =
600 (lambda unrestricted c : Nat .
601 (lambda unrestricted u : Nat .
602 (lambda unrestricted system : (family DataParallelSystem c u) .
603 (lambda unrestricted placement : (family NativeCombinePlacement) .
604 (frameAlign (naturalAdd (nativeCombineRegionEnd placement) (dpValueBytes c u system)))))))
605
606-- The star: capture and release frames and the region checkpoint after the
607-- combine storage, then the owner state.
608def dpWithStarLayout =
609 (lambda unrestricted c : Nat .
610 (lambda unrestricted u : Nat .
611 (lambda unrestricted system : (family DataParallelSystem c u) .
612 (lambda unrestricted role : Nat .
613 (lambda unrestricted epoch : Nat .
614 (lambda unrestricted available : Nat .
615 (lambda unrestricted emit : (pi unrestricted layout : (family NativeDataParallelLayout) . (pi unrestricted star : (family NativeDataParallelStarLayout) . Bytes)) .
616 (let unrestricted digest =
617 (dpIdentityDigest c u system)
618 in
619 (let unrestricted placement =
620 (dpPlacementFor
621 c
622 u
623 system
624 digest
625 (constructor DataParallelTopology DataParallelStar)
626 role)
627 in
628 (let unrestricted frames =
629 (dpPublicationBase c u system placement)
630 in
631 (eliminate
632 StdResult
633 (lambda unrestricted result : (family StdResult (family RegionFrameLayoutFailure) (family RegionFrameLayout)) .
634 Bytes)
635 (planRegionFrameLayout
636 (dpPublicationIdentity c u system digest 0 1 0)
637 (dpStateBytes c u system)
638 512
639 frames
640 available)
641 (branch StdFailure error . b"")
642 (branch
643 StdSuccess
644 capture
645 .
646 (eliminate
647 StdResult
648 (lambda unrestricted result : (family StdResult (family RegionFrameLayoutFailure) (family RegionFrameLayout)) .
649 Bytes)
650 (planRegionFrameLayout
651 (dpPublicationIdentity c u system digest 1 0 1)
652 dpWord
653 512
654 (frameAlign (frameEnd capture))
655 available)
656 (branch StdFailure error . b"")
657 (branch
658 StdSuccess
659 committed
660 .
661 (eliminate
662 StdResult
663 (lambda unrestricted result : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) .
664 Bytes)
665 (planNativeRegionCheckpoint
666 (dpContext c u system digest)
667 (dpRegions c u system)
668 (dpPartitions c u system)
669 epoch
670 (frameAlign (frameEnd committed))
671 available
672 (dpShardCount c u system))
673 (branch StdFailure error . b"")
674 (branch
675 StdSuccess
676 checkpoint
677 .
678 (emit
679 (constructor
680 NativeDataParallelLayout
681 NativeDataParallelLayoutOf
682 placement
683 (nativeRegionEnd checkpoint)
684 digest)
685 (constructor
686 NativeDataParallelStarLayout
687 NativeDataParallelStarLayoutOf
688 capture
689 committed
690 checkpoint))))))))))))))))))
691
692-- ---- local work ----
693def dpAdd =
694 (nativeFiniteFloat64Binary
695 b"data-parallel-add"
696 nativePeerScratchSlot
697 (constructor NativePhysicalFloat64Operation NativePhysicalFloat64Add))
698
699def dpDivide =
700 (nativeFiniteFloat64Binary
701 b"data-parallel-mean"
702 nativePeerScratchSlot
703 (constructor NativePhysicalFloat64Operation NativePhysicalFloat64Divide))
704
705def dpCopy =
706 (lambda unrestricted destination : Nat .
707 (lambda unrestricted source : Nat .
708 (lambda unrestricted bytes : Nat .
709 (nativeMemoryCopyOperands
710 (nativeMemoryState destination)
711 (nativeMemoryState source)
712 bytes
713 nativePeerScratchSlot
714 b"data-parallel-copy"))))
715
716-- `step index` for index in 0..count-1, in order.
717def dpEach =
718 (lambda unrestricted count : Nat .
719 (lambda unrestricted step : (pi unrestricted index : Nat . (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands))) .
720 (lambda unrestricted tail : (family NativePhysicalCommands) .
721 (stdListFold
722 Nat
723 (family NativePhysicalCommands)
724 (lambda unrestricted index : Nat .
725 (lambda unrestricted rest : (family NativePhysicalCommands) . (step index rest)))
726 tail
727 (stdListNaturalsBelow count)))))
728
729-- Combine arithmetic: out_i = left_i + right_i for every numerator word and
730-- the mass, each separately rounded.
731def dpApply =
732 (lambda unrestricted c : Nat .
733 (lambda unrestricted u : Nat .
734 (lambda unrestricted system : (family DataParallelSystem c u) .
735 (lambda unrestricted out : Nat .
736 (lambda unrestricted left : Nat .
737 (lambda unrestricted right : Nat .
738 (dpEach
739 (succ (dpK c u system))
740 (lambda unrestricted index : Nat .
741 (dpAdd
742 (nativePointwiseAt out index)
743 (nativePointwiseAt left index)
744 (nativePointwiseAt right index))))))))))
745
746-- This owner's samples into its (numerator, mass) leaf value, in order,
747-- reading the parameters at `parameters`.
748def dpContribute =
749 (lambda unrestricted c : Nat .
750 (lambda unrestricted u : Nat .
751 (lambda unrestricted system : (family DataParallelSystem c u) .
752 (lambda unrestricted layout : (family NativeDataParallelLayout) .
753 (lambda unrestricted parameters : Nat .
754 (lambda unrestricted owner : Nat .
755 (lambda unrestricted contribution : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
756 (lambda unrestricted tail : (family NativePhysicalCommands) .
757 (let unrestricted k =
758 (dpK c u system)
759 in
760 (let unrestricted s =
761 (dpS c u system)
762 in
763 (let unrestricted leaf =
764 (dpLeafAt layout)
765 in
766 (let unrestricted at =
767 (dpContributionAt c u system layout)
768 in
769 (dpEach
770 (succ k)
771 (lambda unrestricted index : Nat .
772 (nativeMemoryStoreWord64
773 b"data-parallel-zero"
774 (nativePointwiseAt leaf index)
775 (nativeLaunchRecipeImmediate 0)))
776 (dpEach
777 (stdListLength
778 (family StdList StdU64)
779 (dataParallelSamplesOf c u system owner))
780 (lambda unrestricted sample : Nat .
781 (lambda unrestricted rest : (family NativePhysicalCommands) .
782 (dpCopy
783 at
784 parameters
785 (dpParameterBytes c u system)
786 (dpCopy
787 (nativePointwiseAt at k)
788 (naturalAdd
789 (dpSamplesAt c u system layout)
790 (naturalMultiply sample (dpSampleBytes c u system)))
791 (dpSampleBytes c u system)
792 (contribution
793 (dpEach
794 k
795 (lambda unrestricted index : Nat .
796 (dpAdd
797 (nativePointwiseAt leaf index)
798 (nativePointwiseAt leaf index)
799 (nativePointwiseAt at (naturalAdd (naturalAdd k s) index))))
800 (dpAdd
801 (nativePointwiseAt leaf k)
802 (nativePointwiseAt leaf k)
803 (dpOneAt c u system layout)
804 rest)))))))
805 tail))))))))))))))
806
807-- mean = numerator / mass, then the update program on (parameters, state,
808-- mean, rate), then the logical position advances. Every owner runs this on
809-- the replicated root value.
810def dpUpdate =
811 (lambda unrestricted c : Nat .
812 (lambda unrestricted u : Nat .
813 (lambda unrestricted system : (family DataParallelSystem c u) .
814 (lambda unrestricted layout : (family NativeDataParallelLayout) .
815 (lambda unrestricted update : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
816 (lambda unrestricted tail : (family NativePhysicalCommands) .
817 (let unrestricted k =
818 (dpK c u system)
819 in
820 (let unrestricted m =
821 (dpM c u system)
822 in
823 (let unrestricted total =
824 (nativeCombineResultAt (dpPlacement layout))
825 in
826 (let unrestricted at =
827 (dpUpdateAt c u system layout)
828 in
829 (dpEach
830 k
831 (lambda unrestricted index : Nat .
832 (dpDivide
833 (nativePointwiseAt at (naturalAdd (naturalAdd k m) index))
834 (nativePointwiseAt total index)
835 (nativePointwiseAt total k)))
836 (dpCopy
837 at
838 (dpParametersAt layout)
839 (dpReplicatedBytes c u system)
840 (nativeMemoryStoreWord64
841 b"data-parallel-rate"
842 (nativePointwiseAt at (naturalAdd (naturalMultiply 2 k) m))
843 (nativeLaunchRecipeImmediate
844 (modelWord64Natural (dataParallelRateWord c u system)))
845 (update
846 (dpCopy
847 (dpParametersAt layout)
848 at
849 (dpReplicatedBytes c u system)
850 (niAdvanceAt (dpStateAt layout) tail))))))))))))))))
851
852def dpLocal =
853 (lambda unrestricted c : Nat .
854 (lambda unrestricted u : Nat .
855 (lambda unrestricted system : (family DataParallelSystem c u) .
856 (lambda unrestricted layout : (family NativeDataParallelLayout) .
857 (lambda unrestricted owner : Nat .
858 (lambda unrestricted contribution : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
859 (lambda unrestricted update : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
860 (lambda unrestricted operation : (family DataParallelRoundOperation) .
861 (eliminate
862 DataParallelRoundOperation
863 (lambda unrestricted current : (family DataParallelRoundOperation) .
864 (pi unrestricted tail : (family NativePhysicalCommands) .
865 (family NativePhysicalCommands)))
866 operation
867 (branch
868 DataParallelContribute
869 .
870 (dpContribute c u system layout (dpParametersAt layout) owner contribution))
871 (branch
872 DataParallelCombine
873 value
874 .
875 (nativeCombineLocal
876 (dpPlacement layout)
877 (dpLeafAt layout)
878 (dpApply c u system)
879 value))
880 (branch DataParallelUpdate . (dpUpdate c u system layout update)))))))))))
881
882-- ---- the round protocol ----
883def dpEachRole =
884 (lambda unrestricted owners : Nat .
885 (lambda unrestricted operation : (family DataParallelRoundOperation) .
886 (lambda unrestricted tail : (family GlobalProtocol (family DataParallelRoundOperation) (family RegionTransferIdentity) (family ProtocolNoDecision)) .
887 (stdListFold
888 Nat
889 (family
890 GlobalProtocol
891 (family DataParallelRoundOperation)
892 (family RegionTransferIdentity)
893 (family ProtocolNoDecision))
894 (lambda unrestricted role : Nat .
895 (lambda unrestricted rest : (family GlobalProtocol (family DataParallelRoundOperation) (family RegionTransferIdentity) (family ProtocolNoDecision)) .
896 (protocolLocal
897 (family DataParallelRoundOperation)
898 (family RegionTransferIdentity)
899 (family ProtocolNoDecision)
900 role
901 operation
902 rest)))
903 tail
904 (stdListNaturalsBelow owners)))))
905
906def dpRoundEnd =
907 (constructor
908 GlobalProtocol
909 GlobalProtocolEnd
910 (family DataParallelRoundOperation)
911 (family RegionTransferIdentity)
912 (family ProtocolNoDecision))
913
914def dpRound =
915 (lambda unrestricted owners : Nat .
916 (lambda unrestricted combine : (family GlobalProtocol (family OrderedCombineOperation (family RegionTransferIdentity)) (family RegionTransferIdentity) (family ProtocolNoDecision)) .
917 (dpEachRole
918 owners
919 (constructor DataParallelRoundOperation DataParallelContribute)
920 (appendGlobalProtocol
921 (family DataParallelRoundOperation)
922 (family RegionTransferIdentity)
923 (family ProtocolNoDecision)
924 (mapGlobalProtocolOperations
925 (family OrderedCombineOperation (family RegionTransferIdentity))
926 (family DataParallelRoundOperation)
927 (family RegionTransferIdentity)
928 (family ProtocolNoDecision)
929 (lambda unrestricted value : (family OrderedCombineOperation (family RegionTransferIdentity)) .
930 (constructor DataParallelRoundOperation DataParallelCombine value))
931 combine)
932 (dpEachRole owners (constructor DataParallelRoundOperation DataParallelUpdate) dpRoundEnd)))))
933
934def dpLocalAdmitted =
935 (lambda unrestricted owners : Nat .
936 (lambda unrestricted placement : (family NativeCombinePlacement) .
937 (lambda unrestricted role : Nat .
938 (lambda unrestricted operation : (family DataParallelRoundOperation) .
939 (eliminate
940 DataParallelRoundOperation
941 (lambda unrestricted current : (family DataParallelRoundOperation) . Nat)
942 operation
943 (branch DataParallelContribute . (naturalLess role owners))
944 (branch DataParallelCombine value . (nativeCombineLocalAdmitted placement role value))
945 (branch DataParallelUpdate . (naturalLess role owners)))))))
946
947-- The projected round program, repeated `steps` times, for this role.
948def dpProjected =
949 (lambda unrestricted c : Nat .
950 (lambda unrestricted u : Nat .
951 (lambda unrestricted system : (family DataParallelSystem c u) .
952 (lambda unrestricted topology : (family DataParallelTopology) .
953 (lambda unrestricted layout : (family NativeDataParallelLayout) .
954 (lambda unrestricted steps : Nat .
955 (let unrestricted owners =
956 (dpOwners c u system)
957 in
958 (let unrestricted placement =
959 (dpPlacement layout)
960 in
961 (stdResultBind
962 (family OrderedCombineFailure)
963 (family
964 GlobalProtocol
965 (family OrderedCombineOperation (family RegionTransferIdentity))
966 (family RegionTransferIdentity)
967 (family ProtocolNoDecision))
968 (family
969 ParticipantProtocol
970 (family DataParallelRoundOperation)
971 (family RegionTransferIdentity)
972 (family ProtocolNoDecision))
973 (planNativeCombineGlobal
974 placement
975 (dpContract topology owners)
976 owners
977 (dpMembers owners)
978 (dpBaseAnchor c u system (dpDigest layout)))
979 (lambda unrestricted combine : (family GlobalProtocol (family OrderedCombineOperation (family RegionTransferIdentity)) (family RegionTransferIdentity) (family ProtocolNoDecision)) .
980 (eliminate
981 StdResult
982 (lambda unrestricted result : (family StdResult (family ProtocolFailure) (family ParticipantProtocol (family DataParallelRoundOperation) (family RegionTransferIdentity) (family ProtocolNoDecision))) .
983 (family
984 StdResult
985 (family OrderedCombineFailure)
986 (family
987 ParticipantProtocol
988 (family DataParallelRoundOperation)
989 (family RegionTransferIdentity)
990 (family ProtocolNoDecision))))
991 (planParticipantProtocol
992 (family DataParallelRoundOperation)
993 (family RegionTransferIdentity)
994 (family ProtocolNoDecision)
995 owners
996 (nativeCombineRole (nativeCombinePlacementContext placement))
997 (dpLocalAdmitted owners placement)
998 (nativeCombineTransferAdmitted placement)
999 (protocolNoDecision (family RegionTransferIdentity))
1000 (protocolRepeat
1001 (family DataParallelRoundOperation)
1002 (family RegionTransferIdentity)
1003 (family ProtocolNoDecision)
1004 steps
1005 (dpRound owners combine)
1006 dpRoundEnd))
1007 (branch
1008 StdFailure
1009 failure
1010 .
1011 (constructor
1012 StdResult
1013 StdFailure
1014 (family OrderedCombineFailure)
1015 (family
1016 ParticipantProtocol
1017 (family DataParallelRoundOperation)
1018 (family RegionTransferIdentity)
1019 (family ProtocolNoDecision))
1020 (constructor OrderedCombineFailure CombineProtocolRefused failure)))
1021 (branch
1022 StdSuccess
1023 projected
1024 .
1025 (constructor
1026 StdResult
1027 StdSuccess
1028 (family OrderedCombineFailure)
1029 (family
1030 ParticipantProtocol
1031 (family DataParallelRoundOperation)
1032 (family RegionTransferIdentity)
1033 (family ProtocolNoDecision))
1034 projected)))))))))))))
1035
1036-- ---- start, restore, publication ----
1037def dpStoreWords =
1038 (lambda unrestricted at : Nat .
1039 (lambda unrestricted words : (family StdList StdU64) .
1040 (lambda unrestricted tail : (family NativePhysicalCommands) .
1041 (stdListFold
1042 StdU64
1043 (pi unrestricted index : Nat . (family NativePhysicalCommands))
1044 (lambda unrestricted word : StdU64 .
1045 (lambda unrestricted next : (pi unrestricted index : Nat . (family NativePhysicalCommands)) .
1046 (lambda unrestricted index : Nat .
1047 (nativeMemoryStoreWord64
1048 b"data-parallel-constant"
1049 (nativePointwiseAt at index)
1050 (nativeLaunchRecipeImmediate (modelWord64Natural word))
1051 (next (succ index))))))
1052 (lambda unrestricted index : Nat . tail)
1053 words
1054 0))))
1055
1056-- The owner's samples, in order, and the constant 1.0 (sample mass).
1057def dpInitialize =
1058 (lambda unrestricted c : Nat .
1059 (lambda unrestricted u : Nat .
1060 (lambda unrestricted system : (family DataParallelSystem c u) .
1061 (lambda unrestricted layout : (family NativeDataParallelLayout) .
1062 (lambda unrestricted owner : Nat .
1063 (lambda unrestricted tail : (family NativePhysicalCommands) .
1064 (nativeFloat64Natural
1065 b"data-parallel-one"
1066 (dpOneAt c u system layout)
1067 1
1068 (dpStoreWords
1069 (dpSamplesAt c u system layout)
1070 (stdListFold
1071 (family StdList StdU64)
1072 (family StdList StdU64)
1073 (lambda unrestricted sample : (family StdList StdU64) .
1074 (lambda unrestricted rest : (family StdList StdU64) .
1075 (stdListAppend StdU64 sample rest)))
1076 (constructor StdList StdListEmpty StdU64)
1077 (dataParallelSamplesOf c u system owner))
1078 tail))))))))
1079
1080-- Fresh: version and cursor 0, the plan's epoch and the declared initial
1081-- parameters and optimizer state.
1082def dpFresh =
1083 (lambda unrestricted c : Nat .
1084 (lambda unrestricted u : Nat .
1085 (lambda unrestricted system : (family DataParallelSystem c u) .
1086 (lambda unrestricted layout : (family NativeDataParallelLayout) .
1087 (lambda unrestricted epoch : Nat .
1088 (lambda unrestricted tail : (family NativePhysicalCommands) .
1089 (nativeMemoryStoreWord64
1090 b"data-parallel-version"
1091 (dpStateAt layout)
1092 (nativeLaunchRecipeImmediate 0)
1093 (nativeMemoryStoreWord64
1094 b"data-parallel-cursor"
1095 (nativePointwiseAt (dpStateAt layout) 1)
1096 (nativeLaunchRecipeImmediate 0)
1097 (nativeMemoryStoreWord64
1098 b"data-parallel-epoch"
1099 (nativePointwiseAt (dpStateAt layout) 2)
1100 (nativeLaunchRecipeImmediate epoch)
1101 (dpStoreWords
1102 (dpParametersAt layout)
1103 (dataParallelInitialParameters c u system)
1104 (dpStoreWords
1105 (naturalAdd (dpParametersAt layout) (dpParameterBytes c u system))
1106 (dataParallelInitialStateWords c u system)
1107 tail)))))))))))
1108
1109-- After a verified restore of the parameters: the restored (version, cursor,
1110-- epoch) from `capture`, then epoch + 1 (a new membership epoch).
1111def dpResumed =
1112 (lambda unrestricted layout : (family NativeDataParallelLayout) .
1113 (lambda unrestricted capture : Nat .
1114 (lambda unrestricted tail : (family NativePhysicalCommands) .
1115 (nativeMemoryCopyOperands
1116 (nativeMemoryState (dpStateAt layout))
1117 (nativeMemoryState capture)
1118 nativeRegionCaptureBytes
1119 nativePeerScratchSlot
1120 b"data-parallel-restore-capture"
1121 (nativeLaunchRecipeAssertEqual
1122 (nativeMemoryLoad (dpStateAt layout))
1123 (nativeMemoryLoad (nativePointwiseAt (dpStateAt layout) 1))
1124 b"data-parallel-input-position"
1125 (nativeCheckedWordAdd
1126 (nativeMemoryState (nativePointwiseAt (dpStateAt layout) 2))
1127 (nativeMemoryLoad (nativePointwiseAt (dpStateAt layout) 2))
1128 (nativeLaunchRecipeImmediate 1)
1129 nativePeerScratchSlot
1130 b"data-parallel-epoch-overflow"
1131 tail))))))
1132
1133-- The replicated regions' addresses in this owner: parameters, then (when
1134-- the learner has any) optimizer state.
1135def dpDestinations =
1136 (lambda unrestricted c : Nat .
1137 (lambda unrestricted u : Nat .
1138 (lambda unrestricted system : (family DataParallelSystem c u) .
1139 (lambda unrestricted layout : (family NativeDataParallelLayout) .
1140 (constructor
1141 StdList
1142 StdListCons
1143 (family NativeRegionDestination)
1144 (constructor
1145 NativeRegionDestination
1146 NativeRegionDestinationOf
1147 0
1148 (constructor LogicalInterval LogicalIntervalOf 0 (dpParameterBytes c u system))
1149 (dpParametersAt layout))
1150 (nat-eliminate
1151 (lambda unrestricted words : Nat . (family StdList (family NativeRegionDestination)))
1152 (constructor StdList StdListEmpty (family NativeRegionDestination))
1153 (lambda unrestricted previous : Nat .
1154 (lambda unrestricted ignored : (family StdList (family NativeRegionDestination)) .
1155 (constructor
1156 StdList
1157 StdListCons
1158 (family NativeRegionDestination)
1159 (constructor
1160 NativeRegionDestination
1161 NativeRegionDestinationOf
1162 1
1163 (constructor
1164 LogicalInterval
1165 LogicalIntervalOf
1166 0
1167 (dpOptimizerBytes c u system))
1168 (naturalAdd (dpParametersAt layout) (dpParameterBytes c u system)))
1169 (constructor StdList StdListEmpty (family NativeRegionDestination)))))
1170 (dpM c u system)))))))
1171
1172def dpRestore =
1173 (lambda unrestricted c : Nat .
1174 (lambda unrestricted u : Nat .
1175 (lambda unrestricted system : (family DataParallelSystem c u) .
1176 (lambda unrestricted layout : (family NativeDataParallelLayout) .
1177 (lambda unrestricted star : (family NativeDataParallelStarLayout) .
1178 (lambda unrestricted extent : Nat .
1179 (lambda unrestricted tail : (family NativePhysicalCommands) .
1180 (planNativeRegionRestore
1181 (dpCheckpoint star)
1182 (nativeRegionPathArgument (nativeRegionPathFirst (dpPaths c u system)))
1183 (lambda unrestricted index : Nat .
1184 (nativeRegionPathArgument
1185 (naturalAdd (nativeRegionInputShardBase (dpPaths c u system)) index)))
1186 nativePeerListenerSlot
1187 nativePeerScratchSlot
1188 extent
1189 (dpDestinations c u system layout)
1190 (dpResumed layout (nativeRegionCaptureAt (dpCheckpoint star)) tail)))))))))
1191
1192def dpStart =
1193 (lambda unrestricted c : Nat .
1194 (lambda unrestricted u : Nat .
1195 (lambda unrestricted system : (family DataParallelSystem c u) .
1196 (lambda unrestricted layout : (family NativeDataParallelLayout) .
1197 (lambda unrestricted star : (family NativeDataParallelStarLayout) .
1198 (lambda unrestricted extent : Nat .
1199 (lambda unrestricted resume : Nat .
1200 (lambda unrestricted tail : (family NativePhysicalCommands) .
1201 (nat-eliminate
1202 (lambda unrestricted mode : Nat .
1203 (family
1204 StdResult
1205 (family NativeCheckpointFailure)
1206 (family NativePhysicalCommands)))
1207 (constructor
1208 StdResult
1209 StdSuccess
1210 (family NativeCheckpointFailure)
1211 (family NativePhysicalCommands)
1212 (dpFresh c u system layout (nativeRegionEpoch (dpCheckpoint star)) tail))
1213 (lambda unrestricted previous : Nat .
1214 (lambda unrestricted ignored : (family StdResult (family NativeCheckpointFailure) (family NativePhysicalCommands)) .
1215 (dpRestore c u system layout star extent tail)))
1216 resume)))))))))
1217
1218def dpPublication =
1219 (lambda unrestricted c : Nat .
1220 (lambda unrestricted u : Nat .
1221 (lambda unrestricted system : (family DataParallelSystem c u) .
1222 (lambda unrestricted layout : (family NativeDataParallelLayout) .
1223 (lambda unrestricted star : (family NativeDataParallelStarLayout) .
1224 (lambda unrestricted resume : Nat .
1225 (lambda unrestricted edges : (family StdList (family NativePeerEdge)) .
1226 (constructor
1227 NativePeerRegionPublication
1228 NativePeerRegionPublicationOf
1229 (constructor
1230 NativeRegionCheckpoint
1231 NativeRegionCheckpointOf
1232 (nativeRegionManifest (dpCheckpoint star))
1233 (nativeRegionShards (dpCheckpoint star))
1234 (naturalAdd (nativeRegionEpoch (dpCheckpoint star)) resume)
1235 (nativeRegionEnd (dpCheckpoint star)))
1236 (naturalPredecessor (dpOwners c u system))
1237 (dpCaptureFor c u system (dpDigest layout) star)
1238 (dpCommittedFor c u system (dpDigest layout) star)
1239 (nativePeerEdgeConnectionTo edges)
1240 (dpStateAt layout)
1241 (dpStateBytes c u system)
1242 (dpStateBytes c u system)
1243 (lambda unrestricted shard : (family NativeRegionShard) . 0)
1244 (dpShardOffset c u system)
1245 (dpPaths c u system)))))))))
1246
1247def dpOutput =
1248 (lambda unrestricted c : Nat .
1249 (lambda unrestricted u : Nat .
1250 (lambda unrestricted system : (family DataParallelSystem c u) .
1251 (lambda unrestricted layout : (family NativeDataParallelLayout) .
1252 (niOutput (dpStateAt layout) (dpStateBytes c u system) dpHalt)))))
1253
1254def dpRunAdmitted =
1255 (lambda unrestricted c : Nat .
1256 (lambda unrestricted u : Nat .
1257 (lambda unrestricted system : (family DataParallelSystem c u) .
1258 (lambda unrestricted role : Nat .
1259 (lambda unrestricted addresses : (family StdList Bytes) .
1260 (lambda unrestricted resume : Nat .
1261 (lambda unrestricted epoch : Nat .
1262 (lambda unrestricted steps : Nat .
1263 (naturalAnd
1264 (dataParallelAdmitted c u system)
1265 (naturalAnd
1266 (nativePeerStarAdmitted (dpOwners c u system) role addresses)
1267 (naturalAnd
1268 (naturalLessOrEqual resume 1)
1269 (naturalAnd
1270 (naturalNonzero epoch)
1271 (naturalAnd
1272 (naturalBelowTwoPower 64 (naturalAdd epoch resume))
1273 (naturalAnd (naturalNonzero steps) (naturalBelowTwoPower 64 steps)))))))))))))))
1274
1275-- Compile both pointwise programs, project the round protocol under
1276-- `topology` and emit one owner's executable for `target`. `start extent
1277-- tail` begins the owner (fresh or restored); `publish extent success`
1278-- publishes after the last update and continues with `success`.
1279def dpEmitWith =
1280 (lambda unrestricted target : (family NativeHostTarget) .
1281 (lambda unrestricted resources : (family NativeResourceContext) .
1282 (lambda unrestricted c : Nat .
1283 (lambda unrestricted u : Nat .
1284 (lambda unrestricted system : (family DataParallelSystem c u) .
1285 (lambda unrestricted topology : (family DataParallelTopology) .
1286 (lambda unrestricted layout : (family NativeDataParallelLayout) .
1287 (lambda unrestricted role : Nat .
1288 (lambda unrestricted edges : (family StdList (family NativePeerEdge)) .
1289 (lambda unrestricted steps : Nat .
1290 (lambda unrestricted available : Nat .
1291 (lambda unrestricted start : (pi unrestricted extent : Nat . (pi unrestricted tail : (family NativePhysicalCommands) . (family StdResult (family NativeCheckpointFailure) (family NativePhysicalCommands)))) .
1292 (lambda unrestricted publish : (pi unrestricted extent : Nat . (pi unrestricted success : (family NativePhysicalCommands) . (family StdResult (family NativeCheckpointFailure) (family NativePhysicalCommands)))) .
1293 (lambda unrestricted residents : (family ArenaResidents) .
1294 (let unrestricted extent =
1295 (nativePeerEdgesEnd (dpEndpointAt c u system layout role) edges)
1296 in
1297 (let unrestricted placement =
1298 (dpPlacement layout)
1299 in
1300 (eliminate
1301 StdResult
1302 (lambda unrestricted result : (family StdResult Bytes (family NativePhysicalCommands)) .
1303 Bytes)
1304 (planNativePointwiseProgram
1305 c
1306 (dataParallelContributionProgram c u system)
1307 (dpContributionAt c u system layout)
1308 (dpContributionEnd c u system layout)
1309 nativePeerScratchSlot
1310 dpEnd)
1311 (branch StdFailure error . b"")
1312 (branch
1313 StdSuccess
1314 contribution
1315 .
1316 (eliminate
1317 StdResult
1318 (lambda unrestricted result : (family StdResult Bytes (family NativePhysicalCommands)) .
1319 Bytes)
1320 (planNativePointwiseProgram
1321 u
1322 (dataParallelUpdateProgram c u system)
1323 (dpUpdateAt c u system layout)
1324 (dpUpdateEnd c u system layout)
1325 nativePeerScratchSlot
1326 dpEnd)
1327 (branch StdFailure error . b"")
1328 (branch
1329 StdSuccess
1330 update
1331 .
1332 (eliminate
1333 StdResult
1334 (lambda unrestricted result : (family StdResult (family OrderedCombineFailure) (family ParticipantProtocol (family DataParallelRoundOperation) (family RegionTransferIdentity) (family ProtocolNoDecision))) .
1335 Bytes)
1336 (dpProjected c u system topology layout steps)
1337 (branch StdFailure error . b"")
1338 (branch
1339 StdSuccess
1340 projected
1341 .
1342 (eliminate
1343 StdResult
1344 (lambda unrestricted result : (family StdResult (family NativeCheckpointFailure) (family NativePhysicalCommands)) .
1345 Bytes)
1346 (publish
1347 extent
1348 (nativePeerEdgesFold
1349 edges
1350 (lambda unrestricted index : Nat .
1351 (lambda unrestricted edge : (family NativePeerEdge) .
1352 (nativeSocketCloseChecked
1353 (nativeLaunchRecipeSlotValue
1354 (nativePeerEdgeConnectionSlot index))
1355 nativePeerScratchSlot)))
1356 (dpOutput c u system layout)))
1357 (branch StdFailure error . b"")
1358 (branch
1359 StdSuccess
1360 published
1361 .
1362 (nat-eliminate
1363 (lambda unrestricted valid : Nat . Bytes)
1364 b""
1365 (lambda unrestricted previous : Nat .
1366 (lambda unrestricted ignored : Bytes .
1367 (eliminate
1368 StdResult
1369 (lambda unrestricted result : (family StdResult (family NativeCheckpointFailure) (family NativePhysicalCommands)) .
1370 Bytes)
1371 (start
1372 extent
1373 (niFinite
1374 (dpParametersAt layout)
1375 (dpK c u system)
1376 (nativePeerEdgeSetup
1377 role
1378 edges
1379 (dpEndpointAt c u system layout role)
1380 (nativeProtocolFrames
1381 (family DataParallelRoundOperation)
1382 (family RegionTransferIdentity)
1383 (family ProtocolNoDecision)
1384 (lambda unrestricted direction : (family ProtocolDirection) .
1385 (lambda unrestricted identity : (family RegionTransferIdentity) .
1386 (lambda unrestricted value : (family RegionTransferIdentity) .
1387 (nativeFrameInitialize (nativeCombineFrame placement value)))))
1388 projected
1389 (nativeProtocolCommands
1390 (family DataParallelRoundOperation)
1391 (family RegionTransferIdentity)
1392 (family ProtocolNoDecision)
1393 (dpLocal
1394 c
1395 u
1396 system
1397 layout
1398 role
1399 (nativePhysicalProgramComposeCommandsAppend contribution)
1400 (nativePhysicalProgramComposeCommandsAppend update))
1401 (nativeCombineTransfer
1402 placement
1403 (lambda unrestricted peer : Nat .
1404 (nativeLaunchRecipeSlotValue
1405 (nativePeerEdgeConnectionTo edges peer))))
1406 (nativeCombineDecisions placement)
1407 b"data-parallel"
1408 projected
1409 published)))))
1410 (branch StdFailure error . b"")
1411 (branch
1412 StdSuccess
1413 started
1414 .
1415 (nativeHostTargetResourceArtifact
1416 target
1417 resources
1418 (niProgramFor
1419 (nativePeerEdgeSlots edges)
1420 extent
1421 (dpInitialize c u system layout role started)))))))
1422 (naturalAnd
1423 (naturalLessOrEqual extent available)
1424 (arenaCertificate
1425 extent
1426 (nativeCombineResidents
1427 placement
1428 (constructor
1429 ArenaResidents
1430 ArenaResidentsNext
1431 (constructor
1432 ArenaResident
1433 ArenaResidentValue
1434 b"data-parallel-leaf"
1435 (dpLeafAt layout)
1436 (dpValueBytes c u system)
1437 dpWord)
1438 (constructor
1439 ArenaResidents
1440 ArenaResidentsNext
1441 (constructor
1442 ArenaResident
1443 ArenaResidentValue
1444 b"data-parallel-owner-state"
1445 (dpStateAt layout)
1446 (naturalSaturatingSubtract extent (dpStateAt layout))
1447 dpWord)
1448 residents))))))))))))))))))))))))))))))
1449
1450def dpEmit =
1451 (lambda unrestricted target : (family NativeHostTarget) .
1452 (lambda unrestricted resources : (family NativeResourceContext) .
1453 (lambda unrestricted c : Nat .
1454 (lambda unrestricted u : Nat .
1455 (lambda unrestricted system : (family DataParallelSystem c u) .
1456 (lambda unrestricted layout : (family NativeDataParallelLayout) .
1457 (lambda unrestricted star : (family NativeDataParallelStarLayout) .
1458 (lambda unrestricted role : Nat .
1459 (lambda unrestricted edges : (family StdList (family NativePeerEdge)) .
1460 (lambda unrestricted resume : Nat .
1461 (lambda unrestricted steps : Nat .
1462 (lambda unrestricted available : Nat .
1463 (dpEmitWith
1464 target
1465 resources
1466 c
1467 u
1468 system
1469 (constructor DataParallelTopology DataParallelStar)
1470 layout
1471 role
1472 edges
1473 steps
1474 available
1475 (lambda unrestricted extent : Nat .
1476 (lambda unrestricted tail : (family NativePhysicalCommands) .
1477 (dpStart c u system layout star extent resume tail)))
1478 (lambda unrestricted extent : Nat .
1479 (lambda unrestricted success : (family NativePhysicalCommands) .
1480 (planNativePeerRegionPublish
1481 (dpPublication c u system layout star resume edges)
1482 extent
1483 role
1484 success)))
1485 (constructor ArenaResidents ArenaResidentsEnd))))))))))))))
1486
1487def nativeDataParallelArtifact =
1488 (lambda unrestricted target : (family NativeHostTarget) .
1489 (lambda unrestricted resources : (family NativeResourceContext) .
1490 (lambda unrestricted c : Nat .
1491 (lambda unrestricted u : Nat .
1492 (lambda unrestricted system : (family DataParallelSystem c u) .
1493 (lambda unrestricted role : Nat .
1494 (lambda unrestricted addresses : (family StdList Bytes) .
1495 (lambda unrestricted resume : Nat .
1496 (lambda unrestricted epoch : Nat .
1497 (lambda unrestricted steps : Nat .
1498 (lambda unrestricted available : Nat .
1499 (let unrestricted edges =
1500 (nativePeerStarEdges role addresses)
1501 in
1502 (nat-eliminate
1503 (lambda unrestricted valid : Nat . Bytes)
1504 b""
1505 (lambda unrestricted previous : Nat .
1506 (lambda unrestricted ignored : Bytes .
1507 (dpWithStarLayout
1508 c
1509 u
1510 system
1511 role
1512 epoch
1513 available
1514 (lambda unrestricted layout : (family NativeDataParallelLayout) .
1515 (lambda unrestricted star : (family NativeDataParallelStarLayout) .
1516 (dpEmit
1517 target
1518 resources
1519 c
1520 u
1521 system
1522 layout
1523 star
1524 role
1525 edges
1526 resume
1527 steps
1528 available))))))
1529 (dpRunAdmitted c u system role addresses resume epoch steps))))))))))))))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.