Formalizing GPU Instruction Set Architecture in Coq
Nitin Bhatia, Meenakshi D’Souza, Sujit Kumar Chakrabarti · 2019
GPUs are now a mainstream compute device. They are widely used to render images on medical devices. Today, it has become impossible to imagine AI without them. To build confidence on the accuracy of rendering images and complex calculations, it is essential to consider formalizing the behaviour of GPU Instruction Set Architecture (ISA) at the assembly language level. In this paper, we present the formalization of GPU shader programs. We prove some properties of shader programs with respect to operational semantics of our formal model. We use Coq to mechanize the formalization of our model and proofs.