Kuiper: verified and efficient GPU programming
summary
Kuiper is a verified GPU language that uses dependent types and concurrent separation logic (built on F★/Pulse) to guarantee memory safety and race freedom for any well‑typed kernel, while extracting to plain CUDA with no runtime checks. The team implements matrix multiply, reductions and softmax, supports barriers, atomics, tiled shared memory, polymorphic layouts and tile sizes, and models synchronous launches with pledges; their prototype generates about 15,000 lines of CUDA from 15k lines of F★ and matches or beats handwritten performance.
AI-written summary · about
chapters (16)
- 0:00Kuiper introduction
- 1:25Verified efficient GPU programming
- 3:13Pulse separation logic primer
- 5:46Verifying a simple GPU kernel
- 9:39Splitting resources for launches
- 13:10Modeling multi-block GPU grids
- 14:12Kernel descriptions and spawning
- 14:36Polymorphism in Kuiper
- 17:08Matrix layout specialization
- 18:10Specializing tile sizes
- 19:11Fusion and transposition
- 19:53Barriers in separation logic
- 21:40Async launches with pledges
- 23:28Performance of verified kernels
- 24:33Future directions
- 24:56Q&A
related talks
39mFearless Concurrency on the GPU
01h 00mC++ on GPUs done right?
31mGPU Performance Portability Using Standard C++ with SYCL
01h 22mCostless Software Abstractions for Parallel Architectures
01h 02mC++ Performance Portability - A Decade of Lessons Learned
37mC++ for multi-accelerator, multi-vendor systems
01h 26mKhronos Sycl Language Framework for C++ Accelerators: Take Advantage of All the MIPS
01h 02mHPX - A C++ Library for Parallelism and Concurrency