Each demo shows one mechanism. The badge says how it ships: on by default, an API you call, part of the lab runtime, opt-in, a diagnostic, or a property of the formal model.
Click a 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. to close it and watch cancellation reach everything it owns.
Every task belongs to a region, and regions nest. When you close a region, the runtime cancels whatever is still running inside it, waits for those tasks to finish, runs the region's finalizers, and resolves its obligations. Only then does the region report itself closed.
That's the difference from tokio::spawn, which returns a detached task nothing waits for. A task spawned through a CxCxThe capability context every async function receivesCx is how a task spawns children, checks for cancellation, reads its budget and the current time, draws randomness, and records traces. It belongs to a region, so anything spawned through it is owned by that region. A test can hand in a lab Cx and the same code runs on virtual time. belongs to that context's region; tasks spawned from a runtime handle belong to the root region, which is drained at shutdown. The architecture page has the details.
Step through request, drain, and finalize, and compare it with dropping the future.
Cancellation starts as a request. It propagates down the region tree and marks each task with a reason and a cleanup budgetBudgetDeadline, poll quota, cost quota, and priority for a piece of workA small Copy struct: an optional absolute deadline, a poll quota, an optional abstract cost quota, and a priority from 0 to 255. Scopes and tasks carry one, and nested budgets combine with meet, so the tighter constraint always wins. On the production runtime, cleanup budgets are advisory: a task that runs past its budget is not killed.. The task notices at its next cancellation pointCancellation PointWhere a task notices it has been cancelledcx.checkpoint() returns an error once cancellation has been requested, and cancel-aware awaits such as channel receives and lock acquisitions return early the same way. A task that never reaches one is never forcibly stopped, and it holds up its region's close. Loops that do real work should call cx.checkpoint(). (cx.checkpoint() or a cancel-aware await), then drains: it runs its own async cleanup, can still await, and can still return a value. Finalizers run with cancellation masked, and the runtime publishes Cancelled(reason).
The protocol is cooperative. A task stuck in a loop with no checkpoint is never forcibly stopped, and its region's close waits for it. Budgets are advisory on the production runtime, and Runtime::shutdown_timeout bounds how long the caller waits.
Press Cancel Now and watch both runtimes shut down the same work.
In tokio, abort() or dropping a future stops it at its last await. Whatever it was in the middle of stays half-done, and there's no async cleanup hook. Dropping a JoinHandle doesn't cancel anything; the task keeps running, detached. tokio-util's CancellationToken gives you cooperative cancellation if you thread it through by hand.
Asupersync builds the cooperative version into every task: the request propagates on its own, the task drains, finalizers run, and the outcome records why it stopped. It takes longer than a drop, and it depends on the task reaching a checkpoint. In exchange you get a shutdown you can audit, and the lab runtimeLab RuntimeThe deterministic test runtimeRuns async code on virtual time with a seeded scheduler, so the same seed reproduces the same schedule. It captures traces, injects cancellation and chaos deterministically, detects futurelocks, writes crashpacks for failing runs, and checks oracles. Concurrency bugs become reproducible test failures instead of flakes. can check it under many schedules.
Cancel between the two phases and nothing happens.
The demo uses a bank transfer as the analogy. In the library the pattern is concrete: tx.reserve(&cx).await? claims one slot of channel capacity and commits nothing, and permit.send(value) publishes the message. Cancelled while waiting to reserve? Nothing was sent. Dropped the permitPermitA reservation you must commit or aborttx.reserve(&cx).await gives you a permit for one slot of channel capacity. permit.send(value) commits it; dropping it aborts the reservation and frees the slot. Reserving is cancel-safe, which is how a cancelled send avoids losing or half-sending a message.? The slot goes back.
The commit returns an OutcomeOutcomeA four-valued result: Ok, Err, Cancelled, PanickedOutcome<T, E> keeps cancellation and panics separate from ordinary errors. The variants are ordered by severity, Ok < Err < Cancelled < Panicked, and combinators aggregate with that order, so a worse outcome is never hidden by a better one. HTTP layers map them to 200, 4xx/5xx, 499, and 500.; if the receiver has gone away you get the value back instead of losing it. The same shape appears in TwoPhaseNetworkSend and graded obligation tokens. It isn't a general transaction system, and partial I/O like read_exact and write_all documents its own weaker contract.
Follow a permit down the happy path, the abort path, and the leak path.
A reserved channel slot, a semaphore permit, or a lease is an obligationObligation SystemThe runtime's table of permits, acks, and leasesWhen a task reserves a channel slot, takes a semaphore permit, or holds a lease through a runtime-built Cx, the runtime records an obligation. Sending, releasing, or aborting resolves it. A region can't close with unresolved registered obligations, and the obligation_leak oracle names any that escape, by kind and holder. the runtime records. Sending, releasing, or aborting resolves it, and a region can't close cleanly with one outstanding.
Rust's types are affine, so the compiler can't stop a permit from being forgotten. The runtime catches it instead: the lab's obligation_leak oracleObligationLeak OracleReports permits that escaped unresolvedThe obligation_leak oracle. If a permit escapes its task, for example through mem::forget, the oracle reports its kind (such as SendPermit) and its holder. On-ramp level 3 leaks one on purpose to show the report. reports the kind and the holder. On-ramp level 3 leaks one on purpose to show the report.
Cancel, timed, and ready lanes, and the bound that keeps cancellation from starving everything else.
Tasks that are cancelling go to the cancel lane, so cleanup isn't stuck behind new work. Deadline-driven tasks go to the timed lane, earliest deadline first. Everything else waits in the ready lane.
Cancel priority is bounded. With the default limit of 16, ready or timed work gets a slot within 17 dispatches per worker, and the limit widens to 32 while a region is draining. Workers count their longest cancel streak, so fairness can be checked against counters instead of guessed.
Narrow a context and see which operations it can still perform.
Async functions receive &Cx, and spawning, time, randomness, I/O, and remote calls go through it. The context carries a capability rowCapability RowThe five effects a Cx can carryCapSet<SPAWN, TIME, RANDOM, IO, REMOTE> is a type-level record of which effects a context may perform. Cx::restrict narrows it to a subset, and sealed traits such as HasSpawn and HasIo let a function require a capability in its signature. Separately, Macaroon tokens can attenuate a context at runtime with caveats., CapSet<SPAWN, TIME, RANDOM, IO, REMOTE>. Cx::restrict narrows it, and nothing widens it back.
Plain I/O entry points such as TcpStream::connect check the calling task's context and refuse with ASUP-E009 when the IO capability is missing. The boundary has documented gaps: threads outside the runtime aren't checked, and some host-boundary helpers stay outside it.
Add caveats to a token. Each one narrows it, and none can be removed.
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. is a bearer token whose signature is an HMAC chain: every caveat re-keys it, so a holder can add restrictions but can't strip one off. Asupersync supports eight caveat types (TimeBefore, TimeAfter, RegionScope, TaskScope, MaxUses, ResourceScope, RateLimit, Custom) plus third-party caveats with discharges.
Cx::attenuate applies a caveat to a context before you hand it to a child. Having the runtime check every spawn against a token is opt-in, through RuntimeBuilder::with_spawn_authorization_key.
Nest scopes with different limits and see which constraint wins.
A budget has a deadline, a poll quota, a cost quota, and a priority. When scopes nest, budgets combine with meet: the earlier deadline, the smaller quotas, and the higher priority. Each part is a min or a max, so the order you apply them in doesn't matter (budget algebraBudget AlgebraHow nested budgets combinemeet(a, b) takes the earlier deadline, the smaller poll quota, the smaller cost quota, and the higher priority. Because each component is a min or a max, the operation is associative and commutative, so it doesn't matter in which order nested scopes apply their limits. A child can never end up with a looser budget than the scope it runs in.).
A child never ends up with a looser budget than the scope it runs in. On the production runtime, budgets inform scheduling and cancellation, and cleanup budgets are advisory: a task that ignores its budget holds things up and gets reported, but it isn't killed.
Change the seedSeedThe number that fixes a lab scheduleThe lab scheduler's choices come from a seeded deterministic RNG, so the same seed reproduces the same interleaving, timer order, and chaos injections. A failing seed is a reproducible bug report. and the interleaving changes. Keep it and the run repeats exactly.
The lab runtime runs your code on virtual time with a seeded scheduler. Sleeps complete without waiting, timers fire in a fixed order, and the same seed reproduces the same schedule, so a failure that took a thousand CI runs to show up becomes a seed you can rerun.
It records traces, injects cancellation and chaos deterministically, flags futurelocksFuturelockA 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., and attaches a crashpack with a replay command to failing runs. Code reads time and randomness through Cx, which is what lets the same code run in both places.
Cancel at every await point, one run each, and check the oracles after every run.
Most tests run code to completion, so they never see what happens when a task is cancelled halfway through. The injector first records a run to find the await points, then reruns the test once per point, cancelling there.
lab(seed).with_cancellation_injection(InjectionStrategy::AllPoints).with_all_oracles() runs the whole sweep; other strategies sample points, take the first N, or target specific ones. After each run the oracles check for leaked tasks, leaked obligations, and protocol violations. It finds bugs. Passing means no oracle flagged one, which is good evidence but not a proof.
Run a batch of seeds and watch the evidence accumulate.
An oracleOracleA lab-runtime invariant checkA monitor that inspects runtime state after a lab run and reports pass or fail for one invariant. There are 24 built in; the lab runtime feeds 9 of them from its own state today (task leak, obligation leak, quiescence, loser drain, finalizer, region tree, deadline monotonicity, cancellation protocol, DOWN order). The other 15 report as passed and are counted as not fed. checks one invariant after a lab run. There are 24 in the registry, and the lab runtime feeds nine of them from its own state: task leaks, obligation leaks, quiescence, loser drain, finalizers, the region tree, deadline monotonicity, the cancellation protocol, and DOWN-message order.
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. summarizes those verdicts across runs. It's a betting martingale (λ = 0.5, null rate 0.001), and by Ville's inequality you can check it after every run and reject once it passes 1/α = 20 without inflating the false-alarm rate. It doesn't find bugs the oracles miss; it tells you how strong the evidence for a violation rate is.
Toggle pruning to see how many schedules are really the same schedule.
Many interleavings differ only in the order of operations that don't interact, and running all of them wastes time. The schedule explorer detects races with vector clocks, derives new seeds aimed at them, and skips runs whose trace is equivalent to one it has already seen.
It borrows from dynamic partial-order reductionDPORDynamic partial-order reduction, as used here: race-guided searchClassic DPOR explores one schedule per class of equivalent interleavings. Asupersync's explorer borrows the ideas: it detects races with vector clocks, derives new seeds that target them, and skips runs whose Foata fingerprint it has already seen. It doesn't backtrack to an exact prefix, so it is useful bug-finding machinery rather than a proof that every class was covered., but it doesn't backtrack to an exact prefix and force the alternative branch, so it can't promise it covered every class. The number of distinct classes measures the campaign. Treat it as a practical bug finder, not a proof.
Swap independent events and the fingerprint stays the same.
Two traces are Mazurkiewicz-equivalentMazurkiewicz TraceAn execution modulo reordering of independent eventsIf two adjacent events touch different resources, swapping them can't change the result. Mazurkiewicz traces are the equivalence classes this swapping produces. The lab treats executions this way so it can recognize two schedules as the same behavior. if you can turn one into the other by swapping adjacent events that touch different resources. Foata normal form picks one canonical representative by grouping events into layers of mutually independent steps.
Hash that form and you get a fingerprintFoata FingerprintA canonical hash of an execution up to reorderingTwo traces that differ only by swapping adjacent independent events are equivalent (Mazurkiewicz equivalence). Foata normal form picks one canonical representative by grouping events into layers. Hashing it gives a fingerprint the schedule explorer uses to skip runs that are equivalent to one it has already seen. shared by every equivalent schedule. The explorer uses it to recognize runs it has already seen, and replay uses the same canonical form, so equivalent runs compare equal.
Crash several processes at the same virtual instant and watch the order their DOWN messages arrive in.
On a real runtime, simultaneous failures reach a supervisor in whatever order threads happen to race. A bug that depends on that order may never reproduce.
Under the lab runtime, DOWN messages are ordered by completion time, then task ID, then monitor reference. Timers with the same deadline fire by timer ID, and equal-priority tasks follow FIFO order with a seeded tie-break. Replay the same seed and the arrivals repeat.
Calibrate across seeds and flag the runs whose metrics don't fit, even when no invariant failed.
Some lab runs pass every oracle and still look wrong: an unusual number of polls, a slow drain. Split conformal predictionConformal CalibrationDistribution-free anomaly thresholds for lab runsSplit conformal prediction over oracle-report metrics across explored seeds. With the default alpha of 0.05, the prediction set covers a new exchangeable run with probability at least 95%, whatever the underlying distribution. It's opt-in through ScheduleExplorer::with_conformal_calibration, which lists seeds whose metrics fall outside the set even when no invariant failed. sets a threshold from earlier runs that holds without assuming any distribution, as long as the runs are exchangeable.
With the default α of 0.05, a new run lands inside the prediction set at least 95% of the time. ScheduleExplorer::with_conformal_calibration feeds it each explored run's oracle report and lists the seeds that fall outside. No oracle consults it on its own, so no default verdict depends on it.
Send a call to a GenServerGenServerAn OTP-style stateful serverA task that owns state and handles call, cast, and info messages from a bounded mailbox, spawned with cx.spawn_gen_server. Each call hands the server a Reply that wraps a tracked obligation: the server must send or abort it. Dropping it unanswered panics outside of cancellation and unwinding, and the lab's reply_linearity oracle checks the same rule. This is enforced at runtime, not by the compiler. and see what happens when the handler forgets to reply.
SporkSporkAsupersync's OTP-style layerSupervision, a name registry, and actors on top of regions, obligations, and explicit cancellation: GenServers, supervisors, links, monitors, process groups, and AppSpec for declarative topologies. Processes always belong to a region and can't be detached, and restart and DOWN-message order is deterministic under the lab runtime. is Asupersync's OTP-style layer: GenServers, actors with bounded mailboxesMailboxA bounded message queue for an actor or serverActors and GenServers receive messages through a mailbox with a fixed capacity, so a slow consumer applies backpressure instead of growing without bound. The capacity is the second argument to spawn_actor and spawn_gen_server., monitors, links, a name registry, and supervisorsSupervisorRestarts failed children by policyA Spork supervisor compiles a restart topology over regions: boot order, dependencies, and shutdown budgets. Run live with CompiledSupervisor::bind_managed, it cancels and drains a failed child, then restarts it one-for-one, one-for-all, or rest-for-one, within shared intensity and backoff limits. that restart failed children one-for-one, one-for-all, or rest-for-one within intensity and backoff limits. Every process belongs to a region and can't be detached.
Each call hands the server a Reply that wraps a tracked obligation, and the server has to send it or abort it. Dropping one unanswered panics, which the supervisor sees (during unwinding or after cancellation it aborts cleanly instead), and the lab's reply_linearity oracle checks the same rule. The caller gets an answer or an error. The runtime enforces this, not the compiler.
Fail a step midway and watch the completed steps compensate in reverse.
A sagaSagaMulti-step work with compensationEach step has a forward action and a compensating action; if a later step fails, completed steps are compensated in reverse order. remote::Saga provides this for distributed workflows. Separately, the obligation saga planner uses CALM analysis to batch monotone steps between coordination barriers. pairs each forward step with a compensating action. remote::Saga records them as it goes, and if a later step fails, it runs the compensations for completed steps in reverse order.
It lives in the remote runtime alongside region-owned remote spawns, leases that count as obligations, and an idempotency store for retries. Compensations are ordinary code: they need to be idempotent and safe after a partial failure, and no saga can make an irreversible action reversible.
Some steps can be merged without coordination. Others need a barrier first.
The CALM theoremCALM TheoremConsistency As Logical MonotonicityA result from distributed systems (Hellerstein and Alvaro): a program has a consistent, coordination-free implementation exactly when it is monotone, meaning it never has to retract a conclusion it already drew. Asupersync uses it to decide which saga steps can be batched without synchronization. says a computation can run consistently without coordination exactly when it's monotone: it only adds information and never has to retract a conclusion. Asupersync applies that to its saga model's 16 operation kinds.
Seven are monotoneMonotone OperationA step that only adds informationAn operation whose effect never has to be retracted, so its order relative to other monotone operations doesn't matter. In Asupersync's saga model the monotone kinds are Reserve, Send, Acquire, Renew, Delegate, CrdtMerge, and CancelRequest. Runs of them can be merged without coordination. (Reserve, Send, Acquire, Renew, Delegate, CrdtMerge, CancelRequest). Nine aren't, including Commit, Release, and RegionClose, because they depend on knowing nothing else will arrive. MonotoneSagaExecutor merges each run of monotone steps with a lattice join and places one coordination 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 each non-monotone step.
Drop packets at random. The receiver needs enough of them, not particular ones.
A fountain codeFountain CodeA rateless erasure codeThe sender can produce as many encoded symbols as it likes, and the receiver rebuilds the data from any sufficient set of them, regardless of which ones arrived. Lost packets cost bandwidth instead of round trips. RaptorQ is the standardized one. turns K source symbols into as many encoded symbols as you like, and the receiver rebuilds the data from any sufficient set. With RaptorQRaptorQThe RFC 6330 fountain codeA systematic fountain code: the first symbols are the source data itself, and repair symbols can be generated without limit. With K source symbols, receiving K usually suffices and K + 2 almost always does. Asupersync's implementation is deterministic, with a policy-driven decode planner and optional SIMD GF(256) kernels. (RFC 6330), K symbols usually suffice and K + 2 almost always do. Which packets were lost stops mattering, so loss costs bandwidth instead of retransmission round trips.
Asupersync's codec is deterministic, with a decode planner that picks an elimination strategy from the matrix's structure and optional SIMD kernels for GF(256). Its main user is ATP; the ATP page has the measurements, including where it loses to rsync.
Step through the rules that define spawning, cancellation, and region close.
The runtime is designed against a small-step operational semanticsSmall-Step SemanticsThe formal rules the runtime is designed againstRules of the form ⟨e, σ⟩ → ⟨e′, σ′⟩. The spec has 23 core rules (spawn, scheduling, the cancel protocol, region close, reserve/commit/abort, join, tick) plus 10 for distributed dedup and sagas. Lean's Step relation has 22 constructors, and the Lean project proves 189 theorems about it with no sorry. That is a proof about the model, not about the Rust code.: 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. of the form ⟨e, σ⟩ → ⟨e′, σ′⟩ for scheduling, the task lifecycle, the cancellation protocol, region close, obligations, joins, and time. There are 23 core rules, plus 10 for distributed deduplication and sagas.
A Lean project formalizes the core. Its Step relation has 22 constructors, and 189 theorems about it check six invariants with no sorry. That's a proof about the model. Nobody has proved the Rust runtime refines it; the link between the two is tests, oracles, and TLC checks of recorded traces.
Pick a mask depth and count the steps to completion.
To show the cancellation protocol can't cycle, the Lean model gives each cancelled task a 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.: mask + 3 when cancellation is requested, 2 while cancelling, 1 while finalizing, and 0 when complete. Every protocol step lowers it. A masked checkpoint spends one unit of mask, and mask depth is capped at 64.
The theorem cancel_protocol_terminates follows: a cancelled task completes in exactly mask + 3 steps. It counts protocol steps in the model. A task that never reaches a checkpoint never takes the first step, which is why the runtime makes no wall-clock promise.
Watch a weighted measure of outstanding work while the governor steers lane order.
The potentialLyapunov PotentialA weighted measure of outstanding workV = 1.0·live tasks + 5.0·total obligation age + 3.0·draining regions + 2.0·deadline pressure, with those default weights. The optional Lyapunov governor uses it to steer lane ordering so that V tends not to increase. The governor is off by default. adds up what's still outstanding: live tasks (weight 1), the total age of pending obligations (5), draining regions (3), and deadline pressure (2). It gives the scheduler one number to push down.
The optional Lyapunov governor reads runtime snapshots every 32 dispatches and steers lane ordering so the potential tends not to increase. It's off by default, and it's a scheduling heuristic with a principled objective, not a proof that the system makes progress.
A bandit picks how many cancelling tasks run in a row before other work gets a turn.
The fixed limit of 16 cancel-lane dispatches in a row is a judgment call. With enable_adaptive_cancel_streak(true), each worker treats the limit as a choice among 4, 8, 16, 32, and 64 and picks with discounted UCB1Discounted UCB1The opt-in adaptive cancel-streak selectorWith enable_adaptive_cancel_streak(true), each worker picks its cancel-streak limit from {4, 8, 16, 32, 64} with a discounted upper-confidence-bound bandit, updated every 128 dispatches from a reward mixing Lyapunov decrease, fairness, and deadline pressure. It is deterministic (no RNG, no wall clock). It is off by default: measured against the fixed limit of 16, it didn't win on cancel-heavy work and was 1–29% slower elsewhere.: every 128 dispatches it discounts old evidence by 0.95, scores the arm it just used with a reward mixing Lyapunov decrease, fairness, and deadline pressure, and moves to the arm with the best upper confidence bound.
It's deterministic, with no randomness and no wall clock, so the same dispatch sequence makes the same choices. It's also off by default because it didn't earn its place: measured against the fixed limit on two hosts, it didn't win on cancel-heavy work and was 1–29% slower on spawn, yield, and channel round trips.
Build a cycle in the wait graphWait-GraphWho is waiting on whomA directed graph whose nodes are tasks and whose edges mean "A is waiting on B". The task inspector reports wait dependencies, and the spectral health monitor analyzes the graph's Laplacian when you ask it to. and watch its connectivity fall.
The wait graph has a node per task and an edge for each “waiting on”. Its Fiedler valueFiedler ValueAlgebraic connectivity of the wait graphThe second-smallest eigenvalue of a graph's Laplacian. It's zero exactly when the graph is disconnected and small when the graph has a bottleneck. Asupersync's spectral health monitor tracks its trend on the live wait graph as one early-warning signal. A falling value is a topology signal, not proof of a deadlock., the second-smallest eigenvalue of the graph Laplacian, is zero when the graph comes apart and small when it has a bottleneck. The monitor tracks it with a stack of trend statistics, calibrated with split conformal bounds and an anytime-valid e-process, and reports none, watch, warning, or critical.
It's a diagnostic you call (Diagnostics::analyze_structural_health); the scheduler runs its own copy only with the opt-in governor. It doesn't intervene, and a falling value is a signal about the graph's shape, not proof of a deadlock. Trapped-cycle evidence is a separate check.