Specifying and Testing GPU Workgroup Progress Models

Organisation:	Google and Imperial College London (UK) Princeton University and UC Santa Cruz (USA)
Method:	LNT
Tools used:	CADP (Construction and Analysis of Distributed Processes) Alloy
Domain:	GPU Programming
Period:	2021
Size:	n/a
Description:	An increasing number of applications are nowadays offloading computations to GPU devices. Given implementation differences across GPUs, cross-vendor GPU frameworks differ from those of classic CPU programming. In particular, independent forward progress between threads of execution is not always guaranteed on a GPU. This means that it is generally unsafe to write a GPU program where one thread relies on another thread making progress. Full progress guarantees are difficult to provide, given the internal partitioning of threads into groups and the behaviour of the GPU schedulers. To make informed decisions about progress, framework designers must be able to describe forward progress models, to ask questions about the subtle concurrent interactions that a given model allows, and to test whether an implementation satisfies the chosen forward progress model. This work proposes several contributions aiming to support designers in these regards: a simple concurrent programming language for progress reasoning, an executable semantics for progress models in terms of LNT descriptions, a synthesis of litmus tests, and an evaluation of GPU progress models in the field. The approach takes as input the specification of progress models and the constraints over programs that contain potential non-termination due to starvation or livelock. The program constraint specification can be fed to the Alloy Analyzer for progress litmus test synthesis. The progress litmus tests can then be executed using CADP on the LNT model of the program (using any of the six formal progress models described in LNT), providing formal per-model test outcomes. The EVALUATOR model checker is also used to check the LNT model for the absence of non-termination cycles under weak and strong fairness. The litmus tests can also be given as input to a newly developed GPU test compiler, which outputs executable test cases for three common GPGPU frameworks. The formal test results can be cross-referenced with the empirical test to explore which (if any) formal progress model(s) describe the observed behavior across different GPUs.
Conclusions:	This work demonstrates that a progress model can be rigorously described in LNT over a simple concurrent programming language. Using the CADP tools, the designer can investigate whether concurrent programs terminate under various progress models.
Publications:	[Sorensen-Salvador-Raval-et-al-21] Tyler Sorensen, Lucas F. Salvador, Harmit Raval, Hugues Evrard, John Wickerson, Margaret Martonosi, and Alastair F. Donaldson. "Specifying and Testing GPU Workgroup Progress Models". Proc. ACM Program. Lang. vol. 5, no. OOPSLA, Article 131, October 2021. Available on-line at: https://arxiv.org/pdf/2109.06132v1.pdf or from the CADP Web site in PDF or PostScript
Contact:	Hugues Evrard Google Email: hevrard@google.com
Further remarks:	This case-study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page