The semantics of cancellation under algebraic effects

Cancellation gets easier to reason about once you treat it as a protocol over suspended computations rather than expecting one exception or effect operation to do all the work. An effect handler gives an asynchronous request a boundary at which to expose its continuation but the scheduler still has to decide who owns it and what happens when completion races with cancellation. Raising inside an operation clause leaves the captured continuation suspended, whereas discontinuing it raises at the perform site and enters the frames responsible for the resources owned by the computation. Those two paths explain why a cancellation model needs to connect ordinary exception handling to the scheduler registry and the scope tree that keeps unfinished work attached to its owner.

Protocol

Calling cancel sounds like one action but the implementation has to issue a request and make it visible before the target can receive it at an interruption point and finish unwinding. A requester that returns as soon as the token changes offers a different guarantee from one that waits for cleanup, even if both APIs expose exactly 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.

Algebraic effects leave the cancellation policy to the handler because the operation supplies a request and a delimited continuation without deciding how either should be used [1][2]. Defining Cancel as an operation is perfectly reasonable and Leijen does this for structured asynchrony in Koka, where the requesting strand returns 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 surface signature below keeps asynchronous suspension separate from cancellation of a named scope and from an explicit checkpoint where the current computation checks its own cancellation state. It stays small because timeouts and parent failure can produce cancellation reasons through the same interface that a race uses to stop its losing branch:

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 the result index of its request so a read resumes with an int while a timer resumes with unit, with the GADT recovering the required type equality when the handler matches the constructor. 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. Keeping these paths separate gives the handler enough type information to resume an operation correctly without committing the interface to a particular scheduler representation.

Transitions

Let the scheduler state be Σ = ⟨F, R, Q⟩ where F maps fiber identifiers to their states and R maps backend registrations to suspended continuations, with Q holding runnable work. Each cancellation scope carries a monotone token that is either ℒ for live or ℂ(r) for cancelled with reason r, and this model keeps the first reason it receives. Keeping that reason makes repeated requests idempotent and stops a timeout that expires later from replacing the child failure that actually caused 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 fiber observes the token at a checkpoint or when entering a cancellable operation while a parked fiber can be reached through the registration its operation stored 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 fiber can receive cancellation promptly only if its backend registration has a live cancellation function that can remove or invalidate the pending request. Neither route tells the parent that cleanup has finished, so a parent that needs to close the lifetime of the target still has to join it after requesting cancellation.

The token makes this a level triggered model because every later check sees the same cancelled state until execution leaves the scope in which that state applies. Catching one Cancelled exception does not reset anything and the next cancellable operation may raise again, which prevents a broad exception handler from silently making the request disappear. Eio follows this approach by storing cancellation in a context and invoking the current cancellation function of a parked fiber, 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

When Await request reaches the scheduler handler it captures the evaluation context between the perform site and that handler as a continuation k expecting the result type of the request. Registering the external operation and storing k in a parked fiber record transfers responsibility for that continuation from the running stack to the scheduler registry. Leaving it suspended keeps its resource obligations unresolved, while trying to invoke it twice violates the single use discipline needed 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 packages the registration and continuation under one hidden result type so a successful event supplies exactly the value that continue expects. 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 records which terminal action has won ownership and turns the captured stack segment into a scheduler object with a single permitted 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 using heap allocated stack segments rather than copying the entire stack or rewriting every source function into visible continuation passing style. The Multicore OCaml implementation described in the paper allocates fibers 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 fiber pointer and the value, exception and effect closures so capture can detach the segment and resumption can reconnect it. In that representation a fiber 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]. This is why cancellation should consume a parked continuation through the runtime interface rather than leave a collector to reclaim its memory without deterministically releasing the descriptors and locks owned by its frames.

Discontinuation

The primitive that delivers cancellation is Effect.Deep.discontinue k exn, which resumes k by raising exn inside the suspended computation rather than inside the operation clause of the scheduler [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.

Raising the same exception directly inside the operation clause of the scheduler does not enter the suspended computation because the clause executes outside the continuation that it captured. That raise unwinds the handler invocation while leaving k suspended, and 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].

