Performance

Throughput, the optimisation that produced it, and the gap that is left over. Every number here was produced by reference/bench.py on the machine named in the file.

Back to the README

Benchmark

Apple M3, macOS 26.4.1, rustc 1.98.0, Apple clang 21.0.0. Single threaded. stories15M (dim 288, 6 layers, 6 heads, vocab 32000, context 256), 248 generated greedy tokens, 5 runs, median.

Every row was measured in a single session on an otherwise idle machine, with the same run.c binaries, so no row is quoted from a run with different load than the others.

These absolute numbers are not reproducible on a busy machine, and the table should be read with that in mind. Measured later on the same machine while a load average of ~5.7 was running (browser, compilers, terminal), the same 7-run measurement gave 619 tok/s with individual runs spanning 431 to 674 — a 56% spread, not the few percent an idle machine shows. The first run after a rebuild is also reliably ~12% slow, from page faults on the 60 MB checkpoint.

So: quote these figures as "what this engine did on an idle M3", and use them for ratios rather than absolutes. What is reproducible under any load is the byte-identity result below, because that is a correctness claim rather than a timing one.

Greedy output is byte-identical to both run.c builds across all 248 tokens, for all four proofinfer variants.

The 8-lane dot product, including the part I got wrong

a.iter().zip(b).map(|(x, y)| x * y).sum() compiles to a serial chain of floating-point additions. Since addition is not associative, LLVM is forbidden from splitting that chain into parallel partial sums, because doing so would change the answer. One loop-carried dependency per multiply is a latency wall that no amount of -O3 gets past.

Eight independent accumulators remove the dependency. That is the standard advice, and following it exactly gets you to 207.9 tok/s — a real 1.35x, and most of the way short of the real win.

Written that way:

while i + 8 <= n { for lane in 0..8 { acc[lane] += a[i + lane] * b[i + lane]; } }

the eight lanes become eight independent scalar chains. The dependency is gone, but LLVM's loop vectoriser does not fire on that form at all. Rewriting the identical arithmetic as chunks_exact(8) reaches 835.4 tok/s, a further 4.0x, because it presents the eight values as one contiguous chunk and the superword-level pass can pack them into vectors.

Measured in isolation at dim = 288 (the model's hidden size), in Gelem/s:

The indexed form is a 1.5x on the kernel, and looks like the optimisation worked. It is 4.4x short of what the same arithmetic can do.

Nothing is reassociated in either version. Each lane is still a strict left-to-right sum; the eight lanes are just eight interleaved ordered sums. The last bits of the result do change, which is precisely why the differential test is tolerance-based — and the diff test, the mutation check and the byte-identical comparison were all re-run after this change.

The -Ofast gap, reported honestly

run.c -Ofast is 973.6 tok/s and still faster than the 835.4 tok/s this engine reaches with an optimising Rust compiler and explicit SIMD. The gap is about 1.17x.

-Ofast enables -ffast-math, which lets clang reassociate floating-point additions anywhere it likes, including the attention and value-accumulation loops, not just the matmul. This project restricts itself to one documented reassociation in one function, because unrestricted reassociation across the whole forward pass makes the numerics much harder to reason about and much easier to break silently.

The 1.17x is the price of that choice. It is a real cost, reported rather than hidden: the honest summary is that clang, allowed to assume the IEEE 754 rules do not apply, extracts more than a conforming compiler can, and that some of what it extracts is available to a conforming compiler if you write the loop in the right shape — as the chunks_exact result above demonstrates — and some of it is not.

-C target-cpu=native adds 0.2% here (835.4 → 836.8), which is inside the run-to-run noise. That is worth stating plainly because it is not the result one would predict from an x86 machine with AVX-512: on aarch64 the baseline codegen already saturates the available NEON width for this loop, so there is nothing left for a more specific target to unlock. The chunks_exact rewrite, not the target flag, is what unlocked the vectorisation.

Source: https://github.com/blackdragoon26/proofinfer/blob/main/docs/performance.md in the repository.