Regions, the cancellation protocol, obligations, capabilities, the scheduler, and the lab runtime: how each works, and where each one's guarantee stops.
Tasks, actors, fibers, and remote work all hang off one region tree. Obligations are tracked per region, and the scheduler gives cancelling tasks their own lane.
Every task belongs to a region. A region doesn't finish closing until its children have finished, its finalizers have run, and its registered obligations are resolved.
01 asupersync::{main, prelude::*};02 03#[main]04 main(cx: &Cx) {05 // A scope whose tasks get at most 64 polls each.06 scope = cx.scope_with_budget(Budget::new().with_poll_quota(64));07 tasks = JoinSet::new(&scope);08 09 value 1..=2_u32 {10 tasks11 .spawn(cx, |_| { Ok::<_, Error>(value) })12 .expect("spawn region-owned task");13 }14 15 results = tasks.join_all(cx).;16 // Nothing spawned into the set is still running here.17 assert_eq!(results.len(), 2);18}cx.spawn puts the task in the calling context's regionRegionThe scope that owns tasksEvery task belongs to a region, and regions nest into a tree. Closing a region cancels whatever is still running in it, waits for those tasks to finish, runs finalizers, and resolves obligations before it reports done. Tasks spawned through a Cx belong to that Cx's region; tasks spawned through a RuntimeHandle belong to the root region.. cx.scope() gives you a ScopeScopeA handle for spawning into a regioncx.scope() gives you a Scope for the current region; scope.region(…) opens a child region that must reach quiescence before it returns. Scopes also host the drain-correct combinators: race, timeout, hedge, quorum, first_ok, pipeline, and map_reduce. for that region, and scope.region(…) opens a child region that must reach quiescence before it returns. JoinSet owns dynamic fan-out. Tasks spawned through a RuntimeHandle belong to the root region and are drained at shutdown.
The “no orphans” property comes from the shape of the API, region accounting, and runtime and oracle checks, not from discipline. It also isn't a claim that Rust's type system proves every adapter path. Region memory uses generation-checked handles, reclaimed when the region closes; there's no public allocation API for it yet.
Three types carry most of the model: a four-valued result, a budget that composes, and the context every async function receives.
01// src/types/outcome.rs (shape, not a program)02 Outcome<T, E> {03 Ok(T), // success04 Err(E), // application error05 Cancelled(CancelReason), // cancelled, with kind, origin, and cause chain06 Panicked(PanicPayload), // the task panicked07}08// Severity: Ok < Err < Cancelled < Panicked09 10// src/types/budget.rs11 Budget {12 deadline: Option<Time>, // absolute deadline13 poll_quota: u32, // max polls14 cost_quota: Option<u64>, // abstract cost units15 priority: u8, // 0-25516}17// outer.meet(inner): earlier deadline, smaller quotas, higher priority18 19// src/cx/cx.rs (signature sketch)20 Cx {21 spawn<F, Fut>(&, f: F) -> Result<TaskHandle<Fut::Output>, SpawnError>;22 checkpoint(&) -> Result<(), Error>; // Err once cancel is requested23 masked<F, R>(&, f: F) -> R; // defer cancellation for a closure24 budget(&) -> Budget;25 is_cancel_requested(&) -> bool;26}Request, drain, finalize, complete. Cooperative all the way down: the runtime never stops a task that won't check in.
The request propagates down the region tree. Each task is marked CancelRequested with a reason and a cleanup budget.
At its next checkpoint the task sees Cancelled and runs its own cleanup. It can still await, and it can still return a value.
Registered finalizers run with cancellation masked. Region finalizers run LIFO.
The runtime publishes the outcome: Cancelled(reason) when cancellation won, or the task's own value if it finished.
Reasons are ordered. A CancelReasonCancelReasonWhy a task was cancelled, with the cause chainCarries a CancelKind (User, Timeout, Deadline, PollQuota, CostBudget, FailFast, RaceLost, ParentCancelled, ResourceUnavailable, Shutdown, LinkedExit), where it came from, and a bounded chain of causes. The error from cx.checkpoint() carries it, so a joiner can tell why a task stopped. Kinds are ordered by severity, and cleanup budgets shrink as severity rises. carries one of eleven kinds, from least to most severe, and when two requests meet, the more severe kind wins. Cleanup budgets shrink as severity rises, and the error from cx.checkpoint() carries the reason, so a joiner can tell why a task stopped.
Bounds are conditional. Stock operations publish what they can promise through a responsiveness registry: a finite number of polls or checkpoints under stated assumptions, or a typed refusal for masked, blocking, external, or unknown work. Budgets are sufficient conditions only where a concrete bound exists.
In the Lean model, a cancelled task completes in exactly mask + 3 protocol steps (the cancel potentialCancel PotentialThe quantity Lean uses to prove the cancel protocol terminatesIn the Lean model, a task in cancelRequested has potential mask + 3, cancelling 2, finalizing 1, and completed 0. Every protocol step lowers it, so a cancelled task completes in exactly mask + 3 steps, with the mask depth capped at 64. This is a per-task termination proof about the model; it says nothing about a task that never reaches a cancellation point.). On the production runtime, budgets are advisory and Runtime::shutdown_timeout bounds how long you wait.
Permits, acks, and leases taken through a runtime-built Cx are recorded in an obligation table and must be resolved before their region can close.
- SendPermit: mpsc, oneshot, and broadcast reservations
- SemaphorePermit: released when capacity returns
- Ack: acknowledgement for a received message
- Lease: remote leases, renewed or expired
- IoOp: a pending I/O operation
- Transaction: an open database transaction, rolled back on drain if never committed
- Mutex and RwLock guards, which release on drop and have their own queue-cleanup tests
- Session-channel permits, which are standalone typestate tokens the oracles don't see
- Spork name leases, which panic if dropped unresolved but aren't checked at region close yet
- Anything taken through a Cx built without a runtime
A permit that escapes its task through mem::forget is reported by the obligation_leak oracle by kind and holder. A task parked while holding one is flagged as a futurelockFuturelockA task holding obligations that has stopped making progressThe lab runtime flags a task that still holds pending obligations but hasn't been polled for longer than futurelock_max_idle_steps, for example one parked while holding a semaphore permit. It emits a FuturelockDetected trace event with the task, region, and held obligations, and can panic on the spot.. An opt-in Shiryaev–Roberts monitor can watch obligation ages on the production runtime.
A Cx carries a type-level record of five effects. You can narrow it; you can't widen it back.
CapSet<SPAWN, TIME, RANDOM, IO, REMOTE> is a set of const-generic flags. Cx::restrict narrows a context to a subset, and sealed traits such as HasSpawn and HasIo let a function demand an effect in its signature. Reinstalling a narrowed context with Cx::set_current keeps its restrictions.
The boundary has documented gaps. Plain I/O entry points like TcpStream::connect check the calling task's context and refuse with ASUP-E009 without the IO capability, but threads outside the runtime aren't affected, and host-boundary helpers such as OS entropy for temp-file names stay outside the deterministic guarantee.
On top of the static row, a context can carry a macaroonMacaroonA bearer token that can only gain restrictionsAn HMAC-SHA256 chained token: each added caveat re-keys the signature, so anyone can attenuate a token but nobody can remove a caveat. Asupersync's caveats are TimeBefore, TimeAfter, RegionScope, TaskScope, MaxUses, ResourceScope (a glob), RateLimit, and Custom. Cx::attenuate applies them to a context. Checking spawns against a macaroon is opt-in via RuntimeBuilder::with_spawn_authorization_key.: an HMAC-SHA256 chained bearer token with eight caveat types (TimeBefore, TimeAfter, RegionScope, TaskScope, MaxUses, ResourceScope, RateLimit, Custom), plus third-party caveats with discharges. Cx::attenuate adds a caveat. Having the runtime check spawns against a token is opt-in through with_spawn_authorization_key.
Cancelling tasks run first so cleanup isn't starved, deadline work runs earliest-deadline-first, and everything else waits its turn, within explicit bounds.
Tasks in cancellation states. Priority 200–255.
Deadline-driven tasks, earliest deadline first.
Everything else runnable, at default priority.
- Cancel preemption is bounded. With the default cancel_streak_limit of 16, ready or timed work gets a dispatch slot within 17 steps per worker. While draining obligations or regions the bound widens to 32.
- Owners pop their local queue LIFO for cache locality; thieves steal FIFO, so stolen work is older work.
- !Send tasks are pinned to their owner worker on non-stealable queues.
- I/O polling is a leader/follower turn: whichever worker holds the driver lock runs the reactor while the others keep scheduling.
- Idle workers park on a permit-style Parker and recheck the queues after waking, which closes the lost-wakeup race.
- Workers count fairness_yields and max_cancel_streak, so starvation claims can be checked against counters.
- Two controls are opt-in and off by default: a Lyapunov governor that steers lane order from runtime snapshots, and an adaptive discounted-UCB1 cancel-streak selector. Measured against the fixed limit, the selector didn't win.
- Runtime state can be split into independently locked shards (tasks, regions, obligations, instrumentation, config) with
with_sharded_state(true). The default keeps it behind one lock.
A small-step operational semantics, a Lean project that checks six invariants of it, and TLA+ export for recorded traces. Precisely scoped, because the gap between model and code matters.
Core lifecycle, cancel, close, obligations, join, and time, plus distributed dedup and saga rules
All 22 covered; JOIN and the distributed rules aren't in Lean's Step
No sorry, on Lean 4.27
In the model. No proof that the Rust code refines it
The six invariants Lean checks
- ✓Structured concurrency: every task has exactly one owning region
- ✓Region close implies quiescence
- ✓The cancellation protocol's transitions
- ✓Race losers are drained
- ✓No obligation leaks
- ✓No ambient authority
These are theorems about the abstract model, linked to executable tests. The production Rust runtime hasn't been proved to refine that model, so this isn't a mechanized proof of the executor, the adapters, the protocol implementations, or the network transports.
Lab traces can be exported as TLA+ behaviors, and a test runs TLC on a real trace (and on a planted violation it must reject). TLC checks the recorded behavior, not a parametric model of the runtime.
A few of the rulesTransition RuleOne rule of the small-step semanticsEach rule says how one kind of step changes the state, for example CANCEL-REQUEST marking a task and propagating to its region's children, or CLOSE-RUN-FINALIZER popping one finalizer. The rule names in the spec match constructors in Lean's Step relation, with a few merged or split.
R[r].state = Open ⟹ Σ —spawn(r,t)→ Σ′, T′[t] = Created, R′[r].children ∪= {t}A task can only be created in an open region, and it becomes one of that region's children.
Σ —cancel(r, reason)→ Σ′, R′[r].cancel = strengthen(R[r].cancel, reason), ∀r′ ∈ desc(r): ParentCancelled, ∀t ∈ children(r): CancelRequested(reason, budget)Cancelling a region keeps the more severe reason, propagates ParentCancelled to every descendant, and marks its live tasks with a cleanup budget.
T[t] = CancelRequested ∧ mask = 0 ∧ await(checkpoint) ⟹ T′[t] = Cancelling, resume(Cancelled(reason))An unmasked task sees the cancellation at a checkpoint and starts draining.
T[t] = CancelRequested ∧ mask > 0 ∧ await(checkpoint) ⟹ mask′ = mask − 1, resume(Ok(()))Masking defers cancellation, but each deferral spends one unit of a finite mask budget (capped at 64).
R[r].state = Closing ∧ ∃t ∈ children(r) incomplete ⟹ Σ —cancel(r, implicit_close)→ Σ′, R′[r].state = DrainingA closing region cancels whatever is still running in it before it can finish.
reserve(o): O′[o] = Reserved · commit(o): Reserved → Committed · abort(o): Reserved → AbortedTwo-phase effects: reserving commits nothing, the commit performs the effect, and an abort (explicit or by drop) releases capacity with no effect.
The full rule set, with proof sketches and the mapping to runtime state, is in the formal semantics document.
Every LabRuntime report runs the oracle registry. Nine oracles are fed from runtime state today; the rest are registered but nothing feeds them yet.
Four more FABRIC messaging oracles exist behind the messaging-fabric feature.
Summarize oracle verdicts across many seeds with a test you can check after every run without inflating the false-alarm rate.
A fixed-sample test is invalidated if you peek early. An e-processE-ProcessA test statistic you can check after every runA nonnegative supermartingale under the null hypothesis. By Ville's inequality, the chance it ever exceeds 1/α is at most α, so you can look after every observation without inflating the false-alarm rate. The lab's standard monitor tracks task_leak, obligation_leak, and quiescence; each observation is that oracle's own verdict for a run, so it summarizes violation rates across seeds rather than finding new bugs. isn't: it's a betting martingale, E_t = E_(t-1) × (1 + λ(X_t − p₀)), and by Ville's inequality the chance it ever exceeds 1/α under the null is at most α. The standard monitor watches task_leak, obligation_leak, and quiescence with λ = 0.5, p₀ = 0.001, and α = 0.05.
What it doesn't do is find bugs on its own. Each observation is an oracle's pass/fail verdict for one run, and a lab run is deterministic, so the e-process can only reject an invariant some oracle has already flagged. It summarizes violation rates across seeds with an anytime-valid bound.
Two separate pieces: compensating sagas for remote workflows, and a planner that uses CALM analysis to batch obligation steps between coordination barriers.
remote::Saga records a forward action and a compensation for each step. If a later step fails, completed steps are compensated in reverse order. It sits next to the remote runtime's region-owned spawns, obligation-backed leases, and idempotency store.
Separately, the obligation saga model has 16 operation kinds. CALM analysisCALM AnalysisSorting saga steps into coordination-free and barrier-requiringConsistency As Logical Monotonicity applied to obligations. Asupersync's saga operations come in 16 kinds: 7 are monotone (Reserve, Send, Acquire, Renew, Delegate, CrdtMerge, CancelRequest) and 9 are not (Commit, Abort, Recv, Release, RegionClose, CancelDrain, MarkLeaked, BudgetCheck, LeakDetection). MonotoneSagaExecutor merges runs of monotone steps with a lattice join and puts a coordination barrier before each non-monotone one. marks 7 as monotone (Reserve, Send, Acquire, Renew, Delegate, CrdtMerge, CancelRequest) and 9 as not. MonotoneSagaExecutor merges each run of monotone steps with a lattice join and puts a barrierCoordination BarrierA sync point before a non-monotone saga stepMonotoneSagaExecutor runs consecutive monotone steps as one coordination-free batch and inserts a barrier before each non-monotone step such as Commit or Release. The number of barriers is exactly the number of non-monotone steps in the plan. before every non-monotone one. A sheaf-style consistency checker for saga observations exists as an API; nothing runs it automatically.
From the upstream README. Partial means partial.
Deterministic single-thread kernel
Regions, tasks, and the cancellation state machine
A four-valued Outcome ordered by severity: Ok < Err < Cancelled < Panicked
The lab runtime: virtual time, seeded scheduling, trace capture
Parallel scheduler and region heap
Three-lane work-stealing scheduler: cancel, timed (EDF), and ready
Region heap with generation-checked handles, reclaimed when the region closes
Optional sharded runtime state with a fixed lock order
I/O and protocols
epoll reactor with optional io_uring; narrower BSD and Windows reactors
TCP, HTTP/1.1, HTTP/2, TLS, WebSocket, gRPC, and database clients
Native QUIC and HTTP/3; deployment and interop evidence still open
Actors and supervision
GenServers, actors, monitors, and links, on the native runtime and in the lab
Live supervision trees: one-for-one, one-for-all, rest-for-one
Restart intensity and backoff limits
Distributed structured concurrency
Region-owned remote spawn over TCP with mutual TLS
Leases as obligations, an idempotency store, saga compensation
RaptorQ snapshot distribution with quorum recovery
Schedule exploration and formal tooling
Race-guided seed exploration that skips equivalent traces
TLA+ export of lab traces, checked by TLC
Lean checks six model invariants; there is no Rust refinement proof yet
Hardening
Benchmark, golden-output, flamegraph, and proof-note gates before each commit to main
Browser Edition packages, currently a release candidate
Cutting per-task overhead, measured against tokio in the same process