Name
Title | ||
|---|---|---|
Barrier invariants: a shared state abstraction for the analysis of data-dependent GPU kernels |
Abstract | ||
|---|---|---|
Data-dependent GPU kernels, whose data or control flow are dependent on the input of the program, are difficult to verify because they require reasoning about shared state manipulated by many parallel threads. Existing verification techniques for GPU kernels achieve soundness and scalability by using a two-thread reduction and making the contents of the shared state nondeterministic each time threads synchronise at a barrier, to account for all possible thread interactions. This coarse abstraction prohibits verification of data-dependent kernels. We present barrier invariants, a novel abstraction technique which allows key properties about the shared state of a kernel to be preserved across barriers during formal reasoning. We have integrated barrier invariants with the GPUVerify tool, and present a detailed case study showing how they can be used to verify three prefix sum algorithms, allowing efficient modular verification of a stream compaction kernel, a key building block for GPU programming. This analysis goes significantly beyond what is possible using existing verification techniques for GPU kernels. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1145/2509136.2509517 | OOPSLA |
Keywords | Field | DocType |
present barrier invariants,shared state abstraction,gpu kernel,coarse abstraction,efficient modular verification,existing verification technique,shared state,shared state nondeterministic,data-dependent gpu kernel,gpu programming,integrated barrier invariants,concurrency,verification | Programming language,Nondeterministic algorithm,Computer science,Prefix sum,Concurrency,CUDA,Parallel computing,Control flow,Theoretical computer science,Thread (computing),General-purpose computing on graphics processing units,Scalability | Conference |
Volume | Issue | ISSN |
48 | 10 | 0362-1340 |
Citations | PageRank | References |
11 | 0.53 | 26 |
Authors | ||
5 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Nathan Chong | 1 | 185 | 7.91 |
| Alastair F. Donaldson | 2 | 661 | 52.35 |
| Paul H. J. Kelly | 3 | 1361 | 112.65 |
| Jeroen Ketema | 4 | 160 | 13.52 |
| Shaz Qadeer | 5 | 3257 | 239.11 |