Add Asupersync to your Rust project and start building cancel-correct async systems.
Step 1
Add Asupersync with a single command.
$
cargo add asupersyncStep 2
A cancel-correct TCP server in under 25 lines.
examples/server.rs
01 asupersync::{Region, Cx, Outcome, Budget};02 std::time::Duration;03 04#[asupersync::main]05 main(cx: &Cx) -> Outcome<()> {06 // Open a region — all tasks scoped here07 Region::open(cx, "server", |cx| {08 // Spawn a listener with cancel capability09 permit = cx.spawn("listener", |cx| {10 listener = cx.tcp_bind("0.0.0.0:8080").?;11 {12 (stream, _) = listener.accept(cx).?;13 cx.spawn("conn", handle_connection(stream));14 }15 });16 17 // Wait for shutdown signal18 cx.shutdown_signal().;19 20 // Cancel with budget — tasks get 5s to drain21 permit.cancel(Budget::timeout(Duration::from_secs(5)));22 }).23}Syntax_Validation_Active
UTF-8_ENCODEDCore Concepts
The foundations of cancel-correct async programming.
Structured Concurrency
Every task lives in a Region. Regions form a tree. When a Region closes, all tasks within it are cancelled and awaited. No orphaned futures.
Cancel-Correctness
Three-phase protocol: Request → Drain → Finalize. Tasks always get time to clean up. Resources never leak. Buffers always flush.
Deterministic Testing
Lab runtime with seed-controlled execution. DPOR explores interleavings systematically. Replay any bug with the same seed.
FAQ
Answers to the most frequent questions about Asupersync.
When should I use Asupersync instead of Tokio?
Use Asupersync when correctness matters more than raw throughput. If you're building servers, pipelines, or systems where resource leaks, orphaned tasks, or silent cancellation failures would be bugs — Asupersync makes those bugs impossible by construction. Tokio is better for maximum single-server throughput where you're willing to handle cancellation safety manually.
Can I use Tokio crates with Asupersync?
Not directly — Asupersync uses its own runtime and async primitives. However, we provide bridge adapters for common Tokio ecosystem crates. The built-in protocol library covers most needs (TCP, HTTP, channels, mutexes) with cancel-correctness guarantees that Tokio wrappers can't provide.
How does performance compare to Tokio?
For I/O-bound workloads, Asupersync is within 5-15% of Tokio's throughput. The three-lane scheduler adds minimal overhead, and the cancel protocol only activates during actual cancellation. The Lab runtime (deterministic mode) is slower by design — it's for testing, not production.
Is Asupersync production-ready?
Asupersync is currently in v0.2.x — suitable for new projects and experimentation, but not yet battle-tested at scale. The core runtime has 12 formal proofs and extensive property-based testing. We recommend it for greenfield projects where you want correctness guarantees from day one.
What does 'cancel-correct' mean?
Cancel-correct means that when a task is cancelled, it always gets a chance to clean up (Drain phase), its finalizers always run (Finalize phase), and resources are never silently leaked. In Tokio, dropping a future just... stops it. Buffers may not flush. Connections may not close. Locks may not release. Asupersync makes this impossible.
How does the Lab runtime find bugs?
The Lab runtime uses Dynamic Partial Order Reduction (DPOR) to systematically explore task interleavings. Given a concurrent program, it identifies which interleavings produce different outcomes and tests a representative subset. This is far more effective than random testing — it can find bugs that might take billions of random runs to hit.
Do I need to learn a new async syntax?
No — Asupersync uses standard Rust async/await. The main difference is that your main function receives a Cx (capability context) parameter, and you use Region::open instead of bare task spawning. If you've used structured concurrency in Kotlin (coroutineScope) or Swift (TaskGroup), the patterns will feel familiar.
What's the minimum Rust version?
Asupersync requires Rust 1.75+ for async trait support and RPITIT. We track stable Rust and don't require nightly features.
What are Two-Phase Effects?
Two-Phase Effects split side effects into Reserve (stage the change, making it reversible) and Commit (apply it permanently). Think of a bank transfer: first, the money is placed on hold (Reserve). If the operation is cancelled before it finishes, the hold is simply released — no money lost. Only after a cancellation checkpoint confirms no cancel is pending does the transfer actually go through (Commit). This prevents the half-executed side-effects that plague traditional async runtimes.
How does the spectral deadlock detector work?
Asupersync maintains a real-time wait-graph — a directed graph where edges mean 'task A is waiting on task B'. The runtime continuously computes the Fiedler value (second-smallest eigenvalue of the graph's Laplacian matrix). When this value drops near zero, the graph is about to split into disconnected components — the mathematical signature of an emerging deadlock. Think of it like a traffic congestion sensor: it detects gridlock forming before cars actually stop, letting the scheduler intervene proactively.
What makes the formal semantics useful in practice?
The 35 small-step transition rules aren't just academic exercises — they're mechanized in Lean 4, which means a computer has verified they're logically consistent. This bridges the gap between the spec document (what Asupersync should do) and the runtime implementation (what it actually does). When a bug is found, the formal rules precisely identify whether it's a spec error or an implementation error. It also enables automated property-based testing: the Lab runtime generates random programs and checks that every execution trace conforms to the formal rules.
How do the 17 test oracles work together?
Each oracle is an independent correctness monitor that watches for one specific class of bug during Lab testing. TaskLeak catches tasks that outlive their Region. ObligationLeak catches dropped Permits or Leases. CancelProtocol verifies the 3-phase shutdown is followed correctly. BudgetOverrun catches tasks that exceed their Drain budget. When you run a Lab test, all 17 oracles are active simultaneously — like having 17 specialized auditors reviewing every step of your concurrent program's execution.
How does Macaroon-based capability attenuation work?
Capabilities in Asupersync are bearer tokens inspired by Google's Macaroons paper. The key property: anyone holding a capability can add restrictions (caveats) but can never remove them. When you delegate a capability to a child task, you can attenuate it — for example, adding a TimeBefore deadline, restricting it to a specific Region, limiting it to N uses, or applying a rate limit. There are 8 caveat predicates in total, including a Custom(key, value) escape hatch for application-specific restrictions. This means delegation is always safe: you can hand out capabilities freely, knowing they can only become more restricted, never less.
What are E-processes and why do they matter for testing?
E-processes are a modern statistical technique (betting martingales) that let you continuously monitor a hypothesis and reject it the instant evidence is strong enough — without any penalty for 'peeking' at intermediate results. Traditional p-values require you to commit to a fixed sample size upfront. E-processes don't. The Lab runtime uses them to monitor three critical invariants (task leak, obligation leak, quiescence) during testing. Via Ville's inequality, if the E-value ever exceeds 1/α, you know with mathematical certainty that an invariant was violated — no matter when you checked.
How does Saga compensation handle distributed failures?
When a multi-step operation spans several services (create account → send email → charge card), failure at any step triggers automatic LIFO compensation — unwinding completed steps in reverse order. What makes Asupersync's Saga engine special is CALM analysis: it classifies each of the 16 operation kinds as either monotone (coordination-free, like Reserve and Send) or non-monotone (barrier-required, like Commit and Release). Consecutive monotone steps are batched without synchronization, and barriers are inserted only before non-monotone steps. This minimizes coordination overhead while maintaining correctness.
What is the Lyapunov potential function?
It's a 4-component 'energy measure' that the scheduler uses to formally prove the system always makes progress. The four components are: (1) live task count, (2) pending obligation age, (3) draining region count, and (4) deadline pressure. Like a ball rolling downhill, this function strictly decreases with each scheduler step — mathematically guaranteeing the runtime converges toward quiescence. The scheduler can tune the component weights: obligation-focused mode prioritizes clearing aged obligations, while deadline-focused mode prioritizes tasks approaching their deadlines.