Daniel Poetzl University of Oxford ACL2 Seminar, April 17, 2014 Testing GPU Memory Models ------------------------- Graphics processing units (GPUs) are specialized highly concurrent microprocessors. Traditionally, these chips have been used in accelerating graphics rendering. However, since the advent of general purpose GPU programming frameworks such as Nvidia's CUDA, they have found their way into many applications, especially scientific and embedded computing. To enable precise reasoning about GPU programs, a formal memory model is desirable. A necessary first step toward building a model is the thorough testing of the hardware. The model cannot be based on the vendor documentation alone, as it typically contains little detail and is at times ambiguous. In this talk, I will give an introduction to GPU architectures and programming models, and will describe our testing approach and testing results.