Imperial College London
Portrait Picture

ProfessorAlastairDonaldson

Faculty of Engineering, Department of Computing

Professor of Programming Languages
 
 
 
//

Contact

 

+44 (0)20 7594 8266alastair.donaldson Website

 
 
//

Location

 

422Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@article{Sorensen:2021:10.1145/3485508,
author = {Sorensen, T and Salvador, LF and Raval, H and Evrard, H and Wickerson, J and Martonosi, M and Donaldson, A},
doi = {10.1145/3485508},
journal = {Proceedings of the ACM on Programming Languages},
pages = {1--30},
title = {Specifying and testing GPU workgroup progress models},
url = {http://dx.doi.org/10.1145/3485508},
volume = {5},
year = {2021}
}
Download

RIS format (EndNote, RefMan)

TY  - JOUR
AB  - 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
AU  - Sorensen,T
AU  - Salvador,LF
AU  - Raval,H
AU  - Evrard,H
AU  - Wickerson,J
AU  - Martonosi,M
AU  - Donaldson,A
DO  - 10.1145/3485508
EP  - 30
PY  - 2021///
SN  - 2475-1421
SP  - 1
TI  - Specifying and testing GPU workgroup progress models
T2  - Proceedings of the ACM on Programming Languages
UR  - http://dx.doi.org/10.1145/3485508
UR  - http://hdl.handle.net/10044/1/91780
VL  - 5
ER  -
Download