Embedded

A proven allocation-free control kernel on the ESP32

The differentiated claim here is not "C+ does PID." It is: C+ proves an embedded control kernel has no hidden allocation and no blocking, across its entire call graph, before any firmware is flashed. The kernel is a small fixed-point PID step marked #[realtime]; the PID math is ordinary, but slipping a malloc, a lock, or a to_text() into that hot path becomes a compile error, not a latency spike you chase on a scope later.

This is soft real-time, by design: the language proves the kernel is clean. Scheduling, interrupts, and hardware timing live below the language (see Real-time).

What is proven, and what is not

Be precise about the boundary, because it is the whole point:

pid_step carries #[realtime] — which is #[no_alloc] + #[no_block] + bounded recursion, verified transitively. That function, and everything it calls, is proven heap-free and lock-free.
The surrounding loop is not #[realtime], on purpose. It blinks a heartbeat LED, logs telemetry over the UART, and paces itself with delay_ms — all deliberately outside the proven region. The claim is "this control kernel is provably clean," not "this entire firmware loop is real-time." A production loop would be driven by a hardware timer or ISR rather than delay_ms; this one stays simple to keep the focus on the kernel.

The kernel

A real fixed-point PID: proportional, integral (with anti-windup saturation), and derivative, all integer math. The controller state — the running integral and the previous error — is threaded in and out by value, so there is no mutable state to alias.

#[repr(C)]
struct PidOut { control: i32, integral: i32, prev_err: i32 }

// #[realtime] == #[no_alloc] + #[no_block] + bounded recursion, proven across
// the whole call graph. Q8 fixed-point gains (value / 256): Kp ~ 0.80,
// Ki ~ 0.06, Kd ~ 0.13. No floats, no heap.
#[realtime]
fn pid_step(setpoint: i32, measured: i32, integral: i32, prev_err: i32) -> PidOut {
    let err: i32 = setpoint - measured;

    let mut next_integral: i32 = integral + err;
    if next_integral >  2000 { next_integral =  2000; }    // anti-windup
    if next_integral < -2000 { next_integral = -2000; }

    let derivative: i32 = err - prev_err;

    let p: i32 = (205 * err) / 256;
    let i: i32 = (16  * next_integral) / 256;
    let d: i32 = (32  * derivative) / 256;

    let mut control: i32 = p + i + d;
    if control >  255 { control =  255; }                  // saturate the actuator
    if control < -255 { control = -255; }

    return PidOut { control: control, integral: next_integral, prev_err: err };
}

All three terms feed control, the integral is saturated to bound windup, and the actuator command is clamped to its range.

On overflow. The integer math stays in range by construction: the integral is saturated to ±2000 and the output to ±255, and the sampled inputs are bounded (measured here sweeps a small range, setpoint is fixed), so no intermediate — setpoint - measured, 205 * err, integral + err — can overflow i32. If you feed this kernel unbounded inputs, clamp err at the top of the step as well, or use the wrapping operators (+%, *%) where wraparound is acceptable.

Full source

src/main.cplus — the whole firmware:

// An ESP32 firmware whose control kernel (pid_step) is proven allocation-free
// and non-blocking at compile time. Cross-compiled with
// `cpc build --target esp32-xtensa`; the only C is a two-line app_main shim.

import "espidf/gpio" as gpio;
import "espidf/timer" as timer;
import "espidf/task" as task;
import "espidf/log" as log;

const LED: i32 = 2;        // onboard LED (GPIO2 on a WROOM-32D)

#[repr(C)]
struct PidOut { control: i32, integral: i32, prev_err: i32 }

// The proven kernel. Everything this calls is checked heap-free and lock-free.
#[realtime]
fn pid_step(setpoint: i32, measured: i32, integral: i32, prev_err: i32) -> PidOut {
    let err: i32 = setpoint - measured;

    let mut next_integral: i32 = integral + err;
    if next_integral >  2000 { next_integral =  2000; }    // anti-windup
    if next_integral < -2000 { next_integral = -2000; }

    let derivative: i32 = err - prev_err;

    let p: i32 = (205 * err) / 256;        // Kp ~ 0.80
    let i: i32 = (16  * next_integral) / 256;  // Ki ~ 0.06
    let d: i32 = (32  * derivative) / 256;     // Kd ~ 0.13

    let mut control: i32 = p + i + d;
    if control >  255 { control =  255; }                  // saturate the actuator
    if control < -255 { control = -255; }

    return PidOut { control: control, integral: next_integral, prev_err: err };
}

