174def nativePeerRegionPublish =
175 (lambda unrestricted publication : (family NativePeerRegionPublication) .
176 (lambda unrestricted role : Nat .
177 (lambda unrestricted success : (family NativePhysicalCommands) .
178 (eliminate
179 NativePeerRegionPublication
180 (lambda unrestricted current : (family NativePeerRegionPublication) .
181 (family NativePhysicalCommands))
182 publication
183 (branch
184 NativePeerRegionPublicationOf
185 plan
186 peers
187 capture
188 committed
189 connection
190 stateAt
191 stateBytes
192 agreed
193 ownerOf
194 offsetOf
195 paths
196 .
197 (let unrestricted version =
198 (nativeMemoryLoad stateAt)
199 in
200 (let unrestricted epoch =
201 (nativeMemoryLoad
202 (naturalAdd stateAt (naturalMultiply 2 nativeCheckpointWordBytes)))
203 in
204 (nat-eliminate
205 (lambda unrestricted current : Nat . (family NativePhysicalCommands))
206 (nativeRegionPrepareOwner
207 plan
208 stateAt
209 ownerOf
210 offsetOf
211 0
212 stateAt
213 paths
214 (nativePeerEachOwner
215 peers
216 (lambda unrestricted owner : Nat .
217 (lambda unrestricted rest : (family NativePhysicalCommands) .
218 (let unrestricted frame =
219 (capture owner)
220 in
221 (nativeFrameInitializeRound
222 frame
223 epoch
224 version
225 (nativePeerPublicationIO
226 (nativeLaunchRecipeSlotValue (connection owner))
227 0
228 frame
229 (nativeFrameConsume
230 frame
231 (nativeMemoryCompareRegions
232 stateAt
233 (framePayloadAt frame)
234 agreed
235 nativePeerScratchSlot
236 b"checkpoint-captured-position"
237 (nativeRegionPrepareOwner
238 plan
239 stateAt
240 ownerOf
241 offsetOf
242 owner
243 (framePayloadAt frame)
244 paths
245 rest))))))))
246 (nativeRegionPublish
247 plan
248 stateAt
249 (lambda unrestricted index : Nat . (nativeRegionShardPath paths index 1))
250 (nativeRegionPathArgument (nativeRegionManifestCandidateIndex paths))
251 (nativeRegionPathArgument (nativeRegionManifestCommittedIndex paths))
252 (nativeRegionPathArgument (nativeRegionDirectoryIndex paths))
253 nativePeerListenerSlot
254 nativePeerScratchSlot
255 6
256 (nativePeerEachOwner
257 peers
258 (lambda unrestricted owner : Nat .
259 (lambda unrestricted rest : (family NativePhysicalCommands) .
260 (let unrestricted released =
261 (committed owner)
262 in
263 (nativeFrameInitializeRound
264 released
265 epoch
266 version
267 (nativeMemoryStoreWord64
268 b"checkpoint-committed-version"
269 (framePayloadAt released)
270 version
271 (nativePeerPublicationIO
272 (nativeLaunchRecipeSlotValue (connection owner))
273 1
274 released
275 rest))))))
276 success))))
277 (lambda unrestricted previous : Nat .
278 (lambda unrestricted ignored : (family NativePhysicalCommands) .
279 (let unrestricted channel =
280 (nativeLaunchRecipeSlotValue (connection 0))
281 in
282 (let unrestricted frame =
283 (capture role)
284 in
285 (let unrestricted released =
286 (committed role)
287 in
288 (nativeFrameInitializeRound
289 frame
290 epoch
291 version
292 (nativeFrameInitializeRound
293 released
294 epoch
295 version
296 (nativeMemoryCopyOperands
297 (nativeMemoryState (framePayloadAt frame))
298 (nativeMemoryState stateAt)
299 stateBytes
300 nativePeerScratchSlot
301 b"checkpoint-capture-state"
302 (nativePeerPublicationIO
303 channel
304 1
305 frame
306 (nativePeerPublicationIO
307 channel
308 0
309 released
310 (nativeFrameConsume
311 released
312 (nativeLaunchRecipeAssertEqual
313 (nativeMemoryLoad (framePayloadAt released))
314 version
315 b"checkpoint-committed-version"
316 success))))))))))))
317 role))))))))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.