Systems · View as Markdown

Real-time

Audio callbacks, control loops, and frame hot paths cannot afford a hidden allocation or a lock. C+ lets you mark such a function and have the compiler prove the property holds across the entire transitive call graph. A violation is a compile error, not a lint you can ignore.

The near-term target is soft real-time: audio callbacks, game frame loops, robotics control loops, market-data hot paths, and embedded-style firmware on a normal OS. Hard real-time needs scheduler, interrupt, and hardware guarantees that live below the language.

The proof carries onto real hardware: a #[realtime] fixed-point PID controller cross-compiled for esp32-xtensa runs closed-loop on a physical ESP32 at roughly 1.84 µs per step, and the same contract rejects an allocating variant with E0901 at cpc check, before anything is flashed.

For a focused proof recipe, see Realtime audio meter: it has a passing #[realtime] hot path plus negative fixtures for allocation (E0901), blocking (E0907), and stack-budget (E0908) failures.

The `#[realtime]` bundle

#[realtime] is sugar for a bundle of smaller contracts:

#[no_alloc] — no heap allocation
#[no_block] — no blocking call or lock wait
#[bounded_recursion] — no unbounded recursion

Bounded stack usage is checked alongside it. Each smaller attribute is available on its own, because many code paths need only one part of the contract.

#[realtime]
fn process_frame(input: f32x4[], output: f32x4[]) {
    let n: usize = output.len();
    let mut i: usize = 0 as usize;
    while i < n {
        output[i] = input[i] * GAIN;   // pure SIMD math
        i = i +% (1 as usize);
    }
    // a Vec::new, lock, channel recv, sleep, or unknown extern here
    // would not compile (E0901 / E0907)
    return;
}

`#[no_alloc]` — proven allocation-free (E0901)

A #[no_alloc] function rejects any path that reaches the heap. Direct malloc, calloc, realloc, aligned_alloc, and free reject, as do calls through #[link_name = "malloc"]. The check is resolved from sema information, not text, so it also catches allocation through a method call, through string interpolation ("...${x}..."), and through the Vec / HashMap / Box / Arc / Text constructors. The blessed to_text() is rejected at its call site because it allocates.

The contract is transitive: a function called from a #[no_alloc] body must itself be #[no_alloc], and an unknown extern is treated as "not proven" and rejected. The escape hatch is to vouch for a known-safe extern explicitly:

#[no_alloc]
extern fn sinf(x: f32) -> f32;

The check reaches implicit drop-glue too. If a #[no_alloc] function lets a value drop at scope exit and that destructor would allocate or free — a Text / Vec / Box local, or a type whose drop is not itself #[no_alloc] — it is rejected (E0901), reaching through struct fields, enum payloads, and array elements. So a hidden free at the closing brace is caught the same way a direct free call is.

This now covers more than let locals: an owned drop-carrying parameter (a move x, a move-by-default non-Copy struct, or move self) that drops at the end of the function, and a discarded drop-carrying temporary (a returned-but-unused owning value), are both caught as well. Anywhere the compiler would insert a drop that allocates or frees, the contract sees it.

`#[no_block]` — proven non-blocking (E0907)

A #[no_block] function rejects mutex locks, condition-variable waits, thread joins, sleep and timer waits, blocking file and socket I/O, unbounded channel recv, and unknown externs. It allows plain arithmetic, stack memory, atomics, atomic_thread_fence, #cpu_relax, and nonblocking try-style APIs. Like #[no_alloc], it composes transitively.

`#[max_stack(N)]` — bounded frame size (E0908)

#[max_stack(4096)]
fn callback(...) { ... }

The checker estimates the frame from the parameters and typed locals across all nested blocks, using ABI-accurate sizes for primitives, pointers, arrays, structs, enums, and SIMD types, and reports E0908 when the estimate exceeds N. Large local arrays and by-value temporaries become visible in the diagnostic.

Project-wide: `[profile.realtime]`

Rather than annotate every function, a project can opt in globally from its manifest:

[profile.realtime]
deny_alloc = true
deny_block = true
deny_unknown_extern = true
stack_limit = 4096

When present, the driver synthesizes the matching contracts onto every function defined in this package (dependencies are exempt), and the same E0901 / E0907 / E0908 diagnostics do the enforcement. cpc check runs the whole-project front-end gate without codegen, the fast CI check, and cpc check --diagnostics=json emits one machine-readable diagnostic per line for editor and CI tooling.

Threads: `Send` and `Sync` (E0502)

The marker types are enforced structurally. Rc[T] is !Send and !Sync, and MutexGuard[T] is !Send, so handing one to a Send-bounded site such as thread::spawn is E0502. Arc[T] stays Send + Sync as the thread-safe sibling.

A nominal type that transitively hides a raw pointer is !Send and !Sync by default, and the same !Send propagates structurally through a struct that holds an Rc. When a type is in fact safe to move or share, opt back in with a manual unsafe impl Send / unsafe impl Sync — see Threads & atomics for the marker syntax and its conditional, generic form.

Building blocks

The contracts say what a hot path may not do; these packages give it allocation-free, lock-free tools to work with:

rt — a lock-free SPSC ring (SpscRingU64) and a fixed-capacity object pool (FixedPoolU64). Every method is #[no_alloc] and #[no_block], so they are callable from inside a #[realtime] body.
static-arena — a fixed-size, stack-resident arena with zero malloc and zero free.
rt_darwin (see the rt page) — the macOS platform controls: a monotonic clock, audio-QoS thread priority, and page locking, each returning Result. rt_linux and rt_posix will mirror it.

Real-time

The #[realtime] bundle

#[no_alloc] — proven allocation-free (E0901)

#[no_block] — proven non-blocking (E0907)

#[max_stack(N)] — bounded frame size (E0908)

Project-wide: [profile.realtime]