---- local work ----
Means, then this owner's assignments of the update program on its
parameters, shared state and owned coordinate words.
909def dpoUpdate =
910 (lambda unrestricted c : Nat .
911 (lambda unrestricted u : Nat .
912 (lambda unrestricted system : (family DataParallelSystem c u) .
913 (lambda unrestricted q : Nat .
914 (lambda unrestricted p : Nat .
915 (lambda unrestricted layout : (family NativeDataParallelOwnedLayout) .
916 (lambda unrestricted role : Nat .
917 (lambda unrestricted update : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
918 (lambda unrestricted tail : (family NativePhysicalCommands) .
919 (let unrestricted k =
920 (dpK c u system)
921 in
922 (let unrestricted m =
923 (dpM c u system)
924 in
925 (let unrestricted owners =
926 (dpOwners c u system)
927 in
928 (let unrestricted shared =
929 (dpoShared c u system q)
930 in
931 (let unrestricted words =
932 (naturalAdd q p)
933 in
934 (let unrestricted total =
935 (nativeCombineResultAt (dpoSum layout))
936 in
937 (let unrestricted at =
938 (dpUpdateAt c u system (dpoGeneric layout))
939 in
940 (let unrestricted sharedSlot =
941 (nativePointwiseAt at (naturalAdd k (naturalMultiply q k)))
942 in
943 (let unrestricted owned =
944 (dpoOwnedAt c u system q p layout)
945 in
946 (dpoMeans
947 c
948 u
949 system
950 layout
951 role
952 at
953 (dpoUnless
954 p
955 (dpCopy
956 at
957 (dpoParametersAt layout)
958 (dpParameterBytes c u system))
959 (dpCopy
960 sharedSlot
961 (dpoSharedAt c u system p layout)
962 (naturalMultiply dpWord shared)
963 (dpoEachOwned
964 k
965 owners
966 role
967 words
968 (lambda unrestricted coordinate : Nat .
969 (lambda unrestricted word : Nat .
970 (dpCopy
971 (nativePointwiseAt at (dpoSlotOf k p word coordinate))
972 (naturalAdd owned (dpoWordOffset k owners word coordinate))
973 dpWord)))
974 (nativeMemoryStoreWord64
975 b"data-parallel-rate"
976 (nativePointwiseAt at (naturalAdd (naturalMultiply 2 k) m))
977 (nativeLaunchRecipeImmediate
978 (modelWord64Natural (dataParallelRateWord c u system)))
979 (update
980 (dpoUnless
981 p
982 (dpCopy
983 (dpoParametersAt layout)
984 at
985 (dpParameterBytes c u system))
986 (dpCopy
987 (dpoSharedAt c u system p layout)
988 sharedSlot
989 (naturalMultiply dpWord shared)
990 (dpoEachOwned
991 k
992 owners
993 role
994 words
995 (lambda unrestricted coordinate : Nat .
996 (lambda unrestricted word : Nat .
997 (dpCopy
998 (naturalAdd owned (dpoWordOffset k owners word coordinate))
999 (nativePointwiseAt at (dpoSlotOf k p word coordinate))
1000 dpWord)))
1001 (dpoWhen p (dpoRetire c u system layout) tail))))))))))))))))))))))))))))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.