Compile both pointwise programs, 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`.
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))))))))))))))))))))))))))))))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.