Asupersync

Spec-first, cancel-correct, capability-secure async for Rust

Try the Live Interactive WASM Demo

Quick Install

cargo add asupersync --git https://github.com/Dicklesworthstone/asupersync

TL;DR

The Problem: Rust's async ecosystem gives you tools but not guarantees. Cancellation silently drops data. Spawned tasks can orphan. Cleanup is best-effort. Testing concurrent code is non-deterministic. You write correct code by convention, and discover bugs in production.

The Solution: Asupersync is an async runtime where correctness is structural, not conventional. Tasks are owned by regions that close to quiescence. Cancellation is a protocol with bounded cleanup. Effects require capabilities. The lab runtime makes concurrency deterministic and replayable.

Why Asupersync?

Quick Example

Current API note: the structured-concurrency surface is explicit today. Child regions take &mut RuntimeState, a parent &Cx, and an explicit policy.

use asupersync::{Cx, Error, LabConfig, LabRuntime, Outcome, Scope};
use asupersync::runtime::{RegionCreateError, RuntimeState};
use asupersync::types::policy::FailFast;

// Structured concurrency: a child region closes to quiescence before returning.
async fn main_task(
    scope: &Scope<'_>,
    state: &mut RuntimeState,
    cx: &Cx,
) -> Result<Outcome<(), Error>, RegionCreateError> {
    scope
        .region(state, cx, FailFast, |child, state| async move {
            child
                .spawn(state, cx, |task_cx| async move { worker_a(&task_cx).await })
                .expect("spawn worker_a");
            child
                .spawn(state, cx, |task_cx| async move { worker_b(&task_cx).await })
                .expect("spawn worker_b");

            Outcome::ok(())
        })
        .await
}

// Cancellation is a protocol, not a flag.
async fn worker_a(cx: &Cx) -> Outcome<(), Error> {
    cx.checkpoint()?;
    // Do cancel-safe work here, e.g. reserve()/send() on a channel.
    Outcome::ok(())
}

async fn worker_b(cx: &Cx) -> Outcome<(), Error> {
    cx.checkpoint()?;
    Outcome::ok(())
}

// Lab runtime: deterministic testing uses explicit run reports.
#[test]
fn test_cancellation_is_bounded() {
    let mut lab = LabRuntime::new(LabConfig::new(42));

    // Enqueue work into `lab.state` / `lab.scheduler`, then drive to quiescence.
    let report = lab.run_until_quiescent_with_report();

    assert!(report.oracle_report.all_passed());
    assert!(report.invariant_violations.is_empty());
}

Coming from tokio?

If you already know tokio, this section maps the primitives you use daily to their asupersync equivalents. The APIs are intentionally different -- asupersync trades implicit convenience for explicit cancel-correctness -- but the concepts map cleanly.

Concept Mapping

Three things that will surprise you

1. Every async operation takes &Cx. Where tokio reads ambient runtime state from thread-locals, asupersync passes an explicit capability context. This means cancellation and budgets compose structurally -- you can see exactly what a function can do from its signature.

// tokio
let permit = tx.reserve().await?;

// asupersync
let permit = tx.reserve(&cx).await?;

2. No orphan tasks. Scopes close to quiescence. In tokio, tokio::spawn returns a detached task. In asupersync, every task lives in a region. When a scope exits, it waits for all children to finish. No fire-and-forget, no zombie tasks.

3. Outcome instead of just Result. Tokio task results are Result<T, JoinError> where JoinError covers panics and cancellation. Asupersync uses a four-valued Outcome<T, E> that distinguishes Ok, Err, Cancelled(reason), and Panicked(payload). The severity lattice (Ok < Err < Cancelled < Panicked) drives how combinators aggregate results.

Quick example: tokio vs asupersync

tokio:

use tokio::sync::mpsc;
use tokio::time::{sleep, Duration};

#[tokio::main]
async fn main() {
    let (tx, mut rx) = mpsc::channel(10);

    tokio::spawn(async move {
        for i in 0..5 {
            tx.send(i).await.unwrap();
            sleep(Duration::from_millis(100)).await;
        }
    });

    while let Some(val) = rx.recv().await {
        println!("got: {val}");
    }
}

asupersync:

use asupersync::channel::mpsc;
use asupersync::time::sleep;
use std::time::Duration;

