TEXT

Abstract

Graphics Processing Units (GPUs) have risen in importance far beyond their original humble aim. With Moore's Law largely a relic of the past, users have turned to specialized hardware to accelerate program execution. GPUs, thanks to their ability to perform linear algebra calculations with speed, have risen to stardom as drivers of the rise of Machine Learning. However, GPUs' highly concurrent architecture and diverse implementations add unique challenges to their use.

To help users handle the intricacies of highly concurrent programming across diverse architectures, abstractions such as OpenCL, a general purpose graphics programming language, provide guarantees on the behavior of the GPU's concurrent execution. These guarantees, which users rely upon for correct execution of their code, are provided by compilers and hardware; as such, verification of these guarantees is a key area of research, especially considering GPUs' newfound importance.

This thesis will describe a novel approach to verifying GPU Memory Consistency Model behavior that prioritizes reproducibility, effectiveness, and efficiency. Prior work has developed methods for verifying Memory Models through empirical testing of specialized concurrent code with multiple outcomes that correlate to specific memory behaviors, some of which are forbidden or potentially problematic. However, these behaviors can be exceedingly rare, making observation and reproduction difficult.

We present a testing framework that uses statistical metrics to quantify the effect of different testing methods, allowing us to adapt our testing towards being more effective. We postulate experiments through which to validate our novel approach, then demonstrate the power of rigorous analysis in empirical testing. Finally, we deploy a small-scale implementation of our approach to test for forbidden behaviors on a real GPU.

Among the results of this thesis is the discovery of a previously unknown bug in Intel's OpenCL 2.0 Compiler. The approach and tools developed by this thesis led to the identification, report, reproduction, and official patch for this bug.