Asupersync — The Cancel-Correct Async Runtime for Rust

Radically Innovative
Concurrency

The Three-Phase Cancel ProtocolThree-Phase Cancel ProtocolRequest → Drain → FinalizeA rigorous lifecycle for stopping tasks. Phase 1: Request (signal intent to stop). Phase 2: Drain (allow tasks to finish writing to disk, closing network sockets, etc.). Phase 3: Finalize (force-release all remaining resources). This prevents the 'silent drop' problem.

In standard async Rust, dropping a future instantly stops its execution. The resulting "silent drop" leaves database connections open and files half-written.

Asupersync requires a mandatory 3-phase shutdown. Tasks receive a time budgetBudgetCountdown timer for task cleanupsWhen cancellation strikes, tasks aren't killed instantly—they're given a 'Budget' (a specific amount of time, like 5 seconds) to clean up their mess during the Drain phase. If they run out of time, they are forcefully Finalized. to gracefully drainDrain PhaseGraceful cleanup during cancellationThe second phase of the cancel protocol. After a cancel request, tasks enter Drain where they can finish in-flight work, flush buffers, close connections, and release resources within their Budget. their connections and flush buffers before the runtime enforces finalizationFinalize PhaseFinal cleanup after drainingThe Finalize phase runs after Drain completes (or the Budget expires). It executes registered finalizers in LIFO order — similar to defer in Go but tightly integrated with the cancel protocol..

Linear ObligationsLinear ObligationsMandatory return policy for resourcesA strict resource management system backed by Rust's type system. Think of it as a library book you must explicitly return. If a code path forgets to consume a resource (like a Permit or Lease), the program refuses to compile, preventing resource leaks at compile-time.

Every time you spawn a task or borrow a resource, you get a PermitPermitMust-use lifecycle tokenWhen you spawn a task, you get a Permit. You can't just throw it away; you must explicitly wait for the task, detach it, or cancel it. It's how Asupersync enforces that you are always paying attention to the tasks you create. or a LeaseLeaseScoped resource borrowTemporary ownership of a shared resource (like a database connection). Unlike standard Rust where drops are passive, if a Lease's owning Region is cancelled, the resource is actively and safely returned to its pool via the cancel protocol.. The Rust compiler strictly enforces their usage.

You must explicitly await, detach, or cancel these tokens. Dropping one by mistake triggers a compilation error, preventing resource leaks entirely.

The Region TreeRegion TreeHierarchy of nested scopesA family tree for tasks. Instead of tasks floating around independently, every task in Asupersync belongs to a 'Region'. When a parent Region is cancelled, the entire branch of child Regions and tasks is cleanly pruned from the bottom up. No task is ever orphaned.

Asupersync enforces structural integrity. Every task is born into a RegionRegionA structured concurrency scopeA lifetime-bounded scope that owns tasks. When a Region closes, all tasks within it are cancelled (via the cancel protocol), awaited to completion, and their resources cleaned up. Regions nest hierarchically, forming a tree., and regions form a strict parent-child hierarchy.

When a parent Region finishes or gets cancelled, the cancellation cleanly cascades down the entire tree. This cascade guarantees no "zombie" tasks keep running after their parent terminates.

Deterministic Lab RuntimeLab RuntimeDeterministic testing sandboxA virtual time-machine for your code. The Lab Runtime replaces the chaotic real-world scheduler with a perfectly controlled one. By feeding it a 'Seed', developers can reproduce insanely complex concurrency bugs (race conditions) every single time. Bye-bye flaky tests.

Race conditions are notoriously hard to test because standard runtimes behave chaotically. Asupersync provides a deterministic testing environment to solve this.

By providing a SeedSeedDeterministic execution parameterAn integer that controls the Lab runtime's scheduling decisions. The exact same seed always produces the exact same task interleaving, enabling perfectly reproducible testing and bug replay., the Lab Runtime systematically explores different thread interleavings using DPORDPORDynamic Partial Order ReductionA smart algorithm used by the Lab Runtime. Instead of testing every single possible way tasks could overlap (which would take billions of years), DPOR only tests the interleavings that actually interact with each other. It finds the needle in the concurrency haystack mathematically. to find the exact combination that triggers a bug. You can then reproduce the exact bug reliably, every single time.

