Cost semantics and static resource analysis for CUDA
summary
Defines a formal cost semantics for CUDA and a static analysis tool RaCUDA that uses automated amortized resource analysis and quantitative Hoare logic (via Absynth and an LP solver) to bound global-memory sectors, shared-memory bank conflicts, warp-divergence events and a combined Steps metric. Evaluation over 14 benchmarks shows the simulator is within about 20–30% error of profiled runs and RaCUDA produces mostly fast (sub-second) static upper bounds; method extends to detect AES timing leaks and prove relational non-interference.
AI-written summary · about
chapters (6)
- 0:00Cost semantics for CUDA
- 1:34Performance pitfalls in CUDA
- 7:40Formalizing CUDA performance
- 15:14Static resource analysis for CUDA
- 26:12Security implications of performance leaks
- 29:25Q&A
related talks
01h 06mThe One-Decade Task: Putting std::atomic in CUDA.
14mI Fought the Law and the Law Lost: Moore’s Law, Dennard Scaling & RISC-V
14mFoundational HPC Systems for 2020 and Beyond
36mRuby Supercomputing: Using The GPU For Massive Performance Speedup
49mKeynote Address: Everything You Always Wanted to Know about Storage Analysis...
16mCeci N'est Pas un CPU Load
12mGPREEMPT: GPU Preemptive Scheduling Made General and Efficient
33mWas He Wright All Along? Software After Moore's Law