Formalizing PTX in Lean to Prove GPU Kernel Correctness

Luk Koska, Tom Koska, Ben Koska

We present an approach to mathematically formalizing PTX, an approach that allows modeling and reasoning about patterns common in GPU kernels for Deep Learning, including acquire-r…