Kuiper: Correct and Efficient GPU Programming with Dependent Types and Separation Logic
summary
Kuiper is an F library that uses Pulse-based separation logic to verify GPU kernels, extending the logic with forall+ connective and located resources to model memory hierarchy, kernel launches, and synchronization. The system proves safety, data-race freedom, and full functional correctness — including an optimized matrix multiply with two-level block tiling and tensor cores — and extracts zero-overhead CUDA that matches handwritten kernels and is competitive with cuBLAS, while enabling verified auto-tuning* (artifacts available).
AI-written summary · about
chapters (13)
- 0:00Kyber and GPU challenges
- 1:04GPU programming model
- 3:12CUDA kernel example pitfalls
- 5:59Safety vs performance trade-offs
- 7:03Kyber for verified GPU programming
- 8:27Verifying matrix multiplication
- 10:56Justifying kernel calls
- 12:17Packaging kernels with contracts
- 13:19Generalizing with type classes
- 14:41Virtual arrays layout
- 16:05Floating point verification
- 17:48Performance evaluation
- 18:29Q&A
related talks
30mGenerating High Performance Code for Irregular Data Structures using Dependent Types
20mPulseCore: An Impredicative Concurrent Separation Logic for Dependently Typed Programs
15mSpecifying and Testing GPU Workgroup Progress Models
10mMaximizing Kernel Development Productivity Under Performance Constraints
30mData-Parallel Flattening by Expansion
01h 00mBringing Clang and C++ to GPUs: An Open-Source, CUDA-Compatible GPU C++ Compiler
26mOptimising Density Computations in Probabilistic Programs via Automatic Loop Vectorisation
24mVerified Tensor-Program Optimization Via High-Level Scheduling Rewrites