A formal instruction-level GPU model for scalable verification

Yue Xing, Bo Yuan Huang, Aarti Gupta, Sharad Malik

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Scopus citations

Abstract

GPUs 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.

Original languageEnglish (US)
Title of host publication2018 IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2018 - Digest of Technical Papers
PublisherInstitute of Electrical and Electronics Engineers Inc.
ISBN (Electronic)9781450359504
DOIs
StatePublished - Nov 5 2018
Event37th IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2018 - San Diego, United States
Duration: Nov 5 2018Nov 8 2018

Publication series

NameIEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers, ICCAD
ISSN (Print)1092-3152

Other

Other37th IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2018
CountryUnited States
CitySan Diego
Period11/5/1811/8/18

All Science Journal Classification (ASJC) codes

  • Software
  • Computer Science Applications
  • Computer Graphics and Computer-Aided Design

Fingerprint Dive into the research topics of 'A formal instruction-level GPU model for scalable verification'. Together they form a unique fingerprint.

  • Cite this

    Xing, Y., Huang, B. Y., Gupta, A., & Malik, S. (2018). A formal instruction-level GPU model for scalable verification. In 2018 IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2018 - Digest of Technical Papers [a130] (IEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers, ICCAD). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1145/3240765.3240771