// Exported entry point. ESP-IDF's main component keeps a two-line C shim that
// calls this from app_main (see Reproduce). This loop is NOT #[realtime]: it
// does I/O and paces itself with delay_ms, outside the proven kernel.
pub extern fn cplus_app_main() {
    gpio::reset(LED);
    gpio::set_direction(LED, gpio::mode_output());

    let setpoint: i32 = 100;
    let mut integral: i32 = 0;
    let mut prev_err: i32 = 0;
    let mut led: u32 = 0 as u32;
    let mut step: i64 = 0 as i64;

    loop {                                         // diverging: no trailing return
        // A real loop samples a sensor here; this stand-in sweeps a value.
        let measured: i32 = (step % (200 as i64)) as i32;

        let t0: i64 = timer::now_us();
        let out: PidOut = pid_step(setpoint, measured, integral, prev_err);
        let step_us: i64 = timer::now_us() - t0;   // time the proven kernel only

        integral = out.integral;
        prev_err = out.prev_err;

        led = if led == (0 as u32) { 1 as u32 } else { 0 as u32 };
        gpio::set_level(LED, led);                 // heartbeat, not driven by control

        if step % (100 as i64) == (0 as i64) {     // telemetry over the UART
            log::print_i32(c"control:", out.control);
            log::print_i64(c"kernel_us:", step_us);
        }

        step = step + (1 as i64);
        task::delay_ms(10 as u32);                 // ~100 Hz pacing (outside the kernel)
    }
}

The espidf calls are ordinary safe functions — the unsafe FFI is sealed inside the espidf package — so the firmware body has no unsafe blocks at all. gpio and timer are themselves #[no_alloc] + #[no_block] leaves, so pid_step could read the clock or drive a pin and still keep its contract.

Results

Built with cpc build --target esp32-xtensa and linked into an ESP-IDF firmware.


Build output	an `esp32-xtensa` staticlib (object + archive + C header)
`pid_step` (the proven kernel)	~1.84 µs (about 442 cycles) on an ESP32-D0WDQ6, 240 MHz
Float / heap in the kernel	none — fixed-point integer math

One thing to read carefully: ~1.84 µs is the cost of the proven kernel itself, measured around the pid_step call. It is not whole-loop latency or jitter — those also include the GPIO write, the optional UART log, and the delay_ms pacing, none of which are part of the #[realtime] region. The headline isn't the number anyway; it is where the proof happens: the #[no_alloc] / #[no_block] guarantee is checked at cpc check time, so a violation never reaches the chip.

The contract bites

Slip an allocation into the kernel and it stops compiling — on the host or for the device, before flashing:

extern fn malloc(n: usize) -> *u8;

#[realtime]
fn pid_step(setpoint: i32, measured: i32, integral: i32, prev_err: i32) -> PidOut {
    let scratch: *u8 = unsafe { malloc(16 as usize) };   // ← E0901: #[no_alloc] violation
    // ...
}

$ cpc check --target esp32-xtensa
error[E0901]: a #[no_alloc] function must not reach the heap

Reproduce

You need cpc 0.0.21 or newer, the Espressif toolchain (esp-clang, LLVM 19+), and ESP-IDF. See Targets & cross-compilation for how cpc finds esp-clang.

1. The C+ component. Put the source above in src/main.cplus with a manifest that builds a staticlib and depends on espidf:

[package]
name    = "pid_kernel"
version = "0.0.1"
edition = "2026"

[lib]
name = "app"

[dependencies]
espidf = "*"

cpc build --target esp32-xtensa

cpc stops at the archive (target/esp32-xtensa/debug/libapp.a); ESP-IDF's CMake links the firmware.

2. The two-line shim. ESP-IDF calls app_main; the C+ app exports cplus_app_main. The main component keeps one tiny C file:

extern void cplus_app_main(void);
void app_main(void) { cplus_app_main(); }

…and links the staticlib in its CMakeLists.txt:

idf_component_register(SRCS "main.c" INCLUDE_DIRS ".")
target_link_libraries(${COMPONENT_LIB} PRIVATE "${CMAKE_SOURCE_DIR}/path/to/libapp.a")

3. Flash it.

idf.py build flash monitor

The LED blinks as a heartbeat, and the UART monitor prints the control output and the per-kernel-call time. The #[realtime] contract was proven at build time; the chip just runs it.

‹ Back to all examples