Skip to main content

A formal instruction-level GPU model for scalable verification

Author(s): Xing, Yue; Huang, Bo-Yuan; Gupta, Aarti; Malik, Sharad

Download
To refer to this page use: http://arks.princeton.edu/ark:/88435/pr11r79
Full metadata record
DC FieldValueLanguage
dc.contributor.authorXing, Yue-
dc.contributor.authorHuang, Bo-Yuan-
dc.contributor.authorGupta, Aarti-
dc.contributor.authorMalik, Sharad-
dc.date.accessioned2021-10-08T19:46:36Z-
dc.date.available2021-10-08T19:46:36Z-
dc.date.issued2018-11en_US
dc.identifier.citationXing, Yue, Bo-Yuan Huang, Aarti Gupta, and Sharad Malik. "A formal instruction-level GPU model for scalable verification." In Proceedings of the International Conference on Computer-Aided Design (2018): pp. 1-8. doi:10.1145/3240765.3240771en_US
dc.identifier.issn1092-3152-
dc.identifier.urihttp://arks.princeton.edu/ark:/88435/pr11r79-
dc.description.abstractGPUs have been widely used to accelerate big-data inference applications and scientific computing through their parallelized hardware resources and programming model. Their extreme parallelism increases the possibility of bugs such as data races and un-coalesced memory accesses, and thus verifying program correctness is critical. State-of-the-art GPU program verification efforts mainly focus on analyzing application-level programs, e.g., in C, and suffer from the following limitations: (1) high false-positive rate due to coarse-grained abstraction of synchronization primitives, (2) high complexity of reasoning about pointer arithmetic, and (3) keeping up with an evolving API for developing application-level programs. In this paper, we address these limitations by modeling GPUs and reasoning about programs at the instruction level. We formally model the Nvidia GPU at the parallel execution thread (PTX) level using the recently proposed Instruction-Level Abstraction (ILA) model for accelerators. PTX is analogous to the Instruction-Set Architecture (ISA) of a general-purpose processor. Our formal ILA model of the GPU includes non-synchronization instructions as well as all synchronization primitives, enabling us to verify multithreaded programs. We demonstrate the applicability of our ILA model in scalable GPU program verification of data-race checking. The evaluation shows that our checker outperforms state-of-the-art GPU data race checkers with fewer false-positives and improved scalability.en_US
dc.format.extent1 - 8en_US
dc.language.isoen_USen_US
dc.relation.ispartofProceedings of the International Conference on Computer-Aided Designen_US
dc.rightsFinal published version. This is an open access article.en_US
dc.titleA formal instruction-level GPU model for scalable verificationen_US
dc.typeConference Articleen_US
dc.identifier.doi10.1145/3240765.3240771-
dc.identifier.eissn1558-2434-
pu.type.symplectichttp://www.symplectic.co.uk/publications/atom-terms/1.0/conference-proceedingen_US

Files in This Item:
File Description SizeFormat 
FormalInstructionLevelGPUScalableVerification.pdf205.51 kBAdobe PDFView/Download


Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.