Capability SecurityCapability SecurityNeed-to-know task managementA 'Zero Trust' model for concurrency. Tasks receive a 'Cx' token that explicitly grants them permissions—like the ability to spawn other tasks, use the network, or access timers. If a task is hijacked or buggy, its damage is contained to its specific capabilities.

In most runtimes, any task can perform any action at any time. A background worker can unexpectedly open a network connection or read the file system. Asupersync restricts this by default.

Every task receives a Cx tokenCxCapability context tokenThe magic key passed to every task. It controls what operations that task may perform. Spawning, I/O, timers, and other effects are gated by capabilities on the Cx. This enforces the principle of least authority. that explicitly grants it permissions. If a buggy or hijacked task attempts an operation without the right key on its ring, the runtime instantly blocks it. You maintain absolute control over what each component of your system can actually do.

Two-Phase EffectsTwo-Phase EffectReserve/commit pattern preventing partial side-effectsA pattern where side effects are split into two stages: Reserve (stage the effect, making it reversible) and Commit (apply it permanently). If cancellation arrives between Reserve and Commit, the reservation is automatically rolled back. Think of it like a bank placing a hold on your account before transferring — if the transfer is cancelled, the hold is simply released.

Traditional async code often crashes midway through an operation, leaving the system in an inconsistent state. For instance, money might be deducted from one account but never added to the other.

Asupersync introduces a Reserve/Commit pattern. Side-effects are first staged as reversible reservations. If cancellation strikes during this window, the runtime seamlessly rolls back the hold. Only when it is entirely safe do the effects permanently commit.

Spectral Deadlock DetectionSpectral Wait-Graph AnalysisEigenvalue-based deadlock predictionA technique that analyzes the eigenvalues of the wait-graph's Laplacian matrix to predict deadlocks before they fully form. Instead of waiting for tasks to actually freeze, it detects the mathematical signature of an emerging deadlock (the Fiedler value approaching zero) and intervenes proactively.

Deadlocks usually freeze systems silently. Asupersync treats deadlock detection as an active telemetry problem, monitoring a real-time Wait-GraphWait-GraphDirected graph of task dependenciesA directed graph where nodes are tasks and edges represent 'task A is waiting on task B'. The runtime maintains this graph in real time and uses spectral analysis on its Laplacian matrix to detect deadlocks before they fully form. of all tasks.

The scheduler calculates the Fiedler ValueFiedler ValueEigenvalue that signals deadlock riskThe second-smallest eigenvalue of the wait-graph's Laplacian matrix. When it's large, tasks flow freely (no bottleneck). When it drops near zero, the graph is about to split into disconnected components — meaning a deadlock is forming. Think of it as a 'traffic congestion score' for your concurrent system. (the second-smallest eigenvalue of the graph's Laplacian matrix). When this value plummets, it signals an impending traffic jam. The runtime can then intervene proactively before a catastrophic freeze occurs.

RaptorQ Fountain CodesRaptorQRFC 6330 fountain code for erasure-coded transferAn advanced fountain code standardized in RFC 6330 that Asupersync uses for erasure-coded data transfer. It generates repair symbols so efficiently that receivers can reconstruct original data from any sufficient subset of symbols, with less than 1% overhead beyond the theoretical minimum.

Moving data across lossy networks usually requires endless back-and-forth acknowledgments (ACKs) and retransmissions. This degrades performance significantly when connections drop.

Asupersync uses a rateless erasure codeFountain CodeRateless erasure code for data transferA class of erasure codes where the sender generates a potentially infinite stream of encoded symbols, and the receiver can reconstruct the original data from any sufficient subset. Like a magic fountain — you just need to collect enough drops, regardless of which specific drops you catch. protocol. The sender emits an infinite stream of encoded droplets. The receiver only needs to catch a sufficient number of these droplets to perfectly reconstruct the file, completely eliminating the need for retransmission requests.

SporkSporkSpawn + Fork primitiveA portmanteau of Spawn and Fork. It creates a new task while simultaneously branching off a new child Region. The new task inherits a subset of the parent's capabilities and is tightly bound to its new Region's lifecycle. (OTP without the flaws)

Erlang's OTP architecture is legendary, but it relies on developer discipline. Actors can silently crash, messages can accumulate boundlessly in mailboxes until OOM, and servers can forget to reply, leaving clients hanging forever.

Asupersync provides SporkSporkSpawn + Fork primitiveA portmanteau of Spawn and Fork. It creates a new task while simultaneously branching off a new child Region. The new task inherits a subset of the parent's capabilities and is tightly bound to its new Region's lifecycle.—a GenServerGenServerGeneric Server for stateful actorsA battle-tested server pattern borrowed from Erlang/OTP used to encapsulate state, handle concurrent requests, and manage a mailbox. In Asupersync, GenServers are supercharged with compile-time Reply Obligations, meaning a server can mathematically never 'forget' to respond to a client. and SupervisorSupervisorFault-tolerant task managerA task that monitors child tasks and applies restart policies when they fail. Crucially, Supervisors respect the cancel protocol: during Region cancellation, they stop restarting and allow children to drain gracefully. implementation that enforces strict guarantees at compile time. Mailboxes apply explicit backpressure, and every client request generates a linear Reply Obligation. The server mathematically cannot "forget" to reply.

CALM AnalysisCALM AnalysisIdentifies which operations need coordinationConsistency As Logical Monotonicity — a principle that determines which operations can run coordination-free (monotone operations like Reserve and Send) and which require barriers (non-monotone operations like Commit and Release). Asupersync's Saga engine uses CALM to automatically batch consecutive monotone steps, inserting coordination barriers only where the math demands it.

Traditional runtimes sprinkle Mutex locks everywhere to prevent data races, destroying concurrent performance as cores contend for the same cache lines.

Asupersync uses the formal CALM theorem to eliminate locks. Operations are categorized mathematically. Monotone operationsMonotone OperationOrder-independent operation that needs no coordinationAn operation whose result doesn't depend on the order it's executed relative to other monotone operations. Reserve, Send, Acquire, Renew, and CrdtMerge are all monotone in Asupersync's Saga engine. Because they're order-independent, they can be batched and executed without coordination barriers — a key performance optimization identified by CALM analysis. (like appending data) never require locks because they do not rely on checking absences. The runtime batches these entirely coordination-free, drastically scaling multi-core throughput.

Lyapunov PotentialLyapunov Potential4-component energy function proving system progressA formal 'energy measure' composed of four terms: live task count, pending obligation age, draining region count, and deadline pressure. Like a ball's potential energy decreasing as it rolls downhill, this function strictly decreases with each scheduler step — mathematically proving the runtime always makes progress toward quiescence. The scheduler can tune weights (obligation-focused vs deadline-focused) to prioritize different workload patterns.

How do you mathematically prove an async program won't just spin in infinite loops during shutdown?

Asupersync calculates a 4-component energy function in real-time. This function aggregates live tasks, pending obligation age, draining regions, and deadline pressure. Because the runtime mechanics mathematically guarantee this "potential energy" always decreases over time, the system acts as a supermartingale—proving it makes strictly monotonic progress toward quiescenceQuiescenceWhen a region goes completely silentThe state of a Region when all its tasks have finished, and no new tasks can possibly be created inside it. It's the equivalent of making sure everyone has left the building and the doors are locked before turning off the lights..

EXP3 Adaptive SchedulerEXP3 SchedulerAdaptive scheduling via exponential weightsAn online learning algorithm (Exponential-weight algorithm for Exploration and Exploitation) that adapts the scheduler's behavior based on observed cancellation patterns. The scheduler maintains 5 arms [4, 8, 16, 32, 64] representing cancel-streak thresholds. If certain thresholds consistently perform better, EXP3 shifts weight toward them with exploration rate γ=0.07, converging toward the optimal strategy over time.

Hardcoded scheduler heuristics break under adversarial workloads. If a flood of cancellations arrives, a static scheduler might starve normal tasks entirely.

Asupersync replaces static thresholds with an online machine learning algorithm (EXP3). It maintains five "arms" representing different cancel-streak limits. By continuously measuring regret, the scheduler dynamically shifts its probability weights to adapt to the current workload—converging on the optimal strategy without any human tuning.

Systematic Cancellation Testing

Traditional tests run your code to completion. They cannot catch bugs that only surface when your code is cancelled halfway through execution.

Asupersync provides a deterministic Cancellation Injector. It systematically re-runs your test suite, dropping a "cancel bomb" at a different await point on every run to mathematically prove your application survives interruption without leaking resources.

E-Process Test OraclesE-ProcessAnytime-valid statistical monitor using betting martingalesA betting martingale that lets you continuously monitor a hypothesis and reject it the instant the evidence is strong enough — without any penalty for peeking. Unlike traditional p-values (which require a fixed sample size), an E-process stays valid no matter when you check it. Asupersync's Lab runtime uses E-processes to monitor three oracle invariants (task leak, obligation leak, quiescence) with guaranteed Type-I error control via Ville's inequality.

Instead of writing manual assertions, the Lab Runtime is continuously monitored by independent OraclesTest OracleRuntime correctness monitor for Lab testingA specialized runtime monitor that checks a specific class of correctness invariant during Lab testing. Each of the 17 built-in oracles watches for a different kind of bug — from resource leaks to protocol violations to budget overruns — acting as an automated auditor for your concurrent code. that act as automated auditors.

These Oracles use a statistical method called an E-Process (a betting martingale) to continuously evaluate runtime invariants like task leaks and quiescence. Because it is anytime-valid, the Oracle can instantly halt a test the moment evidence of a bug crosses the rejection threshold.

Attenuating CapabilitiesMacaroonDecentralized capability token with attenuating caveatsA bearer credential (inspired by Google's Macaroons paper) where anyone holding the token can add restrictions (caveats) but can never remove them. In Asupersync, capabilities are Macaroon-based: you can delegate a capability to a child task while attenuating it (e.g., adding a deadline, restricting to a specific Region, or limiting to N uses). The 8 caveat predicates include TimeBefore, TimeAfter, RegionScope, TaskScope, MaxUses, ResourceScope, RateLimit, and Custom.

When a parent task spawns an untrusted child, handing over raw capabilities (like full network access) is dangerous.

Asupersync capabilities behave like Macaroons. A parent can attach cryptographic caveats (like "expires in 50ms" or "read-only") before delegating the token. The child can use the token or add further restrictions, but the math prevents them from ever stripping the parent's constraints away.

Cancel Budget AlgebraBudget AlgebraProduct semiring for composing cancel budgetsCancel budgets compose algebraically as a product semiring. When regions nest, their budgets merge element-wise: min(deadlines), min(quotas), max(priority). This means the tightest deadline and smallest quota always win, while the highest priority propagates upward — guaranteeing consistent cancel timing across arbitrarily deep region hierarchies.

In a deep hierarchy of tasks, how do you resolve conflicting timeouts? If a child requests 15 seconds to run, but its parent is shutting down in 5 seconds, chaos ensues.

Asupersync resolves this using a Product SemiringProduct SemiringAlgebraic structure for budget compositionA mathematical structure where budgets compose element-wise using min and max operations. It's called a 'semiring' because it has two combining operations (like addition and multiplication, but using min and max instead). This gives budget composition clean algebraic properties: it's associative, commutative, and has identity elements.. Cancel budgets mathematically compose downwards across nested regions. The runtime clamps child deadlines to the parent's minimum, while propagating maximum priorities upward. A child mathematically cannot outlive the region it was born in.

Foata FingerprintsFoata FingerprintCanonical hash of concurrent execution tracesA technique for canonicalizing concurrent execution traces using Foata normal form. Two interleavings that differ only in the order of independent (non-conflicting) operations produce the same fingerprint. DPOR uses this to detect when two different schedules are actually equivalent — pruning redundant exploration without missing real bugs.

Exhaustively testing concurrency is impossible because thread interleavings explode factorially. However, many of those interleavings are functionally identical because the swapped operations never actually interact.

Asupersync collapses this search space by converting execution traces into a canonical Foata Normal Form. If the runtime sees that two traces belong to the same Mazurkiewicz equivalence classMazurkiewicz TraceEquivalence class of concurrent interleavingsA concept from concurrency theory: two execution traces are 'Mazurkiewicz equivalent' if they differ only in the order of independent (non-conflicting) operations. Asupersync's DPOR uses Mazurkiewicz traces to avoid redundantly testing schedules that produce identical outcomes — a massive reduction in the search space for concurrency testing., they map to the exact same fingerprint, allowing the DPOR algorithm to safely prune the redundant test run.

Conformal CalibrationConformal CalibrationDistribution-free prediction intervals for Lab metricsA statistical technique that produces valid prediction intervals without assuming any particular data distribution. The Lab runtime uses conformal calibration to set alert thresholds on runtime metrics — if a test run's timing falls outside the conformal band, the oracle flags it as anomalous, even if the underlying distribution is completely unknown.

How do you set a timeout for a task if you don't know what the normal distribution of execution times looks like? Standard deviations fail completely if the underlying data isn't a perfect bell curve.

Asupersync's Lab Runtime uses a formal statistical technique called Conformal Prediction. By analyzing historical traces, it draws a mathematically strict boundary that is guaranteed to contain 99% of future tasks—entirely distribution-free. If a task breaks this bound, the runtime knows with mathematical certainty that it represents a true anomaly, not just statistical noise.

Cancel FuelCancel FuelMonotonically decreasing termination counterA counter that strictly decreases with each step of cancel propagation, serving as a termination proof. Like a rocket with a finite fuel tank — the cancel signal can only travel so far before the fuel runs out, mathematically guaranteeing that cancellation always finishes.

When you initiate a shutdown across thousands of nested tasks, how do you mathematically prove that the cancellation cascade will actually finish and not get stuck in an infinite cycle?

Asupersync injects a finite amount of "Cancel Fuel" into the top of the Region Tree. Every time cancellation propagates to a sub-region or a child task, it consumes exactly one unit of fuel. Because the fuel strictly decreases and cannot drop below zero, the runtime guarantees absolute termination.

Trace Replay Stability

If five background nodes crash simultaneously during a test, traditional runtimes report those crashes to the supervisor in a random, chaotic order governed by thread races. A bug caused by one specific arrival order might never reproduce locally.

Asupersync resolves concurrent races mathematically. When simultaneous events occur, the runtime applies a strict deterministic tie-breaker (sorting by virtual timestamp, then by Task ID). Replaying the exact same trace ten thousand times guarantees the exact same arrival order ten thousand times.

Distributed SagasSagaDistributed operation with automatic compensation on failureA pattern for long-running operations that span multiple steps. Each step has a forward action and a compensating action. If any step fails (or cancellation arrives), the Saga automatically runs compensating actions for all completed steps in LIFO order. Asupersync's Saga engine classifies its 16 operation kinds into monotone and non-monotone using CALM analysis, minimizing the coordination overhead.

When a transaction spans multiple microservices, you cannot hold a single database lock. If the workflow fails on step 4, how do you undo the side-effects of steps 1, 2, and 3?

Asupersync provides a first-class Saga engine. You define a forward action and a backward (compensating) action for each step. If any step fails—or if cancellation strikes mid-flight—the runtime automatically walks backward up the tree, executing the compensations in strict LIFO order to restore the system to a clean state.

Small-Step SemanticsSmall-Step SemanticsFormal rules defining single computation stepsA mathematical framework where each computation step is defined by a transition rule of the form ⟨e, σ⟩ → ⟨e′, σ′⟩ (expression e in state σ steps to expression e′ in state σ′). Asupersync has 35 such rules covering spawning, cancellation, effect reservation, region closure, and more — each mechanized in Lean 4 for machine-checked correctness.

Most runtimes are built on an "it compiles, ship it" mentality. Asupersync's core behavior is strictly defined by a set of formal mathematical rules written in Lean 4.

Every evaluation step, cancellation cascade, and obligation transfer corresponds to a specific Transition Rule. These semantics mathematically prove the soundness of the runtime's guarantees before they are ever translated into Rust code.

Built Different

From Theory to crates.io