async fn run(cx: &Cx, scope: &Scope) {
    let (tx, mut rx) = mpsc::channel::<i32>(10);

    scope.spawn(&mut state, cx, move |cx| async move {
        for i in 0..5 {
            let permit = tx.reserve(&cx).await.unwrap(); // cancel-safe
            permit.send(i);                               // cannot fail
            sleep(cx.now(), Duration::from_millis(100)).await;
        }
    });

    while let Ok(val) = rx.recv(&cx).await {
        println!("got: {val}");
    }
}

The key differences: reserve/send two-phase pattern prevents message loss on cancellation, &cx threads through capabilities, and the task is owned by the scope rather than detached.

Design Philosophy

1. Structured Concurrency by Construction

Tasks don't float free. Every task is owned by a region. Regions form a tree. When a region closes, it guarantees all children are complete, all finalizers have run, all obligations are resolved. This is the "no orphans" invariant, enforced by the type system and runtime rather than by discipline.

// Typical executors: what happens when this scope exits?
spawn(async { /* orphaned? cancelled? who knows */ });

// Asupersync: scope guarantees quiescence
scope
    .region(
        &mut state,
        &cx,
        asupersync::types::policy::FailFast,
        |sub, state| async move {
            sub.spawn(state, &cx, |task_cx| async move {
                task_cx.checkpoint()?;
                Outcome::ok(())
            })
                .expect("spawn task_a");
            sub.spawn(state, &cx, |task_cx| async move {
                task_cx.checkpoint()?;
                Outcome::ok(())
            })
                .expect("spawn task_b");
            Outcome::ok(())
        },
    )
    .await
    .expect("create child region");
// ← guaranteed: nothing from inside is still running once the child region closes

2. Cancellation as a First-Class Protocol

Cancellation operates as a multi-phase protocol, not a silent drop:

Running → CancelRequested → Cancelling → Finalizing → Completed(Cancelled)
            ↓                    ↓             ↓
         (bounded)          (cleanup)    (finalizers)

• Request: propagates down the tree
• Drain: tasks run to cleanup points (bounded by budgets)
• Finalize: finalizers run (masked, budgeted)
• Complete: outcome is Cancelled(reason)

Primitives publish cancellation responsiveness bounds. Budgets are sufficient conditions for completion.

Cancellation progress is continuously certifiable. ProgressCertificate tracks potential descent, classifies the current drain regime (warmup, rapid_drain, slow_tail, stalled, quiescent), and emits variance-adaptive concentration bounds (Freedman with Azuma as a conservative baseline). This turns "is shutdown actually converging?" into a measurable claim instead of a guess.

3. Two-Phase Effects Prevent Data Loss

Anywhere cancellation could lose data, Asupersync uses reserve/commit:

let permit = tx.reserve(cx).await?;  // ← cancel-safe: nothing committed yet
permit.send(message);                 // ← linear: must happen or abort

Dropping a permit aborts cleanly. Message never partially sent.

4. Capability Security (No Ambient Authority)

All effects flow through explicit capability tokens:

async fn my_task(cx: &mut Cx) {
    cx.spawn(...);        // ← need spawn capability
    cx.sleep_until(...);  // ← need time capability
    cx.trace(...);        // ← need trace capability
}

Swap Cx to change interpretation: production vs. lab vs. distributed.

5. Deterministic Testing is Default

The lab runtime provides: - Virtual time: sleeps complete instantly, time is controlled - Deterministic scheduling: same seed → same execution - Trace capture/replay: debug production issues locally - Schedule exploration: DPOR-class coverage of interleavings

Concurrency bugs become reproducible test failures.

"Alien Artifact" Quality Algorithms

Asupersync deliberately uses mathematically rigorous machinery where it buys real correctness, determinism, and debuggability. The intent is to make concurrency properties structural, so both humans and coding agents can trust the system under cancellation, failures, and schedule perturbations.

Formal Semantics and Lean-Checked Core Invariants

The runtime design is backed by a small-step operational semantics (asupersync_v4_formal_semantics.md) and a Lean project (formal/lean/Asupersync.lean) that checks the six non-negotiable runtime invariants recorded in formal/lean/coverage/invariant_status_inventory.json: structured concurrency single-owner, region-close quiescence, cancellation protocol, race loser drain, obligation no leaks, and no ambient authority.

The proof posture is exact: these are Lean-checked core invariants with theorem and executable-test linkage. This is not a blanket mechanized proof of every adapter, protocol implementation, platform backend, or distributed r