This article describes cancellation as a protocol over suspended computations rather than as a distinguished exception or a single algebraic operation. An effect handler supplies the control boundary at which an asynchronous request can expose its continuation, but the cancellation policy still has to determine who owns that continuation, when a request becomes observable and which event wins if completion arrives concurrently. The distinction matters because raising an exception in an operation clause doesn't cancel the continuation captured by that clause, while discontinuing the continuation raises at the original perform site and therefore traverses the frames that own the suspended computation's resources. A useful semantics must connect those source level facts to the scheduler registry, the one shot claim on each continuation and the scope tree which prevents canceled work from escaping its owner.
Protocol
Cancellation is usually discussed as though one action changes a fiber from running to dead, but an implementation has at least four observably different events: a request is issued, the request becomes visible to the target, control is delivered through an interruption point and the target finishes unwinding.
The requester may return after the first event or may wait for the last one, so two APIs with identical cancel functions can provide very different lifetime guarantees.
Structured interfaces normally make scope exit wait for child termination because returning while a child still owns a socket or a continuation would break the scope's resource invariant.
An unstructured token can only record intent unless some separate join establishes that the target has acknowledged the request and completed its cleanup.
Algebraic effects don't select one cancellation policy by themselves.
They provide operations whose meaning is supplied by handlers and they expose a delimited continuation when an operation is handled, as established by the operational and direct style programming accounts of handlers [1][2].
A library may define Cancel as an operation, as Leijen does for structured asynchrony, but that operation belongs to the requesting strand and can return normally after it has canceled outstanding awaits [3].
The strands being canceled still need a delivery mechanism which turns their saved continuations into exceptional resumptions or otherwise prevents those continuations from running again.
The following surface signature separates asynchronous suspension, cancellation of a named scope and an explicit cancellation checkpoint. It is deliberately small because timeouts, racing computations and parent failure can all be reduced to different producers of a cancellation reason rather than separate forms of interruption:
The type of Await preserves the result index of each request, so a readable file descriptor can resume with an integer while a timer resumes with unit.
Cancel returns unit to the requester because issuing cancellation doesn't manufacture a result for the target's pending request.
Check_cancel is also typed as returning unit, although its handler may instead discontinue the current computation with a cancellation exception.
This split keeps the request path, the target path and the result type of an outstanding operation distinct before any scheduler representation is chosen.
Transitions
Let a scheduler state be Σ = ⟨F, R, Q⟩ where F maps fiber identifiers to fiber states, R maps backend registrations to suspended continuations and Q is the runnable queue. Each cancellation scope carries a monotone token whose state is either ℒ for live or ℂ(r) for canceled with reason r. The model used here keeps the first reason, making repeated requests idempotent and preventing a later timeout from replacing the failure which initiated sibling cancellation. Other policies can combine reasons, but they must still specify a deterministic observation rather than leave the selected exception dependent on an arbitrary handler traversal.
A running fiber observes the token when it executes a checkpoint or enters a cancellable operation, while a parked fiber can be reached through the registration stored by that operation. Delivery to a running fiber is cooperative in this model because arbitrary pure code doesn't consult the token and the handler has no saved continuation to discontinue while the code remains between operations. Delivery to a parked fiber is prompt only if the backend registration has an active cancellation function which can remove or invalidate the pending request. Neither path implies that cleanup has completed, so a parent that requires lifetime closure must still join the target after sending the request.
This model is level triggered rather than edge triggered: once a scope is canceled, every later check observes the same state until execution leaves that scope.
Catching one Cancelled exception therefore doesn't reset the token and a subsequent cancellable operation may raise again, which prevents an accidental broad exception handler from permanently defeating cancellation.
Eio uses this style by storing cancellation in a context, invoking a parked fiber's current cancellation function and checking the context when many operations begin [7].
The exact checkpoint placement is a library decision, but persistence of the token is what gives a request meaning beyond one attempted exception delivery.
Ownership
When Await request reaches the scheduler handler, evaluation between the perform site and that handler is reified as a continuation k whose input type is the request's result type.
The scheduler registers the external operation and stores k in a parked fiber record, thereby transferring responsibility for the continuation from the running stack to the scheduler registry.
This transfer is not merely an implementation convenience because abandoning k retains its captured frames while invoking it twice repeats control which may own linear resources.
OCaml enforces at most one continuation resumption dynamically and its manual requires the scheduler discipline to continue or discontinue each captured continuation exactly once [5].
The existential Suspended constructor keeps the request registration and the continuation under the same hidden result type.
A successful backend event can therefore extract a value of exactly that type before calling continue, while cancellation needs no such value because discontinue injects an exception at the continuation's entry point.
The atomic claim records which terminal action consumed the continuation and turns a physical pointer to a captured stack segment into a linearly owned scheduler object [11].
The runtime detects a second resumption, but a separate claim is still needed when two backend agents race because discovering the programming error after both events have already scheduled work is too late to preserve higher level invariants.
OCaml implements captured continuations using heap allocated stack segments rather than by copying the entire stack or converting every source function to visible continuation passing style. Capturing a continuation detaches the relevant fiber segment and resumption reconnects it, which supports the one shot discipline used by concurrent schedulers [4]. The representation explains why cancellation should consume a parked continuation through the same runtime interface as normal completion instead of dropping a pointer and hoping finalization eventually releases its frames. A garbage collector may eventually reclaim an unreachable stack segment, but it can't replace deterministic unwinding for file descriptors, locks or protocol state owned by those frames.
Discontinuation
The critical OCaml primitive is Effect.Deep.discontinue k exn, which resumes k by raising exn inside the suspended computation [6].
If k was captured by perform (Await r), the exception appears at that perform site and unwinds through every frame between the site and the handler delimiter.
A Fun.protect frame inside that extent executes its finalizer because the continuation has actually been reentered on an exceptional path.
This behavior is the semantic bridge between cancellation recorded by a scheduler and ordinary language level cleanup in the target computation.
Raising the same exception directly inside the scheduler's operation clause is different.
The clause runs outside the captured continuation, so a direct raise unwinds the handler invocation while leaving k suspended and every resource frame inside it untouched.
Returning from the clause without either resuming or storing k causes the same resource leak in a quieter form because the continuation becomes unreachable without traversing its protected frames.
The OCaml manual's exchanger example uses discontinue for precisely this reason when a blocked continuation can no longer make progress [5].
In the usual deep handler rule, handling an operation from evaluation context E binds a continuation which reinstalls the handler around the context when resumed. Cancellation doesn't require a new reduction rule for this step because exceptional resumption can be represented as applying the same delimited continuation to an exceptional outcome at the runtime boundary. What is new is the scheduler state which delays that application and allows a cancellation request to compete with the operation's ordinary result. The algebraic handler explains the continuation boundary, while the concurrent registry explains who may consume it and when that consumption becomes linearized.
Lowering
A minimal scheduler handler needs an effect for suspension whose argument receives the current fiber context and an enqueue function for its eventual result.
The enqueue function packages both normal and exceptional completion, then converts the selected result into continue or discontinue only when the fiber returns to the scheduler's runnable queue.
Deferring actual resumption matters because backend callbacks may execute inside signal processing, an event loop callback or another domain where reentering arbitrary user code would violate scheduler assumptions.
The following skeleton shows the control boundary without committing to a particular poller or run queue implementation:
The effect clause captures a continuation whose input type follows the existential type of Suspend, so the Ok value branch remains type safe without casting through a universal payload.
The error branch is independent of that input type because an exception can discontinue a continuation expecting any value.
A production scheduler also records tracing state, clears any installed cancellation function before resumption and prevents the fiber from being placed on the queue twice.
Eio's backend handlers follow this shape by wrapping a captured continuation with its fiber context and dispatching an enqueued Ok through continue or an Error through discontinue [9].
The handler should check an already canceled context before publishing a new request because the cancellation traversal may have completed just before the fiber tried to park. It must also arrange publication so cancellation can't observe the fiber without finding either a valid cancellation function or a state which proves the operation has already won. On a single scheduler domain this ordering can be established by running the state transition without yielding, while multi-domain completion requires an atomic protocol around the backend request. The abstract effect signature hides those details from user code but doesn't remove them from the semantics of the handler which interprets the operation.
Races
A parked read can become ready at the same time that its parent scope is canceled, and there is no universally correct rule which says the value or the cancellation must always win. The implementation must instead choose a linearization point and document the result after that point, since both the I/O completion and the cancellation callback may already be in flight. Eio explicitly notes that an operation which succeeds before cancellation but is still waiting on the run queue may return its result, while a later cancellation check can still fail the next operation [7]. That policy preserves an operation result once the backend has committed it without pretending that the enclosing scope became live again.
The smallest useful state machine has one nonterminal state, Waiting, and two terminal claims, Resumed and Discontinued.
Completion changes Waiting to Resumed before scheduling continue k v, while cancellation changes it to Discontinued before scheduling discontinue k c.
Exactly one compare and exchange can succeed, so the continuation is consumed at most once even when the backend and cancellation traversal execute on different cores.
The losing event still performs any backend specific disposal needed for its own event record, but it doesn't enqueue another resumption.
Visibility of the initialized continuation and registration must come from the release and acquire edge which publishes the slot to the competing agents; it doesn't arise merely because both agents later compare and exchange claim.
The successful memory_order_acq_rel operation shown here is a conservative choice for synchronizing winner state, while the failure order may be weaker if the losing path doesn't inspect data published by the winner [12].
A complete implementation must also solve lifetime reclamation for the slot itself.
The compare and exchange is the linearization point for semantic ownership rather than a general promise that external I/O has been undone.
A canceled read may already have consumed bytes in the kernel or a remote service may still process a request after the local waiter disappears.
Cancellation therefore terminates the local obligation to resume the computation, while compensation for externally visible effects belongs to the protocol implemented above that operation.
Registrations
A timer identifier, readiness subscription or completion callback remains a resource even after its continuation has been discontinued. If cancellation only marks the fiber then a stale callback can retain the continuation, occupy a poller slot and later attempt a second resumption. Leijen's structured asynchrony implementation calls this out for timers and installs cancellation cleanup which clears the timeout registration [3]. The one shot claim protects semantic control from a late callback, but deregistration is still required to bound memory and backend work.
A cancellable operation consequently publishes two related pieces of state: a registration which can be removed and an enqueue capability which can complete the suspension.
Removal usually returns whether cancellation won because the backend may have already detached the request for completion.
The same winner test controls whether the cancellation path enqueues an exception or leaves the successful path to enqueue its value.
The following OCaml model makes that contract visible without tying it to epoll, kqueue, IOCP or io_uring:
In the sketch, Cancel_context.publish is a linearized handoff: it either installs the prepared request into a live context or delivers cancellation through that request before Poller.arm can expose backend completion.
Real backends differ in whether removal can synchronously prove that no callback will run, so the poller's cancellation operation represents a backend contract rather than a portable operating system call.
If the platform can only request cancellation asynchronously, both callbacks must still converge on a shared winner cell before touching the continuation.
The fiber's cancellation function is cleared once either path wins so a later traversal doesn't keep calling an obsolete backend hook.
Eio's cancellation context follows the same ownership rule by replacing each registered fiber cancellation function with ignore before invoking it [9].
Unwinding
Resource safety depends on where acquisition and cleanup sit relative to the handler boundary.
If a file is opened inside the computation and its Fun.protect frame lies between the await site and the scheduler handler, discontinuation reenters that extent and executes the release action.
If the resource is owned by the scheduler outside the continuation, the scheduler must release it explicitly when the claim changes state because unwinding the target can't reach it.
A code review should therefore assign every registration, descriptor and lock to either the captured stack or the scheduler state rather than assuming one cancellation path cleans both.
The first function guarantees that release runs on normal return and on an exception delivered by discontinue, but it doesn't say whether the release action can itself be interrupted by persistent cancellation.
The second moves release into a protected cancellation context so the parent's canceled token doesn't immediately abort a cleanup operation which needs to suspend.
Eio exposes this behavior through Cancel.protect and runs switch release hooks under that protection after attached fibers have finished [13].
Protection should remain narrow because a finalizer which waits forever also prevents the parent scope from establishing that its children and resources have terminated.
Cleanup failures require an explicit precedence rule as well. A cancellation exception usually records why the computation was asked to stop, while a release failure may show that the state left behind is corrupt or incomplete. Silently replacing either one loses information, so runtimes commonly preserve a primary failure and attach cleanup failures as suppressed or combined exceptions. Cancellation itself is generally control information rather than the error reported to the caller, which is why a structured parent should retain the original child failure that caused sibling cancellation.
Protection
A mask doesn't revoke a cancellation request; it defers observation while an invariant is temporarily exposed. The canonical use is the narrow interval between making a resource reachable and installing the release action which owns it, because delivery in that interval can leak the resource even though both surrounding states are valid. Asynchronous exception work in Haskell introduced scoped blocking and unblocking for the same reason, with delivery state restored on every exit path [10]. An effect based runtime can represent that dynamic state in a cancellation context or fiber local field, but it must capture and restore the state with the continuation when control suspends.
There are two useful protection policies which shouldn't be conflated.
Deferred delivery records cancellation and raises as soon as execution leaves the protected region, while detached protection runs in a child context which isn't canceled by its parent and may return a value even though the parent remains canceled.
Eio's Cancel.protect implements the second shape and deliberately doesn't check the parent when the protected function returns [7].
A language primitive modeled after asynchronous exception masking may implement the first, so portable reasoning should state whether unmasking itself is a cancellation point.
Masking is not permission to expose arbitrary noninterruptible regions around application logic. A protected commit may need to publish a state update and durable log record as one protocol step, but network conversation, user callbacks and unbounded retries should remain cancellable. The semantic obligation is that every protected region has a bounded route to a state in which cancellation can be observed without violating an invariant. This restriction converts masking from a global liveness hazard into a local proof boundary around resource publication or cleanup.
Scopes
Structured concurrency gives cancellation a direction by making each spawned fiber a child of a lexical scope which can't finish until that fiber terminates. Cancellation normally propagates from a scope to its descendants, while completion values and failures travel from children back to the owner which joins them. Protected subscopes stop downward propagation for carefully delimited cleanup, but they remain owned and must still finish before their enclosing resource scope disappears. Eio represents cancellation contexts as a tree, recursively marks child contexts and stops at protected nodes [9].
The tree is an ownership relation rather than a scheduling order.
A child may run before its parent next reaches the queue and siblings may execute on other domains, yet the scope still knows which descendants must be canceled and joined when one branch fails.
This is what lets both cancel one branch after the other raises and then wait for both branches before rethrowing the original failure, as documented by Eio's fiber interface [8].
The same discipline allows a race to select one result while ensuring that losing work has completed cancellation before the race scope returns.
Eio.Fiber.first also documents an unavoidable race in which both branches may succeed before either result is observed, so its result combiner specifies what happens when there are two successful values [8].
Cancellation can't retroactively erase a completion which has already crossed its linearization point.
The scope can still prevent the later branch from continuing into another cancellable operation because its token remains canceled after that result is produced.
Treating the race winner as a semantic claim rather than as wall clock chronology avoids promising an ordering the scheduler and backend can't observe.
Reporting
Failure and cancellation share an exceptional delivery mechanism but carry different obligations.
A child failure is evidence that work attempted by the scope didn't complete correctly, so the scope records it, cancels siblings and eventually reports it to its owner.
A sibling's resulting Cancelled exception is evidence that shutdown was obeyed and normally shouldn't replace the initiating failure.
If cancellation cleanup raises a new exception, the scope must retain both because the second failure may describe damage encountered while establishing the postcondition.
User initiated cancellation can be the primary reason when no computation has failed, but that still doesn't mean every canceled fiber should log an error independently. Reporting at each target duplicates the same control event and obscures the operation which initiated shutdown. A better rule is for the owner of the cancellation scope to decide whether its reason is expected, diagnostic or fatal after all children have reached terminal states. This separation mirrors Eio's distinction between cancelling a context to stop fibers and failing a switch to record an error for later reporting [7].
Catching Cancelled inside arbitrary application code is dangerous when the handler continues with unrelated work because the cancellation token remains set and the scope owner is waiting for termination.
Cleanup code may catch it long enough to restore an invariant, then should return or rethrow unless it has explicitly moved into a protected scope with a new ownership contract.
A library which catches all exceptions should recheck cancellation before ignoring one because the exception may have crossed an abstraction that doesn't know its concrete wrapper.
Persistent context checks make this mistake recoverable at the next suspension point, although they can't prevent CPU bound code from running until that point.
Extent
An algebraic operation travels to the nearest handler which accepts it, so moving a cancellation handler changes which outstanding operations a request can reach.
Leijen's cancelable handler tracks awaits in its lexical scope and forwards explicit cancellation identifiers outward when a request targets an enclosing scope [3].
A nested handler can isolate a race or timeout without granting it authority over unrelated siblings managed by an outer scheduler.
This lexical delimiter is the control analogue of the ownership tree, although the runtime may represent scope identity explicitly so another fiber can request cancellation remotely.
Deep and shallow handlers also differ in what happens after a suspended continuation resumes. A deep continuation reinstalls its handler, so later awaits return to the same scheduler unless another inner handler intercepts them. A shallow continuation doesn't include the handler and must be resumed with a handler chosen for the next step, which can make protocol state changes explicit but also places more responsibility on the scheduler. OCaml exposes both forms and documents the reinstatement difference in its effects chapter [5].
Cancellation state must follow the fiber rather than the operating system thread because effect handlers can suspend one fiber and resume another on the same domain. It must also survive migration if a scheduler moves a runnable continuation between domains. Storing the current context in fiber local state satisfies that requirement and lets an inner scope replace it dynamically while preserving the parent link for propagation. The handler boundary provides delimited control, while the context value provides stable identity across nonlocal scheduling transitions.
Delivery
Cooperative cancellation can't stop a pure loop which performs no effect, allocation check or explicit checkpoint.
Effect handlers only receive control when an operation reaches them, so the existence of a Cancel constructor doesn't create preemption between ordinary instructions.
A compiler may insert polls at loop back edges or allocation paths, but that is a separate runtime mechanism whose cost and memory model must be specified.
Without such polling, cancellation latency is bounded by the longest region between cancellation points rather than by the time required to set the scope token.
Foreign calls introduce a second gap because the managed runtime may not be able to unwind a C stack while an operating system function is blocked.
A cancellable binding can arrange an external wakeup, close or backend cancellation request, then deliver Cancelled after the call returns to managed code.
A noncancellable binding can only leave the request pending until return, and hard termination of the underlying system thread may violate language and library invariants.
The article's semantics therefore promise cooperative promptness at registered operations rather than asynchronous destruction at an arbitrary machine instruction.
The same limit applies to cleanup. A finalizer which calls an uncancellable foreign function may hold the scope open despite correct discontinuation of the managed continuation. This isn't a failure of the one shot protocol because the continuation has been consumed and is executing its exceptional path, but it is a liveness failure in the resource contract. Production libraries consequently need cancellation aware bindings and bounded cleanup behavior in addition to correct handler semantics.
Properties
The implementation can be reviewed against a small set of safety and liveness properties which remain meaningful across different scheduler backends. First, each suspended continuation is consumed at most once by a successful claim and is eventually continued or discontinued if its owning scope terminates. Second, a cancellation token moves monotonically from live to canceled and every descendant which was still active when the request arrived either observes that state or reaches a terminal state before the owning scope returns. Third, every backend registration is either completed or withdrawn, so no event retains a continuation after its claim becomes terminal.
Resource safety adds a stack property: discontinuation raises inside the captured extent and therefore runs every cleanup frame between the perform site and its delimiter exactly as ordinary exceptional unwinding would. Scope safety adds a tree property: a scope doesn't return while any owned child or protected cleanup scope remains active. Race safety adds a linearizability property: completion and cancellation agree on one winner even if their callbacks execute concurrently. None of these properties follows from the operation signature alone because each depends on the handler, registry and ownership structure used to interpret that signature.
The final liveness formula needs fairness and cooperation assumptions because a runnable fiber which never yields can prevent every other scheduler action, while a backend which never reports completion can keep an uncancellable wait parked forever. Protected regions also need a termination assumption or a bound because protection intentionally blocks downward cancellation propagation. Stating those premises is preferable to claiming that structured cancellation guarantees prompt termination under arbitrary foreign code. The semantics gives a disciplined route to termination when the program and backend honor their cancellation points, not a machine level kill switch.
Composition
Algebraic effects make suspension explicit at a handler boundary and provide the delimited continuation which represents the remainder of a fiber.
Cancellation gives the scheduler a competing exceptional result for that continuation, but a complete design also needs a persistent scope token, an atomic winner for every parked operation and a join which waits for unwinding to finish.
discontinue is the mechanism which delivers cancellation through ordinary exception semantics; it isn't the policy which decides propagation, masking, reason precedence or backend withdrawal.
Keeping those layers distinct makes cancellation compositional because handlers delimit control, scopes delimit ownership and the registry connects both to external events without violating one shot continuation use.
References
- Gordon D. Plotkin and Matija Pretnar. Handling Algebraic Effects. Logical Methods in Computer Science 9(4), 2013. Establishes the algebraic account of handlers and the continuation supplied to an operation clause.
- Andrej Bauer and Matija Pretnar. Programming with Algebraic Effects and Handlers. Journal of Logical and Algebraic Methods in Programming 84(1), 2015. Includes cooperative scheduling expressed with effect operations and handler managed continuations.
- Daan Leijen. Structured Asynchrony with Algebraic Effects. Microsoft Research Technical Report MSR-TR-2017-21, 2017. Develops scoped asynchronous operations, cancellation, timeout, callback withdrawal and cancellation aware resumption.
- K. C. Sivaramakrishnan, Stephen Dolan, Leo White, Tom Kelly, Sadiq Jaffer and Anil Madhavapeddy. Retrofitting Effect Handlers onto OCaml. PLDI 2021. Describes OCaml's stack segment representation, one shot continuations and the runtime costs of capture and resumption.
- The OCaml developers. Language extensions: effect handlers. OCaml 5.3 Reference Manual. Documents deep and shallow handlers, linear continuation use and discontinuation for deterministic resource unwinding.
-
The OCaml developers. Effect.Deep. OCaml 5.3 library reference. Specifies
continue,discontinueand the exception raised when a continuation is resumed more than once. - The Eio developers. Eio.Cancel. Documents cancellation context trees, persistent checks, protected subcontexts, cancellation functions and result precedence around run queue delays.
- The Eio developers. Eio.Fiber. Documents structured fiber combinators, sibling cancellation, joining and the case where both branches of a race have already succeeded.
-
The Eio developers. Cancellation context implementation, revision
53856d7. Shows context states, protected child traversal, fiber cancellation functions and the single domain mutation rule in the pinned implementation inspected for this article. - Simon Marlow, Simon Peyton Jones, Andrew Moran and John Reppy. Asynchronous Exceptions in Haskell. PLDI 2001. Gives a formal operational treatment of asynchronous delivery, scoped masking, interruptible operations and resource bracketing.
- Carl Bruggeman, Oscar Waddell and R. Kent Dybvig. Representing Control in the Presence of One Shot Continuations. PLDI 1996. Develops implementation techniques and ownership assumptions for continuations which are invoked at most once.
- ISO/IEC JTC1/SC22/WG14. N1570: Programming Languages C, 2011. Sections 5.1.2.4 and 7.17 define the C11 atomic operations and memory orders used by the illustrative continuation claim.
- The Eio developers. Eio.Switch. Specifies resource ownership, waiting for attached fibers, failure propagation and protected LIFO release hooks at switch termination.