From the SentryWard project
Blog
A closer look at how GPU kernels synchronize, what goes wrong, and how we verify them.
Technical walkthrough
SentryWard: Formal Verification of Warp-Specialized GPU Kernels
Follow a kernel from asynchronous copies and barriers to race checking and a reference-guided equivalence proof. Includes interactive figures, issues found in PyTorch, TileLang, and CUTLASS, and results from removing redundant synchronization.
Read the post