---- start, restore, publication ----
Fresh: the declared replicated words and this owner's own words (owned
word j of coordinate i is the initial value at j k + i of the parameters,
when partitioned, followed by the optimizer state). Resume: the verified
restore of exactly those, then the restored prefix and a new membership
epoch.
2313def dpoFresh =
2314 (lambda unrestricted c : Nat .
2315 (lambda unrestricted u : Nat .
2316 (lambda unrestricted system : (family DataParallelSystem c u) .
2317 (lambda unrestricted q : Nat .
2318 (lambda unrestricted p : Nat .
2319 (lambda unrestricted layout : (family NativeDataParallelOwnedLayout) .
2320 (lambda unrestricted role : Nat .
2321 (lambda unrestricted tail : (family NativePhysicalCommands) .
2322 (let unrestricted k =
2323 (dpK c u system)
2324 in
2325 (let unrestricted owners =
2326 (dpOwners c u system)
2327 in
2328 (let unrestricted initial =
2329 (dataParallelInitialStateWords c u system)
2330 in
2331 (let unrestricted ownedInitial =
2332 (stdListAppend
2333 StdU64
2334 (stdListTake
2335 StdU64
2336 (naturalMultiply p k)
2337 (dataParallelInitialParameters c u system))
2338 initial)
2339 in
2340 (nativeMemoryStoreWord64
2341 b"data-parallel-version"
2342 (dpoStateAt layout)
2343 (nativeLaunchRecipeImmediate 0)
2344 (nativeMemoryStoreWord64
2345 b"data-parallel-cursor"
2346 (nativePointwiseAt (dpoStateAt layout) 1)
2347 (nativeLaunchRecipeImmediate 0)
2348 (nativeMemoryStoreWord64
2349 b"data-parallel-epoch"
2350 (nativePointwiseAt (dpoStateAt layout) 2)
2351 (nativeLaunchRecipeImmediate (dpoEpoch layout))
2352 (dpoUnless
2353 p
2354 (dpStoreWords
2355 (dpoParametersAt layout)
2356 (dataParallelInitialParameters c u system))
2357 (dpStoreWords
2358 (dpoSharedAt c u system p layout)
2359 (stdListDrop StdU64 (naturalMultiply q k) initial)
2360 (dpoEachOwned
2361 k
2362 owners
2363 role
2364 (naturalAdd q p)
2365 (lambda unrestricted coordinate : Nat .
2366 (lambda unrestricted word : Nat .
2367 (nativeMemoryStoreWord64
2368 b"data-parallel-owned-initial"
2369 (naturalAdd
2370 (dpoOwnedAt c u system q p layout)
2371 (dpoWordOffset k owners word coordinate))
2372 (nativeLaunchRecipeImmediate
2373 (modelWord64Natural
2374 (stdListHeadOr
2375 StdU64
2376 (modelWord64FromNaturalTruncated 0)
2377 (stdListDrop
2378 StdU64
2379 (naturalAdd (naturalMultiply word k) coordinate)
2380 ownedInitial)))))))
2381 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.