warp-types¶
Linear typestate for GPU warp divergence: compile-time prevention of shuffle-from-inactive-lane bugs.
Status: v0.3.2 on crates.io. Nelson-Oppen SMT combination (QF_UFBV) shipped.
Repository: github.com/modelmiser/warp-types
What it is¶
A Rust type system that makes GPU divergence bugs into compile errors. When a warp diverges (some lanes take one branch, others take the other), shuffles and reductions become unsafe — reading from an inactive lane is undefined behavior. warp-types encodes the divergence state in the type system so the compiler rejects these bugs before they reach the GPU.
Blog posts¶
- A Cap Makes Brute Force Win — we aimed our own IC3/PDR model checker at the split-brain proof expecting it to beat explicit-state enumeration. It lost — because the lease guard caps one quantity, and that collapses the space brute force has to search
- Intervals Collapse to Points — what happens to formal verification when the hardware is deterministic
- The Bug That Wasn't There — a one-line soundness hole that zero tests caught and zero users triggered