Golly! Granular Bug Finding via Polyhedral Analysis of GPU Kernels

Abstract

In this era of multicore programming, industry engineers and scientists alike have turned to parallel algorithms to improve algorithmic performance at scale, resulting in a demand for massively parallel processors that manufacturers have been only too eager to meet. However, programming for performance in accelerators has proven to be error-prone, with data races being one of the most common, yet most difficult to detect, bugs encountered in the GPU domain on a daily basis. In this paper, we propose a polyhedral approach to the analysis of CUDA programs, and demonstrate the capability of Presburger logic to compactly model the peculiarities of working with GPU hardware accelerators. Polyhedral analysis has long been used to validate program transformations in optimizing compilers. By abstracting the concept of affine loops to scanning polyhedra, many hardware-focused optimizations such as tiling and vectorization can be applied through polyhedral analysis. We observe that there is a duality between the thread organization of graphics cards and nested loops, and attempted to apply the polyhedral model to analyze GPU-targeted programs — colloquially referred as ‘kernels’ — and realized that the further delineation of thread blocks into warps can be succinctly described in Presburger logic. However, we realize that the polyhedral model alone is insufficient to describe synchronization, and extended the model with a mph{synchronization schedule} that encapsulated the pair-wise synchronization relation for use in the integer linear program solver. We implement our findings in our ILP-based tool, Golly, using a multitude of control flow analyses to extract the polyhedral model from LLVM IR. We then empirically evaluate the capabilities of our tool on a set of benchmarks in comparison to existing SMT-based static detectors. Our results retain a high precision while achieving an average speedup of 75% over previous work. In summary, the key contributions of this work are as follows: the extension of the polyhedral model to account for synchronization, the modeling of hardware-level concepts in the polyhedral model, an application of said model by applying it in the context of race detection, and an evaluation of the approaches mentioned.