Under the usual deep handler rule an operation captured from evaluation context E receives a continuation that reinstalls the handler around that context when it resumes. 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 minimal scheduler handler needs a suspension effect whose argument receives the current fiber context and an enqueue function for whichever result eventually wins the operation. The enqueue function packages normal and exceptional completion uniformly but waits until the fiber reaches the runnable queue before turning that result into continue or discontinue. This delay matters because a backend callback may run in an event loop or on another domain where entering arbitrary application code would break the assumptions of the scheduler. The following skeleton isolates that control boundary and leaves fiber_context, report_failure and the run queue to the surrounding scheduler rather than pretending to implement a complete backend:

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 continuation captured by the effect clause takes its input type from Suspend, which keeps the Ok value branch type safe without routing results through a universal payload. The exceptional branch works for any input type because discontinuation raises at the suspended operation instead of trying to manufacture a 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 fiber from entering the runnable queue twice.

The handler needs to check for an already cancelled context before publishing a new request because cancellation may have completed its traversal just before the fiber tries 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. The effect signature keeps those details out of application code but the handler still has to implement them for the operation to have the promised semantics.

Races

A parked read can become ready just as its parent is cancelled and neither event has an unconditional right to win before the implementation has defined its linearisation point. Both callbacks may already be in flight by then, so the contract needs to say which result is committed rather than simply promise 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 smallest useful claim state has Waiting as its only nonterminal value and lets completion claim Resumed or cancellation claim Discontinued before either 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, which gives the following C example its single consumer guarantee:

#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;
}

The initialised continuation and registration must become visible through the release and acquire edge that publishes the slot, since later comparisons of claim do not establish that publication by themselves. 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 also does not undo external I/O because a read may already have consumed bytes or a remote service may continue processing 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

A timer identifier or readiness subscription remains a backend resource after its continuation has been discontinued, and merely marking the fiber can leave a stale callback holding that 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 prevents that late callback from consuming the continuation again but deregistration is still needed to bound the memory and backend work left behind.

A cancellable operation therefore publishes both a removable registration and an enqueue capability, with the removal result normally indicating 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 makes that contract explicit without choosing 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 this sketch Cancel_context.publish either installs the prepared request into a live context or delivers cancellation before Poller.arm can expose backend completion, with arming required to respect the terminal state of the request. Real backends differ in whether removal can prove synchronously that no callback will run, so this cancellation operation expresses a contract rather than one portable system call. 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 fiber 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 comes down to where acquisition and cleanup sit relative to the handler boundary because discontinuation can only unwind frames inside 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 a review needs to assign every registration and descriptor to the stack or scheduler state before relying on either cleanup path.

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 runs release when the protected computation returns normally or exits through an exception delivered by discontinue, but that 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 fibers have finished [13]. Protection still needs to stay narrow because a finaliser that waits indefinitely also prevents its parent scope from establishing that every owned resource has been released.

Cleanup needs an explicit exception precedence rule because a cancellation reason and a failure during release describe different events even when they come from the same fiber. Discarding either one can lose information, so the owner should preserve the primary failure and retain cleanup failures as suppressed or combined exceptions where its reporting model allows. 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 leaves the cancellation request pending while deferring observation through a region whose resource invariant is temporarily exposed, rather than making the request disappear from the token. The usual example is the interval between acquiring a resource and installing its release action because delivery there can leak a resource even though both 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].

Protection has two different meanings here and it helps to state which one an API provides before relying on what happens when the protected function returns. Deferred delivery records the request and raises when execution leaves the protected region, whereas detached protection runs in a child context that its parent does not cancel. 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.

Wrapping arbitrary application logic in protection may hide an intermittent cancellation race but it also removes the ability of the owner to stop that work while the protected region remains active. 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. Each protected region therefore owes a bounded route to a state where cancellation can be observed without breaking the invariant that protection was introduced to preserve.

Scopes

