CUDA au Coq: A Framework for Machine-validating GPU Assembly Programs

Benjamin Ferrell, Jun Duan, Kevin W. Hamlen
The University of Texas at Dallas
26th Design, Automation & Test in Europe Conference & Exhibition (DATE), 2019


   title={CUDA au Coq: A Framework for Machine-validating GPU Assembly Programs},

   author={Ferrell, Benjamin and Duan, Jun and Hamlen, Kevin W},



Download Download (PDF)   View View   Source Source   



A prototype framework for formal, machinechecked validation of GPU pseudo-assembly code algorithms using the Coq proof assistant is presented and discussed. The framework is the first to afford GPU programmers a reliable means of formally machine-validating high-assurance GPU computations without trusting any specific source-to-assembly compilation toolchain. A formal operational semantics for the PTX pseudo-assembly language is expressed as inductive, dependent Coq types, facilitating development of proofs and proof tactics that refer directly to the compiled PTX object code. Challenges modeling PTX’s complex and highly parallelized computation model in Coq, with sufficient clarity and generality to tractably prove useful properties of realistic GPU programs, are discussed. Examples demonstrate how the prototype can already be used to validate some realistic programs.
No votes yet.
Please wait...

* * *

* * *

* * *

HGPU group © 2010-2022 hgpu.org

All rights belong to the respective authors

Contact us: