Specifying and testing GPU workgroup progress models
File(s)
Published version
Author(s)
Type
Journal Article
Abstract
As GPU availability has increased and programming support has matured, a wider variety of applications arebeing ported to these platforms. Many parallel applications contain fine-grained synchronization idioms; assuch, their correct execution depends on a degree of relative forward progress between threads (or threadgroups). Unfortunately, many GPU programming specifications (e.g. Vulkan and Metal) say almost nothingabout relative forward progress guarantees between workgroups. Although prior work has proposed aspectrum of plausible progress models for GPUs, cross-vendor specifications have yet to commit to any model.This work is a collection of tools and experimental data to aid specification designers when consideringforward progress guarantees in programming frameworks. As a foundation, we formalize a small parallelprogramming language that captures the essence of fine-grained synchronization. We then provide a means offormally specifying a progress model, and develop a termination oracle that decides whether a given programis guaranteed to eventually terminate with respect to a given progress model. Next, we formalize a set ofconstraints that describe concurrent programs that require forward progress to terminate. This allows us tosynthesize a large set of 483 progress litmus tests. Combined with the termination oracle, we can determinethe expected status of each litmus test – i.e. whether it is guaranteed to eventually terminate – under variousprogress models. We present a large experimental campaign running the litmus tests across 8 GPUs from 5different vendors. Our results highlight that GPUs have significantly different termination behaviors underour test suite. Most notably, we find that Apple and ARM GPUs do not support thelinear occupancy-boundmodel, as was hypothesized by prior work
Date Issued
2021-10-01
Date Acceptance
2021-08-31
Citation
Proceedings of the ACM on Programming Languages, 2021, 5 (OOPSLA), pp.1-30
ISSN
2475-1421
Publisher
Association for Computing Machinery (ACM)
Start Page
1
End Page
30
Journal / Book Title
Proceedings of the ACM on Programming Languages
Volume
5
Issue
OOPSLA
Copyright Statement
© 2021 Copyright held by the owner/author(s). This work is licensed under a Creative Commmons Attribution International License 4.0 (https://creativecommons.org/licenses/by/4.0/)
License URL
Sponsor
Engineering & Physical Science Research Council (E
Engineering and Physical Sciences Research Council
Grant Number
Ref: 542716
EP/L016796/1
Subjects
Science & Technology
Technology
Computer Science, Software Engineering
Computer Science
liveness
semantics
GPU
model checking
test case synthesis
WEAK MEMORY
Publication Status
Published
Article Number
ARTN 131