Formal analysis techniques for reliable GPU programming

GPU-accelerated computing is being adopted increasingly in a number of areas, ranging from highend scientific computing to mobile and embedded computing. While GPU programs routinely provide high computational throughput in a number of areas, they also prove to be notoriously difficult to write and optimize correctly, largely due to the subtleties of GPU concurrency. This chapter discusses several issues that make GPU programming hard, and examines recent progress on rigorous methods for formal analysis of GPU software. Our key observation is that given the fastpaced advances in GPU programming, the use of rigorous specification and verification methods must be an integral part of the culture of programming and training, and not an afterthought.