Who holds a shard, and where it lies in that owner's state.
1895def dpoShardOwner =
1896 (lambda unrestricted c : Nat .
1897 (lambda unrestricted u : Nat .
1898 (lambda unrestricted system : (family DataParallelSystem c u) .
1899 (lambda unrestricted q : Nat .
1900 (lambda unrestricted p : Nat .
1901 (lambda unrestricted shard : (family NativeRegionShard) .
1902 (let unrestricted owner =
1903 (naturalModuloUnchecked
1904 (naturalModuloUnchecked (dpoShardWord shard) (dpK c u system))
1905 (dpOwners c u system))
1906 in
1907 (naturalSelect
1908 (naturalEqual
1909 (nativeRegionOrdinal shard)
1910 (dpoCoordinateOrdinal (dpoShared c u system q)))
1911 owner
1912 (naturalSelect (naturalAnd p (naturalIsZero (nativeRegionOrdinal shard))) owner 0)))))))))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.