warp-types: Session-Typed GPU Divergence
Abstract
A type system that prevents shuffle-from-inactive-lane bugs in GPU warp programming by tracking active lane masks at compile time. Diverged warps literally cannot call shuffle — the method does not exist on the type. Zero runtime overhead verified at Rust MIR, LLVM IR, and NVIDIA PTX levels. Real GPU execution on NVIDIA H200 SXM and RTX 4000 Ada (4 typed kernels PASS on both); AMD MI300X mask-correctness verified via HIP. v0.3.1 fixes WarpBuilder target-cpu (PTX 6.0 support), adds ballot setp/selp workaround, and hardens warp_kernel macro.
Fields of Study & Subjects
Parallel Computing and Optimization Techniques
Logic
programming
and type systems
Embedded Systems Design Techniques
Publication details
- Journal / source
- Zenodo (CERN European Organization for Nuclear Research)
- Publication date
- 15 March 2026
- Language
- EN