On this page

Priority and completion

An action can be legal for one participant at one point and unavailable a moment later. A timing contract makes that permission explicit. A completion contract then says when the caller may resume and which finished work satisfies its obligation.

Read resources and payment for atomic commitment and its pending boundary. Read objects and lifetime for references that must not silently change their target.

A window defines opportunities

A priority window needs participants, a current permission to act, eligible options and a rule for closing. Giving a participant priority does not make every action available: each option must still meet its costs, targets and other restrictions.

In a two-participant window that closes after two consecutive passes, the sequence below illustrates the distinction between passing and withdrawing permanently:

Step	Choice	Consequence for consecutive passes
1	A passes.	One pass.
2	B performs an eligible action.	The pass sequence is broken.
3	B completes the action, receives priority again and passes.	One pass.
4	A passes.	Two consecutive passes; the window can close.

This is an authored example of the teaching profile’s closure rule, not a captured execution. Completing an action returns priority to the acting participant and clears the earlier pass. Priority therefore does not automatically alternate after an action. A pass costs only what its contract specifies; it is not a general promise to refrain from later action.

The exact PassWindow definition handles passing. CompleteOption handles the action’s return:

priority · input revision 1 · CC0 1.0

CompleteOption(before, receipt, returnedHolder, keepPreviousPass) ==
    LET finished ==
        [before EXCEPT !.busyActor = "None", !.call = 0, !.transaction = 0,
         !.child = 0, !.childComplete = FALSE,
         !.previousPass = IF keepPreviousPass THEN @ ELSE FALSE,
         !.consecutivePasses = 0, !.usedReceipts = @ \cup {receipt.id},
         !.nextReceipt = @ + 1, !.lastReturn = receipt,
         !.returnAudit =
           [expectedWindow |-> 1, actualWindow |-> receipt.window,
            expectedCall |-> before.call, actualCall |-> receipt.call,
            expectedChild |-> before.child, actualChild |-> receipt.child,
            expectedTransaction |-> before.transaction, actualTransaction |-> receipt.transaction,
            expectedReception |-> before.reception, actualReception |-> receipt.reception],
         !.lastEvent = "Return", !.lastActor = before.busyActor]
    IN ReceivePriority(finished, returnedHolder)

Definition and resolved references · Exact module download · Source bundle and reproduction instructions

Payment is not effect completion

An eligible action may first commit costs and record use, then resolve its effect and any required follow-up work. The point at which an ability is used can therefore precede the point at which its effect finishes.

For the payment specialization, paid is recorded with the debit while pending remains true until completion. A surrounding priority procedure must not treat that pending action as absent or offer its use again merely because the final effect has not returned.

Separate the relevant questions:

• Was the option legal when selected?

• Were its full costs accepted and committed?

• Which use and event records now exist?

• Has all required completion work drained?

• Which caller is entitled to resume?

Answering one does not settle the others.

Suspend the caller while child work runs

A procedure may pause to run another procedure. Its state needs enough information to resume the exact caller at the exact continuation point.

For example, a parent action waits for completion record 21. It starts child procedure 34 and preserves its own continuation. Finishing a different child, or presenting an old record with a similar shape, cannot satisfy that wait. A useful return contract binds the caller, child, obligation and completion identity rather than accepting a generic “done” flag.

The identities in this example are explanatory labels. They do not name a captured execution. The model’s actual references and guards determine how the relationship is represented.

A checkpoint is a required completion boundary

A checkpoint can require follow-up processing before an ordinary action continues. The caller must wait until the required work is complete; it cannot infer completion merely from a numerical cost reaching zero or an effect returning a value.

Some models receive a trusted completion witness from a supplied provider. Others model the processing that produces it. The first can check how the caller consumes a correctly formed witness without establishing that a complete checkpoint executor exists. Read supplied-provider assumptions alongside the transition they enable.

Wrong-caller records, stale completions, duplicate returns and continuation before the required boundary are useful failure cases. They need properties that observe those distinctions; a balance or object-type invariant alone cannot detect them.

Follow ReturnMatches for the exact return guard and ReceivePriority for admission of the matching return. The priority evidence includes the ordinary finite check and deliberately defective alternation, pass-marker and wrong-caller variants.

Keep progress assumptions visible

A pending procedure can be safe while waiting forever. To claim eventual return, a model must address the environment that supplies child completion and the schedule that selects an enabled return.

Weak fairness can exclude endlessly postponing a continuously enabled action. It does not create an unavailable completion witness or prove that a trusted provider finishes its work. The checking chapter explains why a temporal result must identify those assumptions.

The finite priority profile checks caller/return safety with supplied completion providers and no fairness assumption. It does not implement a complete checkpoint executor or establish eventual return. Use its source and evidence together: find the acting participant, suspended caller, required completion identity, return guard and remaining provider assumptions. The cost reference provides a compact lookup example, while Reading a model provides the entry path through notation and claims.