Realtime audio meter

This example is a proof recipe for the #[realtime] claim. It combines an audio-style hot path with the real rt package shapes from the C+ source tree: vendor/rt/src/rt.cplus ships SpscRingU64, and vendor/rt/src/pool.cplus ships FixedPoolU64. Their hot-path methods are annotated #[no_alloc] and #[no_block], and the compiler E2E suite checks the diagnostics this page depends on.

The important property is not the audio math. The important property is that the compiler rejects code paths that would allocate, block, or exceed the stack budget before the callback can ship.

Claim	How this example checks it
#[realtime] accepts arithmetic-only hot paths	src/main.cplus checks cleanly
allocation is rejected	bad/alloc.cplus reports E0901
blocking is rejected	bad/block.cplus reports E0907
oversized stack frames are rejected	bad/stack.cplus reports E0908

Compiler-backed evidence

The source tree has two layers of evidence behind this recipe:

Evidence	What it proves
vendor/rt/src/rt.cplus	SpscRingU64::new, len, is_empty, is_full, push, and pop are fixed-capacity, nonblocking, allocation-free operations marked #[no_alloc] #[no_block]
vendor/rt/src/pool.cplus	FixedPoolU64 provides an allocation-free fixed pool with acquire, release, get, and set marked #[no_alloc] #[no_block]
cpc/tests/e2e.rs	compiler tests reject allocation with E0901, blocking calls with E0907, oversized frames with E0908, and JSON realtime reports with nonzero exit on violations

Representative E2E test names include realtime_profile_rejects_local_allocation, realtime_profile_clean_program_passes, no_alloc_rejects_allocating_method_through_receiver, no_alloc_allows_marked_method_through_receiver, no_alloc_rejects_to_string, no_block_rejects_blocking_method_through_receiver, realtime_report_json_flags_violations, and realtime_report_clean_exits_zero.

Project layout

realtime_meter/
├── Cplus.toml
├── src/main.cplus
└── bad/
    ├── alloc.cplus
    ├── block.cplus
    └── stack.cplus

Cplus.toml enables the project-wide realtime gate as well as the explicit attribute on the callback. That makes cpc check useful in CI: a new helper function cannot quietly add a heap allocation or a blocking wait.

[package]
name    = "realtime-meter"
version = "0.0.1"
edition = "2026"

[[bin]]
name = "realtime-meter"
path = "src/main.cplus"

[dependencies]
rt = "*"

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

Passing callback

The callback reads a block of samples, applies a gain, writes the output, and publishes a fixed-point peak value into a lock-free SPSC ring. It allocates nothing and has no operation that can wait.

import "rt/rt" as rt;

const GAIN: f32 = 0.80f32;

fn abs_f32(x: f32) -> f32 {
    if x < 0.0f32 { return 0.0f32 - x; }
    return x;
}

fn peak_to_u64(x: f32) -> u64 {
    let clamped: f32 = if x > 1.0f32 { 1.0f32 } else { x };
    return (clamped * 1000000.0f32) as u64;
}

#[realtime]
#[max_stack(1024)]
fn process_audio(input: f32[], output: f32[], mut peaks: rt::SpscRingU64) -> i32 {
    let n: usize = output.len();
    let mut i: usize = 0 as usize;
    let mut peak: f32 = 0.0f32;

    while i < n {
        let y: f32 = input[i] * GAIN;
        output[i] = y;

        let a: f32 = abs_f32(y);
        if a > peak { peak = a; }

        i = i +% (1 as usize);
    }

    let _ok: bool = peaks.push(peak_to_u64(peak));
    return 0;
}

fn main() -> i32 {
    let mut input: f32[8] = [0.10f32, -0.20f32, 0.30f32, -0.40f32, 0.25f32, -0.50f32, 0.75f32, -1.00f32];
    let mut output: f32[8] = [0.0f32, 0.0f32, 0.0f32, 0.0f32, 0.0f32, 0.0f32, 0.0f32, 0.0f32];
    let peaks: rt::SpscRingU64 = rt::SpscRingU64::new();

    return process_audio(input, output, peaks);
}

The ring write is deliberately nonblocking: if the consumer falls behind, push returns false; the callback does not wait.

The package implementation follows the same rule. SpscRingU64::push checks capacity and returns false when full:

#[no_alloc] #[no_block]
pub fn push(mut self, v: u64) -> bool {
    let head: u64 = unsafe { atomic::atomic_load_u64(#addr_of(self.head), atomic::Ordering::Acquire) };
    let tail: u64 = unsafe { atomic::atomic_load_u64(#addr_of(self.tail), atomic::Ordering::Relaxed) };
    if (tail -% head) >= (1024 as u64) {
        return false;
    }
    let idx: usize = (tail % (1024 as u64)) as usize;
    self.buf[idx] = v;
    unsafe { atomic::atomic_store_u64(#addr_of(self.tail), tail +% (1 as u64), atomic::Ordering::Release); }
    return true;
}

FixedPoolU64::acquire uses the same contract style: bounded state, no heap, and failure as a value instead of a wait.

#[no_alloc] #[no_block]
pub fn acquire(mut self) -> option::Option[u32] {
    if self.free_head == pool_none() {
        return option::Option[u32]::None;
    }
    let idx: u32 = self.free_head;
    self.free_head = self.links[idx as usize];
    self.in_use = self.in_use +% (1 as usize);
    return option::Option[u32]::Some(idx);
}

Negative fixture: allocation

This fixture is the kind of change a model might accidentally introduce while trying to make a diagnostic string. to_text() allocates, so it is rejected inside the realtime contract.

#[realtime]
fn process_bad_alloc(x: f32) -> i32 {
    let label = "peak=".to_text();
    if x > 0.0f32 { return label.len() as i32; }
    return 0;
}

Expected diagnostic shape:

bad/alloc.cplus:3:24: error[E0901]: function `process_bad_alloc` is marked `#[no_alloc]` but calls allocating function `to_text`

Negative fixture: blocking

The callback cannot sleep, wait on a timer, block on a mutex, join a thread, or perform blocking I/O. This fixture should be rejected with E0907.

import "stdlib/thread" as thread;

#[realtime]
fn process_bad_block() -> i32 {
    thread::sleep_ms(1 as u64);
    return 0;
}

Expected diagnostic shape:

bad/block.cplus:5:5: error[E0907]: function `process_bad_block` is marked `#[no_block]` but calls blocking function `sleep_ms`

Negative fixture: stack budget

Large locals are visible to #[max_stack]. This fixture intentionally exceeds a small budget.

#[realtime]
#[max_stack(256)]
fn process_bad_stack() -> i32 {
    let scratch: u8[2048] = [0u8; 2048];
    return scratch[0] as i32;
}

Expected diagnostic shape:

bad/stack.cplus:3:1: error[E0908]: function `process_bad_stack` stack frame exceeds 256 bytes

Reproduce

cpc check
cpc check bad/alloc.cplus --diagnostics=json
cpc check bad/block.cplus --diagnostics=json
cpc check bad/stack.cplus --diagnostics=json

The first command should pass. The three bad/ commands should fail, and the JSON diagnostics should include E0901, E0907, and E0908 respectively.

That is the proof boundary: the claim is not "the programmer remembered not to allocate." The claim is that the compiler rejects the callback if allocation, blocking, or an oversized frame becomes reachable. The public recipe is small, but the backing checks live in the compiler suite and in the rt package source.