Sec Manual / Cancellation and Context

Cancellation and Context

Cancellation in Sec is cooperative. One execution entity may request that another stop, but safe Sec code is not torn down at an arbitrary instruction. Cancellation becomes terminal only when the target execution observes the request and commits cancellation at an explicit check or a cancellation-aware operation boundary.

Sec deliberately separates two related but different mechanisms. Execution cancellation applies to the current Task[T] or Thread[T]. Context cancellation is an operation-local capability used to propagate a cancellable branch and optional deadline through APIs without granting a callee authority to cancel its caller's execution identity.

Core rule: RequestCancel() requests cooperative cancellation. It does not consume a lifecycle handle and does not mean the target has already stopped. Terminal cancellation is a separate committed control-flow event.

Purpose

Concurrent code needs a way to stop work that is no longer required without losing ownership, skipping cleanup or introducing unsafe asynchronous teardown. Sec's cancellation model therefore preserves deterministic destruction and explicit lifecycle ownership while still allowing waits and long-running operations to react to cancellation requests.

The model covers:

  • requesting cancellation of tasks and threads;
  • observing cancellation on the current logical task or physical thread;
  • the terminating cancel statement;
  • cancellation-aware operation commit races;
  • compiler-inferred requirements for cancellable execution;
  • Context, ContextSource and deadlines;
  • deterministic cleanup and memory visibility.

Cooperative Cancellation

A cancellation request is state, not an asynchronous exception. Safe Sec does not destroy a task or thread merely because another execution called RequestCancel().

The target may react through:

  • an explicit CancelRequested check followed by cancel;
  • a cancellation-aware wait such as await, lock acquisition or a channel wait;
  • another operation whose rulebook defines a cancellation commit boundary.

Cancellation is distinct from a normal return, Err(E), panic, hard thread termination, process termination and hardware reset. A timeout on one operation is also not automatically terminal cancellation of the task or thread that performed it.

Task and Thread Identity

Sec supports cooperative cancellation for two execution identities: 

Task[T]
Thread[T]

A task is a logical Sec execution identity. A thread is a physical/native execution identity. They remain distinct even when a task currently runs on that thread.

Task migration does not change task cancellation identity. Likewise, cancelling a task must not implicitly cancel its executor thread, and cancelling a physical thread must not silently rewrite the cancellation state of a logical task running on it.

RequestCancel()

Both owning handle types expose the same cancellation request operation: 

impl Task[T] {
    fn RequestCancel() void
}

impl Thread[T] {
    fn RequestCancel() void
}

RequestCancel() is:

  • cooperative;
  • idempotent;
  • non-consuming;
  • a no-op after terminal completion.
let worker := try spawn Work()
worker.RequestCancel()
let outcome := await worker

Requesting cancellation does not resolve the lifecycle obligation. An owning task or thread handle must still be awaited, joined, detached or transferred according to the owning lifecycle rules.

Current Execution Contexts

Current-execution observation deliberately mirrors the two execution identities: 

Task.Current().CancelRequested
Thread.Current().CancelRequested

The compiler-known views are:

type TaskContext

type ThreadContext

TaskContext is a non-owning view of the current logical task; ThreadContext is a non-owning view of the current physical thread. Neither view grants lifecycle ownership or cancellation authority over an owning handle.

Task.Current() is valid only where a logical task context exists. Thread.Current() additionally depends on the selected target/profile having a physical-thread context. The compiler must not fabricate one from the other.

The cancel Statement

The complete Sec 0.1 source syntax is:

cancel

cancel is a terminating statement, not an expression. It commits terminal cooperative cancellation of the current cancellable execution entity.

If a logical task exists, bare cancel terminates that task. Otherwise, in an explicit cancellable physical thread callable, it terminates that thread. Task identity therefore takes precedence when task code is running on a worker thread. 

if Task.Current().CancelRequested {
    cancel
}

