1module Runtime.NativeDataParallelOwnedTree
2
3import Learning.DataParallel
4import Learning.Transition
5import Learning.Numerics
6import Runtime.NativeDataParallel
7import Runtime.NativeDataParallelOwned
8import Runtime.NativeCombine
9import Runtime.NativeIndependentState
10import Runtime.NativePeerEndpoint
11import Runtime.NativePeerTree
12import Runtime.NativeHostTarget
13import Runtime.NativeResourcePlan
14import Runtime.NativePhysicalProgram
15import Runtime.NativeMemoryPlan
16import Runtime.RegionTransfer
17import Runtime.RegionFrame
18import Compiler.Planning.RegionFrame
19import Runtime.NativeRegionFrame
20import Runtime.ArenaCertificate
21import Checkpoint.Envelope
22import Checkpoint.NativeEnvelope
23import Checkpoint.NativeRegions
24import Checkpoint.NativePeerPublication
25import Checkpoint.NativeTreePublication
26import Checkpoint.RegionManifest
27import Representation.ParticipantTree
28import Representation.Partition
29import Data.Bytes
30import Std.Foundation
31import Std.List
32import Std.Natural
33
34-- Per-coordinate ownership (Runtime.NativeDataParallelOwned: optimizer state
35-- and, with p = 1, parameters) over a bounded-fan-out hierarchy
36-- (Representation.ParticipantTree) instead of a star:
37-- combine: the sum and the assembly run on the hierarchy's tree
38-- (Runtime.NativeCombine), so a participant exchanges with at most
39-- fanout + 1 peers per combine;
40-- publication: Checkpoint.NativeTreePublication. Every owner writes the
41-- shards of its own words (its coordinates' optimizer state and, when
42-- partitioned, parameters); the root also writes the replicated words
43-- (replicated parameters, shared state). Each commitment carries the
44-- child's capture prefix and replicated words, which the parent compares
45-- with its own, so diverged replicas publish no root, and no owner ever
46-- holds another owner's words;
47-- restore: every owner reads its manifest path, its own shards and, below
48-- the root, only the root's replicated shards.
49-- The checkpoint's identity is the star's for replicated parameters with the
50-- hierarchy's combine order, and for partitioned parameters the learner's
51-- placement-independent identity tagged with the hierarchy's manifest tree.
52family NativeDataParallelOwnedTreeLayout : Type 0
53constructor NativeDataParallelOwnedTreeLayoutOf
54-- template frames, planned for the edge of role 1; every edge's frames share
55-- this storage
56field unrestricted dataParallelOwnedTreeCommitment : (family RegionFrameLayout)
57field unrestricted dataParallelOwnedTreeRelease : (family RegionFrameLayout)
58field unrestricted dataParallelOwnedTreeCheckpoint : (family NativeTreeCheckpoint)
59-- below the root, the root's replicated shards as this owner restores them
60-- (none at the root, whose replicated words are its own shards)
61field unrestricted dataParallelOwnedTreeRootShards : (family NativeRegionCheckpoint)
62
63end-family
64
65def dpotCommitment =
66 (lambda unrestricted tree : (family NativeDataParallelOwnedTreeLayout) .
67 (eliminate
68 NativeDataParallelOwnedTreeLayout
69 (lambda unrestricted current : (family NativeDataParallelOwnedTreeLayout) .
70 (family RegionFrameLayout))
71 tree
72 (branch NativeDataParallelOwnedTreeLayoutOf commitment release checkpoint root . commitment)))
73
74def dpotRelease =
75 (lambda unrestricted tree : (family NativeDataParallelOwnedTreeLayout) .
76 (eliminate
77 NativeDataParallelOwnedTreeLayout
78 (lambda unrestricted current : (family NativeDataParallelOwnedTreeLayout) .
79 (family RegionFrameLayout))
80 tree
81 (branch NativeDataParallelOwnedTreeLayoutOf commitment release checkpoint root . release)))
82
83def dpotCheckpoint =
84 (lambda unrestricted tree : (family NativeDataParallelOwnedTreeLayout) .
85 (eliminate
86 NativeDataParallelOwnedTreeLayout
87 (lambda unrestricted current : (family NativeDataParallelOwnedTreeLayout) .
88 (family NativeTreeCheckpoint))
89 tree
90 (branch NativeDataParallelOwnedTreeLayoutOf commitment release checkpoint root . checkpoint)))
91
92def dpotRootShards =
93 (lambda unrestricted tree : (family NativeDataParallelOwnedTreeLayout) .
94 (eliminate
95 NativeDataParallelOwnedTreeLayout
96 (lambda unrestricted current : (family NativeDataParallelOwnedTreeLayout) .
97 (family NativeRegionCheckpoint))
98 tree
99 (branch NativeDataParallelOwnedTreeLayoutOf commitment release checkpoint root . root)))
100
101def dpotTopology =
102 (lambda unrestricted fanout : Nat .
103 (constructor DataParallelTopology DataParallelHierarchy fanout))
104
105-- ---- who holds which words ----
106-- The one-word intervals of the indices below `count` whose coordinate
107-- (index mod k) this role owns.
108def dpotOwnedWords =
109 (lambda unrestricted k : Nat .
110 (lambda unrestricted owners : Nat .
111 (lambda unrestricted role : Nat .
112 (lambda unrestricted count : Nat .
113 (stdListFold
114 Nat
115 (family StdList (family LogicalInterval))
116 (lambda unrestricted index : Nat .
117 (lambda unrestricted rest : (family StdList (family LogicalInterval)) .
118 (nat-eliminate
119 (lambda unrestricted held : Nat . (family StdList (family LogicalInterval)))
120 rest
121 (lambda unrestricted previous : Nat .
122 (lambda unrestricted ignored : (family StdList (family LogicalInterval)) .
123 (constructor
124 StdList
125 StdListCons
126 (family LogicalInterval)
127 (dpoInterval (naturalMultiply dpWord index) dpWord)
128 rest)))
129 (dpoOwns owners role (naturalModuloUnchecked index k)))))
130 (constructor StdList StdListEmpty (family LogicalInterval))
131 (stdListNaturalsBelow count))))))
132
133-- A partition of `ordinal` when it holds any interval.
134def dpotPart =
135 (lambda unrestricted ordinal : Nat .
136 (lambda unrestricted intervals : (family StdList (family LogicalInterval)) .
137 (lambda unrestricted rest : (family StdList (family CheckpointRegionPartition)) .
138 (nat-eliminate
139 (lambda unrestricted empty : Nat . (family StdList (family CheckpointRegionPartition)))
140 (constructor
141 StdList
142 StdListCons
143 (family CheckpointRegionPartition)
144 (constructor CheckpointRegionPartition CheckpointRegionPartitionOf ordinal intervals)
145 rest)
146 (lambda unrestricted previous : Nat .
147 (lambda unrestricted ignored : (family StdList (family CheckpointRegionPartition)) .
148 rest))
149 (naturalIsZero (stdListLength (family LogicalInterval) intervals))))))
150
151def dpotWhole =
152 (lambda unrestricted held : Nat .
153 (lambda unrestricted bytes : Nat .
154 (nat-eliminate
155 (lambda unrestricted current : Nat . (family StdList (family LogicalInterval)))
156 (constructor StdList StdListEmpty (family LogicalInterval))
157 (lambda unrestricted previous : Nat .
158 (lambda unrestricted ignored : (family StdList (family LogicalInterval)) .
159 (constructor
160 StdList
161 StdListCons
162 (family LogicalInterval)
163 (dpoInterval 0 bytes)
164 (constructor StdList StdListEmpty (family LogicalInterval)))))
165 held)))
166
167-- The replicated words the root alone publishes: the parameters when they
168-- are replicated, then the shared state.
169def dpotReplicatedOf =
170 (lambda unrestricted c : Nat .
171 (lambda unrestricted u : Nat .
172 (lambda unrestricted system : (family DataParallelSystem c u) .
173 (lambda unrestricted q : Nat .
174 (lambda unrestricted p : Nat .
175 (let unrestricted shared =
176 (dpoShared c u system q)
177 in
178 (dpotPart
179 0
180 (dpotWhole (naturalIsZero p) (dpParameterBytes c u system))
181 (dpotPart
182 dpoSharedOrdinal
183 (dpotWhole (naturalNonzero shared) (naturalMultiply dpWord shared))
184 (constructor StdList StdListEmpty (family CheckpointRegionPartition))))))))))
185
186-- A role's own partitions, in region order: its parameter words (all of them
187-- at the root when replicated), the shared state at the root, its
188-- coordinates' optimizer-state words.
189def dpotOwnOf =
190 (lambda unrestricted c : Nat .
191 (lambda unrestricted u : Nat .
192 (lambda unrestricted system : (family DataParallelSystem c u) .
193 (lambda unrestricted q : Nat .
194 (lambda unrestricted p : Nat .
195 (lambda unrestricted role : Nat .
196 (let unrestricted k =
197 (dpK c u system)
198 in
199 (let unrestricted owners =
200 (dpOwners c u system)
201 in
202 (let unrestricted shared =
203 (dpoShared c u system q)
204 in
205 (let unrestricted root =
206 (naturalIsZero role)
207 in
208 (dpotPart
209 0
210 (nat-eliminate
211 (lambda unrestricted current : Nat .
212 (family StdList (family LogicalInterval)))
213 (dpotWhole root (dpParameterBytes c u system))
214 (lambda unrestricted previous : Nat .
215 (lambda unrestricted ignored : (family StdList (family LogicalInterval)) .
216 (dpotOwnedWords k owners role k)))
217 p)
218 (dpotPart
219 dpoSharedOrdinal
220 (dpotWhole
221 (naturalAnd root (naturalNonzero shared))
222 (naturalMultiply dpWord shared))
223 (dpotPart
224 (dpoCoordinateOrdinal shared)
225 (dpotOwnedWords k owners role (naturalMultiply q k))
226 (constructor StdList StdListEmpty (family CheckpointRegionPartition)))))))))))))))
227
228-- The global shard number of a word (dpoPartitions' order: parameters, one
229-- per word when partitioned; shared state; coordinate words), which names
230-- its file.
231def dpotGlobalOf =
232 (lambda unrestricted c : Nat .
233 (lambda unrestricted u : Nat .
234 (lambda unrestricted system : (family DataParallelSystem c u) .
235 (lambda unrestricted q : Nat .
236 (lambda unrestricted p : Nat .
237 (lambda unrestricted ordinal : Nat .
238 (lambda unrestricted begin : Nat .
239 (let unrestricted shared =
240 (dpoShared c u system q)
241 in
242 (let unrestricted word =
243 (naturalDivideUnchecked begin dpWord)
244 in
245 (let unrestricted parameters =
246 (naturalSelect p (dpK c u system) 1)
247 in
248 (naturalSelect
249 (naturalIsZero ordinal)
250 (naturalSelect p word 0)
251 (naturalSelect
252 (naturalEqual ordinal (dpoCoordinateOrdinal shared))
253 (naturalAdd (naturalAdd parameters (naturalNonzero shared)) word)
254 parameters))))))))))))
255
256-- The global shard numbers of a role's own shards, in its record order.
257def dpotOwnGlobals =
258 (lambda unrestricted c : Nat .
259 (lambda unrestricted u : Nat .
260 (lambda unrestricted system : (family DataParallelSystem c u) .
261 (lambda unrestricted q : Nat .
262 (lambda unrestricted p : Nat .
263 (lambda unrestricted role : Nat .
264 (stdListFold
265 (family CheckpointRegionPartition)
266 (family StdList Nat)
267 (lambda unrestricted part : (family CheckpointRegionPartition) .
268 (lambda unrestricted rest : (family StdList Nat) .
269 (stdListAppend
270 Nat
271 (stdListMap
272 (family LogicalInterval)
273 Nat
274 (lambda unrestricted interval : (family LogicalInterval) .
275 (dpotGlobalOf
276 c
277 u
278 system
279 q
280 p
281 (checkpointPartitionOrdinal part)
282 (intervalBegin interval)))
283 (checkpointPartitionIntervals part))
284 rest)))
285 (constructor StdList StdListEmpty Nat)
286 (dpotOwnOf c u system q p role))))))))
287
288def dpotNth =
289 (lambda unrestricted values : (family StdList Nat) .
290 (lambda unrestricted index : Nat . (stdListHeadOr Nat 0 (stdListDrop Nat index values))))
291
292-- argv for n owners and h global shards, positions after the program name:
293-- 1 the previous root manifest; 1 + r the previous group manifest of role
294-- r >= 1; n + 1 + g the previous shard g; n + 1 + h + 2r and n + 2 + h + 2r
295-- the candidate and committed group manifest of role r (role 0's is the
296-- published root); 3n + 1 + h + 2g and 3n + 2 + h + 2g the candidate and
297-- committed shard g; 3n + 1 + 3h the generation directory. Every owner
298-- receives the same argv; a role's own shard j is the global shard its
299-- record names.
300def dpotPaths =
301 (lambda unrestricted c : Nat .
302 (lambda unrestricted u : Nat .
303 (lambda unrestricted system : (family DataParallelSystem c u) .
304 (lambda unrestricted q : Nat .
305 (lambda unrestricted p : Nat .
306 (lambda unrestricted role : Nat .
307 (let unrestricted owners =
308 (dpOwners c u system)
309 in
310 (let unrestricted shards =
311 (dpoShardCount c u system q p)
312 in
313 (let unrestricted groups =
314 (naturalAdd (succ owners) shards)
315 in
316 (let unrestricted outputs =
317 (naturalAdd (succ (naturalMultiply 3 owners)) shards)
318 in
319 (let unrestricted globals =
320 (dpotOwnGlobals c u system q p role)
321 in
322 (constructor
323 NativeTreePaths
324 NativeTreePathsOf
325 (lambda unrestricted at : Nat . (succ at))
326 (lambda unrestricted index : Nat .
327 (succ (naturalAdd owners (dpotNth globals index))))
328 (naturalAdd groups (naturalMultiply 2 role))
329 (succ (naturalAdd groups (naturalMultiply 2 role)))
330 (lambda unrestricted index : Nat .
331 (naturalAdd outputs (naturalMultiply 2 (dpotNth globals index))))
332 (lambda unrestricted index : Nat .
333 (succ (naturalAdd outputs (naturalMultiply 2 (dpotNth globals index)))))
334 (naturalAdd (succ (naturalMultiply 3 owners)) (naturalMultiply 3 shards))))))))))))))
335
336-- ---- publication frames ----
337def dpotIdentity =
338 (lambda unrestricted c : Nat .
339 (lambda unrestricted u : Nat .
340 (lambda unrestricted system : (family DataParallelSystem c u) .
341 (lambda unrestricted digest : Bytes .
342 (lambda unrestricted q : Nat .
343 (lambda unrestricted p : Nat .
344 (lambda unrestricted operation : Nat .
345 (lambda unrestricted sender : Nat .
346 (lambda unrestricted receiver : Nat .
347 (constructor
348 RegionTransferIdentity
349 RegionTransferIdentityOf
350 digest
351 b"data-parallel-owned-tree-publication-v1"
352 b"replicated-words"
353 b"finite-f64-rne-separate"
354 (constructor LearningRound LearningRoundOf 1 0)
355 operation
356 sender
357 receiver
358 (constructor
359 LogicalInterval
360 LogicalIntervalOf
361 0
362 (dpoAgreedBytes c u system q p))))))))))))
363
364def dpotParent =
365 (lambda unrestricted fanout : Nat .
366 (lambda unrestricted count : Nat .
367 (lambda unrestricted role : Nat .
368 (participantTreeParentOf (participantTreeNode fanout count role)))))
369
370def dpotCommitmentBytes =
371 (lambda unrestricted c : Nat .
372 (lambda unrestricted u : Nat .
373 (lambda unrestricted system : (family DataParallelSystem c u) .
374 (lambda unrestricted q : Nat .
375 (lambda unrestricted p : Nat .
376 (nativeTreeCommitmentBytesOf (dpoAgreedBytes c u system q p)))))))
377
378def dpotCommitmentFor =
379 (lambda unrestricted c : Nat .
380 (lambda unrestricted u : Nat .
381 (lambda unrestricted system : (family DataParallelSystem c u) .
382 (lambda unrestricted digest : Bytes .
383 (lambda unrestricted q : Nat .
384 (lambda unrestricted p : Nat .
385 (lambda unrestricted fanout : Nat .
386 (lambda unrestricted tree : (family NativeDataParallelOwnedTreeLayout) .
387 (lambda unrestricted child : Nat .
388 (niFrameAt
389 (dpotIdentity
390 c
391 u
392 system
393 digest
394 q
395 p
396 2
397 child
398 (dpotParent fanout (dpOwners c u system) child))
399 (dpotCommitmentBytes c u system q p)
400 (dpotCommitment tree)))))))))))
401
402def dpotReleaseFor =
403 (lambda unrestricted c : Nat .
404 (lambda unrestricted u : Nat .
405 (lambda unrestricted system : (family DataParallelSystem c u) .
406 (lambda unrestricted digest : Bytes .
407 (lambda unrestricted q : Nat .
408 (lambda unrestricted p : Nat .
409 (lambda unrestricted fanout : Nat .
410 (lambda unrestricted tree : (family NativeDataParallelOwnedTreeLayout) .
411 (lambda unrestricted child : Nat .
412 (niFrameAt
413 (dpotIdentity
414 c
415 u
416 system
417 digest
418 q
419 p
420 3
421 (dpotParent fanout (dpOwners c u system) child)
422 child)
423 dpWord
424 (dpotRelease tree)))))))))))
425
426-- ---- layout ----
427-- Below the root, the root's replicated shards' layouts after this role's
428-- tree checkpoint; none at the root or when nothing is replicated.
429def dpotPlanRootShards =
430 (lambda unrestricted c : Nat .
431 (lambda unrestricted u : Nat .
432 (lambda unrestricted system : (family DataParallelSystem c u) .
433 (lambda unrestricted identity : Bytes .
434 (lambda unrestricted q : Nat .
435 (lambda unrestricted p : Nat .
436 (lambda unrestricted fanout : Nat .
437 (lambda unrestricted role : Nat .
438 (lambda unrestricted checkpoint : (family NativeTreeCheckpoint) .
439 (lambda unrestricted available : Nat .
440 (let unrestricted base =
441 (nativeCheckpointAlign (nativeTreeEnd checkpoint))
442 in
443 (nat-eliminate
444 (lambda unrestricted current : Nat .
445 (family
446 StdResult
447 (family NativeCheckpointFailure)
448 (family NativeRegionCheckpoint)))
449 (constructor
450 StdResult
451 StdSuccess
452 (family NativeCheckpointFailure)
453 (family NativeRegionCheckpoint)
454 (constructor
455 NativeRegionCheckpoint
456 NativeRegionCheckpointOf
457 (nativeTreeGroup checkpoint)
458 (constructor StdList StdListEmpty (family NativeRegionShard))
459 (nativeTreeEpoch checkpoint)
460 base))
461 (lambda unrestricted previous : Nat .
462 (lambda unrestricted ignored : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) .
463 (planNativeTreeRootShards
464 (dpoContext c u system q p (dpotTopology fanout) identity)
465 (dpoRegions c u system q)
466 (lambda unrestricted owner : Nat .
467 (dpotReplicatedOf c u system q p))
468 checkpoint
469 base
470 available)))
471 (naturalAnd
472 (naturalNonzero role)
473 (naturalNonzero
474 (stdListLength
475 (family CheckpointRegionPartition)
476 (dpotReplicatedOf c u system q p))))))))))))))))
477
478-- The root's record number of its first replicated shard: they follow its
479-- own parameter words when parameters are partitioned.
480def dpotReplicatedFirst =
481 (lambda unrestricted c : Nat .
482 (lambda unrestricted u : Nat .
483 (lambda unrestricted system : (family DataParallelSystem c u) .
484 (lambda unrestricted p : Nat .
485 (naturalMultiply
486 p
487 (stdListLength
488 (family LogicalInterval)
489 (dpotOwnedWords (dpK c u system) (dpOwners c u system) 0 (dpK c u system))))))))
490
491-- Combine storage (the sum, the assembly, this owner's offer and read
492-- replica), then the edge frames, the tree checkpoint and the root's
493-- replicated shard layouts, then the owner state.
494def dpotWithLayout =
495 (lambda unrestricted c : Nat .
496 (lambda unrestricted u : Nat .
497 (lambda unrestricted system : (family DataParallelSystem c u) .
498 (lambda unrestricted q : Nat .
499 (lambda unrestricted p : Nat .
500 (lambda unrestricted g : Nat .
501 (lambda unrestricted fanout : Nat .
502 (lambda unrestricted role : Nat .
503 (lambda unrestricted epoch : Nat .
504 (lambda unrestricted available : Nat .
505 (lambda unrestricted emit : (pi unrestricted layout : (family NativeDataParallelOwnedLayout) . (pi unrestricted tree : (family NativeDataParallelOwnedTreeLayout) . Bytes)) .
506 (let unrestricted digest =
507 (dpIdentityDigest c u system)
508 in
509 (let unrestricted contextDigest =
510 (dpoContextDigest c u system p digest)
511 in
512 (let unrestricted sum =
513 (dpPlacementFor c u system digest (dpotTopology fanout) role)
514 in
515 (let unrestricted assemble =
516 (dpoAssemblePlacementFor
517 c
518 u
519 system
520 digest
521 (dpotTopology fanout)
522 role
523 sum)
524 in
525 (let unrestricted gradients =
526 (dpoGradientsFor
527 c
528 u
529 system
530 g
531 digest
532 (dpotTopology fanout)
533 role
534 (dpoPublicationStart c u system p assemble))
535 in
536 (eliminate
537 StdResult
538 (lambda unrestricted result : (family StdResult (family RegionFrameLayoutFailure) (family RegionFrameLayout)) .
539 Bytes)
540 (planRegionFrameLayout
541 (dpotIdentity c u system digest q p 2 1 0)
542 (dpotCommitmentBytes c u system q p)
543 512
544 (dpoGradientsEnd
545 c
546 u
547 system
548 gradients
549 (dpoPublicationStart c u system p assemble))
550 available)
551 (branch StdFailure error . b"")
552 (branch
553 StdSuccess
554 commitment
555 .
556 (eliminate
557 StdResult
558 (lambda unrestricted result : (family StdResult (family RegionFrameLayoutFailure) (family RegionFrameLayout)) .
559 Bytes)
560 (planRegionFrameLayout
561 (dpotIdentity c u system digest q p 3 0 1)
562 dpWord
563 512
564 (frameAlign (frameEnd commitment))
565 available)
566 (branch StdFailure error . b"")
567 (branch
568 StdSuccess
569 release
570 .
571 (eliminate
572 StdResult
573 (lambda unrestricted result : (family StdResult (family NativeCheckpointFailure) (family NativeTreeCheckpoint)) .
574 Bytes)
575 (planNativeTreeCheckpoint
576 (dpoContext
577 c
578 u
579 system
580 q
581 p
582 (dpotTopology fanout)
583 contextDigest)
584 (dpoRegions c u system q)
585 fanout
586 (dpOwners c u system)
587 role
588 (dpotOwnOf c u system q p)
589 epoch
590 (frameAlign (frameEnd release))
591 available)
592 (branch StdFailure error . b"")
593 (branch
594 StdSuccess
595 checkpoint
596 .
597 (eliminate
598 StdResult
599 (lambda unrestricted result : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) .
600 Bytes)
601 (dpotPlanRootShards
602 c
603 u
604 system
605 contextDigest
606 q
607 p
608 fanout
609 role
610 checkpoint
611 available)
612 (branch StdFailure error . b"")
613 (branch
614 StdSuccess
615 root
616 .
617 (emit
618 (constructor
619 NativeDataParallelOwnedLayout
620 NativeDataParallelOwnedLayoutOf
621 sum
622 assemble
623 (nativeCheckpointAlign (nativeRegionEnd root))
624 (nativeTreeEpoch checkpoint)
625 digest
626 gradients)
627 (constructor
628 NativeDataParallelOwnedTreeLayout
629 NativeDataParallelOwnedTreeLayoutOf
630 commitment
631 release
632 checkpoint
633 root))))))))))))))))))))))))))
634
635-- ---- start, publication ----
636-- Fresh: the declared words. Resume: the verified manifest path, this
637-- owner's own shards and, below the root, the root's replicated shards, then
638-- the restored prefix and a new membership epoch.
639def dpotStart =
640 (lambda unrestricted c : Nat .
641 (lambda unrestricted u : Nat .
642 (lambda unrestricted system : (family DataParallelSystem c u) .
643 (lambda unrestricted q : Nat .
644 (lambda unrestricted p : Nat .
645 (lambda unrestricted layout : (family NativeDataParallelOwnedLayout) .
646 (lambda unrestricted tree : (family NativeDataParallelOwnedTreeLayout) .
647 (lambda unrestricted fanout : Nat .
648 (lambda unrestricted role : Nat .
649 (lambda unrestricted resume : Nat .
650 (lambda unrestricted tail : (family NativePhysicalCommands) .
651 (let unrestricted checkpoint =
652 (dpotCheckpoint tree)
653 in
654 (let unrestricted owners =
655 (dpOwners c u system)
656 in
657 (let unrestricted destination =
658 (lambda unrestricted shard : (family NativeRegionShard) .
659 (naturalAdd
660 (dpoStateAt layout)
661 (dpoShardOffset c u system q p shard)))
662 in
663 (let unrestricted rootGlobals =
664 (dpotOwnGlobals c u system q p 0)
665 in
666 (constructor
667 StdResult
668 StdSuccess
669 (family NativeCheckpointFailure)
670 (family NativePhysicalCommands)
671 (nat-eliminate
672 (lambda unrestricted mode : Nat .
673 (family NativePhysicalCommands))
674 (dpoFresh c u system q p layout role tail)
675 (lambda unrestricted previous : Nat .
676 (lambda unrestricted ignored : (family NativePhysicalCommands) .
677 (nativeTreeRestoreManifests
678 checkpoint
679 fanout
680 owners
681 role
682 (dpotOwnOf c u system q p)
683 (dpotPaths c u system q p role)
684 (nativeTreeRestoreOwn
685 checkpoint
686 (dpotPaths c u system q p role)
687 destination
688 (nativeTreeRestoreShardsFrom
689 (nativeTreeRootLayout checkpoint)
690 (dpotReplicatedFirst c u system p)
691 (nativeRegionShards (dpotRootShards tree))
692 (lambda unrestricted index : Nat .
693 (succ (naturalAdd owners (dpotNth rootGlobals index))))
694 destination
695 (dpResumed
696 (dpoGeneric layout)
697 (nativeTreeRestoredCaptureAt checkpoint)
698 tail))))))
699 resume)))))))))))))))))
700
701-- Every edge's frames share the template's storage exactly.
702def dpotFramesAdmitted =
703 (lambda unrestricted c : Nat .
704 (lambda unrestricted u : Nat .
705 (lambda unrestricted system : (family DataParallelSystem c u) .
706 (lambda unrestricted digest : Bytes .
707 (lambda unrestricted q : Nat .
708 (lambda unrestricted p : Nat .
709 (lambda unrestricted fanout : Nat .
710 (lambda unrestricted tree : (family NativeDataParallelOwnedTreeLayout) .
711 (stdListFold
712 Nat
713 Nat
714 (lambda unrestricted index : Nat .
715 (lambda unrestricted rest : Nat .
716 (naturalAnd
717 rest
718 (naturalAnd
719 (naturalEqual
720 (frameEnd
721 (dpotCommitmentFor c u system digest q p fanout tree (succ index)))
722 (frameEnd (dpotCommitment tree)))
723 (naturalEqual
724 (frameEnd
725 (dpotReleaseFor c u system digest q p fanout tree (succ index)))
726 (frameEnd (dpotRelease tree)))))))
727 1
728 (stdListNaturalsBelow (naturalPredecessor (dpOwners c u system))))))))))))
729
730-- After the last update: the tree publication of this generation, under the
731-- new membership epoch after a resume. Every owner's shards are read from its
732-- own state; commitments carry the capture prefix and replicated words.
733def dpotPublish =
734 (lambda unrestricted c : Nat .
735 (lambda unrestricted u : Nat .
736 (lambda unrestricted system : (family DataParallelSystem c u) .
737 (lambda unrestricted q : Nat .
738 (lambda unrestricted p : Nat .
739 (lambda unrestricted layout : (family NativeDataParallelOwnedLayout) .
740 (lambda unrestricted tree : (family NativeDataParallelOwnedTreeLayout) .
741 (lambda unrestricted fanout : Nat .
742 (lambda unrestricted role : Nat .
743 (lambda unrestricted edges : (family StdList (family NativePeerEdge)) .
744 (lambda unrestricted resume : Nat .
745 (lambda unrestricted success : (family NativePhysicalCommands) .
746 (nat-eliminate
747 (lambda unrestricted valid : Nat .
748 (family
749 StdResult
750 (family NativeCheckpointFailure)
751 (family NativePhysicalCommands)))
752 (constructor
753 StdResult
754 StdFailure
755 (family NativeCheckpointFailure)
756 (family NativePhysicalCommands)
757 (constructor NativeCheckpointFailure NativeCheckpointBounds))
758 (lambda unrestricted previous : Nat .
759 (lambda unrestricted ignored : (family StdResult (family NativeCheckpointFailure) (family NativePhysicalCommands)) .
760 (constructor
761 StdResult
762 StdSuccess
763 (family NativeCheckpointFailure)
764 (family NativePhysicalCommands)
765 (nativeTreePublish
766 (nativeTreeCheckpointAdvanced (dpotCheckpoint tree) resume)
767 fanout
768 (dpOwners c u system)
769 role
770 edges
771 (dpotCommitmentFor
772 c
773 u
774 system
775 (dpoDigest layout)
776 q
777 p
778 fanout
779 tree)
780 (dpotReleaseFor c u system (dpoDigest layout) q p fanout tree)
781 (dpoStateAt layout)
782 (dpoAgreedBytes c u system q p)
783 (dpoShardOffset c u system q p)
784 (dpotPaths c u system q p role)
785 success))))
786 (dpotFramesAdmitted c u system (dpoDigest layout) q p fanout tree))))))))))))))
787
788-- The publication's arena: both frame templates, the tree checkpoint's
789-- staging and, below the root, the root's replicated shard layouts.
790def dpotResidents =
791 (lambda unrestricted layout : (family NativeDataParallelOwnedLayout) .
792 (lambda unrestricted tree : (family NativeDataParallelOwnedTreeLayout) .
793 (let unrestricted staged =
794 (nativeTreeResidents (dpotCheckpoint tree))
795 in
796 (let unrestricted rootBase =
797 (nativeCheckpointAlign (nativeTreeEnd (dpotCheckpoint tree)))
798 in
799 (let unrestricted rootBytes =
800 (naturalSaturatingSubtract (nativeRegionEnd (dpotRootShards tree)) rootBase)
801 in
802 (constructor
803 ArenaResidents
804 ArenaResidentsNext
805 (constructor
806 ArenaResident
807 ArenaResidentValue
808 b"tree-commitment-frame"
809 (frameBase (dpotCommitment tree))
810 (naturalSaturatingSubtract
811 (frameEnd (dpotCommitment tree))
812 (frameBase (dpotCommitment tree)))
813 1)
814 (constructor
815 ArenaResidents
816 ArenaResidentsNext
817 (constructor
818 ArenaResident
819 ArenaResidentValue
820 b"tree-release-frame"
821 (frameBase (dpotRelease tree))
822 (naturalSaturatingSubtract
823 (frameEnd (dpotRelease tree))
824 (frameBase (dpotRelease tree)))
825 1)
826 (nat-eliminate
827 (lambda unrestricted current : Nat . (family ArenaResidents))
828 staged
829 (lambda unrestricted previous : Nat .
830 (lambda unrestricted ignored : (family ArenaResidents) .
831 (constructor
832 ArenaResidents
833 ArenaResidentsNext
834 (constructor
835 ArenaResident
836 ArenaResidentValue
837 b"tree-root-shards"
838 rootBase
839 rootBytes
840 nativeCheckpointWordBytes)
841 staged)))
842 (naturalNonzero rootBytes)))))))))
843
844def dpotRunAdmitted =
845 (lambda unrestricted c : Nat .
846 (lambda unrestricted u : Nat .
847 (lambda unrestricted system : (family DataParallelSystem c u) .
848 (lambda unrestricted q : Nat .
849 (lambda unrestricted p : Nat .
850 (lambda unrestricted g : Nat .
851 (lambda unrestricted fanout : Nat .
852 (lambda unrestricted role : Nat .
853 (lambda unrestricted addresses : (family StdList Bytes) .
854 (lambda unrestricted resume : Nat .
855 (lambda unrestricted epoch : Nat .
856 (lambda unrestricted steps : Nat .
857 (naturalAnd
858 (dataParallelAdmitted c u system)
859 (naturalAnd
860 (nativePeerTreeListedAdmitted
861 fanout
862 (dpOwners c u system)
863 role
864 addresses)
865 (naturalAnd
866 (naturalLessOrEqual resume 1)
867 (naturalAnd
868 (naturalNonzero epoch)
869 (naturalAnd
870 (naturalBelowTwoPower 64 (naturalAdd epoch resume))
871 (naturalAnd
872 (naturalNonzero steps)
873 (naturalAnd
874 (naturalBelowTwoPower 64 steps)
875 (naturalAnd
876 (naturalAnd
877 (naturalLessOrEqual p 1)
878 (naturalLessOrEqual g 1))
879 (dataParallelSeparable c u system q)))))))))))))))))))))
880
881-- One owner of the hierarchy, for `target`.
882def nativeDataParallelOwnedTreeArtifact =
883 (lambda unrestricted target : (family NativeHostTarget) .
884 (lambda unrestricted resources : (family NativeResourceContext) .
885 (lambda unrestricted c : Nat .
886 (lambda unrestricted u : Nat .
887 (lambda unrestricted system : (family DataParallelSystem c u) .
888 (lambda unrestricted q : Nat .
889 (lambda unrestricted p : Nat .
890 (lambda unrestricted g : Nat .
891 (lambda unrestricted fanout : Nat .
892 (lambda unrestricted role : Nat .
893 (lambda unrestricted addresses : (family StdList Bytes) .
894 (lambda unrestricted resume : Nat .
895 (lambda unrestricted epoch : Nat .
896 (lambda unrestricted steps : Nat .
897 (lambda unrestricted available : Nat .
898 (let unrestricted edges =
899 (nativePeerTreeEdgesListed
900 fanout
901 (dpOwners c u system)
902 role
903 addresses)
904 in
905 (nat-eliminate
906 (lambda unrestricted valid : Nat . Bytes)
907 b""
908 (lambda unrestricted previous : Nat .
909 (lambda unrestricted ignored : Bytes .
910 (dpotWithLayout
911 c
912 u
913 system
914 q
915 p
916 g
917 fanout
918 role
919 epoch
920 available
921 (lambda unrestricted layout : (family NativeDataParallelOwnedLayout) .
922 (lambda unrestricted tree : (family NativeDataParallelOwnedTreeLayout) .
923 (dpoEmitWith
924 target
925 resources
926 c
927 u
928 system
929 q
930 p
931 (dpotTopology fanout)
932 layout
933 role
934 edges
935 steps
936 available
937 (lambda unrestricted extent : Nat .
938 (lambda unrestricted tail : (family NativePhysicalCommands) .
939 (dpotStart
940 c
941 u
942 system
943 q
944 p
945 layout
946 tree
947 fanout
948 role
949 resume
950 tail)))
951 (lambda unrestricted extent : Nat .
952 (lambda unrestricted success : (family NativePhysicalCommands) .
953 (dpotPublish
954 c
955 u
956 system
957 q
958 p
959 layout
960 tree
961 fanout
962 role
963 edges
964 resume
965 success)))
966 (dpotResidents layout tree)))))))
967 (dpotRunAdmitted
968 c
969 u
970 system
971 q
972 p
973 g
974 fanout
975 role
976 addresses
977 resume
978 epoch
979 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.