Continuation ownership and cancellation under algebraic effects

Cancellation is a protocol over suspended computations. An effect handler exposes the continuation of an asynchronous request, while the scheduler determines its owner and resolves competition between completion and cancellation. Raising an exception in an operation clause leaves the captured continuation suspended. Discontinuing it raises at the perform site and enters the frames that own the computation's resources. A cancellation model must therefore connect exception delivery to the scheduler registry and to the scope tree recording ownership of unfinished work.

Protocol

Calling cancel initiates a request which must become visible to the target, be observed at an interruption point, and be followed by unwinding. Returning after the token changes establishes a weaker completion guarantee than waiting for cleanup, even when the two interfaces have the same signature. Structured scope exit waits for child termination because a child that still owns a socket or a live continuation also leaves the resource obligations of the scope unfinished. An unstructured token only records the request unless a separate join establishes that the target has acknowledged cancellation and finished whatever cleanup it still owes.

An algebraic operation supplies a request and a delimited continuation, leaving cancellation policy to the handler [1][2]. Leijen defines Cancel as an operation for structured asynchrony in Koka, with the requesting strand returning normally after cancelling its outstanding awaits [3]. The strands being cancelled still need a delivery mechanism that turns their saved continuations into exceptional resumptions or otherwise ensures that those continuations cannot run again.

The interface distinguishes asynchronous suspension, cancellation of a named scope and an explicit checkpoint that examines the current computation's cancellation state. Timeouts, parent failure and races can supply cancellation reasons through this shared interface:

open Effect

type reason =
  | Timeout
  | Parent_failed of exn
  | Explicit of string

type scope = int

type _ request =
  | Read : Unix.file_descr * bytes -> int request
  | Sleep_until : int64 -> unit request

type _ Effect.t +=
  | Await : 'a request -> 'a Effect.t
  | Cancel : scope * reason -> unit Effect.t
  | Check_cancel : unit Effect.t

let await request = perform (Await request)
let cancel scope reason = perform (Cancel (scope, reason))
let check_cancel () = perform Check_cancel

Await preserves its request's result index: a read resumes with an int and a timer with unit. Matching the GADT constructor recovers the type equality required by the handler. Issuing Cancel does not produce a value for the pending request of the target and therefore returns unit to the requester rather than borrowing the result type of the target. The same return type suits Check_cancel even though its handler may discontinue the current computation with an exception instead of returning normally to the checkpoint. This separation retains the information needed for typed resumption without fixing the scheduler representation.

Transitions

Let the scheduler state be $\Sigma = \langle F, R, Q \rangle$ where $F$ maps fibre identifiers to their states and $R$ maps backend registrations to suspended continuations, with $Q$ holding runnable work. A cancellation scope stores a monotone token, either $\mathcal{L}$ for live or $\mathcal{C}(r)$ for cancelled with reason $r$, and retains the first reason received in this model. Retaining the first reason makes repeated requests idempotent. A later timeout cannot replace the child failure that initiated sibling cancellation. Combining reasons is another possible policy but it needs a deterministic observation rule rather than leaving the reported exception to whichever traversal order happens to occur.

A running fibre observes its token at a checkpoint or on entry to a cancellable operation. A parked fibre is reached through its operation's registration in $R$. Delivery to running code is cooperative here because pure computation does not consult the token and the handler has no saved continuation to discontinue between operations. A parked fibre can receive cancellation promptly only if its backend registration has a live cancellation function that can remove or invalidate the pending request. Neither delivery route establishes that cleanup has finished. The parent must join the target after requesting cancellation to establish the end of its lifetime.

Cancellation is level triggered: subsequent checks observe the cancelled state until execution leaves its applicable scope. Catching Cancelled does not reset the token. The next cancellable operation may raise again, so a broad exception handler cannot clear the request merely by catching its first delivery. Eio follows this approach by storing cancellation in a context and invoking the current cancellation function of a parked fibre, with checks performed when cancellable operations begin rather than after their results arrive [7]. Libraries can choose different checkpoint placements while still using a persistent token to give cancellation meaning beyond the first attempt to deliver an exception.