Merely reading CancelRequested does not terminate execution. Code may observe the request, perform bounded cleanup or bookkeeping, and execute cancel when it is ready to commit terminal cancellation.

Cancellation Cleanup

Terminal cooperative cancellation follows ordinary deterministic cleanup rules. Active defer blocks run, owned values are destroyed and resources release through their normal ownership paths.

A live MutexGuard[T] owned by the cancelling execution must therefore be destroyed and release its lock before terminal cancellation completes.

Rule: cancel is invalid inside defer. Cleanup code may not recursively replace the terminal control flow already performing that cleanup.

Cancellation does not fabricate a normal result value and does not become an Err(E) merely because the callable's declared return type is Result[T, E].

Inferred Cancellation Requirement

Sec 0.1 has a compiler-inferred semantic effect meaning that a callable requires a current cancellable execution context. There is no required source annotation such as @cancellable. 

fn Inner() void {
    cancel
}

fn Outer() void {
    Inner()
}

Both functions require current cancellable execution. The requirement propagates transitively through the semantic call graph, recursion, generic instantiation and indirect callable values. Storing a cancellation-dependent function in a function value must not erase the requirement.

Task.Current() carries the more specific requirement that a current logical task exists. Thread.Current() instead carries a physical-thread capability requirement.

Cancellation Points

A cancellation point is an operation boundary where pending current-execution cancellation may compete with the operation's own normal commit.

Examples include:

  • await;
  • cancellation-aware join;
  • blocking channel send/receive;
  • waiting select;
  • mutex acquisition;
  • timer and I/O waits;
  • runtime/task yield where the owning rule defines cancellation awareness;
  • target-declared interruptible waits.

Each owning rulebook defines exactly what counts as a successful operation commit. Cancellation does not invent a generic fallback result for every operation.

Commit Races

Every cancellation-aware operation must resolve to exactly one committed source-level outcome.

  • If cancellation commits first, no partial operation result or ownership transfer may remain.
  • If the operation commits first, its result and ownership effects are real.
  • A later cancellation observation must not roll back a committed operation.
  • Runtime wakeup races must not produce both outcomes.
  • Runtime wakeup races must not lose both outcomes and abandon ownership/state.

This first-commit discipline is the common rule used by await, select, channels, mutex acquisition and other waits.

Await and Join

Cancellation of the waiting execution is different from cancellation of the execution being awaited or joined.

For consuming await, the await rulebook defines the stronger cleanup rule: if caller cancellation wins before await commit, await retains lifecycle ownership, requests cancellation of the child, waits for a terminal child outcome, destroys that outcome exactly once and only then allows caller cancellation to complete.

Join remains distinct because it preserves the owning handle. Cancellation must not lose that handle in a completion/cancellation race.

Channels and Select

Cancellation must never partially transfer a channel message. If cancellation wins before channel commit, ownership remains according to the channel's pre-commit state. If the channel operation commits first, its exact send/receive result and ownership changes remain committed.

For select, a cancellation winner before branch commit means that no branch may consume ownership, no message may transfer, no task/thread result may be consumed and losing registrations must be removed.

Sec 0.1 channel APIs do not implicitly read a lexical Context. Channel wait timeouts are composed explicitly through select and after.

Mutex Acquisition

Ordinary Mutex[T].Lock() acquisition and current-execution cancellation compete at the acquisition boundary.

  • If cancellation commits first, no MutexGuard[T] exists.
  • If acquisition commits first, the caller owns the guard.
  • If cancellation follows, deterministic cleanup releases the acquired guard.

A Context-aware lock additionally has a separate operation-local Context outcome. That does not merge Context cancellation with current task/thread cancellation.

Memory Semantics

Cancellation request state must be safely observable and data-race-free. The compiler and runtime may use atomics or another target primitive internally, but the source semantics remain the same.

A cancellation request does not automatically publish unrelated application data. Shared mutable data still requires a mutex, atomic, channel, completion synchronization or another canonical happens-before relation.

