Automated Verification of Functional Correctness of Race-Free GPU Programs

作者：Kojima Kensuke^*; Imanishi Akifumi; Igarashi Atsushi

来源：Journal of Automated Reasoning, 2018, 60(3): 279-298.

DOI：10.1007/s10817-017-9428-2

• Program verification
• GPGPU
• SMT
• Symbolic execution

We study an automated verification method for functional correctness of parallel programs running on graphics processing units (GPUs). Our method is based on Kojima and Igarashi's Hoare logic for GPU programs. Our algorithm generates verification conditions (VCs) from a program annotated by specifications and loop invariants, and passes them to off-the-shelf SMT solvers. It is often impossible, however, to solve naively generated VCs in reasonable time. A main difficulty stems from quantifiers over threads due to the parallel nature of GPU programs. To overcome this difficulty, we additionally apply several transformations to simplify VCs before calling SMT solvers. Our implementation successfully verifies correctness of several GPU programs, including matrix multiplication optimized by using shared memory. In contrast to many existing verification tools for GPU programs, our verifier succeeds in verifying fully parameterized programs: parameters such as the number of threads and the sizes of matrices are all symbolic. We empirically confirm that our simplification heuristics is highly effective for improving efficiency of the verification procedure.

• 出版日期2018-3