×

Interleaving and lock-step semantics for analysis and verification of GPU kernels. (English) Zbl 1381.68139

Felleisen, Matthias (ed.) et al., Programming languages and systems. 22nd European symposium on programming, ESOP 2013, held as part of the European joint conferences on theory and practice of software, ETAPS 2013, Rome, Italy, March 16–24, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-37035-9/pbk). Lecture Notes in Computer Science 7792, 270-289 (2013).
Summary: We study semantics of GPU kernels – the parallel programs that run on graphics processing units (GPUs). We provide a novel lock-step execution semantics for GPU kernels represented by arbitrary reducible control flow graphs and compare this semantics with a traditional interleaving semantics. We show for terminating kernels that either both semantics compute identical results or both behave erroneously.
The result induces a method that allows GPU kernels with arbitrary reducible control flow graphs to be verified via transformation to a sequential program that employs predicated execution. We implemented this method in the GPUVerify tool and experimentally evaluated it by comparing the tool with the previous version of the tool based on a similar method for structured programs, i.e., where control is organised using if and while statements. The evaluation was based on a set of 163 open source and commercial GPU kernels. Among these kernels, 42 exhibit unstructured control flow which our novel method can handle fully automatically, but the previous method could not. Overall the generality of the new method comes at a modest price: Verification across our benchmark set was 2.25 times slower overall; however, the median slow down across all kernels was 0.77, indicating that our novel technique yielded faster analysis in many cases.
For the entire collection see [Zbl 1268.68016].

MSC:

68Q55 Semantics in the theory of computing
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
PDFBibTeX XMLCite
Full Text: DOI