Context Model

Context is a separate capability model for operation-local cancellation and deadlines. Sec separates observation/propagation from cancellation authority.

  • Context is the observation and propagation capability.
  • ContextSource owns cancellation authority for one derived branch.
  • A callee receiving only ref Context cannot cancel its caller's branch.
  • Context termination does not itself terminally cancel the current task or thread.

Context Types

The canonical source-visible types are:

enum ContextError error {
    // Explicit or inherited Context cancellation committed first.
    Cancelled

    // The effective Context deadline expired first.
    DeadlineExceeded
}

@noCopy
type Context

@noCopy
type ContextSource

Context may be owned as a standalone value, moved to another owner and borrowed as ref Context. It does not grant cancellation authority.

ContextSource owns exactly one child Context, cancellation authority for that branch and the associated deadline/timer/cancellation registrations. A child Context owned by a source cannot be moved out of it.

Context API

The canonical public surface is:

impl Context {
    static fn Background() Context

    fn WithCancel() ContextSource
    fn WithTimeout(timeout: duration) ContextSource
    fn WithDeadline(deadline: Instant) ContextSource

    IsCancelled bool
    Error Option[ContextError]
    Deadline Option[Instant]
}

impl ContextSource {
    Context ref Context

    fn Cancel() void
}

Context intentionally has no Cancel() method. Cancellation authority remains with ContextSource. Its Context property is borrowed access to the child and has static type ref Context.

ContextSource.Cancel() is idempotent. It changes the still-existing child Context to its terminal cancellation state when cancellation wins, but it does not destroy either the Context or the source.

Context Hierarchy

Parent cancellation propagates downward to still-existing descendants. Cancellation does not propagate upward, and cancelling one child branch does not automatically cancel sibling branches. 

let root := Context.Background()
let request := root.WithCancel()
let database := request.Context.WithTimeout(2)

A derived ContextSource depends on its parent Context lifetime and cannot outlive that parent. This keeps the cancellation tree and borrowed Context identities deterministic under ordinary ownership rules.

Deadlines and Timeouts

Context timeouts use Sec's existing lowercase duration type. Absolute deadlines use Instant. 

let child := parent.WithTimeout(5)
let deadlineChild := parent.WithDeadline(deadline)

A child cannot have an effective deadline later than an earlier parent deadline. WithTimeout derives a monotonic deadline from the current monotonic time, then applies the parent bound.

A Context has exactly one committed terminal cause: Cancelled or DeadlineExceeded. Whichever commits first remains the immutable Context.Error; a later cancellation or deadline expiry does not rewrite it.

Context vs Execution Cancellation

Passing ref Context to an operation does not make that Context the current task or thread cancellation identity.

If a Context-aware operation sees its supplied Context cancel first, it returns or propagates ContextError.Cancelled. If the effective deadline wins, it returns or propagates ContextError.DeadlineExceeded. Neither event by itself terminally cancels the current task or thread.

Current-execution cancellation remains independently active and, when it wins at a cancellation point, follows terminal execution cancellation cleanup rather than being converted into a ContextError.

Ownership and Lifetimes

Both Context and ContextSource are @noCopy. Standalone Context values move according to ordinary Sec ownership rules. The child Context inside a source is borrow-only outside that source. 

fn QueryDatabase(ctx: ref Context) Result[Data, DatabaseError] {
    let query := ctx.WithTimeout(2)
    return ExecuteQuery(query.Context)
}

A function that only needs to observe or propagate Context should normally accept ref Context. If it needs its own cancellation authority, it derives its own child source instead of receiving authority over the parent's branch.

Destroying ContextSource destroys its child Context and associated registrations according to ownership rules. Destruction itself is not a cancellation event and must not synthesize ContextError.Cancelled.

Target and Runtime Requirements

The selected CompilationPlan determines how cooperative cancellation, wakeups, timers and waiting operations are implemented. A target may use atomics, scheduler state, RTOS primitives, native thread facilities or another mechanism as long as the same Sec semantics are preserved.

