Corey James- 12 of 12bitwise on both routes at the release
- 100+lane notes voided and the count rebuilt from proofs
- 3proofs before any lane may call a route native
A rewrite is finished when you can prove it behaves like the original. For a GPU serving runtime that means proving it on the real device, under concurrency, cancellation and shutdown, against a baseline that is not even bit-stable with itself in batched mode. Partway through the ActiveKV port I discovered that a long run of passing trials had been testing Python against Python, and the rule that came out of it now sits in the definition of done.
The challenge
Three distinct problems hide inside "does the rewrite match". The baseline is not deterministic: stock vLLM's batched output varies between its own runs, so a naive bitwise gate would fail the original against itself. A test can pass without testing the served path: CPU differential suites fed with stand-in objects can be green while the real server, which passes different object types, fails at startup. And the native code has to be the code that runs.
Constraints
Some references are non-deterministic, and loosening the gate everywhere to accommodate them would hide real divergence. Native safety checks could not be removed to make outputs line up. And with agents working in parallel lanes, each lane's claim of success had to be independently provable or it was worth nothing.
My approach
Bitwise only where the reference is bitwise with itself. Run the reference twice first. Where the two runs agree, demand bitwise equality from the port. Where they differ, judge the port within the reference's own spread. Each mode is compared against its own reference.
A green suite is a claim about the thing it ran.
Parity never removes a guard. When the native engine refuses something Python allowed, first prove which check fired and why. If the refusal is correct, the Python behaviour was the bug.
"Switched" means proven on the real startup path. A claim that a native route is in use requires the binding site, every call-site condition, and the run-log ordering that shows the binding happened before the decision.
What I built
Per-lane differential suites fed with served object types, the same geometry, cache-manager and wire objects the real server passes.
Device proof runs that exercise cancellation, refusal and shutdown and keep the evidence, and process-map and stack captures showing that no product Python frames execute on the native route.
A switch-brief rule that no lane note may claim a route is native without the three proofs above, and a reachability count that treats a dispatch site as native only with a bind-order proof attached.
Difficult decisions
Voiding the passing trials. The CPU suites had passed. They had been testing Python stand-ins instead of the real server's objects, and a device proof run failed at startup. The trials were declared void and the suites were rebuilt around served types.
Classifying dozens of refusals one by one. The native engine refused cases the Python engine had accepted. Each was traced to the guard that fired. None of the guards was relaxed; the cases where Python had been wrong became documented safe divergences.
Re-folding the count instead of patching it. When the bind-order defect surfaced, the lane notes resting on the false claim were voided and the count rebuilt from proofs.
Results
Port parity was thirteen of thirteen exact cells and twelve of twelve hybrid cells, bitwise, and proof that the native route runs is a required criterion in the definition of done.
Technologies used
C++ · Python · vLLM · PyTorch XPU · Bitwise comparison harnesses · Sampling profilers for process evidence · pybind11
What this demonstrates
I am rigorous about what a test proves, and I check that the thing a suite ran is the thing that runs. When the process fails at program scale, I fix the process.