@article{GURDEEPSINGH2023102989,
title = {Gaiwan: A size-polymorphic typesystem for GPU programs},
journal = {Science of Computer Programming},
volume = {230},
pages = {102989},
year = {2023},
issn = {0167-6423},
doi = {https://doi.org/10.1016/j.scico.2023.102989},
url = {https://www.sciencedirect.com/science/article/pii/S0167642323000710},
author = {Robbert {Gurdeep Singh} and Christophe Scholliers},
keywords = {GPU, Polymorphism, Type system, OpenCL, Unification},
abstract = {General-purpose computing on graphics processing units (GPGPU) is increasingly used for number crunching tasks such as analyzing time series data. GPUs are a good fit for these tasks as they can execute many computations in parallel. To leverage this parallelism, the programmer is forced to carefully divide their input data into data blocks that are then distributed over the many GPU cores. The optimal block sizes are unrelated to the programmers goals, instead, they are based on characteristics of the used GPU and the input data. GPGPU programmers must additionally be wary of introducing race conditions in their programs. We believe that GPGPU programmers should be able to express GPU transformations without worrying about splitting data or race conditions. For this, we created Gaiwan, a GPGPU programming language with a size-polymorphic type system that only features data race free operations. Programmers can declare the effects of program steps on the sizes of buffers by using affine functions int[2n]->int[n+1]. From a step sequence, Gaiwan derives a set of constraints on the size and shape of valid inputs. Gaiwan guarantees that the program will run for any input satisfying these constraints. This means that one program may analyze both a hundred data points and millions of data points, as long as the input satisfies the constraints. We prove that our system is sound and show it works with two usage examples. Our benchmarks show that our initial OpenCL-based implementation of Gaiwan scales to handling large programs.}
}