Target/runtime choices must preserve data-race-free request observation, exactly-one commit at cancellation points, deterministic cleanup and exactly-one terminal Context cause. Unsupported target capabilities are diagnosed through target validation rather than by changing the source type model.

Diagnostics and Tooling

Useful diagnostics include:

cancel is not valid inside defer cleanup

call to ProcessBatch requires a current cancellable task or thread execution context

ContextSource.Context is borrowed from its ContextSource and cannot be moved out

Context does not grant cancellation authority; cancel the owning ContextSource instead

Tooling should preserve the symmetric Task/Thread API names while still showing their distinct identities. LSP hover and completion should expose the canonical RequestCancel(), CancelRequested, ContextError and Context surfaces from compiler/Sema facts rather than maintaining a parallel model.

Implementation Status

The cancellation rulebook is normative revision 2.0. The current implementation is partial and is tracked in governance/concurrency_cancellation.yaml.

Implemented today:

  • Task[T] and Thread[T] expose compiler-known RequestCancel().
  • The call has the exact zero-argument, void, idempotent, non-consuming surface.
  • Sema and LSP preserve the canonical member identity and hover/completion information.

Still planned or incomplete:

  • Task.Current() and full TaskContext cancellation observation;
  • full synchronization of Thread.Current()/ThreadContext;
  • runtime cancellation state, wakeups and cancellation-point commit races;
  • deterministic runtime cancellation cleanup and terminal outcome publication;
  • compiler-inferred cancellation effects through the complete call graph;
  • the complete Context/ContextSource/ContextError subsystem;
  • Semantic IR and target/runtime lowering for cancellation.

Best Practices

  • Treat RequestCancel() as a request, not proof that the target has stopped.
  • Resolve lifecycle ownership after requesting cancellation.
  • Use Task.Current() for logical task cancellation and Thread.Current() for physical thread cancellation.
  • Use cancel only to commit terminal cancellation of the current execution.
  • Do not use cancel inside defer.
  • Do not treat Context cancellation as terminal current-execution cancellation.
  • Pass ref Context when a callee needs observation/propagation but not cancellation authority.
  • Derive a child ContextSource when a callee needs to cancel its own branch.
  • Use duration and Instant for timeout/deadline APIs; do not invent another duration type.
  • Remember that cancellation-state publication does not synchronize unrelated mutable application data.
  • At cancellation points, reason in terms of operation commit versus cancellation commit, never partial success.

Summary

  • Cancellation in Sec is cooperative and never arbitrary safe-code teardown.
  • Task[T] and Thread[T] expose non-consuming, idempotent RequestCancel().
  • Task and thread cancellation identities remain distinct.
  • Task.Current().CancelRequested observes logical task cancellation.
  • Thread.Current().CancelRequested observes physical thread cancellation.
  • cancel terminally cancels the current task when one exists, otherwise an eligible explicit thread.
  • Terminal cancellation runs ordinary defer/destruction cleanup.
  • Cancellation requirements are compiler-inferred and propagate transitively through callables.
  • Cancellation-aware waits use an exactly-one commit discipline.
  • Operation success cannot be rolled back after commit, and cancellation cannot leave partial ownership transfer.
  • Context is an operation-local cancellation/deadline capability, not the current execution identity.
  • Context grants observation/propagation; ContextSource grants cancellation authority.
  • ContextError is exactly Cancelled or DeadlineExceeded.
  • Context terminal cause is first-wins and immutable.
  • Parent Context cancellation propagates downward, never upward.
  • Both Context and ContextSource are @noCopy.
  • The child Context owned by ContextSource is borrowed through ContextSource.Context.
  • Cancellation requests and Context state are safely observable but do not publish unrelated program data.
  • The normative model is complete; current implementation support remains partial.
Previous: Threads and Thread-Local Storage Next: Scheduling, Blocking and Structured Concurrency