Compile the contribution program and this owner's part of the update
program, project the round protocol under `topology` and emit one owner's
executable for `target`. `start extent tail` begins the owner (fresh or
restored); `publish extent success` publishes after the last update and
continues with `success`; `residents` are the topology's publication
storage.
2554def dpoEmitWith =
2555 (lambda unrestricted target : (family NativeHostTarget) .
2556 (lambda unrestricted resources : (family NativeResourceContext) .
2557 (lambda unrestricted c : Nat .
2558 (lambda unrestricted u : Nat .
2559 (lambda unrestricted system : (family DataParallelSystem c u) .
2560 (lambda unrestricted q : Nat .
2561 (lambda unrestricted p : Nat .
2562 (lambda unrestricted topology : (family DataParallelTopology) .
2563 (lambda unrestricted layout : (family NativeDataParallelOwnedLayout) .
2564 (lambda unrestricted role : Nat .
2565 (lambda unrestricted edges : (family StdList (family NativePeerEdge)) .
2566 (lambda unrestricted steps : Nat .
2567 (lambda unrestricted available : Nat .
2568 (lambda unrestricted start : (pi unrestricted extent : Nat . (pi unrestricted tail : (family NativePhysicalCommands) . (family StdResult (family NativeCheckpointFailure) (family NativePhysicalCommands)))) .
2569 (lambda unrestricted publish : (pi unrestricted extent : Nat . (pi unrestricted success : (family NativePhysicalCommands) . (family StdResult (family NativeCheckpointFailure) (family NativePhysicalCommands)))) .
2570 (lambda unrestricted residents : (family ArenaResidents) .
2571 (let unrestricted generic =
2572 (dpoGeneric layout)
2573 in
2574 (let unrestricted extent =
2575 (nativePeerEdgesEnd
2576 (dpEndpointAt c u system generic role)
2577 edges)
2578 in
2579 (eliminate
2580 StdResult
2581 (lambda unrestricted result : (family StdResult Bytes (family NativePhysicalCommands)) .
2582 Bytes)
2583 (planNativePointwiseProgram
2584 c
2585 (dataParallelContributionProgram c u system)
2586 (dpContributionAt c u system generic)
2587 (dpContributionEnd c u system generic)
2588 nativePeerScratchSlot
2589 dpEnd)
2590 (branch StdFailure error . b"")
2591 (branch
2592 StdSuccess
2593 contribution
2594 .
2595 (eliminate
2596 StdResult
2597 (lambda unrestricted result : (family StdResult Bytes (family NativePhysicalCommands)) .
2598 Bytes)
2599 (planNativePointwiseProgram
2600 u
2601 (dataParallelOwnedProgram
2602 c
2603 u
2604 system
2605 q
2606 (dpoOwns (dpOwners c u system) role))
2607 (dpUpdateAt c u system generic)
2608 (dpUpdateEnd c u system generic)
2609 nativePeerScratchSlot
2610 dpEnd)
2611 (branch StdFailure error . b"")
2612 (branch
2613 StdSuccess
2614 update
2615 .
2616 (eliminate
2617 StdResult
2618 (lambda unrestricted result : (family StdResult (family OrderedCombineFailure) (family ParticipantProtocol (family DataParallelOwnedOperation) (family RegionTransferIdentity) (family ProtocolNoDecision))) .
2619 Bytes)
2620 (dpoProjected c u system p topology layout steps)
2621 (branch StdFailure error . b"")
2622 (branch
2623 StdSuccess
2624 projected
2625 .
2626 (eliminate
2627 StdResult
2628 (lambda unrestricted result : (family StdResult (family NativeCheckpointFailure) (family NativePhysicalCommands)) .
2629 Bytes)
2630 (publish
2631 extent
2632 (nativePeerEdgesFold
2633 edges
2634 (lambda unrestricted index : Nat .
2635 (lambda unrestricted edge : (family NativePeerEdge) .
2636 (nativeSocketCloseChecked
2637 (nativeLaunchRecipeSlotValue
2638 (nativePeerEdgeConnectionSlot index))
2639 nativePeerScratchSlot)))
2640 (dpoOutput c u system q p layout)))
2641 (branch StdFailure error . b"")
2642 (branch
2643 StdSuccess
2644 published
2645 .
2646 (nat-eliminate
2647 (lambda unrestricted valid : Nat . Bytes)
2648 b""
2649 (lambda unrestricted previous : Nat .
2650 (lambda unrestricted ignored : Bytes .
2651 (eliminate
2652 StdResult
2653 (lambda unrestricted result : (family StdResult (family NativeCheckpointFailure) (family NativePhysicalCommands)) .
2654 Bytes)
2655 (start
2656 extent
2657 (niFinite
2658 (naturalSelect
2659 p
2660 (dpoOwnedAt c u system q p layout)
2661 (dpoParametersAt layout))
2662 (naturalSelect
2663 p
2664 (dpoPerOwner (dpK c u system) (dpOwners c u system))
2665 (dpK c u system))
2666 (nativePeerEdgeSetup
2667 role
2668 edges
2669 (dpEndpointAt c u system generic role)
2670 (nativeProtocolFrames
2671 (family DataParallelOwnedOperation)
2672 (family RegionTransferIdentity)
2673 (family ProtocolNoDecision)
2674 (lambda unrestricted direction : (family ProtocolDirection) .
2675 (lambda unrestricted identity : (family RegionTransferIdentity) .
2676 (lambda unrestricted value : (family RegionTransferIdentity) .
2677 (nativeFrameInitialize
2678 (nativeCombineFrame (dpoPlacementOf layout value) value)))))
2679 projected
2680 (nativeProtocolCommands
2681 (family DataParallelOwnedOperation)
2682 (family RegionTransferIdentity)
2683 (family ProtocolNoDecision)
2684 (dpoLocal
2685 c
2686 u
2687 system
2688 q
2689 p
2690 layout
2691 role
2692 (nativePhysicalProgramComposeCommandsAppend contribution)
2693 (nativePhysicalProgramComposeCommandsAppend update))
2694 (lambda unrestricted direction : (family ProtocolDirection) .
2695 (lambda unrestricted identity : (family RegionTransferIdentity) .
2696 (lambda unrestricted value : (family RegionTransferIdentity) .
2697 (nativeCombineTransfer
2698 (dpoPlacementOf layout value)
2699 (lambda unrestricted peer : Nat .
2700 (nativeLaunchRecipeSlotValue
2701 (nativePeerEdgeConnectionTo edges peer)))
2702 direction
2703 identity
2704 value))))
2705 (nativeCombineDecisions (dpoSum layout))
2706 b"data-parallel-owned"
2707 projected
2708 published)))))
2709 (branch StdFailure error . b"")
2710 (branch
2711 StdSuccess
2712 started
2713 .
2714 (nativeHostTargetResourceArtifact
2715 target
2716 resources
2717 (niProgramFor
2718 (nativePeerEdgeSlots edges)
2719 extent
2720 (dpInitialize c u system generic role started)))))))
2721 (naturalAnd
2722 (naturalLessOrEqual extent available)
2723 (arenaCertificate
2724 extent
2725 (nativeCombineResidents
2726 (dpoSum layout)
2727 (constructor
2728 ArenaResidents
2729 ArenaResidentsNext
2730 (constructor
2731 ArenaResident
2732 ArenaResidentValue
2733 b"data-parallel-leaf"
2734 (dpLeafAt generic)
2735 (dpValueBytes c u system)
2736 dpWord)
2737 (nativeCombineResidents
2738 (dpoAssemblePlacement layout)
2739 (constructor
2740 ArenaResidents
2741 ArenaResidentsNext
2742 (constructor
2743 ArenaResident
2744 ArenaResidentValue
2745 b"data-parallel-offer"
2746 (nativeCombineRegionEnd (dpoAssemblePlacement layout))
2747 (dpoOfferBytes c u system)
2748 dpWord)
2749 (dpoReplicaResidents
2750 c
2751 u
2752 system
2753 p
2754 layout
2755 (dpoGradientResidents
2756 c
2757 u
2758 system
2759 layout
2760 (constructor
2761 ArenaResidents
2762 ArenaResidentsNext
2763 (constructor
2764 ArenaResident
2765 ArenaResidentValue
2766 b"data-parallel-owner-state"
2767 (dpoStateAt layout)
2768 (naturalSaturatingSubtract extent (dpoStateAt layout))
2769 dpWord)
2770 residents))))))))))))))))))))))))))))))))))))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.