Architecture

How Asupersync enforces cancel-correctness, structured concurrency, and deterministic testing.

Overview

Runtime Architecture

Asupersync's runtime is built on three pillars: Regions for structure, the Cancel Protocol for cleanup, and the Lab for testing.

APPLICATION LAYERRegion Tree (structured concurrency scopes)CANCEL PROTOCOL1. Request2. Drain3. FinalizeSCHEDULERCancel Lane (hi)Timed Lane (mid)Ready Lane (lo)
Core Model

Structured Concurrency

Every task lives inside a Region. Regions form a tree. When a parent Region closes, all children are cancelled — automatically.

regions.rs
01// Regions scope task lifetimes02Region::open(cx, "server", 
async
 |cx| {03    // Child tasks are bound to this Region04    cx.spawn("worker-1", handle_requests());05    cx.spawn("worker-2", process_queue());06 07    // When this Region closes, workers are cancelled08    // via the cancel protocol (not silently dropped)09    cx.shutdown_signal().
await
;10}).
await
Syntax_Validation_Active
UTF-8_ENCODED

Unlike Tokio's tokio::spawn which creates globally-scoped tasks, Asupersync tasks are always scoped to a Region. This eliminates orphaned futures — if you can't see the task, it can't outlive you.

Safety

Cancel Protocol

Three phases ensure resources are always cleaned up, even during cancellation.

1. Request

Cancel signal sent. Task sees CancelRequested on its Cx. Can begin graceful shutdown.

2. Drain

Task gets budgeted time to finish in-flight work. Flush buffers, close connections, release locks.

3. Finalize

Registered finalizers run in LIFO order. Like defer in Go, but integrated with the cancel protocol.

Development

Build Timeline

From formal proofs to published crate.

Phase 1

Core Runtime & Region Model

  • Designed the Region tree model with parent-child lifetime scoping

  • Implemented the three-phase cancel protocol (Request → Drain → Finalize)

  • Built the Cx capability context with spawn/IO/timer gates

  • Formal proofs for cancel-safety and region closure guarantees

Runtime Log v0.2
Phase 2

Linear Obligations & Permits

  • Designed the Permit/Lease linear type system

  • Implemented compile-time must-use enforcement

  • Built the three consumption paths: Send, Complete, Abort

  • Added Spork (spawn + fork) for structured task hierarchies

Runtime Log v0.2
Phase 3

Three-Lane Scheduler

  • Implemented Cancel/Timed/Ready lane architecture

  • Built priority inversion prevention for cancel propagation

  • Designed quiescence detection for region closure

  • Benchmarked against Tokio's work-stealing scheduler

Runtime Log v0.2
Phase 4

Lab Runtime & DPOR

  • Built deterministic executor with seed-controlled ordering

  • Implemented Dynamic Partial Order Reduction for systematic testing

  • Added replay capability for reproducing concurrency bugs

  • Integrated with cargo test for seamless developer experience

Runtime Log v0.2
Phase 5

Built-in Protocols & Ecosystem

  • Implemented cancel-correct TCP, HTTP/1.1, and WebSocket protocols

  • Built cancel-aware channels, mutexes, and semaphores

  • Added supervisor trees with restart policies

  • Published to crates.io with comprehensive documentation

Runtime Log v0.2
Interactive DemosGet Started