Checkpoints as owed work and matched returns¶
A checkpoint is a procedure with an identity, caller, snapshot references and a queue of obligations. It lets a caller wait until the relevant cleanup and recognition work is complete. Calling a state a checkpoint, or observing an empty pending set, is insufficient to establish that return boundary.
Read priority and completion for the basic caller relationship, and composition and assumptions for the joins between action payment, nested work and final completion.
Open from an actual completed site¶
Inputs include a completed event, its site record, the enclosing timing structures and the set of checkpoint identifiers already used. The site distinguishes the relevant cost, instruction, timing-structure end or priority-reception event. Its caller, event identifier and snapshot must agree with that event’s context.
reference-profile · input revision 2 · CC0 1.0
OpenCheckpointAtSite103(frame,id,site,event,insideStructures,usedCheckpoints) ==
/\ CheckpointSite103(site,event,insideStructures) /\ id \in (Nat \ {0}) \ usedCheckpoints
/\ frame=NewCheckpoint103(id,site.caller,site.snapshotId,site.inside)Definition and resolved references · Exact module download · Source bundle and reproduction instructions
Opening chooses a fresh positive checkpoint identifier and creates the frame’s ordered obligations. A structure-end site also adjusts the enclosing-structure set for the structure that actually ended. A matching event tag without the caller, identity and completion relationships is insufficient.
An authored example has checkpoint 41 opened for caller A at snapshot 7. An otherwise similar receipt for checkpoint 42, caller B or another snapshot cannot discharge 41’s obligations. This illustrates identity matching; it is not a retained execution.
Treat the stage queue as procedure state¶
The frame records the remaining ordered stages, completed stages, explicitly discharged stages, current point and latest processing snapshot. CheckpointAt103 requires a live steps-phase frame whose current point is the head of that queue.
CheckpointStageAdvance103 removes that head and records completion. It is a bookkeeping relation. The stage-specific wrapper must establish the work that makes advancing valid: for example, object cleanup, registry updates or reaction recognition. Calling the queue helper directly cannot establish that all such state changes occurred.
The local record updates preserve the frame’s other fields. An outer transition still needs to constrain object maps, ledgers, windows and other variables that the wrapper does not receive. This is the frame-condition issue introduced in reading a model.
Bind recognition to both observation boundaries¶
Recognition identifies the checkpoint and caller, the begin snapshot and the processing snapshot. It consumes the supplied ordinary or persistent processing context and captures the recognized member map in the frame. These captures let later steps distinguish an occurrence recognized here from a similar occurrence elsewhere.
The begin and processing snapshots have different jobs. A stage can update the current world while retaining the observation boundary from which this checkpoint began. Combining a ledger from one processing snapshot with a frame from another would discard that relationship.
Conditional instances can also lose availability after recognition. The recognized membership remains a record of what was captured; a particular instance’s status and current activity epoch determine what may still resolve. A lost pending instance is not revived simply because a later permission set resembles the earlier one.
The supplied metadata, conditional tests, authorization facts and state observations remain inputs to recognition. The checkpoint does not derive all those facts from an untyped description, and its internal recognition record does not grant either seat permission to inspect hidden metadata.
Finish all obligations before opening the return boundary¶
The ordinary completion relation requires an exhausted queue, complete stage coverage, a bound recognition record, a matching current world and a playing outcome:
reference-profile · input revision 2 · CC0 1.0
CheckpointCompletion103(frame,ledger,world,receipt) ==
/\ frame.phase="Completed" /\ ~frame.returned /\ frame.point="ProcedureCodeb74d673a0fc6" /\ frame.owed= <<>>
/\ frame.done \cup frame.discharged=CheckpointStageSet103 /\ frame.done \cap frame.discharged={}
/\ CheckpointCaptured103(frame,ledger) /\ frame.snapshotId=world.id /\ frame.outcome="Playing"
/\ receipt=PersistentCheckpointCompletion912(ledger,frame.recognition,world)Definition and resolved references · Exact module download · Source bundle and reproduction instructions
The completed and discharged stage sets must cover the required stages without overlap. Explicit discharge is not silent omission. RewriteCheckpointOrder103 requires the compiled exception, the actual resolved execution and explicit replacement obligations while preserving the remaining obligation set without duplicates.
When no members were recognized, the checkpoint has a separate return-without-reaction relation. When recognized members exist, opening the reaction window binds that exact member map, caller and checkpoint. A set of current pending instances can be smaller than the recognized set because some have become lost.
The playing-outcome guard also matters. A terminal objective result does not pass through this ordinary completion relation merely because its cleanup queue is empty. A composed procedure must follow the outcome branch that its contract actually provides.
Drain nested work before returning to the caller¶
Returning after a reaction requires the captured membership, drained conditional work and the matching top window:
reference-profile · input revision 2 · CC0 1.0
ReturnCheckpointAfterReaction103(before,after,ledger,beforeStack,afterStack,caller) ==
/\ before.phase="Reaction" /\ ~before.returned /\ caller=before.caller
/\ CheckpointCaptured103(before,ledger) /\ DOMAIN before.recognized#{}
/\ ConditionalCheckpointDrained96(ledger,beforeStack,before.id)
/\ Len(beforeStack)>0 /\ WindowTop9(beforeStack).id=before.windowId
/\ DOMAIN WindowTop9(beforeStack).members=DOMAIN before.recognized
/\ \A id \in DOMAIN before.recognized : WindowTop9(beforeStack).members[id]=before.recognized[id]
/\ PopClosedPriorityWindow9(beforeStack,afterStack)
/\ after=[before EXCEPT !.phase="Returned",!.returned=TRUE]Definition and resolved references · Exact module download · Source bundle and reproduction instructions
ConditionalCheckpointDrained96 accounts for instance completion or loss and the relevant windows’ closure and busy work. An empty pending set while a nested procedure is still busy therefore does not suffice. The closed top window is popped only under the full return relation.
CheckpointDrained103 then binds the returned frame, stage coverage, captured recognition and drained conditional work. Priority reception and resumption of paid or conditional instructions consume the corresponding matching receipt. They do not manufacture it from the fact that a caller is waiting.
Leave cleanup and unsupported cases visible¶
Host departure can make dependent objects eligible for cleanup. The checkpoint accounts for current successors, historical departures and objects protected by a paid procedure’s still-live hold. Cleanup may create further departures, requiring another pass at the relevant stage. Clearing the original host row alone cannot demonstrate that every dependent relationship has been handled.
Some legality questions remain explicit provider boundaries. CheckpointIllegalDisposition103 reports an unsupported disposition when no supplied retirement set makes the result legal. It does not choose an arbitrary cleanup and declare success. A host must retain that limitation or add a separately justified contract.
The composition evidence records the finite compositions, assertion selectors and meaningful controls associated with these joins. Those classes establish different facts. A source-span counterpart, a selector that checks constructed values and a transition driver that reaches a complete return cannot be substituted for one another. Supplied providers, finite carriers and outer scheduling assumptions remain part of every resulting claim.