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

Simple item page
dc.contributor.VIAF50151836493420401232 (Hamlen, KW)
dc.contributor.authorFerrell, Benjamin
dc.contributor.authorDuan, Jun
dc.contributor.authorHamlen, Kevin W.
dc.contributor.utdAuthorFerrell, Benjamin
dc.contributor.utdAuthorDuan, Jun
dc.contributor.utdAuthorHamlen, Kevin W.
dc.date.accessioned2020-03-11T19:23:06Z
dc.date.available2020-03-11T19:23:06Z
dc.date.issued2019-03-25
dc.descriptionDue to copyright restrictions and/or publisher's policy full text access from Treasures at UT Dallas is limited to current UTD affiliates (use the provided Link to Article).
dc.description.abstractA prototype framework for formal, machine-checked 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. © 2019 EDAA.
dc.description.departmentErik Jonsson School of Engineering and Computer Science
dc.description.sponsorshipONR award N00014-17-1-2995, NSF award #1513704, an NSF IUCRC award from Lockheed Martin
dc.identifier.bibliographicCitationFerrell, B., J. Duan, and K. W. Hamlen. 2019. "CUDA au Coq: A Framework for Machine-Validating GPU Assembly Programs." Design, Automation and Test in Europe Conference and Exhibition, 2019: 474-479, doi: 10.23919/DATE.2019.8715160
dc.identifier.isbn9783981926323
dc.identifier.urihttp://dx.doi.org/10.23919/DATE.2019.8715160
dc.identifier.urihttps://hdl.handle.net/10735.1/7390
dc.language.isoen
dc.publisherInstitute of Electrical and Electronics Engineers Inc.
dc.relation.isPartOfDesign, Automation and Test in Europe Conference and Exhibition, 2019
dc.rights©2019 EDAA
dc.subjectGraphics processing units
dc.subjectSemantics
dc.subjectAssembly languages (Electronic computers)
dc.subjectTheorem proving
dc.subjectParallel processing (Electronic computers)
dc.titleCUDA au Coq: A Framework for Machine-Validating GPU Assembly Programs
dc.type.genrearticle

Files

Original bundle

Now showing 1 - 1 of 1
Thumbnail Image
Name:
JECS-6565-261013.95-LINK.pdf
Size:
166.65 KB
Format:
Adobe Portable Document Format
Description:
Link to Article
Download

Collections

Hamlen, Kevin W.