Ownership

Handling Await request captures the evaluation context from the perform site to the scheduler handler as a continuation $k$ expecting the result type of the request. Registering the backend operation and storing $k$ in a parked fibre record transfers responsibility for that continuation from the running stack to the scheduler registry. Suspension leaves resource obligations unresolved. Resuming twice violates the single use discipline required by frames that may own linear resources. OCaml detects repeated resumption with Effect.Continuation_already_resumed and the manual requires each captured continuation eventually to be continued or discontinued, which together give the scheduler its exactly once obligation [14][5].

open Effect.Deep

type claim = Waiting | Resumed | Discontinued

type 'a registration = {
  claim : claim Atomic.t;
  cancel_backend : unit -> unit;
  enqueue : ('a, exn) result -> unit;
}

type suspended =
  | Suspended : {
      k : ('a, unit) continuation;
      registration : 'a registration;
    } -> suspended

type fiber_state =
  | Running
  | Parked of suspended
  | Cancelling of exn
  | Finished of (unit, exn) result

The existential Suspended constructor associates the registration and continuation with one hidden result type. A successful event can therefore supply the value expected by continue. Cancellation does not need to construct such a value because discontinue injects an exception at the entry point of the continuation instead of supplying a normal operation result. The atomic claim identifies the terminal action that owns the captured stack segment, enforcing a single consumer [11]. Runtime detection of a second resumption is still useful but it comes too late if two competing callbacks have already enqueued work under incompatible ownership assumptions.

OCaml represents captured continuations as heap allocated stack segments. Capture therefore requires neither a copy of the entire stack nor a visible continuation passing transformation of application functions. The Multicore OCaml implementation described in the paper allocates fibres on the C heap with malloc and caches recently freed stacks to reduce the cost of later allocations [4]. A handler_info block holds the parent fibre pointer and the value, exception and effect closures so capture can detach the segment and resumption can reconnect it. In that representation a fibre switch saves and reloads the exception and stack pointers, while relocation updates two fiber_info fields because generated OCaml code holds no pointers into the stack [4]. Cancellation must consume a parked continuation through the runtime interface to enter its cleanup frames. Reclaiming stack memory through the collector would not deterministically release their descriptors and locks.

Discontinuation

Cancellation is delivered through Effect.Deep.discontinue k exn, which resumes $k$ by raising exn inside the suspended computation, outside the scheduler's operation clause [6]. If capture happened at perform (Await r) then the exception appears there and follows ordinary exception handling through the captured extent, with discontinue_with_backtrace available when the original backtrace matters. A Fun.protect frame runs its finaliser when that exceptional path exits its protected computation, connecting the cancellation decision made by the scheduler to cleanup written in ordinary application code.

The scheduler's operation clause executes outside the captured continuation. Raising the exception there therefore does not enter the suspended computation. That raise unwinds the handler invocation while leaving $k$ suspended, while returning without resuming or storing $k$ likewise abandons the cleanup frames that the target still owns. The exchanger example in the manual uses discontinue for exactly this reason when the run queue empties with an exchanger still blocked, delivering Improper_synchronization through the continuation instead of merely reporting failure outside it [5].

The deep handler rule associates an operation captured from evaluation context $E$ with a continuation that reinstalls the handler around that context on resumption. Cancellation uses the same boundary with an exceptional outcome, so the extra machinery is in the scheduler that delays resumption and lets cancellation compete with a normal result. The handler determines which context is captured while the concurrent registry determines who may consume it and where that ownership decision takes effect in the following rules.

Lowering

A scheduler handler can expose suspension through an effect whose argument receives the current fibre context and an enqueue capability for the operation's eventual outcome. The enqueue function packages normal and exceptional completion uniformly but waits until the fibre reaches the runnable queue before turning that result into continue or discontinue. Deferring resumption is necessary when a backend callback runs in an event loop or another domain that cannot safely enter application code. The following skeleton isolates that control boundary and leaves fiber_context, report_failure and the run queue to the surrounding scheduler while leaving the backend implementation unspecified:

open Effect
open Effect.Deep

type 'a enqueue = ('a, exn) result -> unit

type _ Effect.t +=
  | Suspend : (fiber_context -> 'a enqueue -> unit) -> 'a Effect.t
  | Get_context : fiber_context Effect.t

let run_fiber enqueue_ready context computation =
  match_with computation ()
    {
      retc = (fun () -> ());
      exnc = report_failure context;
      effc =
        (fun (type a) (op : a Effect.t) :
             ((a, unit) continuation -> unit) option ->
          match op with
          | Get_context -> Some (fun k -> continue k context)
          | Suspend register ->
              Some
                (fun k ->
                  let enqueue = function
                    | Ok value ->
                        enqueue_ready (fun () -> continue k value)
                    | Error exn ->
                        enqueue_ready (fun () -> discontinue k exn)
                  in
                  register context enqueue)
          | _ -> None);
    }

The captured continuation takes its input type from Suspend, retaining type safety in the Ok value branch without a universal result payload. The exceptional branch applies to every input type because discontinuation raises at the suspension point and requires no value of that type. Naming the parameter op also avoids the effect keyword introduced with handler syntax in OCaml 5.3, while the return annotation on effc keeps its locally abstract a properly scoped [5]. Without that annotation the Get_context branch can force a to fiber_context and leave the Suspend branch unable to typecheck against its own continuation input. A production scheduler must additionally record tracing state and clear installed cancellation functions before resumption while preventing the same fibre from entering the runnable queue twice.

Before publishing a request, the handler checks whether the context is already cancelled. Cancellation traversal may have finished immediately before the fibre attempts to park. Publication must then ensure that a cancellation traversal finds either a valid cancellation function or a state establishing that the operation has already won its race. A single scheduler domain can maintain that ordering by completing the transition without yielding, whereas completion across domains needs an atomic protocol around the backend request itself. These ordering requirements remain the handler's responsibility even though the effect signature hides them from application code.

Races

Readiness and parent cancellation can occur concurrently for a parked read. The operation's linearisation point determines which result is committed. Since both callbacks may already be in flight, the contract cannot assume that cancellation always takes priority. Eio allows an operation that succeeded before cancellation to return its result even while it waits on the run queue, with the cancelled context still able to reject the next operation [7]. That preserves a result the backend has already committed without implying that the scope token has somehow returned to its live state in the meantime.

The claim state begins at Waiting. Completion claims Resumed and cancellation claims Discontinued before the winning path schedules its continuation. Completion then schedules continue k v and cancellation schedules discontinue k c, with exactly one compare and exchange succeeding even if the callbacks run on different cores. The loser still disposes of whatever backend event record it owns but cannot enqueue another resumption, establishing the single consumer guarantee in the following C example:

#include <stdatomic.h>
#include <stdbool.h>
#include <stdint.h>

enum claim { WAITING, RESUMED, DISCONTINUED };

struct continuation;
struct value { uintptr_t bits; };
struct exception { void *payload; };

void schedule_continue(struct continuation *, struct value);
void schedule_discontinue(struct continuation *, struct exception);

struct wait_slot {
  _Atomic enum claim claim;
  struct continuation *continuation;
};

bool claim_value(struct wait_slot *slot, struct value value) {
  enum claim expected = WAITING;
  if (!atomic_compare_exchange_strong_explicit(
          &slot->claim, &expected, RESUMED,
          memory_order_acq_rel, memory_order_relaxed))
    return false;

  schedule_continue(slot->continuation, value);
  return true;
}

bool claim_cancel(struct wait_slot *slot, struct exception reason) {
  enum claim expected = WAITING;
  if (!atomic_compare_exchange_strong_explicit(
          &slot->claim, &expected, DISCONTINUED,
          memory_order_acq_rel, memory_order_relaxed))
    return false;

  schedule_discontinue(slot->continuation, reason);
  return true;
}

Slot publication must establish a release and acquire edge making the initialised continuation and registration visible. Comparing claim later does not itself establish publication. The successful memory_order_acq_rel shown here is conservative and C11 separately requires the failure order to exclude memory_order_release and memory_order_acq_rel while being no stronger than the success order [12]. Reclaiming the slot remains a separate lifetime problem that a complete implementation must solve through scheduler ownership or a mechanism such as epochs or hazard pointers. Winning the claim cannot undo external I/O. A read may have consumed bytes already, and remote processing may continue after its local waiter has disappeared. Cancellation settles the local continuation obligation while any compensation for those external effects belongs to the protocol implemented above the operation rather than to this atomic cell.

Registrations

Discontinuing a continuation does not remove its timer identifier or readiness subscription. Marking the fibre alone can leave a stale callback retaining the backend resource indefinitely. The callback may also retain the continuation and later attempt a second resumption, which is why Leijen installs an on-cancel cleanup to withdraw timer registrations when cancellation crosses their enclosing scope [3]. The claim blocks a second consumption of the continuation, while deregistration bounds the retained memory and backend work.

A cancellable operation publishes a removable registration and an enqueue capability. The removal result normally indicates whether cancellation won before the backend detached the request for completion. The same winner test determines whether cancellation should enqueue an exception or leave the successful path to supply its value through the existing completion capability. The following model expresses this contract independently of epoll, kqueue, IOCP or io_uring, and its poller names stand for the surrounding backend implementation:

let await_readable poller fd =
  Suspend.enter "await_readable" @@ fun fiber enqueue ->
  let request =
    Poller.prepare_readable poller fd
      ~ready:(fun () -> enqueue (Ok ()))
      ~cancelled:(fun exn -> enqueue (Error exn))
  in
  Cancel_context.publish fiber request;
  Poller.arm request

let complete_readable request =
  Poller.try_complete request

let cancel_request request reason =
  Poller.try_cancel request reason

In the sketch, Cancel_context.publish installs the prepared request in a live context or delivers cancellation before Poller.arm exposes completion. Arming must respect the request's terminal state. The cancellation operation specifies a contract. Backends differ in whether removal can establish synchronously that no callback will run. For io_uring a cancellation request can return -EALREADY when the target has progressed beyond cancellation or -ENOENT when no matching request is found, including when it has already completed [15]. If cancellation itself is asynchronous then both callbacks must still use the shared winner cell before touching the continuation, regardless of which backend result they receive. Eio clears the cancel_fn of a registered fibre by replacing it with ignore before invoking the saved function, which prevents a later traversal from repeatedly calling the same obsolete hook [9].

Unwinding

Resource safety depends on acquisition and cleanup positions relative to the handler boundary. Discontinuation can unwind only the frames within the continuation it enters. A file opened inside the computation is covered when its Fun.protect frame lies between the await site and the scheduler handler and the exceptional path exits that frame. A resource owned outside the continuation remains the responsibility of the scheduler, so every registration and descriptor needs an assigned stack or scheduler owner before either cleanup path can establish resource safety.

let with_resource acquire release use =
  let resource = acquire () in
  Fun.protect
    ~finally:(fun () -> release resource)
    (fun () -> use resource)

let with_protected_release acquire release use =
  let resource = acquire () in
  Fun.protect
    ~finally:(fun () ->
      Eio.Cancel.protect (fun () -> release resource))
    (fun () -> use resource)

The first function invokes release after normal completion or exceptional exit through discontinue. This alone does not protect release from persistent cancellation. The second function puts release inside a protected cancellation context so the cancelled token of the parent does not immediately interrupt cleanup that needs to suspend before it can finish. Eio uses this protection for switch release hooks and runs them in LIFO order after the main function has returned and all attached fibres have finished [13]. Protection must remain bounded in purpose and duration. A finaliser waiting indefinitely prevents its parent scope from establishing that all owned resources have been released.

Cleanup requires an explicit exception precedence rule. A cancellation reason and a release failure describe separate events even when they arise from the same fibre. The owner should preserve the primary failure and retain cleanup failures as suppressed or combined exceptions where the reporting model supports them. Eio combines exceptions raised by cancellation functions through Exn.combine, while a structured parent also needs to retain the original child failure that caused its siblings to be cancelled [9].

Protection

A mask preserves the pending request while deferring observation in a region whose resource invariant is temporarily exposed. The interval between resource acquisition and installation of its release action requires such protection: cancellation delivered there can leak the resource although the surrounding states are valid. Scoped blocking and unblocking in Haskell restore delivery state on every exit path for the same reason, and an effect runtime must preserve its corresponding dynamic state when a continuation suspends [10].

An API must specify which of two protection policies it implements, since they differ in behaviour on return. Deferred delivery records the request and raises on exit from protection. Detached protection runs in a child context exempt from parent cancellation. The Cancel.protect function in Eio follows the second policy and deliberately skips a parent cancellation check on return so the caller can handle the protected result even though its parent remains cancelled [7][9]. A masking primitive can follow the first policy instead, which means portable reasoning has to specify whether leaving protection is itself a point where cancellation can be delivered.

Protecting arbitrary application logic prevents its owner from stopping the computation while protection remains active. It may conceal a cancellation race without resolving the ownership problem. A commit may need protection while publishing a state update and durable log record, whereas network conversations and unbounded retries need a route back to cancellable execution. Every protected region requires a bounded route to a state where observing cancellation preserves its resource invariant.

Scopes

Structured concurrency assigns every spawned fibre to an owning scope which waits for its termination. Cancellation propagates down the ownership tree, and results return to the joining owner. Protected cleanup subscopes block cancellation propagation while remaining owned work that must terminate before the enclosing resource scope returns. Eio represents cancellation contexts as a tree within each domain and keeps child contexts and fibres in intrusive Lwt_dllist lists, traversing children recursively while stopping at protected nodes [9].

The scope tree records ownership independently of execution order. Scheduling a child before its parent next reaches the queue does not change the parent's obligation to join it. Schedulers that distribute work across domains must preserve the same ownership obligations even though the tree itself does not impose an ordering on when siblings execute. The both combinator in Eio cancels one branch when the other fails and waits for both to finish before raising the original failure, while a race likewise waits for its losing work to terminate [8].

let concurrently left right =
  Eio.Fiber.both left right

let race left right =
  Eio.Fiber.first left right

let serve listener handle =
  Eio.Switch.run @@ fun sw ->
  while true do
    let connection, address = Eio.Net.accept ~sw listener in
    Eio.Fiber.fork ~sw (fun () -> handle connection address)
  done

Eio.Fiber.first allows for both branches succeeding before either result is observed and supplies a combine argument that defaults to fun a _ -> a when two successful values exist [8]. A committed completion cannot be erased retrospectively. The cancelled token can still prevent the branch from initiating another cancellable operation. Defining the winner by the committed scheduler decision avoids relying on a wall clock order that the scheduler and backend may observe differently.

Reporting

Failure and cancellation share an exceptional delivery mechanism but require distinct reporting decisions from the owning scope. A child failure says the attempted work did not complete correctly and gives the scope a reason to cancel siblings before reporting that failure to its own owner. A sibling's resulting Cancelled exception normally confirms shutdown. An independent cleanup exception is an additional failure and must not silently replace the initiating error.

User initiated cancellation may be the primary reason when no computation has failed. Logging the same event independently for every cancelled fibre can obscure that initiating reason. The scope owner should classify the reason after all children reach terminal states. Eio keeps this distinction between cancelling a context to stop fibres and failing a switch to record an error that Switch.run will later raise [7][13].

Catching Cancelled does not clear the token or end the owner's wait for termination. Continuing unrelated application work then conflicts with the scope's lifetime contract. Cleanup may catch it long enough to restore an invariant and then return or raise it again unless it has explicitly entered protection with a different ownership arrangement. A library that catches every exception should check cancellation before swallowing one because an intervening abstraction may hide the concrete exception wrapper it originally received. Persistent checks reassert cancellation at the next checkpoint, but cannot force uncooperative CPU bound code to reach it.

Extent

An algebraic operation reaches the nearest accepting handler. Moving a cancellation handler consequently changes which outstanding operations a request can reach. The cancelable handler developed by Leijen tracks awaits in its lexical scope and forwards cancellation identifiers outward when the request targets an enclosing scope rather than the local one [3]. That allows a nested timeout or race to remain isolated from unrelated siblings while explicit scope identities can still let another fibre request cancellation remotely.

Resuming a deep continuation reinstalls its handler. Subsequent awaits therefore reach the same scheduler unless intercepted by an inner handler. A shallow continuation carries no handler of its own and Effect.Shallow.continue_with requires one explicitly through the type ('c, 'a) continuation -> 'c -> ('a, 'b) handler -> 'b [16]. That extra argument makes the next protocol state explicit at the cost of more scheduler bookkeeping, with both forms and their reinstatement behaviour documented in the OCaml manual [5].

Cancellation state belongs to the fibre. A domain can suspend one fibre and run another with a different context, so operating system thread state cannot identify the applicable cancellation scope. A scheduler that permits migration also has to preserve that context across domains, while the representation described in the OCaml paper makes relocating a fibre comparatively cheap through two fiber_info updates [4]. Fibre local storage preserves context identity. Permission to mutate its cancellation tree still depends on domain ownership. Eio enforces that distinction with an ownership check that raises Invalid_argument for access from the wrong domain, turning the single writer rule of the context into a runtime invariant [9].

Delivery

A pure loop without cancellation checkpoints cannot be stopped by this cooperative protocol. Defining a Cancel constructor does not transfer control to the handler. A compiler can insert polls at loop back edges or allocation paths but those polls need an explicit cancellation mechanism rather than automatically inheriting the policy of the handler. Without such a mechanism, the longest interval between checkpoints determines cancellation latency. Updating the token promptly does not establish prompt termination.

A foreign call may block in an operating system function while the managed runtime cannot unwind its C stack. A cancellable binding can arrange an external wakeup or backend cancellation and deliver Cancelled once execution returns to managed code, provided that action respects the resource contract of the binding. Without this support, the request remains pending until return. Terminating the underlying thread could violate language runtime and foreign library invariants.

An uncancellable foreign function inside a finaliser can keep the scope open even after correct discontinuation of the continuation. The claim protocol has established a single consumer, but the resource contract supplies no terminating exceptional path for the owner. Correct handler semantics therefore need cancellation aware bindings and bounded cleanup behaviour before the library can promise that joining a cancelled child will finish promptly.

Properties

Safety and liveness obligations can be stated independently of the scheduler's poller representation. A successful claim permits at most one consumption of a suspended continuation. Its owning scope cannot finish until it has eventually been continued or discontinued. Tokens move only from live to cancelled and active descendants either observe cancellation or terminate before scope exit, while registrations must eventually complete or be withdrawn without retaining dead continuations indefinitely.

Resource safety requires discontinuation within the captured extent, followed by ordinary exception handling and cleanup as protected frames are exited. Scope safety requires every owned child and protected cleanup scope to terminate before the owner returns, while race safety requires concurrent completion and cancellation to agree on one consumer. Establishing these invariants requires the handler, registry and ownership tree; the operation signature alone is insufficient.

The liveness formula assumes fairness and cooperation. A runnable fibre that never yields can starve scheduler work, and an unresponsive backend can leave an operation parked indefinitely. Protected regions require a termination assumption or bound, since they suppress the propagation that would otherwise request their shutdown. With those premises the semantics describes a route to termination when the program and backend honour their cancellation points, without promising to stop arbitrary foreign code at any machine instruction.

Composition

At an algebraic effect boundary, the scheduler receives a continuation that can be resumed with an operation result or discontinued with a cancellation exception. This decision requires a persistent scope token, a single winner for each parked operation, and a join that waits for unwinding to complete. The discontinue primitive supplies exceptional resumption while propagation and protection remain policy decisions, with handlers delimiting control and scopes delimiting ownership as the registry connects both to external events.

References

1. Gordon D. Plotkin and Matija Pretnar establish the algebraic account of handlers and operation clause continuations in Handling Algebraic Effects, published in Logical Methods in Computer Science 9(4) in 2013.
2. Andrej Bauer and Matija Pretnar describe cooperative scheduling through effect operations and handler managed continuations in Programming with Algebraic Effects and Handlers, published in the Journal of Logical and Algebraic Methods in Programming 84(1) in 2015.
3. Daan Leijen develops scoped asynchronous operations and cancellation aware resumption together with timeouts and callback withdrawal in Structured Asynchrony with Algebraic Effects, a Microsoft Research technical report published in 2017.
4. K. C. Sivaramakrishnan, Stephen Dolan, Leo White, Tom Kelly, Sadiq Jaffer and Anil Madhavapeddy describe the stack segment representation and runtime costs of capture and resumption in Retrofitting Effect Handlers onto OCaml, presented at PLDI 2021.
5. The effect handlers chapter of the OCaml 5.3 Reference Manual documents deep and shallow handlers alongside linear continuation use and discontinuation for deterministic resource unwinding.
6. The OCaml developers specify continue and discontinue together with discontinue_with_backtrace and the deep handler record in the Effect.Deep library reference for OCaml 5.3.
7. The Eio.Cancel documentation describes cancellation context trees and persistent checks together with protected subcontexts and the precedence of results that are waiting on the run queue.
8. The Eio.Fiber documentation specifies structured fiber combinators and joining behaviour, including sibling cancellation and the combine argument used when both branches of a race have succeeded.
9. The Eio cancellation context implementation at revision 53856d7 supplies the concrete context states and protected child traversal discussed here together with cancellation functions and the domain ownership check.
10. Simon Marlow, Simon Peyton Jones, Andrew Moran and John Reppy give an operational treatment of asynchronous delivery and scoped masking in Asynchronous Exceptions in Haskell, presented at PLDI 2001 with interruptible operations and resource bracketing.
11. Carl Bruggeman, Oscar Waddell and R. Kent Dybvig develop implementation techniques and ownership assumptions for continuations invoked at most once in Representing Control in the Presence of One Shot Continuations, presented at PLDI 1996.
12. The WG14 N1570 draft of Programming Languages C from 2011 defines the relevant memory model and atomic operations in sections 5.1.2.4 and 7.17, with compare and exchange failure orders constrained by section 7.17.7.4.
13. The Eio.Switch documentation specifies resource ownership and waiting for attached fibers alongside failure propagation and the protected LIFO release hooks that run when a switch terminates.
14. The OCaml developers document the effect type and perform alongside Unhandled and Continuation_already_resumed in the Effect library reference for OCaml 5.3.
15. The io_uring_prep_cancel(3) manual by Jens Axboe describes asynchronous cancellation and its -EALREADY and -ENOENT outcomes when the target cannot be cancelled or found.
16. The Effect.Shallow library reference for OCaml 5.3 specifies continue_with and discontinue_with together with the handler argument required by every shallow resumption.