Structured concurrency gives each spawned fiber an owning scope that cannot finish until the fiber terminates, with cancellation travelling down the ownership tree and results travelling back towards the joining owner. Protected subscopes stop cancellation propagation for their cleanup but remain owned work that must finish before the enclosing resource scope can return to its caller. Eio represents cancellation contexts as a tree within each domain and keeps child contexts and fibers in intrusive Lwt_dllist lists, traversing children recursively while stopping at protected nodes [9].

The scope tree records ownership rather than execution order, so a child running before its parent next reaches the queue does not change who must eventually 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 completion that has crossed its linearisation point cannot be erased retrospectively, although the cancelled token can still prevent that branch from starting another cancellable operation. Treating the winner as a committed scheduler decision avoids promising a wall clock ordering that the scheduler and backend cannot necessarily observe in the same way.

Reporting

Failure and cancellation can use the same exceptional delivery mechanism while still requiring different reporting decisions from the scope that owns the computation and its resources. 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. The resulting Cancelled exception from a sibling normally confirms that shutdown was obeyed, while a new exception during cleanup adds a separate failure that must not silently replace the original.

User initiated cancellation can be the primary reason when no computation has failed but that does not make an independent error log from every cancelled fiber useful to the caller. Repeating the same control event across targets can obscure the initiating operation, so the scope owner should classify the reason after all children have reached terminal states. Eio keeps this distinction between cancelling a context to stop fibers and failing a switch to record an error that Switch.run will later raise [7][13].

Catching Cancelled and continuing with unrelated application work leaves the token set while the owner waits for termination, which makes the apparent recovery conflict with the lifetime contract of the scope. 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 can recover at the next cancellation point but cannot force CPU bound code to reach that point while it continues executing without cooperation.

Extent

An algebraic operation travels to the nearest handler that accepts it, so moving a cancellation handler changes which outstanding operations a particular request has authority to 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 fiber request cancellation remotely.

A deep continuation reinstalls its handler when resumed so later awaits return to the same scheduler unless an inner handler accepts those operations before they reach it. 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 has to follow the fiber rather than the operating system thread because a domain can suspend one fiber and run another with a different current context. A scheduler that permits migration also has to preserve that context across domains, while the representation described in the OCaml paper makes relocating a fiber comparatively cheap through two fiber_info updates [4]. Keeping a context in fiber local state preserves its identity but does not by itself grant permission to mutate the same cancellation tree from any domain. 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

Cooperative cancellation cannot stop a pure loop that never reaches a cancellation checkpoint because the handler receives no control merely from the existence of a Cancel constructor. 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 that mechanism the longest region between cancellation points determines latency, so setting the scope token quickly says very little about when the target will actually stop.

Foreign calls add another gap because the managed runtime may be unable to unwind a C stack while an operating system function is blocked inside it. 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. A binding without that support must leave the request pending until return because killing the underlying thread can violate the invariants of both the language runtime and the foreign library.

Cleanup has the same limitation because a finaliser that enters an uncancellable foreign function can hold the scope open even after the continuation has been discontinued correctly. The continuation claim has done its job in that case but the resource contract has failed to provide a terminating exceptional path for the scope 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

The implementation can be checked against safety and liveness properties that stay meaningful when the scheduler changes its backend rather than depending on a particular poller representation. Each suspended continuation is consumed at most once through a successful claim and must eventually be continued or discontinued before its owning scope can finish. 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 to enter the captured extent and follow ordinary exception handling so cleanup runs as protected frames are exited rather than being bypassed by a scheduler exception. 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. These properties depend on the handler and registry as well as the ownership tree, so the operation signature alone cannot establish the invariants expressed below.

The liveness formula needs fairness and cooperation assumptions because a runnable fiber that never yields can starve scheduler work and a backend that never responds can leave a wait parked indefinitely. Protected regions also need their own termination assumption or bound because stopping downward cancellation propagation removes the mechanism that would otherwise ask that work to finish. 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

Algebraic effects expose suspension at a handler boundary and give the scheduler a continuation that can eventually receive either the normal result of the operation or a cancellation exception. Making that choice safely still requires a persistent scope token and a single winner for each parked operation together with a join that waits for unwinding to finish. 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.